Project topics and materials
Get Complete Project Material File(s) Now! »
Constructive completeness for Boolean models
In Foundations of Mathematics, the completeness problem appears as a natural question as soon as we start to consider formal systems for giving a rig-orous treatment of mathematical arguments. The problem, for classical predi-cate logic apparently first posed in print by Hilbert and Ackermann in [104], is the problem of adequacy of the formal system under consideration, that is, the question: Can every true statement be derived in finitely many steps by means of the axioms and rules of inference of the formal system?
While from the work of Bernays [34] it was known that the answer is positive for the propositional fragment, due to the existence of the decision procedure based on truth tables, for predicate logic the existence of such a procedure was unknown, and was actually a major research problem known as the Entschei-dungsproblem. (German for ’decision problem’)
Not long after Hilbert and Ackermann, the completeness problem was re-posed and answered positively for predicate logic by Gödel in his doctoral dis-sertation [82], published as article in [83]. His solution circumvented the Entschei-dungsproblem, which remained unsolved until the results of Church [46] and Turing [167].
In this chapter we will take a fresh look at the completeness theorem for classical predicate logic. We will start with a historic overview of the versions of the proof from the one of Gödel, through the one of Henkin [94], to the one of Krivine [125], which represents the first constructive proof. Then, we will go on, following Berardi and Valentini [29], to develop a detailed constructive argu-ment (Sections 1.2 and 1.3), which was a subject of partial formalisation in the Coq proof assistant [62] (Section 1.5), and to discuss the computational content (Section 1.4) and the remaining related works (Section 1.6).
Historical overview
Basic definitions
The completeness theorem connects an intuitive notion of truth of a mathematical statement to that of its provability in a formal system. At the time of Gödel’s early works, and up to the 1950s, around was a notion of truth that was an intuitive extension, to deal with quantifiers, of the truth-table validity of propositional logic. Today, the intuitive notion that Gödel and others worked with can be recognised as an instance of the standard Tarski truth definition of Model Theory.1
1However, Tarski’s truth definition only took its definite model-theoretic form in [159], while the first publish theory of truth of Tarski [158] had a more generic approach. In [158] Tarski pro-posed a syntactic notion of truth, based on two separate formal languages: an object language L (the language whose truth is to be defined), and a meta-language M (the language used to define truth of sentences of L). In the spirit of his time, Tarski assumed [105] that L and M would be based on some kind of higher-order logic, but he was aware of the fact that M has to be stronger than L
Definition. A signature K is a collection of individual constants c0, c1, . . . (finitely or infinitely many), and predicate and function symbols with finite ari-ties, P0, P1, . . . Pn and f0, f1, . . . fm .
Definition. The language of signature K consists of formulae, which are built up inductively, using individual variables, standard logical constants, and the symbols of K :
• ⊥ is a formula
• Pi (t1, . . . , tn ) is a formula, if t1, . . . , tn are terms;
– an individual variable x is a term;
– an individual constant c j of K is a term;
– if t1, . . . , tm are terms, so is fl (t1, . . . , tm ).
• if A, B are formulae, then A ∧ B, A ∨ B, and A → B are formulae;
• if A is a formula, possibly containing x as a free individual variable, then ∃x A and ∀x A are formulae.
The formulae of the first two forms are called prime or atomic. The formula ¬A is an abbreviation for A → ⊥. We call sentence a formula in which all individual variables are bound by a quantifier.
Remark. Often, a special predicate symbol “=” is taken as a default mem-ber of every signature. For simplicity, similarly to Gödel, Henkin, and Krivine, we do not treat “=” as special.
Definition. A structure of signature K ,
M = (M, P0M , . . . , PnM , f0M , . . . , fmM , c0M , c1M , . . .), consists of:
• a domain of individuals M, typically a set;
• for each predicate symbol P of arity k of K , a k-ary relation P M on the domain M, that is, a subset of Mk ;
• for each function symbol f of arity k of K , a k-ary function f M from Mk into M;
• for each constant symbol c of K , an element cM of M to denote c.
Definition. We say that a structure M is a model of a formula A, that M satisfies A, or that M realises A, and write M A, if the following primitive-recursive meta-language interpretation of A holds:
• for A ≡ ⊥, M ⊥ ;
• for A ≡ P (a1, . . . , ak ), M A if (a1, . . . , ak ) ∈ P M ;
• for A ≡ A1 ∧ A2, M A if M A1 and M A2;
• for A ≡ A1 ∨ A2, M A if M A1 or M A2;
• for A ≡ A1 → A2, M A if M A1 implies M A2;
• for A ≡ ∀xB, M A if M B[a/x] for all a ∈ M;
• for A ≡ ∃xB, M A if M B[a/x] for some a ∈ M.
We say that A is satisfiable, or realisable, or has a model, if there exists a structure M which is a model of A.
in order for the Liar paradox [85] to be avoided. Nowadays, in Model Theory, a full set theory with an axiom of choice is standardly assumed for M.
Definition. Let K be a signature. We say that a formula A, written in the language of signature K , is true, or valid, if any structure M of signature K is a model of A.
We now have set up the basic framework for looking at the major instances of the theorem which appeared through history. In this chapter ⊢ A will stand for derivability of A inside a system for classical predicate logic. In Subsections 1.1.2, 1.1.3, and 1.1.4, we assume also a classical metalanguage.
Gödel’s proof. We give a sketch of Gödel’s original proof, based on [84, 83, 82]. The key role is played by the following lemma, today known as Model Existence Lemma.
Lemma. For every formula A of a language with signature K , either there exists a structure M of signature K such that M A, or ⊢ ¬A.
Theorem (Completeness). If A is true, then A is derivable.
PROOF. We apply Lemma 1.1.7 on the formula ¬A. Then, if there is a model M of ¬A, we obtain contradiction, since M is by hypothesis also a model of A. Otherwise, the formula ¬¬A is derivable, hence A is itself derivable .
PROOF SKETCH OF LEMMA 1.1.7. We say that a formula A is refutable if ¬A is derivable. Gödel shows that every formula is either satisfiable or refutable, by showing that every formula in prenex normal form is either satisfiable or refutable, since we know that the equivalence between a formula and its prenex normal form is derivable. Actually, it is enough to consider prenex normal forms where the left-most quantifier is universal, because each prefixing existential quantifier can be immediately eliminated by replacing the variable it binds with a constant. Let the degree of such a prenex normal formula be the number of blocks of universal quantifiers separated by existential ones. The proof is by in-duction on the degree:
(1) If every formula of degree k is either satisfiable or refutable, then so is every formula of degree k + 1. This is proved by Skolemisation. A for-mula of degree k + 1 is transformed into one of degree k which is equi-satisfiable with the first one. New function symbols are introduced in the process.
(2) Every formula of degree 1 is either satisfiable or refutable. A formula P of degree 1 is of the form ∀r ∃n A(r ; n), where r denotes a q-tuple of variables, and n denotes an s-tuple of variables. Let (rn ) be an infinite sequence of q-tuples of variables x0, x1, x2 . . . generated in (some) lexi-cographical order:
r 1 = (x0, x0, . . . , x0)
r 2 = (x1, x0, . . . , x0)
r 3 = (x0, x1, . . . , x0)
We define the sequence of formulae An by
A 1 = A(r1; x1, x2, . . . xs )
A 2 = A(r2; x1+s , x2+s , . . . x2s ) ∧ A1
An = A(rn ; x(n−1)s+1, x(n−1)s+2, . . . xns ) ∧ An−1
where, for each An , the variables put in the places bound by the exis-tential quantifier do not appear in the formulae Am for m < n. We denote by Pn the formula ∃x0 • • • ∃xns An . It is easy to show that P ⇒ Pn is derivable. Now, because each of An is a formula of propositional logic,
(a) either some An is refutable, and hence P is refutable because Pn is refutable;
(b) or, no An is refutable, that is, all An are satisfiable, and hence we get an infinite sequence of models
M1 ⊆ M2 ⊆ • • • ⊆ Mn ⊆ • • • .
Then M := ∪i ∈NMi is a model of the formula P .
The introduction notes to [82, 83, 84] see in the last step an application of K˝onig’s lemma, although Gödel himself justifies the step by “familiar argu-ments”.
Henkin’s proof.
It was Henkin who apparently first remarked the slight imprecision in the Skolemisation step of Gödel’s proof. Namely, in order to elim-inate existential quantifiers that follow universal ones, Skolemisation introduces new function symbols which are not interpreted in the models M1 ⊆ M2 ⊆ • • •, because they come from an extended language.
It is Henkin’s proof which is standard in today’s textbooks on logic. It was carried out in his PhD thesis and published in article form as [94]. Henkin’s the-sis goes beyond the article [94], because it also discusses completeness in the context of higher-order logic and proves, using completeness, Stone’s represen-tation theorem for Boolean algebras.
The key role is played by the following Model Existence Lemma.
Lemma. Let S0 be a signature. If Λ is a set of sentences of signature S0, which is consistent (Λ ⊥ ), then Λ has a model.
PROOF SKETCH. Let Si +1 be a signature that extends Si with countably many new constant symbols u0i+1, u1i+1, . . .. A set of sentences Γ of signature S will be called maximal consistent if, for any sentence A of signature S, A Γ → Γ, A ⊢
⊥ & Γ ⊥ , that is, if (Γ, A ⊢ ⊥ → Γ ⊢ ⊥) implies A ∈ Γ.
We will now construct Γ0, a maximal consistent set of sentences of S0, that contains the given set Λ. Let Γ0,0 := Λ. We fix an enumeration of formulae of signature S0. Let Γ0,1 := Γ0,0 ∪ {B1}, where B1 is the first formula from the enu-meration such that Γ0,0 ∪ {B1} is consistent. In general, let Γ0,i +1 := Γ0,i ∪ {Bi +1}, where Bi +1 is the (i + 1)-th formula from the enumeration such that Γ0,i ∪ {Bi +1} is consistent. We set Γ0 := ∪i ∈NΓ0,i , for which we have that:
• Λ⊆Γ0;
• Γ0 is consistent, because each one of Γ0,i is consistent by definition;
• Γ0 is maximal consistent: given A such that Γ0, A ⊢ ⊥ → Γ0 ⊢ ⊥, that is, given Γ0, A ⊥ , that is, given Γ0, A is consistent, we have that each Γ0,i , A is consistent. Since A also appears in the enumeration of formu-lae, for some j , A ∈ Γ0, j , hence A ∈ Γ0.
We have thus built a maximally consistent set of sentences of S0, Γ0.
We will now proceed to build a maximally consistent set of sentences of signature S1, Γ1.
Fix an enumeration of the sentences of Γ0. Select the first sentence of form ∃x A from the enumeration, and let A′ := A{u11/x}. We have replaced the free variable x of A with the first new constant from S1. The set Γ0, A′ is consistent: if Γ0, A′ ⊢ ⊥, then Γ0 ⊢ ¬A′, hence Γ0 ⊢ ∀x¬A, and Γ0 ⊢ ¬ x A, which contradicts the fact that Γ0 is consistent, since A ∈ Γ0.
Hence we can add to Γ0 all such A′, keeping it consistent. We now construct Γ1 in the same way we constructed Γ0, but starting from the consistent set of sentences Γ0, A′1, A′2, . . . .
We can iterate this procedure constructing a maximally consistent set Γi of sentences of signature Si , by starting from the consistent set Γi −1, Ai1′, Ai2′, . . ..
We can now define the set of sentences Γω := ∪i ∈NΓi , and easily see that it satisfies two properties:
(1) Γω is a maximally consistent set of sentences of signature Sω;
(2) if (∃x A) ∈ Γω, then A′ ∈ Γω.
Actually, as Henkin remarks, the entire construction was just in order to obtain these two properties.
We can now define the model promised by the statement of the Lemma. Let I be a structure of signature Sω in which the domain of individuals consists of all individual constants (the old constants of S0 and all the new ones). For an atomic formula A, we define the truth of A in I , by the derivability of A from Γω. The use of properties (1) and (2) is in showing that the extension to composite formulae A of the property, I A iff Γω ⊢ A, holds, that is, that validity in I is well defined. The proof is by induction on the complexity of A. Property (1) is used to handle implication (and negation), and property (2) is used to handle the quantifiers.
Table of contents :
Acknowledgements
Introduction
Chapter 1. Constructive completeness for Boolean models
1.1. Historical overview
1.2. Constructive ultra-filter theorem
1.3. Constructive Henkin-style proof
1.4. Computational content
1.5. Aspects of the Coq formalisation
1.6. Related and future work
Chapter 2. Kripke-stylemodels for classical logic
2.1. Normalisation-by-evaluation as completeness
2.2. Sequent calculus LKμ˜μ
2.3. Kripke-style models, call-by-name variant
2.4. Kripke-style models, call-by-value variant
2.5. Computational content
2.6. Aspects of the Coq formalisation
2.7. Related and future work
Chapter 3. Kripke-stylemodels for intuitionistic logic
3.1. Historical overview
3.2. Type-directed partial evaluation for ¸-calculus with sum
3.3. Completeness for Kripke-style models
3.4. Computational content
3.5. Aspects of the Coq formalisation
3.6. Related and future work
Chapter 4. Extension of intuitionistic logic with delimited control
4.1. The systemMQC+
4.2. Relationship to MQC and CQC
4.3. Subject reduction and progress
4.4. Normalisation, disjunction and existence properties
4.5. Applications, related and future work
Bibliography
Appendix A. Additional material for MQC+
A.1. Call-by-name translation forMQC+
A.2. Explicit version of the two-level CPS transform
