October 19, 2010 13:38  World Scientific Book - 9in x 6in  note

i

1: Completeness

1.1: Completeness of Gentzen’s system

Recall exercise ?? and the discussion just after the introduction of Gentzen’s system for FOL in Section ??.??.

(A) We assume that the new rules added in the FOL system are invertible in the same sense as are the propositional rules (exercise ??). More precisely,

for any rule \frac{Γ_{i} ⊢_{G} Δ_{i}}{Γ ⊢_{G} Δ} , if the conclusion is valid, ⋀ Γ ⇒ ⋁ Δ, then so

are all the assumptions, ⋀ Γ_{i} ⇒ ⋁ Δ_{i}. We can strengthen this, since this implication holds also when validity is replaced by truth in an arbitrary structure. I.e., for any structure M, if M ⊧ ⋀ Γ → ⋁ Δ then likewise M ⊧ ⋀ Γ_{i} → ⋁ Δ_{i} for each assumption i. Verification of this fact is left as an exercise.

(B) We proceed as we did in exercise ??, constructing a counter-model for any unprovable seuquent. But now we have to handle the additional complications of possibly non-terminating derivations. To do this, we specify the following strategy for an exhaustive bottom-up proof search.

(B.1) First, we have to ensure that even if a branch of a proof does not terminate, all formulae in the sequent are processed. Let us therefore view a sequent as a pair of (finite) sequences Γ = G_{1}, ..., G_{a} and Δ = D_{1}, ..., D_{c}. Such a sequent is processed by applying bottom-up the appropriate rule first to G_{1}, then to G_{2}, to G_{3}, etc. until G_{a}, and followed by D_{1} through D_{c}. If no rule is applicable to a formula, it is skipped and one continues with the next formula. New formulae arising from rule applications are always placed at the start of the appropriate sequence (on the left or on the right of ⊢_{G}). These restrictions are particularly important for the quantifier rules which introduce new formulae, i.e.:

6. ⊢∃ \frac{Γ ⊢_{G} A_{t}^{x} … ∃xA …}{Γ ⊢_{G} … ∃xA …} A_{t}^{x} legal 6′. ∀ ⊢ \frac{A_{t}^{x} … ∀xA … ⊢_{G} Δ}{… ∀xA … ⊢_{G} Δ} A_{t}^{x} legal

These two rules might start a non-terminating, repetitive process introducing new substitution instances of A without ever considering the remaining formulae. Processing formulae from left to right, and placing new formulae to the left of the actually processed ones, makes sure that all formulae

ii Notes....

in a sequent will be processed, before starting the processing of the newly introduced formulae.

(B.2) We must also ensure that all possible substitution instances of quantified formulae are attempted in search for axioms. To do this, it suffices to require that the formula A_{t}^{x}, introduced by an application of rule 6 or 6’, does not already occur in the sequence to which it is introduced.

(C) Let now Γ ⊢_{G} Δ be an arbitrary sequent for which the above strategy does not yield a proof. There are two cases.

(C.1) If every branch in the obtained proof tree is finite, then all its leafs contain irreducible sequents, some of which are non-axiomatic. Select such a non-axiomatic leaf, say, with Φ ⊢_{G} Ψ. Irreducibility means that no rule can be applied to this sequent, i.e., all its formulae are atomic. That it is non-axiomatic means that Φ ∩ Ψ = ∅. Construct a counter-model M by taking all terms occurring in the atoms of Φ, Ψ as the intepretation domain \underline{M}. (In particular, if there are open atomic formulae, their variables are treated as elements on line with ground terms.) Interpret the predicates over these elements by making all atoms in Φ true and all atoms in Ψ false. This is possible since Φ ∩ Ψ = ∅. (E.g., a leaf P (x) ⊢_{G} P (t) gives the structure with \underline{M} = \{x, t\} where t ∉ [[P]]^{M} = \{x\}.)

Invertibility of the rules implies now that this is also a counter-model to the initial sequent, i.e., ⋀ Γ ⇏ ⋁ Δ.

