display all the ideas for this combination of philosophers
5 ideas
| 9719 | A proof theory is 'sound' if its valid inferences entail semantic validity [Enderton] |
| Full Idea: If every proof-theoretically valid inference is semantically valid (so that |- entails |=), the proof theory is said to be 'sound'. | |
| From: Herbert B. Enderton (A Mathematical Introduction to Logic (2nd) [2001], 1.1.7) |
| 9720 | A proof theory is 'complete' if semantically valid inferences entail proof-theoretic validity [Enderton] |
| Full Idea: If every semantically valid inference is proof-theoretically valid (so that |= entails |-), the proof-theory is said to be 'complete'. | |
| From: Herbert B. Enderton (A Mathematical Introduction to Logic (2nd) [2001], 1.1.7) |
| 9995 | Proof in finite subsets is sufficient for proof in an infinite set [Enderton] |
| Full Idea: If a wff is tautologically implied by a set of wff's, it is implied by a finite subset of them; and if every finite subset is satisfiable, then so is the whole set of wff's. | |
| From: Herbert B. Enderton (A Mathematical Introduction to Logic (2nd) [2001], 2.5) | |
| A reaction: [Enderton's account is more symbolic] He adds that this also applies to models. It is a 'theorem' because it can be proved. It is a major theorem in logic, because it brings the infinite under control, and who doesn't want that? |
| 9996 | Expressions are 'decidable' if inclusion in them (or not) can be proved [Enderton] |
| Full Idea: A set of expressions is 'decidable' iff there exists an effective procedure (qv) that, given some expression, will decide whether or not the expression is included in the set (i.e. doesn't contradict it). | |
| From: Herbert B. Enderton (A Mathematical Introduction to Logic (2nd) [2001], 1.7) | |
| A reaction: This is obviously a highly desirable feature for a really reliable system of expressions to possess. All finite sets are decidable, but some infinite sets are not. |
| 9997 | For a reasonable language, the set of valid wff's can always be enumerated [Enderton] |
| Full Idea: The Enumerability Theorem says that for a reasonable language, the set of valid wff's can be effectively enumerated. | |
| From: Herbert B. Enderton (A Mathematical Introduction to Logic (2nd) [2001], 2.5) | |
| A reaction: There are criteria for what makes a 'reasonable' language (probably specified to ensure enumerability!). Predicates and functions must be decidable, and the language must be finite. |