|
|
|
to be rewritten |
|
(to be rewritten...) |
|
where (P) is the remainder of the prefix of φ (it is thus of degree k-1) and ψ is the quantifier-free matrix of φ. Note that x, y, u and v denote here tuples of variables rather than single variables; e.g. (∀x) really stands for ∀x1∀x2...∀xn) where x1...xn are some distinct variables. |
|
where (P) is the remainder of the prefix of φ (it is thus of degree k-1) and ψ is the quantifier-free matrix of φ. Note that x, y, u and v denote here tuples of variables rather than single variables; e.g. (∀x) really stands for ∀x1∀x2...∀xn where x1...xn are some distinct variables. |
|
Now Φ has the form (S)ρ ∧ (S')ρ' , where (S) and (S') are some quantifier strings, ρ and ρ' are quantifier-free, and, furthermore, no variable of (S) occurs in ρ' and no variable of (S') occurs in ρ. Under such conditions every formula of the form (T)(ρ ∧ ρ'), where (T) is a string of quantifiers containing all quantifiers in (S) and (S') interleaved among themselves in any fashion, but maintaining the relative order inside (S) and (S'), will be equivalent to the original formula (this is yet another basic result in first-order predicate calculus that we rely on). To wit, we form Ψ as follows: |
|
Now Φ' has the form (S)ρ ∧ (S')ρ' , where (S) and (S') are some quantifier strings, ρ and ρ' are quantifier-free, and, furthermore, no variable of (S) occurs in ρ' and no variable of (S') occurs in ρ. Under such conditions every formula of the form (T)(ρ ∧ ρ'), where (T) is a string of quantifiers containing all quantifiers in (S) and (S') interleaved among themselves in any fashion, but maintaining the relative order inside (S) and (S'), will be equivalent to the original formula Φ'(this is yet another basic result in first-order predicate calculus that we rely on). To wit, we form Ψ as follows: |
|
Now Ψ is a formula of degree k and therefore by assumption either refutable or satisfiable. If Ψ is satisfiable in a structure M, then, considering Ψ≡Φ'≡Φ and Φ→φ, we see that φ is satisfiable as well. If Ψ is refutable, then so is Φ which is equivalent to it; thus ¬Φ is provable. |
|
Now Ψ is a formula of degree k and therefore by assumption either refutable or satisfiable. If Ψ is satisfiable in a structure M, then, considering Ψ≡Φ'≡Φ and Φ→φ, we see that φ is satisfiable as well. If Ψ is refutable, then so is Φ which is equivalent to it; thus ¬Φ is provable. Now we can replace all occurrances of Q inside the provable formula ¬Φ by some other formula dependent on the same variables, and we will still get a provable formula (long note: this is yet another basic result of first-order predicate calculus. Depending on the particular formalism adopted for the calculus, it may be seen as a simple application of a "functional substitution" rule of inference (thus in Gödel's paper) or it may be proved by considering the formal proof of ¬Φ, replacing in it all occurences of Q by some other formula with the same free variables, and noting that all logical axioms in the formal proof remain logical axioms after the substitution, and all rules of inference still apply in the same way). In this particular case, we replace Q in ¬Φ with the formula (∀u)(∃v)(P)ψ(x,y|x',y') . ¬Φ then becomes |
|
¬ ( (∀x')(∃y') (∀u)(∃v)(P)ψ(x,y|x',y'); ∧ (∀x)(∀y) ( (∀u)(∃v)(P)ψ → (∀u)(∃v)(P)ψ ) ) |
|
to be completed |
|
and this formula is provable; since the part under negation and after the ∧ sign is obviously provable, and the under negation and part before the ∧ sign is obviously φ, just with x and y replaced by x' and y', we see that ¬φ is provable, and φ is refutable. We have proved that φ is either satisfiable or refutable, and this concludes the proof of the Lemma. |
![[Home]](wikipedia.png)