Section 1.7: Compactness and Effectiveness
A set of wffs is satisfiable iff every finite subset is satisfiable.
Given a set of wffs that is finitely satisfiable, extend it recursively by including each possible wff (there are countably many) or its negation depending on which one makes the extended set finitely satisfiable at each step. Then, the resulting set contains and all wffs or their negations, and is finitely satisfiable. Now, for each sentence symbol we assign iff is in the extended set (i.e. iff is in the extended set; both and cannot be there, as it would make an unsatisfiable finite subset of ). Then, satisfies a wff iff it is in .
If , then there is a finite subset s.t. .
- In fact, the corollary is equivalent to the Compactness Theorem, that is the truth of the latter can be shown if the truth of the corollary is assumed.
A set of expressions is called decidable iff there is an effective procedure that, given an expression, will decide whether it belongs to or not.
A set of expressions is called effectively enumerable (semidecidable) iff there is an effective procedure that, given an expression, produces a positive answer iff it belongs to .
- A set of expressions is effectively enumerable iff there is an effective procedure that lists all the members of .
- The Parsing Algorithm of Section 1.3 ensures that the set of wffs is decidable.
(Kleene’s Theorem) A set of expressions
is decidable iff both it and its complement are effectively enumerable.
- The class of effectively enumerable sets is closed under union and intersection.
- The class of decidable sets is closed under union, intersection and complementation.
A function is effectively computable (or simply computable) iff there is an effective procedure that, given any , produces .
The truth table procedure of Section 1.2 ensures that there is an effective procedure to decide whether
for a finite
- In particular, the set of tautological consequences of a finite set is decidable.
- The set of tautologies is decidable.
is infinite, even if decidable itself, the set of its tautological consequences may not be decidable.
- If is effectively enumerable, the set of its tautological consequences is effectively enumerable as well (follows from compactness).
- If is effectively enumerable, and such that for any , or (in either exclusive or inclusive meaning of “or”), then the set of its tautological consequences is decidable.
These facts are more important for the first-order logic and will reappear in Section 2.4.
Define a deduction from to be a finite sequence of wffs such that for each one of the following holds: , , or there are : ( is obtained by modus ponens from and ).
- If , there is a deduction from .