(C.2) In the other case, the resulting tree has an infinite branch. We then select an arbitrary infinite branch B and construct a counter-model M from all the terms occurring in the atomic formulae on B. (Again, variables occurring in such formulae are taken as elements on line with ground terms.) The predicates are defined by

\overline{t} ∈ [[P]]^{M} iff there is a node on B with P (\overline{t}) on the left of ⊢_{G} (*)

The claim is now that M is a counter-model to every sequent on the whole B. We show, by induction on the complexity of the formulae, that all those occurring on B on the left of ⊢_{G} are true and all those on the right false. The claim is obvious for the atomic formulae by the definition (*). In particular, since atomic formulae remain unchanged once they appear on B, and since no node is axiomatic, no formula occurring on the left of ⊢_{G} in B occurs also on the right. The claim is easily verified for the propositional combinations of formulae by the invertibility of the propositional rules. Consider now any quantified formula occurring on the left. Due to fairness strategy (B.1), it

iii

has been processed. If it is universal, it has been processed by the rule:

6′. ∀ ⊢ \frac{A_{t}^{x} … ∀xA … ⊢_{G} Δ}{… ∀xA … ⊢_{G} Δ} A_{t}^{x} legal.

Then [[A_{t}^{x}]]^{M} = 1 by IH and, moreover, since all such substitution instances are tried on every infinite branch (B.2), so [[A_{t_{i}}^{x}]]^{M} = 1 for all terms t_{i}. But this means that M ⊧ ∀xA. If the formula is existential, it is processed by the rule:

7′. ∃ ⊢ \frac{Γ, A_{x′}^{x} ⊢_{G} Δ}{Γ, ∃xA ⊢_{G} Δ} x′ fresh.

Then x′ occurs in the atomic subformula(e) of A and is an element of \underline{M}. By IH, [[A_{x′}^{x}]]^{M} = 1 and hence also [[∃xA]]^{M} = 1.

Similarly, by (B.1) every quantified formula on the right of ⊢_{G} has been processed. Universal one was processed by the rule

7. ⊢∀ \frac{Γ ⊢_{G} A_{x′}^{x}, Δ}{Γ, ⊢_{G} ∀xA, Δ} x′ fresh

Then x′ ∈ \underline{M} and, by IH, [[A_{x′}^{x}]]^{M} = 0. Hence also [[∀xA]]^{M} = 0. An existential formula on the right is processd by the rule

6. ⊢∃ \frac{Γ ⊢_{G} A_{t}^{x} … ∃xA …}{Γ ⊢_{G} … ∃xA …} A_{t}^{x} legal

and, by the exhaustive fairness strategy (B.2), all such substitution instances A_{t_{i}}^{x} appear on the right of ⊢_{G} in B. By IH, [[A_{t_{i}}^{x}]]^{M} = 0 for all t_{i}, which means that [[∃xA]]^{M} = 0.

(D) Since the sequent Γ ⊢_{G} Δ is on B, (C.1) and (C.2) together show that M |̸= ⋀ Γ → ⋁ Δ., i.e., that unprovability of a sequent, Γ ⊬_{G} Δ, implies the existence of a counter-model for it, ⋀ Γ ⇏ ⋁ Δ. Formulated contrapositively, if a sequent is valid (has no counter-model), ⋀ Γ ⇒ ⋁ Δ, then it is provable, Γ ⊢_{G} Δ.

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

(C) It should be clear (even if not formally established) that if there is a proof of Γ ⊢_{G} Δ, then it can be obtained in this way. The only difference is that an efficient proof may terminate quickly by choosing appropriate formulae to process or terms to substitute, while this exhaustive search only makes sure that no formula nor term remains ignored. Since formulae have finite complexity, one can also easily show by induction that, in (B.1), for every sequent one will always, eventually, process its whole sequence on the left, and then on the right of ⊢_{G}, even though new formulae can appear at the start of both. Enumeration of terms in (B.3) can be also used by the rules 7 and 7’, so

iv Notes....

that whenever required to introduce a fresh variable, they choose the first variable term on the list, not used so far.