A proof procedure is correct when, in every proof using it, the conclusion logically follows from the premises. In other words, if in a correct proof procedure we derive a given sentence σ from a set of sentences Δ, then we have the guarantee that σ will logically follow from Δ. According to the definition of logical inference in Section 3.4: Syntax and Semantics of Predicate Logic, this means that in every structure where the sentences in Δ are true, the sentence σ is also true.
Completeness is the opposite of correctness. A proof procedure is complete when every logical inference between sentences can be proven with the procedure. In other words, if some sentence σ logically follows from a set of sentences Δ, we have the guarantee that there exists a proof in the procedure that starts from the sentences in Δ and arrives at the sentence σ (however, this does not mean that we are guaranteed to find this proof).
We will demonstrate that the proof procedure for predicate logic, introduced in Section 3.5: Proof Procedure, is both correct and complete.
We will assume the definitions of various syntactic and semantic concepts as provided in Section 3.4: Syntax and Semantics of Predicate Logic, such as those of formula, free and bound variables, structure, universe of discourse, interpretation, assignment of values, model, logical inference, logical equivalence, and so on.
With x, x1, ..., xn, we usually refer to arbitrary variables, and with c, c1, ..., cn, to arbitrary constants.
Expressions like α(x1...xn) will denote formulas in which, if there are free variables, they are among x1, ..., xn. It's important to note in this notation that some of the variables x1, ..., xn may not be free in the formula α (there may not even be any free variables in it). Similarly, with expressions like α(c1...cn), we will refer to formulas in which (potentially) the constants c1, ..., cn are involved. Often, this latter type of expression will be used in the same context as the former type of expressions in the following manner. α(c1...cn) can be obtained from α(x1...xn) by substituting each free occurrence of x1 with c1, x2 with c2, and so on; and vice versa – α(x1...xn) can be obtained from α(c1...cn) by substituting the constants c1, ..., cn with new variables x1, ..., xn (the fact that the variables are new guarantees that they will not be bound by quantifiers in α). Sometimes, for brevity, after we have started talking about α(x1...xn) or about α(c1...cn), we will only mention α, assuming that it is either α(x1...xn) or α(c1...cn).
If A is a structure and a1, ..., an are objects from the universe of discourse of A (not necessarily distinct), then by A ⊨ α(x1...xn)[a1...an], we express that the formula α(x1...xn) is true in A when the variable x1 takes the value a1, x2 takes the value a2, and so on, up to xn taking the value an. The assignment [a1...an] represents values assigned to the free variables in α (if any). In this context, the correspondence between variables and objects is determined by their order from left to right in "x1...xn" and "a1...an", not by their indices. The first variable from left to right corresponds to the first object from left to right, the second corresponds to the second, and so forth. Occasionally, to streamline the expression, we may omit "(x1...xn)", implying that α represents α(x1...xn).
A ⊭ α(x1...xn)[a1…an] indicates that the formula α is false in structure A for this assignment of values to its free variables.
If F is an n-ary predicate symbol, then FA represents the interpretation of F in structure A; that is, the set of ordered n-tuples of objects from the universe of discourse of A assigned to F by the interpretation in A.
"Terms" refer to both free variables and constants (when we want to remain ambiguous about whether we are discussing variables or constants). To denote an arbitrary term, we will use the symbol "t" (potentially with an index). In structures, terms signify objects (if the term is a free variable, the object is the value assigned to the variable). We will employ expressions like tA or tA(x1…xn)[a1…an] to denote the object represented by term t in structure A. The latter, more intricate expression accounts for the possibility that t may be a variable. If t is a constant, the denoted object depends solely on the interpretation, and the part "(x1…xn)[a1…an]" after tA is irrelevant. However, if t is a variable, the expression t(x1…xn) indicates that it must be one of the variables x1, ..., xn, and "[a1…an]" shows the value of each of these variables. For instance, if t is x2, then tA(x1…xn)[a1…an] will be a2 – t represents the second variable in the sequence x1, ..., xn, and thus takes the second object in the sequence a1, ..., an.
We will use "iff" as an abbreviation for "if and only if."
α1, …, αn ⇒ β means that the formula β logically follows from the formulas α1, …, αn; that is, in every structure where α1, …, αn are true, β is also true. If Δ is a set of formulas (which may be infinite), Δ ⇒ β means that β logically follows from the formulas in Δ (in every structure where the first ones are true, the latter one is true as well). Δ, α ⇒ β means that the formula β follows from the formulas in Δ and the formula α.
α ⇔ β means that the formulas α and β are logically equivalent; that is, they have the same truth value in every structure, for every assignment of values to their free variables (if any).
α1, …, αn ⊢ β means that there exists a proof (within some given proof procedure) where the sentences (formulas without free variables) α1, …, αn are premises and which concludes with the sentence β (the conclusion of the proof). If Δ is a set (which may be infinite) of sentences, Δ ⊢ β means that there exists a proof where some sentences from Δ are premises and β is the conclusion. Δ, α ⊢ β means that there exists a proof where some sentences from Δ and the sentence α are premises, and β is the conclusion.
The following terminological distinction is important in the context of correctness and completeness. We will say that σ logically follows from Δ, denoted as Δ ⇒ σ, and that σ is derivable from Δ, denoted as Δ ⊢ σ. The first concept is semantic, while the second relates to proof procedures. The relationship between the two concepts raises the question of the correctness and completeness of proof procedures.
We will discuss different languages and their lexicons. The lexicon consists of some set of predicate symbols (which may be infinite – for example, "F1", "F2", ...) and some set of constants (which may also be infinite). A language is completely defined by its lexicon. The language is the set of all formulas (well-formed formulas, see Section 3.4: Syntax and Semantics of Predicate Logic) that can be formed from the lexicon symbols, logical symbols ("→", "¬", "∀", ...), auxiliary bracket symbols ("(" and ")"), and an unlimited number of variables ("x1", "x2", "x3", ...). When a set of formulas is given, we will assume that it is part of some language. This could be the language whose lexicon consists of the predicates and constants involved in the formulas, but it could also be a language whose lexicon, in addition to these, includes predicate or constant symbols that do not participate in the formulas.
The proof procedure, whose correctness and completeness we will prove, is the proof procedure for predicate logic from Section 3.5: Proof Procedure. It utilizes inference rules, equivalence schemes, one axiom scheme, one special scheme (existential instantiation), and two types of subproofs with assumptions. More precisely, the procedure includes the following:
| Inference Schemes: |
| (From the formulas to the left of "⊢", the formula to the right can be inferred. α, β, γ, and δ are arbitrary sentences (formulas without free variables). "x" is an arbitrary variable. "c", "c1", and "c2" are arbitrary constants. α(x) is an (possibly) open sentence where the variable x is free.) |
| Modus Ponens: α→β, α ⊢ β |
| Modus Tollens: α→β, ¬β ⊢ ¬α |
| Disjunctive Syllogism: α∨β, ¬α ⊢ β |
| Hypothetical Syllogism: α→β, β→γ ⊢ α→γ |
| Simplification: α∧β ⊢ α |
| Addition: α ⊢ α∨β |
| Conjunction: α, β ⊢ α∧β |
| Constructive Dilemma: α∨γ, (α→β)∧(γ→δ) ⊢ β∨δ |
| Absorption: α→β ⊢ α→(α∧β) |
| Universal Instantiation: ∀xα(x) ⊢ α(c) where α(c) is obtained from α(x) by replacing all free occurrences of x in α(x) with the constant c |
| Indiscernibility of Identicals: c1=c2, α(c1) ⊢ α(c2) where α(c2) is obtained from α(c1) by replacing some (not necessarily all) occurrences of c1 with c2 |
| Equivalence Schemes: |
| (Unlike inference schemes, here α, β, and γ are formulas that can have free variables, i.e., they should be considered as abbreviations of α(x1…xn), β(x1…xn), γ(x1…xn). Equivalence schemes are used based on the following rule. Let the corresponding scheme be γ ⊣⊢ δ (or δ ⊣⊢ γ). If the formula γ is a subformula of the formula φ and the formula ψ is obtained from φ by replacing γ with δ, then ψ can be inferred from φ. In particular, the subformula of φ can be the formula φ itself. Then φ will be γ, and ψ – δ. Informally, this rule is based on the principle of substitutability of equivalents, according to which, if a subformula in a formula is replaced with a logically equivalent one, we obtain a formula that is logically equivalent to the original one. So, through equivalence schemes, we derive sentences that are logically equivalent to previous ones.) |
|
Transposition:
α→β ⊢ α→(α∧β) |
|
Double Negation:
¬¬α ⊣⊢ α |
|
Exportation:
(α∧β)→γ ⊣⊢ α→(β→γ) |
|
Material Implication:
α→β ⊣⊢ ¬α∨β ¬(α→β) ⊣⊢ α∧¬β |
|
De Morgan:
¬(α∧β) ⊣⊢ ¬α∨¬β ¬(α∨β) ⊣⊢ ¬α∧¬β |
|
Commutation:
α∨β ⊣⊢ β∨α α∧β ⊣⊢ β∧α |
|
Association:
α∧(β∧γ) ⊣⊢ (α∧β)∧γ α∨(β∨γ) ⊣⊢ (α∨β)∨γ |
|
Distribution:
α∧(β∨γ) ⊣⊢ (α∧β)∨(α∧γ) α∨(β∧γ) ⊣⊢ (α∨β)∧(α∨γ) |
|
Material Equivalence:
α↔β ⊣⊢ (α→β)∧(β→α) α↔β ⊣⊢ (α∧β)∨(¬α∧¬β) |
|
Tautology:
α∧α ⊣⊢ α α∨α ⊣⊢ α |
|
Relationship between Quantifiers:
¬∀xα ⊣⊢ ∃x¬α ∀x¬α ⊣⊢ ¬∃xα ¬∀x¬α ⊣⊢ ∃xα ∀xα ⊣⊢ ¬∃x¬α |
| Axiom Schemes: |
| (Sentences with this form can be derived at any time without assumptions.) |
| Law of identity: c=c where c is any constant |
| Other Schemes: |
| Existential Instantiation: ∃α(x) ⊢ α(c) where α(c) is obtained from α(x), by replacing all free occurrences of x with the constant c, and c does not occur in the premises, the conclusion, or any previous lines of the proof or subproof in which this scheme is applied |
| Subproofs with Assumption: |
| (Γ is the set of premises, i.e., the outer sentences used in the subproof. α and β are sentences, from which α is the assumption.) |
| Reductio ad absurdum: If Γ, α ⊢ β∧¬β, then Γ ⊢ ¬α |
| Conditional Proof: If Γ, α ⊢ β, then Γ ⊢ α→β |
Before we delve into correctness and completeness, we will prove a fundamental fact about semantic structures: that each structure is consistent and entirely determined. Additionally, we will establish the principle of substitutability of equivalents, upon which the use of equivalence schemes is based.
In structures, formulas become true or false. The following theorem guarantees us that every formula of the language of a structure is either true or false in it, and that it is not possible for a formula to be both true and false in it. Due to the semantic rule for negation (see 3.4 Syntax and Semantics of Predicate Logic), this means that for every formula of the language of the structure, it holds that either it or its negation is true in the structure, and it is not possible for a formula and its negation to be simultaneously true in it.
(1) Let A be an arbitrary structure, φ(x1…xn)1 be an arbitrary formula of the language of A, and a1, …, an be arbitrary objects from the universe of A. Then the following holds: A ⊨ φ[a1…an] or A ⊭ φ[a1…an], but not both.
Proof:
We will use induction based on the complexity of the formula φ. We define the complexity of a formula as follows. If the formula is atomic, its complexity is 0. If the maximum complexity of its subformulas, which are different from it, is s, then its complexity is s+1. For example, "Fx" has complexity 0, "Fx ∧ Ga" has complexity 1, "∃xFx ∧ Ga" has complexity 2, "¬(Fx ∧ Ga)" also has complexity 2, "∃x¬(Fx ∧ Ga)" has complexity 3, ... and so on. First, we will show that the asserted proposition holds for all formulas φ(x1…xn) with complexity 0. Then, assuming it holds for all formulas with complexity k (we will refer to this assumption as the "induction hypothesis"), we will show that it holds for all formulas with complexity k+1. Thus, we obtain the following: the proposition holds for all formulas with complexity 0; therefore, it holds for all formulas with complexity 1; therefore, it holds for all formulas with complexity 2, ... and so on; meaning, there is no formula for which it does not hold. So, let φ(x1…xn) have complexity 0.
Case 1, φ(x1…xn) is an atomic formula of the form Ft1…tm(x1…xn)2.
We consider an arbitrary structure A and arbitrary objects a1, …, an in it. Let t1A(x1…xn)[a1…an]3 be the object b1, t2A(x1…xn)[a1…an] be the object b2, …, tmA(x1…xn)[a1…an] be bm. According to the semantic rules (see 3.4 Syntax and Semantics of Predicate Logic), Ft1…tm(x1…xn)[a1…an] is true in A if and only if the tuple of m elements (b1, …, bm) is an element of FA (the set of tuples of m elements that the interpretation of A assigns to the predicate letter F). (b1, …, bm) is either an element or not an element of FA, but not both. Therefore, A ⊨ Ft1…tm(x1…xn)[a1…an] or A ⊭ Ft1…tm(x1…xn)[a1…an], but not both (i.e., A ⊨ φ(x1…xn)[a1…an] or A ⊭ φ(x1…xn)[a1…an], but not both).
Case 2, φ(x1…xn) is an atomic formula of the form t1=t2(x1…xn).
We consider an arbitrary structure A and arbitrary objects a1, …, an in it. Let t1A(x1…xn)[a1…an] be the object b1, and t2A(x1…xn)[a1…an] be the object b2 in A. According to the semantic rules, A ⊨ t1=t2(x1…xn)[a1…an] if and only if t1A(x1…xn)[a1…an] = t2A(x1…xn)[a1…an], meaning b1 is the same object as b2. b1 and b2 are either different objects or the same object, but not both. Therefore, A ⊨ t1=t2(x1…xn)[a1…an] or A ⊭ t1=t2(x1…xn)[a1…an], but not both (i.e., in the considered case, the proposition holds).
There are no other formulas with complexity 0. Therefore, now we assume that the asserted proposition holds for all formulas with complexity k, and we assume that φ(x1…xn) has complexity k+1. Now, φ cannot be an atomic formula (because its complexity is at least 1), but it is either a negation, conjunction, disjunction, conditional, biconditional, universal formula, or existential formula. We will show that in each of these cases, the asserted proposition holds.
Case 3, φ(x1…xn) takes the form of negation, i.e., φ is ¬ψ(x1…xn).
Let A be an arbitrary structure and a1, …, an be arbitrary objects in it. According to the semantic rules, A ⊨ ¬ψ[a1…an], if and only if A ⊭ ψ[a1…an] (i.e., if and only if ψ[a1…an] is not true in A). From the induction hypothesis (since ψ(x1…xn) has complexity k), ψ[a1…an] is either false (i.e., it is not true) in A, or it true (i.e., it is not the case that it is not true) in A, but not both. Therefore, A ⊨ ¬ψ[a1…an] or A ⊭ ¬ψ[a1…an], but not both (i.e., in the considered case, the proposition holds).
Case 4: φ(x1…xn) takes the form of conjunction, meaning φ is ψ1∧ψ2(x1…xn).
Let A be an arbitrary structure and a1, …, an represent arbitrary objects within it. According to the semantic rules, A ⊨ ψ1∧ψ2[a1…an], if and only if A ⊨ ψ1[a1…an] and A ⊨ ψ2[a1…an]. Given the induction hypothesis, each of ψ1[a1…an] and ψ2[a1…an] is either true in A, or false in A, but not both. Therefore (considering the four possible exclusive cases for the truth or falsity of ψ1[a1…an] and ψ2[a1…an] in A), A ⊨ ψ1∧ψ2[a1…an] or A ⊭ ψ1∧ψ2[a1…an], but not both (i.e., in this particular case, the proposition holds).
Case 5: φ(x1…xn) takes the form of disjunction, meaning φ is ψ1∨ψ2(x1…xn).
This case is entirely analogous to Case 4, using the semantic rule for disjunction instead of conjunction.
Case 6: φ(x1…xn) takes the form of conditional, meaning φ is ψ1→ψ2(x1…xn).
This case is entirely analogous to Case 4, using the semantic rule for conditional instead of conjunction.
Case 7: φ(x1…xn) takes the form of biconditional, meaning φ is ψ1↔ψ2(x1…xn).
This case is entirely analogous to Case 4, using the semantic rule for biconditional instead of conjunction.
Case 8: φ(x1…xn) is a universal formula, meaning φ is ∀xiψ(x1…xi…xn).
Let A be an arbitrary structure and a1, …, an be arbitrary objects in it. According to the semantic rules, A ⊨ ∀xiψ(x1…xi…xn)[a1…an], if and only if for every object b from the universe of A, A ⊨ ψ(x1…xi…xn)[a1…b…an]. From the induction hypothesis, for every object b from A, A ⊨ ψ(x1…xi…xn)[a1…b…an] or A ⊭ ψ(x1…xi…xn)[a1…b…an], but not both. This means ψ(x1…xi…xn)[a1…b…an] will be true for every object b from A or it won't be, but not both. By semantic rules, A ⊨ ∀xiψ(x1…xi…xn)[a1…an] or A ⊭ ∀xiψ(x1…xi…xn)[a1…an], but not both (i.e., in the considered case, the proposition holds).
Case 9: φ(x1…xn) is an existential formula, meaning φ is ∃xiψ(x1…xi…xn).
This case is entirely analogous to Case 8, using the semantic rule for existential quantifier instead of universal. With this, the induction and the proof are completed.
The use of equivalence schemes in the proof procedure relies on this principle. Although the formula on each line in a proof has no free variables, when we use equivalence schemes, we could replace a subformula of the formula, in which there are free variables. Therefore, we need to prove the principle of substitutability of equivalents for any formulas, not just sentences with no free variables:
(2) Let φ(x1…xn) be a subformula of γ(x1…xn) and φ(x1…xn) ⇔ ψ(x1…xn). Let also δ(x1…xn) be obtained from γ(x1…xn) by replacing φ(x1…xn)4 with ψ(x1…xn). Then γ(x1…xn) ⇔ δ(x1…xn).
Proof:
As in the proof of (1), we will employ induction, but this time it will not be based on the complexity of the formulas, but rather on what we will refer to as the "depth" of a subformula within a formula. We define depth based on complexity (defined in the proof of (1)) as follows: if φ is a subformula of γ, then the "depth of φ in γ" is the difference between their complexities. For example, let's examine the depths of the different subformulas of "∀y(Gy ∧ ∃xFx)". This formula has a complexity of 3. Its subformula "Fx" (with complexity 0) has a depth of 3 (3-0) within it; "∃xFx" (with complexity 1) has a depth of 2 (3-1) within it, " Gy ∧ ∃xFx" (with complexity 2) has a depth of 1 (3-2) within it. If φ coincides with γ, φ has a depth of 0 within γ. Alternatively, depth corresponds to the level (top-down, starting from 0) at which the subformula is located in the syntactic tree of the formula of which it is a part (for syntactic trees, see 1.3 Truth Tables). Induction will be based on the depth of φ in γ in the formulation of the theorem.
So, first, we consider the case when φ(x1…xn) has a depth of 0 within γ(x1…xn). Then γ coincides with φ and ψ coincides with δ, and since φ ⇔ ψ, γ ⇔ δ.
As the next step, we assume that when the depth of a subformula in a formula is k, the principle of substitutability of equivalents is valid. We want to show that the principle will then also be valid when the depth of a subformula in a formula is k+1. So let the depth of φ in γ be k+1. Since the depth of φ in γ is at least 1, φ cannot coincide with γ. Then the immediate context of φ (the simplest formula, different from it, of which it is a subformula) is either a negation, conjunction, disjunction, conditional, biconditional, existential formula, or universal formula. We will show that in all these cases, the asserted proposition, namely γ ⇔ δ, holds.
Case 1, the immediate context of φ(x1…xn) is negation, i.e., γ(x1…xn) is …¬φ…(x1…xn).
Let A be an arbitrary structure and a1, …, an be arbitrary objects in it. Then the following holds:
| A ⊨ ¬φ[a1…an] |
|
iff
(by semantic rules) |
| A ⊭ φ[a1…an] |
|
iff
(from φ ⇔ ψ, because φ and ψ have the same truth value in every structure, for every assignment of values to their free variables) |
| A ⊭ ψ[a1…an] |
|
iff
(by semantic rules) |
| A ⊨ ¬ψ[a1…an] |
The above sequence of equivalences shows that ¬φ and ¬ψ have the same truth value in every structure, for any assignment of values to their free variables, i.e., ¬φ ⇔ ¬ψ. The depth of ¬φ in γ is k (unlike the depth of φ in γ, which is k+1), and thus (from the induction hypothesis) the substitutability of equivalents holds for this formula. Since in this case δ is obtained from γ not only by replacing φ with ψ, but also by replacing ¬φ with ¬ψ, by the substitutability of equivalents, we obtain γ ⇔ δ.
Case 2, the immediate context of φ(x1…xn) is conjunction, i.e., γ(x1…xn) is …(φ∧χ)…(x1…xn) or …(χ∧φ)…(x1…xn).
Let A be an arbitrary structure and a1, …, an be arbitrary objects in it. Then the following holds:
| A ⊨ φ∧χ[a1…an] |
|
iff
(by semantic rules) |
| A ⊨ φ[a1…an] and A ⊨ χ[a1…an] |
|
iff
(from φ ⇔ ψ) |
| A ⊨ ψ[a1…an] and A ⊨ χ[a1…an] |
|
iff
(by semantic rules) |
| A ⊨ ψ∧χ[a1…an]5 |
The above sequence of equivalences shows that φ∧χ ⇔ ψ∧χ. The depth of the formula φ∧χ in γ is k, and thus (from the induction hypothesis) the substitutability of equivalents holds for this formula. Since in this case δ is also obtained from γ by replacing φ∧χ with ψ∧χ (for which the principle holds), then γ ⇔ δ.
Case 3, the immediate context of φ(x1…xn) is disjunction, i.e., γ(x1…xn) is …(φ∨χ)…(x1…xn) or …(χ∨φ)…(x1…xn).
This case is entirely analogous to Case 2, using the semantic rules for disjunction instead of conjunction.
Case 4, the immediate context of φ(x1…xn) is conditional, where φ(x1…xn) is the antecedent, i.e., γ(x1…xn) is …(φ→χ)…(x1…xn).
This case is entirely analogous to Case 2, using the semantic rules for conditional instead of conjunction.
Case 5, the immediate context of φ(x1…xn) is conditional, where φ(x1…xn) is the consequent, i.e., γ(x1…xn) is …(χ→φ)…(x1…xn).
This case is entirely analogous to Case 2, using the semantic rules for conditional instead of conjunction.
Case 6, the immediate context of φ(x1…xn) is biconditional, i.e., γ(x1…xn) is …(φ↔χ)…(x1…xn) or …(χ↔φ)…(x1…xn).
This case is entirely analogous to Case 2, using the semantic rules for biconditional instead of conjunction.
Case 7, φ(x1…xn) is the scope of an existential quantifier, i.e., γ(x1…xn) is …∃xiφ…(x1…xi…xn).
Let A be an arbitrary structure and a1, …, an be arbitrary objects in it. Then the following holds:
| A ⊨ ∃xiφ(x1…xi…xn)[a1…an] |
|
iff
(by semantic rules) |
| For some object b from the universe of A, A ⊨ φ(x1…xi…xn)[a1…b…an] |
|
iff
(from φ ⇔ ψ) |
| For some object b from the universe of A, A ⊨ ψ(x1…xi…xn)[a1…b…an] |
|
iff
(by semantic rules) |
| A ⊨ ∃xiψ(x1…xi…xn)[a1…an] |
The above series of equivalences shows that ∃xiφ(x1…xi…xn) ⇔ ∃xiψ(x1…xi…xn). Since the depth of ∃xiφ(x1…xi…xn) in γ is k, the substitutability of equivalents holds for this formula. Since in this case δ is also obtained from γ by replacing ∃xiφ(x1…xi…xn) with ∃xiψ(x1…xi…xn), γ ⇔ δ.
Case 8, φ(x1…xn) is the scope of a universal quantifier, i.e., γ(x1…xn) is …∀xiφ…(x1…xi…xn).
This case is entirely analogous to Case 7, using the semantic rules for the universal quantifier instead of the existential.
We have examined all cases for a subformula φ(x1…xn) of a formula γ(x1…xn), when its depth in γ(x1…xn) is k+1, and we have seen that the principle of substitutability for equivalents holds (assuming it holds for subformulas with depth k). With this, the induction and proof are completed.
By using the symbolism introduced in the Concepts and notations above, the correctness of a proof procedure can be succinctly expressed as follows:
For every set of sentences Δ and every sentence σ, if Δ ⊢ σ, then Δ ⇒ σ.
We will demonstrate that for our proof procedure the following holds:
(3.1) If in a proof there are no subproofs with assumptions and every line, which is not a premise and not derived by existential instantiation, follows logically from previous lines or is a logically valid sentence, then the conclusion of this proof follows logically from its premises.
(3.2) All inference schemes are logically valid. (That is, in every structure where sentences in the form of their premises are true, the corresponding sentences in the form of their conclusions are also true.)
(3.3) All equivalence schemes are logically valid. (That is, if the scheme is γ ⊣⊢ δ and any formulas φ(x1…xn) and ψ(x1…xn) have the forms respectively of γ and δ, then φ(x1…xn) and ψ(x1…xn) are logically equivalent.)
(3.4) All axiom schemes are logically valid. (That is, if a sentence has the form of an axiom scheme, then it is true in every structure.)
(3.5) For every subproof with assumption "If Γ, p ⊢ r, then Γ ⊢ q", where Γ is the set of premises of the subproof (i.e., the external premises used), p is the assumption, and q is its conclusion 6, it holds: if Γ, p ⇒ r, then Γ ⇒ q.
Then the proof procedure will be correct due to the following. Let's consider an arbitrary proof within it with premises being the sentences from some set Δ and a conclusion being some sentence σ. We want to show that σ logically follows from Δ.
First, let's assume that the proof does not use subproofs with assumptions. Then (3.1)-(3.4) guarantee that σ logically follows from Δ due to the following reasoning. In such a proof, for every sentence p not included in the premises Δ and not derived with existential instantiation, we have three possibilities. First, p may have the form of an axiom scheme and consequently be derived without premises. According to (3.4), in this case, p is a logically valid sentence. Second, p may be obtained from previous lines via some inference scheme, which is logically valid as per (3.2), meaning that in deductions made with it, conclusions logically follow from the premises. Third (and lastly), p may be derived from the sentence q on some previous line via some equivalence scheme, where some subformula φ(x1…xn) of q has been replaced with a formula ψ(x1…xn). Following (3.3), φ(x1…xn) and ψ(x1…xn) are logically equivalent. Hence, from the principle of substitutability of equivalents established in (2), it follows that p and q are logically equivalent, and therefore, p logically follows from q. Thus, every line that is not a premise and is not derived with existential instantiation either logically follows from previous lines or is a logically valid sentence. Consequently, based on (3.1), σ logically follows from Δ.
Now, let's remove the restriction that there are no subproofs with assumptions in the proof. On the contrary, let's imagine that there are subproofs within which there are others, and so on. It is clear that in such chains of nested subproofs, we eventually reach subproofs where there are no further subproofs. These latter ones are essentially ordinary proofs of the form Γ, p ⊢ r, where Γ consists of sentences external to the subproof, and p is the assumption. In the preceding paragraph, we demonstrated that such proofs are correct (under the conditions of (3.1)-(3.5)), i.e., we have Γ, p ⇒ r. Consequently, based on (3.5), it follows that Γ ⇒ q; in other words, the conclusion of the subproof logically follows from some sentences before the subproof. This allows us to eliminate the subproof by simply removing it and retaining only its conclusion q. What matters is that q logically follows from some previous sentences. Suppose for a moment that there are no other (not yet deleted) subproofs at the same level as the deleted one, i.e., there are no other (not deleted) subproofs initiated within the same higher-level subproof where the deleted one starts. The aforementioned higher-level subproof will then become a sequence of lines starting with its assumption and proceeding in such a way that each subsequent line in it, not logically valid and not derived with existential instantiation, logically follows from some previous lines7. Similar to the first deleted subproof, from (3.1) and (3.5), it follows that the conclusion of this higher-level subproof logically follows from earlier sentences external to it, thereby allowing us to remove it and retain only its conclusion. Thus, beginning from the outermost subproofs and progressing upwards, eliminating all subproofs, what remains ultimately is a sequence of sentences starting with the premises of the entire proof Δ and concluding with its conclusion σ, devoid of subproofs, wherein each sentence, not part of Δ and not derived with existential instantiation, either logically follows from some previous sentences or is logically valid. Consequently, based on (3.1), σ logically follows from Δ, as intended.
The proof of correctness will be completed once we demonstrate that the conditions (3.1) through (3.5) are satisfied for our proof procedure. The most crucial of these is (3.1), which essentially concerns the use of existential instantiation in principle.
Let's reconsider statement (3.1):
If in a proof there are no subproofs with assumptions and every line, which is not a premise and not derived by existential instantiation, follows logically from previous lines or is a logically valid sentence, then the conclusion of this proof follows logically from its premises.
Its significance is that existential instantiation does not compromise the proof procedure. Although this scheme is not logically valid, (3.1) assures us that if the remaining schemes are logically valid, the conclusions of our proofs and subproofs will follow from their premises despite this invalid inference scheme. This is possible due to the restrictions placed on its usage. As can be seen from Proof procedure, these restrictions are that the instantiated constant should not appear 1) in the premises, 2) in the conclusion, 3) in previous lines of the proof or subproof where we apply the scheme.
Proof of (3.1):
Let's examine an arbitrary proof in which there are no subproofs with assumptions, and in which every sentence that is not a premise and is not derived with existential instantiation logically follows from previous sentences or is logically valid. Let the premises of this proof be sentences from the set Δ, and its conclusion be the sentence σ. We want to show that σ logically follows from Δ. The predicate and constant symbols participating in the sentences in Δ and in σ define some language L (they constitute its lexicon). To prove that Δ ⇒ σ, i.e., that every model of Δ is also a model of σ, we will consider an arbitrary structure A with language L, in which all sentences in Δ are true, and we will show that σ is also true in A. To achieve this, we will construct a structure that is an expansion of A. In principle, a structure A′ with language L′ is called an expansion of a structure A with language L when A′ is the same structure as A except that in its language (L′) there are additional symbols that it interprets in some way. Thus, the lexicon of L is a proper subset of the lexicon of L′. For structures and their expansions, the following holds: The sentences from the poorer language L that are true in the expansion A′ are the same as the sentences true in A. The additional symbols from L′ do not participate in these sentences and are not related to determining their truth value in A′, and abstracting from the additional symbols the two structures are one and the same structure. In other words, because concerning the poorer language L, the two structures do not differ, the same sentences from this poorer language are true in both of them. The opposite term of expansion is reduct – when A′ is an expansion of A, A is a reduct of A′.
Returning to the proof of (3.1), in order to demonstrate that in every structure А, where the sentences from Δ are true, σ is also true, we will construct a structure А′, which is an expansion of А, where all lines of the proof (including lines derived with existential instantiation) are true. This implies that σ will be true in А′. Since σ is from the language of А and is true in А′ (the expansion of А), this implies that σ will be true in А, which is what we aim to demonstrate. The additional symbols in А′ will be the new constants introduced in the proof through existential or universal instantiation.8 This is the idea of the proof; the proof itself follows.
Let c1, …, cn be all the new (not from the lexicon of L) constants introduced through existential or universal instantiation in the proof of σ from Δ, with their order corresponding to their appearance sequence in the proof. Adding them to the lexicon of L yields a new, richer language L′. We consider the following sequence of structures:
А, А1, А2, …, Аn (=A′)
The structure А1 is an expansion of the structure А, where its language is obtained from that of А by adding the constant c1. А2 is an expansion of А1, where its language is obtained from that of А1 by adding the constant c2, and so on. The structure Аn is the last in this sequence and coincides with А′ (the expansion we discussed in the previous paragraph). Each constant ci from the constants c1, ..., cn appears for the first time in some line of the proof as part of the sentence φi(ci), which is derived from ∃φi(x)9 on a higher line by existential instantiation or from ∀xφi(x) by universal instantiation. We will define each structure Аi, while simultaneously showing that all sentences in the proof up to φi(ci), inclusive, are true in Аi.
First, the sentences on each line in the proof until the first new constant c1 appears in φ1(c1) are true in structure A, because they are either premises in the proof (and are true in A according to the initial assumption), or they are logically valid sentences (and are true in every structure, including A), or they logically follow from previous sentences, which in turn follow from previous sentences, ... and so on, with the beginnings of these chains being either premises of the proof or logically valid sentences (both true in A), and logical inference guarantees the truth of conclusions in structures where the premises are true. Since all sentences before φ1(c1) are true in A, then the sentence from which φ1(c1) is derived – ∃xφ1(x) or ∀xφ1(x) (depending on whether it is derived by existential or universal instantiation) – is true in A. This (by semantic rules) means that in the universe of A, there exists (at least one) object a1, for which A ⊨ φ1(x)[a1]. We define structure A1 as an expansion of A, interpreting the new constant c1 as the object a1. Then from A ⊨ φ1(x)[a1], it follows that A1 ⊨ φ1(c1), i.e., φ1(c1) is true in A1. Furthermore, all previous sentences are also true in A1, because they are true in A, and A1 is an expansion of A. Thus, we have simultaneously defined A1 and shown that all sentences in the proof up to φ1(c1) inclusive are true in A1. We continue with A2. Until the point where the new constant c2 appears in the proof as part of the sentence φ2(c2) (obtained by existential or universal instantiation from ∃xφ2(x) or ∀xφ2(x)), all sentences are true in A1, because they are logically valid or logically follow from sentences we have already shown to be true in A1. Therefore, the sentence ∃xφ2(x) or ∀xφ2(x) is also true in A1. By semantic rules, this implies that there exists (at least one) object a2 in A1 such that A1 ⊨ φ2(x)[a2]. A2 is obtained from A1 by interpreting c2 as a2. Then from A1 ⊨ φ2(x)[a2], it follows that A2 ⊨ φ2(c2), i.e., φ2(c2) is true in A2, and furthermore, all sentences before it are also true in A2, because they are true in A1, and A2 is an expansion of A1. Thus, we have simultaneously defined A2 and shown that all sentences in the proof up to φ2(c2) inclusive are true in A2 ... and so on. We continue in the same manner until we reach the point in the proof where existential or universal instantiation yields φn(cn). Then similarly, we simultaneously define An (previously denoted as A′) and demonstrate that all sentences in the proof up to φn(cn) inclusive are true in An. If the sentence φn(cn) is derived by existential instantiation, then it cannot be the conclusion of the proof σ, because restrictions on existential instantiation forbid constants introduced by existential instantiation to appear in the conclusion of the proof, but (since there are no existential instantiations later in the proof) σ is derived through logically valid inferences, and therefore follows logically from sentences that are true in An. So, σ is true in An. Then, since σ is from the language of A, and An is an expansion of A (it is clear that expanding an expansion of a structure is an expansion of that structure), σ is also true in A, as desired. Since A was an arbitrary structure, it follows that in every structure where the sentences in Δ are true, the sentence σ is true, i.e., σ follows logically from Δ. The proof of (3.1) is complete.
Up to this point (since we haven't used anything specific to our proof procedure), we have actually shown that every proof procedure that uses valid inference, equivalence, and axiom schemes, that employs correct subproofs with assumptions, and in which the only logically invalid scheme is existential instantiation (with its restrictions), is correct. Now it remains to show that specifically our proof procedure is such, by demonstrating that it satisfies conditions (3.2)-(3.4) (the inference, equivalence, and axiom schemes used are logically valid) and (3.5) (both subproofs with assumptions are correct).
For each inference scheme φ1, …, φn ⊢ ψ in Proof Procedure excluding the last two (universal instantiation and indiscernibility of identicals)10, it can be verified (using truth tables or truth-functional analysis) that if we form the conditional of the conjunction of its premises and its conclusion, i.e., (φ1∧…∧φn)→ψ, we obtain a tautology. According to (1), any sentence α, β, γ, or δ (the inference schemes are formulated using these four Greek letters) in φ1, …, φn, and ψ attains some truth value in any structure A, which in turn determines in some way (by the semantic rules for logical connectives) the truth values of φ1, …, φn, and ψ. Then, if the premises φ1, …, φn are true in A (i.e., their conjunction φ1∧…∧φn is true in A), the conclusion ψ must also be true in A, because otherwise the conditional (φ1∧…∧φn)→ψ would have a value of F, which contradicts the fact that it is a tautology. Therefore, in every structure where the premises are true, the conclusion is also true, i.e., the inference schema is logically valid. Let's now see why the inference schemes of universal instantiation and indiscernibility of identicals are also valid.
For universal instantiation (∀xα(x) ⊢ α(c)), let the sentence ∀xα(x) be true in an arbitrary structure A, i.e., A ⊨ ∀xα(x). The interpretation of A assigns some object b from the universe of A to the constant c. By the semantic rules for the universal quantifier, from A ⊨ ∀xφ(x), it follows that for every object a from the universe of A, A satisfies φ[a]. Thus, in particular, A satisfies φ[b]. Since the constant c denotes b, from A ⊨ φ[b], it follows that A ⊨ φ(c). Therefore, in every structure where ∀xφ(x) is true, φ(c) is also true, i.e., ∀xα(x) logically entails α(c).
For indiscernibility of identicals (c1=c2, α(c1) ⊢ α(c2)), let the sentences c1=c2 and α(c1) be true in an arbitrary structure A, i.e., A ⊨ c1=c2 and A ⊨ α(c1). The constant c1 denotes some object a from the universe of A, and from A ⊨ c1=c2 (by the semantic rules), it follows that c2 also denotes a. By replacing those occurrences of c1 in α(c1) that correspond to the occurences of c2 in α(c2) with a new variable x, we obtain the formula α(x) (the fact that x is new ensures that all its occurrences are free in α(x)). From A ⊨ α(c1), it follows that A ⊨ α(x)[a] (i.e., α(x) is true in A when x takes as its value the object with which c1 is interpreted). But from the latter and the fact that c2 is also interpreted as a, it follows that A ⊨ α(c2). We have thus shown that in every structure where the sentences c1=c2 and α(c1) are true, α(c2) is also true, i.e., the latter sentence logically follows from the former two. With this, we have demonstrated that all inference schemes in our proof procedure are logically valid.
We move on to the equivalence schemes. For each equivalence scheme φ ⊣⊢ ψ in the proof procedure excluding the last one (the four forms of the relationship between quantifiers)11, it can be verified using a truth table or truth-functional analysis that φ↔ψ is a tautology. Let A be an arbitrary structure and a1, …, a1 be arbitrary objects in it. According to (1), the formulas α(x1…xn), β(x1…xn), and γ(x1…xn)12, which participate as subformulas in φ and ψ, are either true or false in A for a1, …, an, i.e., α(x1…xn)[a1…an], β(x1…xn)[a1…an], and γ(x1…xn)[a1…an] are true or false in A. This, in turn, determines in some way (according to the semantic rules for logical connectives) the truth values of φ(x1…xn)[a1…an] and ψ(x1…xn)[a1…an] in A. These truth values must be the same in A, because the opposite would mean that the formula φ↔ψ can evaluate to F, which contradicts the fact that it is a tautology. It follows that φ and ψ have the same truth value in every structure for any values of their free variables, i.e., φ ⇔ ψ.
Regarding the relationship between quantifiers. Concerning ¬∀xα ⊣⊢ ∃x¬α: based on the semantic rules, for an arbitrary structure A and arbitrary objects a1, …, an in it, the following holds:
| A ⊨ ¬∀xiα(x1…xi…xn)[a1…an] |
| iff |
| A ⊭ ∀xiα(x1…xi…xn)[a1…an] |
| iff |
| For some object a in A, A ⊭ α(x1…xi…xn)[a1…a…an] |
| iff |
| For some object a in A, A ⊨ ¬α(x1…xi…xn)[a1…a…an] |
| iff |
| A ⊨ ∃xi¬α(x1…xi…xn)[a1…an] |
It follows that ¬∀xα and ∃x¬α have the same truth value in every structure for any values of their free variables, i.e., ¬∀xα ⇔ ∃x¬α.
Concerning ∀x¬α ⊣⊢ ¬∃xα: based on the semantic rules, for an arbitrary structure A and arbitrary objects a1, …, an in it, the following holds:
| A ⊨ ∀xi¬α(x1…xi…xn)[a1…an] |
| iff |
| For every object a in A, A ⊨ ¬α(x1…xi…xn)[a1…a…an] |
| iff |
| For every object a in A, it is not true that A ⊨ α(x1…xi…xn)[a1…a…an] |
| iff |
| It is not true that for some object a in A, A ⊨ α(x1…xi…xn)[a1…a…an] |
| iff |
| It is not true that A ⊨ ∃xiα(x1…xi…xn)[a1…an] |
| iff |
| A ⊨ ¬∃xiα(x1…xi…xn)[a1…an] |
It follows that ∀x¬α and ¬∃xα have the same truth value in every structure for any values of their free variables, i.e., ∀x¬α ⇔ ¬∃xα.
Regarding ¬∀x¬α ⊣⊢ ∃xα: based on the semantic rules, for an arbitrary structure А and arbitrary objects a1, …, an in it, the following holds:
| A ⊨ ¬∀xi¬α(x1…xi…xn)[a1…an] |
| iff |
| It is not true that A ⊨ ∀xi¬α(x1…xi…xn)[a1…an] |
| iff |
| It is not true that for every object a in A, A ⊨ ¬α(x1…xi…xn)[a1…a…an] |
| iff |
| It is not true that for every object a in A, it is not true that A ⊨ α(x1…xi…xn)[a1…a…an] |
| iff |
| For some object a in A, A ⊨ α(x1…xi…xn)[a1…a…an] |
| iff |
| A ⊨ ∃xiα(x1…xi…xn)[a1…an] |
It follows that ¬∀x¬α and ∃xα have the same truth value in every structure for any values of their free variables, i.e., ¬∀x¬α ⇔ ∃xα.
Regarding ∀xα ⊣⊢ ¬∃x¬α: based on the semantic rules, for an arbitrary structure А and arbitrary objects a1, …, an in it, the following holds:
| A ⊨ ¬∃xi¬α(x1…xi…xn)[a1…an] |
| iff |
| It is not true that A ⊨ ∃xi¬α(x1…xi…xn)[a1…an] |
| iff |
| It is not true that for some object a in A, A ⊨ ¬α(x1…xi…xn)[a1…a…an] |
| iff |
| It is not true that for some object a in A, it is not true that A ⊨ α(x1…xi…xn)[a1…a…an] |
| iff |
| For every object a in A, A ⊨ α(x1…xi…xn)[a1…a…an] |
| iff |
| A ⊨ ∀xiα(x1…xi…xn)[a1…an] |
It follows that ∀xα and ¬∃x¬α have the same truth value in every structure for any values of their free variables, i.e., ∀xα ⇔ ¬∃x¬α. Thus, the logical validity of the relationship between quantifiers and, in general, the equivalence schemes of the proof procedure, is proven.
As for the sole axiom scheme, the law of identity (c=c), its validity is a direct consequence of the semantic rule for identity ("=").
It remains to show that the two subproofs with assumptions, reductio ad absurdum (if Γ, α ⊢ β∧¬β, then Γ ⊢ ¬α) and conditional proof (if Γ, α ⊢ β, then Γ ⊢ α→β), satisfy (3.5) (For each subproof with assumption "If Γ, p ⊢ r, then Γ ⊢ q" holds: if Γ, p ⇒ r, then Γ ⇒ q), i.e., we need to prove:
If Γ, α ⇒ β∧¬β, then Γ ⇒ ¬α
If Γ, α ⇒ β, then Γ ⇒ α→β
For the first proposition: let Γ, α ⇒ β∧¬β and let every proposition in Γ be true in an arbitrary structure A (A ⊨ Γ). If α is true in A, from A ⊨ Γ and Γ, α ⇒ β∧¬β, it follows that β∧¬β must be true in A, which, based on (1), is impossible. Therefore, α is not true in A, from which, according to semantic rules, it follows that A ⊨ ¬α. Thus, if Γ, α ⇒ β∧¬β, then every model of Γ is a model of ¬α, i.e., Γ ⇒ ¬α, which is what needed to be proved.
For the second proposition: let Γ, α ⇒ β and let A be an arbitrary structure such that A ⊨ Γ. If α is not true in A, according to semantic rules, α→β is true in A. If α is true in A, from A ⊨ Γ and Γ, α ⇒ β, it follows that β is also true in A, and thus (according to semantic rules) α→β is true in A. Therefore, in all cases, α→β is true in A. So, if Γ, α ⇒ β, then every model of Γ is a model of α→β, i.e., Γ ⇒ α→β, which was to be proven.
With this, the proof of the correctness of the proof procedure is completed. We proceed to prove its completeness.
So far, we have used the following definitions for correctness and completeness. A proof procedure is correct when, for every set of sentences Δ and every sentence σ, it holds that if σ is derivable from Δ, σ logically follows from Δ:
| 1) | If Δ ⊢ σ, then Δ ⇒ σ. (correctness) |
A proof procedure is complete when, for every Δ and σ, it holds that if σ logically follows from Δ, σ is derivable from Δ:
| 2) | If Δ ⇒ σ, then Δ ⊢ σ. (completeness) |
Besides the terms derivation and logical inference, correctness and completeness can also be expressed using the terms consistency and satisfiability, which have the following meanings in this context.
A set of sentences Δ is consistent if no contradiction can be derived from it, i.e., if there is no sentence p such that Δ ⊢ p∧¬p. Accordingly, Δ is inconsistent if there exists a sentence p such that Δ ⊢ p∧¬p. The concept of consistency (in the defined sense) is in the same realm as that of derivation – it presupposes some proof procedure under which sets of sentences are either consistent or not. A set of sentences can be consistent under one proof procedure and inconsistent under another, just as a sentence can be derivable from certain premises using one proof procedure and not derivable using another.
A set of sentences Δ is satisfiable if it has a model (i.e., if there exists a structure in which every sentence in Δ is true). Accordingly, Δ is unsatisfiable if it has no model. Instead of "satisfiable" and "unsatisfiable," we often use the more explicit "has a model" and "has no model." The concept of satisfiability is in the same realm as that of logical consequence – both relate to semantics and are independent of proof procedures.
Correctness and completeness can be defined in terms of consistency and satisfiability as follows. A proof procedure is correct when, for every set of sentences Δ, the following holds:
| 3) | If Δ is satisfiable (has a model), then Δ is consistent. (correctness) |
A proof procedure is complete when, for every set of sentences Δ, the following holds:
| 4) | If Δ is consistent, then Δ is satisfiable (has a model). (completeness) |
We will show that conditions 1) and 3), on one hand, and 2) and 4), on the other, are equivalent, and therefore, it doesn't matter which pair of concepts (derivation – logical inference or consistency – satisfiability) we use.
Regarding the equivalence of 1) and 3). Let's first assume that 1) holds (derivability implies logical inference). We want to show that then 3) also holds (satisfiability implies consistency). Let's assume that a set of sentences Δ is inconsistent, i.e., Δ ⊢ p∧¬p (for some sentence p). From 1), it follows that Δ ⇒ p∧¬p, meaning every model of Δ is also a model of p∧¬p, but since, according to (1), every structure is consistent, the latter implies that Δ has no models. This shows that under the condition of 1), if a set of sentences is inconsistent, then it's unsatisfiable. The latter, by contraposition, is equivalent to 3) (if a set of sentences is satisfiable, then it's consistent), so 3) follows from 1).
Conversely, let's assume 3) holds (satisfiability implies consistency). We want to show that then 1) also holds (derivability implies logical inference). Let's assume the opposite – that some sentence σ is derivable from some set of sentences Δ (Δ ⊢ σ), but σ does not logically follow from Δ (Δ ⇏ σ). The latter means there is a structure that is a model of Δ but not a model of σ, and thus (by the semantic rule of negation) is a model of ¬σ. Therefore, the set of sentences obtained by adding ¬σ to Δ (such a set is often denoted by Δ∪{¬σ}) has a model (is satisfiable). From the latter and 3), it follows that Δ∪{¬σ} is consistent, which contradicts Δ ⊢ σ (since σ being provable from Δ, adding ¬σ to Δ makes the resulting set inconsistent). Therefore, our assumption (Δ ⇏ σ) is false, implying that if 3) holds, then 1) also holds. Thus, we have shown that the two formulations of the correctness, condition 1) and 3), are equivalent.
Before we show that the conditions for completeness 2) and 4) are also equivalent, we will prove the following proposition.
(4) If a sentence σ cannot be derived from the set of sentences Δ (i.e., if Δ ⊬ σ), then Δ∪{¬σ}14 is consistent.
Proof:
If a set of sentences is inconsistent, any sentence can be derived from it due to the following. By definition, inconsistency of a set of sentences means that p∧¬p can be derived from it for some sentence p. From p∧¬p, any sentence q can be derived in the following manner:
| 1. p∧¬p |
| 2. p 1, simplification |
| 3. ¬p 1, commutation, and simplification |
| 4. p∨q 2, addition |
| 5. q 3, 4, disjunctive syllogism |
Let the condition of the proposition to prove be satisfied: Δ ⊬ σ. The set of sentences Δ is consistent because otherwise every sentence would be derivable from it, including σ. Let's assume the negation of what we want to prove: Δ∪{¬σ} is inconsistent. This means that for some sentence p, Δ∪{¬σ} ⊢ p∧¬p. Then from the sentences in Δ, we can derive the following:
| 1. ¬σ assumption |
| 2. p∧¬p from Δ and 1, using the derivation Δ∪{¬σ} ⊢ p∧¬p |
| 3. ¬¬σ 1-2, reductio ad absurdum |
| 4. σ 3, double negation |
So, we have Δ ⊢ σ, which contradicts Δ ⊬ σ. Therefore, our assumption is not true, and Δ∪{¬σ} is consistent. The proof is complete.
Let's now see why 2) and 4) are equivalent. First, assume that 2) holds (logical inference implies derivability), and assume for contradiction that 4) does not hold, i.e., some set of sentences Δ is consistent but has no model. From the latter, it follows (trivially) that every model of Δ is a model of σ and that every model of Δ is a model of ¬σ, meaning that both σ and ¬σ logically follow from Δ. But then, from 2), both σ and ¬σ will be derivable from Δ and thus, by the inference rule of conjunction, σ∧¬σ will also be derivable, i.e., Δ is inconsistent, contradicting our assumption, which means it must be false, i.e., 4) holds if 2) holds.
Conversely, let's assume 4) holds (consistency implies satisfiability). Assume, for contradiction, that 2) does not hold – meaning some sentence σ logically follows from some set of sentences Δ but cannot be derived from them. Based on (4), the latter implies that Δ∪{¬σ} is consistent, and so, according to 4), has some model A. In A, ¬σ is true, but because σ logically follows from Δ and A is a model of Δ, σ is also true. This contradicts (1) (structures are consistent). Therefore, our assumption is false, and 2) holds when 4) holds. Thus, we have shown that 2) and 4), the two alternative formulations of completeness of a proof procedure, are equivalent.
Above, we proved the correctness of our proof procedure in terms of derivability and logical inference. For the completeness of the procedure, we will use the other two terms - consistency and satisfiability. Before that, however, we will introduce some concepts and prove some propositions from set theory that we will use in the proof of completeness.
Sets are fully defined by their elements, so a standard way to denote them is to specify their elements in some manner. For example, {a, b, c} is the set whose elements are the objects a, b, and c. Sometimes we will use the same notation for infinite sets. For example, the set of natural numbers can be denoted as: {0, 1, 2, …}. The third way of denoting sets that we will use is simply with symbols - capital Latin letters.
If X and Y are sets, their union X∪Y is the set that contains the elements of X and the elements of Y, and no other elements. We can talk about the union of more than two sets by placing a large union symbol in front of the term for the set of those sets. For example, if X, Y, and Z are some sets, their union (the combination of their elements into one set) is ⋃{X, Y, Z}. This notation is particularly useful when we want to talk about the union of infinitely many sets. For example, if X1, X2, X3, … is an infinite sequence of sets, then ⋃{X1, X2, X3, …} is their union – the set of those and only those things that are elements of at least one of the sets X1, X2, X3, ….
Under function, we will understand a definite relation of each of the elements of one set to one and only one element of another set (the two sets may coincide). For example, if X is the set {1, 2, 3}, and Y is the set {3, 4, 5}, then the relation of 1 to 4, 2 to 3, and 3 to itself is a function. Let's denote this function as f. The elements of X are called the arguments of f (respectively, X is the set of arguments of f), and the elements of Y to which f relates elements of X are called values of f (respectively, Y is the set of values of f). All this is briefly indicated as follows: f: X → Y. The element y from the set Y, to which f relates an element x from the set X, is denoted by f(x) – hence the well-known identity from high school f(x) = y.
Every function relates every single element of X (the set of its arguments) to only one element of Y (the set of its values), but it could relate two or more elements of X to one element of Y. When this is not the case, i.e., when there is no element of Y to which more than one element of X is related, we say that the function is one-to-one. Furthermore, every function relates every single element of X to some element of Y, but among the elements of Y, there may be those to which no element of X is related. When this is not the case, i.e., when to every element of Y, one or more than one element of X is related, we say that the function is onto.
If a function f: X → Y is simultaneously one-to-one and onto, we call it a bijection between X and Y. The existence of (at least one) bijection between two sets X and Y (i.e., a one-to-one and onto function, whose set of arguments and set of values are respectively X and Y) guarantees us that the elements of X and Y can be matched so that to every element of one set corresponds exactly one element of the other – every element of X is matched with one and only one element of Y, and in Y, there is no element to which an element of X is not matched. When the sets are finite, counting their elements shows whether their number is the same or not. However, when they are infinite, counting is not possible. Then, the existence of a bijection between the sets is the only way to make sense of the statement that the number of their elements is the same. Regardless of whether two sets are finite or infinite, comparing the number of their elements in set theory is conceptualized and defined through the notion of a bijection. X and Y have the same number of elements when there exists at least one bijection between them; and they have a different number of elements when there is no bijection between them.
We will call a set countable if it is finite or if it is infinite but there exists a bijection between it and the set of natural numbers {0, 1, 2, 3, ...}. In the latter case, the bijection allows the elements of this infinite set to be enumerated. (Enumerating the elements of finite sets is obviously always possible.) Not all infinite sets are countable15. Two theorems about countable sets follow.
(5) The union of two countable sets is a countable set.
Proof:
Let X and Y be countable sets. We can assume that they have no common elements, because we want to show that their union is not too "large" (so that it is no longer countable), and if they have no common elements, their union is the "largest possible." If X and Y are finite, their union is also finite, and therefore countable. Let both be infinite. Since they are countable, we can consider their elements as numbered. Then we relate an arbitrary element a from X∪Y to the following natural number: if a is the n-th element (counting from 0) of X, we relate a to the n-th even number, i.e., to 2n. If a is the n-th element of Y, we relate a to the n-th odd number, i.e., to 2n+1. This way, we obtain a one-to-one correspondence (bijection) between the elements of X∪Y and the natural numbers, because, firstly, every element of X∪Y is related to a distinct natural number, and secondly, there is no natural number to which no element of X∪Y is related, so X∪Y is countable. If one set is finite and the other is infinite, this mapping of elements from their union to natural numbers will be such that not every natural number corresponds to an element of the union, but in turn, every element of the union will be numbered with a distinct (unique to it) natural number. Then, we can renumber the elements of X∪Y as follows: we relate the element with the smallest number to 0 (which is 0 itself), the element with the next larger number to 1, the element with the next larger number to 2, and so on. It is clear that in this way, we obtain a bijection between the natural numbers and X∪Y (every element of X∪Y is related to a distinct natural number, and since X∪Y is infinite, there is no natural number to which no element of X∪Y is related), so X∪Y is countable. The aforementioned renumbering shows in principle that if we manage to relate every element of an infinite set to a distinct (unique to it) natural number (even though not every natural number is related to an element), then the set is countable (we will use this later on). End of proof.
(6) The set of all finite sequences of elements from a countable set is a countable set.
Proof:
The proposition is an obvious truth if the set is finite. Let X be an infinite countable set, and let Y be the set of all finite sequences of elements from X. We will show that every element of Y can be related to a distinct (unique to it) natural number. From this, it will follow that Y is countable (see the end of the previous proof).
Since X is countable, there exists a bijection f between X and the set of natural numbers, which enumerates the elements of X, with the number of an arbitrary element a from X being f(a). We relate each element (a1, …, an) of Y to the following natural number:
2f(a1)+1 . 3f(a2)+1 . … . pnf(an)+1
This is a product of powers of the first n prime numbers (2 is the first prime number, 3 is the second, 5 is the third, …, pn is the n-th). Each member of the product corresponds to an element of the finite sequence (a1, …, an). To a1, we assign 2f(a1)+1; to a2, we assign 3f(a2)+1; and so on, where the power of each prime number is the number given to the corresponding element by the bijection f, plus 1. Adding one is necessary because it is possible for the value of f for some ai to be 0, which would make pif(ai) equal to 1 - we want to exclude this possibility. In arithmetic, there is a theorem, proven by Euclid, called the "Fundamental Theorem of Arithmetic," which states that every natural number greater than 1 is a unique product of primes16. This theorem guarantees us that every element of Y, i.e., every finite sequence (a1, …, an) of elements from X, will receive its own, unique number due to the following. First, if two sequences have different numbers of elements, the product corresponding to the longer will involve a prime number not involved in the product corresponding to the shorter sequence, and second, if the two sequences are of equal length, (because they are different) some element from one will be different from the corresponding element of the other, causing the power of the corresponding prime number in the two products to be different. (The reason for adding one to the powers is that if the exponent is 0, the prime number with that exponent would disappear from the product.) Thus, every element of Y will receive a distinct product of prime numbers, and (according to the Fundamental Theorem of Arithmetic) there are no two distinct products of prime numbers that are the same number – meaning every element of Y will receive a distinct natural number. From this, it follows that Y (the set of all finite sequences of elements from X) is countable. End of proof.
We want to demonstrate that if a set of sentences (formulas without free variables) Δ is consistent, then it has a model. Δ can be an infinite set. The sentences in Δ are part of a language L, whose lexicon comprises a set of predicate symbols and a set of constants, both of which may be empty. The lexicon of a natural language (the set of all its words) is finite, but we will not impose this restriction on formal languages – we will only assume that the two sets constituting the lexicon of L (predicate symbols and constants) are countable. For instance, the lexicon could encompass the infinite countable set of predicates {F1, F2, …} and the infinite countable set of constants {c1, c2, …}. Since, according to (5), the union of two countable sets is countable, the lexicon of L (the union of the set of constants and the set of predicates) will be a countable set. Furthermore, (5) implies that if we opt to enrich a language, we can introduce new symbols (including infinitely many) to its lexicon, and its lexicon will remain a countable set provided the added symbols are countable.
Unlike the lexicon of a language L, which may be a finite set, the language L itself is always an infinite set of formulas. This is true even when the lexicon is empty (the language has no predicate or constant symbols), because then L will contain, for example, the sentences "∀x x=x", "(∀x x=x) ∧ (∀x x=x)", "(∀x x=x) ∧ (∀x x=x) ∧ (∀x x=x)", … and so on. From (5) and (6) it follows that if the lexicon of L is a countable set (which we assume), then L itself will be a countable set. This is because: The symbols involved in the formulas of L are a countable (infinite) set, because besides the lexicon, these symbols include a finite number of logical and auxiliary symbols ("¬", "∀", parentheses, … and so on) and a countably infinite set of variables ("x1", "x2", …). Based on (5), the set of all symbols in L is countable, since it is the union of three countable sets (the lexicon, the logical symbols, and the variables). But since the symbols form a countable set, (6) implies that all possible finite sequences of symbols form a countable set, and since the formulas are a subset of these sequences (each formula is a finite sequence of symbols), then L (the set of all formulas) will also be a countable set (the argument with renumbering from the end of the proof of (5)).
From the fact that if a language has a countable lexicon, then it itself is countable, it follows that if we enrich its lexicon with an arbitrary countable set (including infinite) of new symbols, the resulting enriched language will continue to be a countable set, since based on (5), its lexicon (which is the union of two countable sets) will be a countable set (we will use this below).
We will refer to a set of sentences from a given language as "complete" (this completeness is distinct from the completeness of a proof procedure) when for every sentence p in the language, either p or ¬p is an element of it. We will be interested in sets of sentences that are simultaneously consistent and complete. We can think of such sets as theories that have an opinion on absolutely everything – i.e., they contain an answer to every possible question that can be formulated in the language. In the proof of the completeness theorem, we will utilize the following general principle, which ensures that by adding sentences, any consistent set can become complete (while continuing to be consistent):
(7) (Lindenbaum's Lemma) Let Δ be an arbitrary consistent set of sentences from some language L. Then Δ can be extended to a set of sentences Γ, which is consistent and complete (i.e., for every sentence from L, either it or its negation is in Γ).
Proof:
Let Δ be a consistent set of sentences from some language L. Since (as we assume) L is a countable set, the set of all sentences (formulas without free variables) in L (which is a subset of L) is also countable, i.e., we can arrange these sentences in an infinite sequence (corresponding to the sequence of natural numbers): φ1, φ2, …, φn, …. Regarding this sequence, we consider an infinite sequence of extensions of the set of sentences Δ: Δ1, Δ2, …, Δn, …, where each extension is obtained from the previous one as follows. Δ1 is obtained from Δ as follows: if φ1 is consistent with Δ, i.e., if the set obtained by adding φ1 to Δ is consistent, we add φ1 to Δ (if it is not already there). Otherwise, we add ¬φ1. This can be stated more succinctly as follows: if Δ∪{φ1} is consistent, then Δ1 is Δ∪{φ1}; if Δ∪{φ1} is inconsistent, then Δ1 is Δ∪{¬φ1}. Δ2 is obtained from Δ1 in the same way, but with respect to φ2: if Δ1∪{φ2} is consistent, then Δ2 is Δ1∪{φ2}; if Δ1∪{φ2} is inconsistent, then Δ2 is Δ1∪{¬φ2} … and so on.
We will demonstrate that each Δn constitutes a consistent set of sentences. Each Δn is derived from the preceding set of sentences always in the same way, starting from the consistent set Δ. Therefore, it suffices to show that this method preserves the consistency of the sets, i.e., to show that if Δn-1 is consistent, then Δn is consistent as well. If Δn-1∪{φn} is consistent, then this set is indeed Δn, indicating that Δn remains consistent. If Δn-1∪{φn} is inconsistent, because Δn-1 is consistent, φn is not already an element of Δn-1 and cannot be deduced from it. From the latter and (4), it follows that Δn-1∪{¬φn}, which is Δn, is consistent. Thus, in all scenarios, Δn is consistent if Δn-1 is so.
Let Γ be the union of all these extensions of Δ, i.e., Γ is ⋃{Δ1, Δ2, …, Δn, …}. We will demonstrate that Γ is a consistent and complete extension of Δ (i.e., the set of sentences we seek). Firstly, it contains Δ, since it contains Δ1, which is Δ∪{φ1} or Δ∪{¬φ1}. Secondly, Γ is consistent due to the following. Let's assume it is not, i.e., Γ ⊢ p∧¬p for some sentence p. This implies the existence of a proof that (like any proof) uses some finite set of premises from Γ and reaches p∧¬p. Since every sentence in Γ is either already in Δ or was added during the construction of some Δn from Δn-1, we can take such an m (sufficiently large) that all these finite premises from which p∧¬p is derived belong to Δm. But this would imply that Δm is inconsistent, which contradicts the fact that each of the extensions of Δ is consistent. Hence, Γ is a consistent set of sentences. Thirdly, the construction of Γ shows that it is a complete set: initially, we arranged all sentences of the language L in the sequence φ1, φ2, …, φn, … and for each φn, either it or its negation is in Δn, and each Δn is a subset of Γ; thus, either φn or ¬φn is in Γ. End of proof.
We proceed to prove the completeness of the proof procedure. We will start with an arbitrary consistent set of sentences Δ from a language L and show that Δ has a model. We will go through the following main steps. First, we will add to the lexicon of L a countably infinite set of new constants, obtaining the richer language L′. Then we will extend Δ to a consistent and complete in L′ set Γ, which, viewed as a theory, implies that everything that (according to this theory) exists is denoted by some of the added constants. Then we will construct a model of Γ, A′, in which, roughly speaking, the objects will be the constants of L′ themselves (the constants will denote themselves). Since Δ is a subset of Γ, A′ will be a model of Δ. Then, the reduct A of A′ to the language L17 will be the sought structure for the language L, which is a model of Δ, because A′ is a model of Δ, A is a reduct of A′ to the language L, and Δ is in L. This is the idea of the proof; now we proceed to the proof itself.
Let Δ be an arbitrary consistent set of sentences (formulas without free variables) from an arbitrary language L. Let the language L′ be obtained from L by adding a countably infinite set of new constants {c1, c2, …, cn, …}. In view of what was said above, L′ is a countable set of formulas, and thus every subset of it is also countable. This allows us to arrange in an infinite sequence corresponding to the sequence of natural numbers all the formulas in L′ of the form ∃xφ(x) (“x” stands for any variable). Let this sequence be: ∃xφ1(x), ∃xφ2(x), …, ∃xφn(x), …18. With respect to each of these existential sentences, we construct successive extensions of Δ in the language L′: Δ1, Δ2, …, Δn, … as follows. Δ1 is obtained from Δ by adding ∃xφ1(x)→φ1(ci), where ci is the first constant from {c1, c2, …, cn, …} that does not appear in φ1 (since φ1 is from L′, it may involve some of the new constants), and φ1(ci) is obtained from φ1(x) by replacing all occurrences of x with ci. (Note that ci does not appear in Δ (the previous set of sentences) – this will repeat for the subsequent extensions.) Similarly, Δ2 is obtained from Δ1 by adding ∃xφ2(x)→φ2(ci), where ci is the first constant from {c1, c2, …, cn, …} that does not appear in φ1 and φ2. (Therefore, ci does not appear in Δ1, since all constants from {c1, c2, …, cn, …} that participate in sentences from Δ1 are in φ1.) … and so on. Accordingly, Δn is obtained from Δn-1 by adding ∃xφn(x)→φn(ci), where ci is the first constant from {c1, c2, …, cn, …} that does not appear in φ1, φ2, …, φn. (The constants from {c1, c2, …, cn, …} that appear in φ1, φ2, …, φn are finite in number, so we can talk about the first one that does not appear in these sentences.) Moreover, ci does not participate in the sentences in Δn-1, since the only constants from {c1, c2, …, cn, …} that participate in sentences from Δn-1 are in φ1, φ2, …, φn-1.
We will show that each of the extensions of Δ – Δ1, Δ2, …, Δn, … is a consistent set of sentences. To do this, since each one is obtained from the previous one in the same way, starting with the consistent set Δ (which we can think of as Δ0), it suffices to show that if Δn is consistent, then Δn+1 is also consistent. Assume the opposite for the sake of contradiction – that Δn is consistent while Δn+1 is inconsistent. Since the inconsistent set Δn+1 is actually Δn∪{∃xφn+1(x)→φn+1(c)}, for some statement p it follows that Δn, ∃xφn+1(x)→φn+1(c) ⊢ p∧¬p. By using only premises from Δn, we can derive the following:
| 1. ∃xφn+1(x) assumption |
| 2. φn+1(c) 1, existential instantiation (the constant c does not appear in Δn or ∃xφn+1(x))19 |
| 3. ¬∃xφn+1(x) ∨ φn+1(c) 2, addition and commutation |
| 4. ∃xφn+1(x) → φn+1(c) 3, material implication |
| 5. p∧¬p Δn, 4, since Δn, ∃xφn+1(x) → φn+1(c) ⊢ p∧¬p (repeating the proof) |
| 6. ¬∃xφn+1(x) 1-5, reductio ad absurdum |
| 7. ¬∃xφn+1(x) ∨ φn+1(c) 6, addition |
| 8. ∃xφn+1(x) → φn+1(c) 7, material implication |
| 9. p∧¬p Δn, 8, since Δn, ∃xφn+1(x) → φn+1(c) ⊢ p∧¬p (repeating the proof) |
It follows that Δn is inconsistent, contradicting the first part of our assumption. Therefore, our entire assumption (that Δn is consistent and Δn+1 is not) is false, i.e., if Δn is consistent, then Δn+1 is also consistent. Thus, we have shown that each of Δ1, Δ2, ..., Δn, ... is consistent.
Let's consider ⋃{Δ1, Δ2, …, Δn, …} – the union of all these extensions of Δ. We will show that it is also consistent. Suppose it's not, i.e., ⋃{Δ1, Δ2, …, Δn, …} ⊢ p∧¬p for some sentence p. In other words, there exists a proof in the procedure, which uses some finite set of premises from ⋃{Δ1, Δ2, …, Δn, …} and arrives at p∧¬p. Since every sentence in ⋃{Δ1, Δ2, …, Δn, …} is either already in Δ or added during the construction of some Δn+1 from Δn, we can take such an m (sufficiently large) that all these (finite number of) premises from which p∧¬p is derived are in Δm. But this would mean that Δm is inconsistent, which contradicts the fact that each of the extensions of Δ is consistent. Hence, ⋃{Δ1, Δ2, …, Δn, …} is a consistent set of sentences.
Based on (7), there exists a complete and consistent extension of ⋃{Δ1, Δ2, …, Δn, …}. Let's call this containing Δ, consistent and complete in L′ set of sentences Γ.
Every complete and consistent set of sentences (Γ included) has the following (very convenient) property: if a sentence can be derived from it, then it's already in it. In other words, nothing can be derived from complete sets that isn't already an element of them. This is because of the following. Let's assume that for some sentence σ, Γ ⊢ σ. From the completeness of Γ, it follows that σ or ¬σ are elements of Γ, but the latter together with Γ ⊢ σ would imply that Γ is inconsistent. Therefore, σ is already an element of Γ. Below, we will repeatedly use this property to conclude that since certain sentences are derivable from Γ, they are its elements.
The construction of Γ is such that anything Γ claims to exist is denoted by some constant from the language L′. This is because for every existential sentence ∃xφ(x) from L′, Γ contains the sentence ∃xφ(x)→φ(c), where c is a constant from {c1, c2, …, cn, …}. Γ is constructed this way because the initial idea is for the objects in the intended model of Γ to be the constants from the language of Γ (constants that denote themselves). However, it's very possible that Γ may contain sentences implying that certain objects are denoted by more than one constant. Therefore, the objects in the structure we will construct for Γ, which we will call A′ (in accordance with the previous exposition of the main steps of the proof), will not be constants from L′, but rather sets of constants from L′. Thus, when Γ implies that several constants denote the same object, that object will be the set of those constants (which wouldn't be possible if the objects from the universe were the constants themselves – different constants are different objects). To define the universe of the structure A′, we introduce the following notation:
If c is an arbitrary constant from L′, then [c] is the set of those and only those constants d in L′, for which the sentences "c=d" and "d=c" are elements of Γ.
Using the above notation, we define the universe of discourse of A′ as follows:
The set of all [c], where c is a constant from L′.
Let's see what follows from the definition of the universe of A′. First, for every constant c from L′, [c] is a single object – some set of constants from L′. This is because for every constant d from L′, either the sentences "c=d" and "d=c" are elements of Γ (and then d is an element of [c]), or they are not (and then d is not an element of [c]). So, for every constant c in L′, there is one and only one object (set of constants) [c]. At the same time, there is no hindrance for some constants c1 and c2, [c1] and [c2] to be the same set. Therefore, the objects in the universe of A′ are not more than the constants in L′, which means that the universe of A′ is a countable set, because the constants of L′ are a countable set.
Secondly, for no constant c in L′, [c] is an empty set, because at least c is its element. This is because based on the axiom schema of the law of identity, the sentence "c=c" is derivable from Γ and thus is an element of Γ (due to the property of complete sets, as discussed above), from which it follows, based on the definition of [c], that c is an element of [c]. Thus, [c] contains at least c, but it may contain other constants from L′.
Another consequence of defining the universe of A′ requires a longer justification, so we will number and prove it as a theorem:
(8) If c and d are constants from L′, then [c]=[d] if and only if "c=d" is an element of Γ.
Proof:
One direction of this biconditional is easily seen: if [c]=[d] (i.e., [c] and [d] are the same set), since d is an element of [d] (see the first consequence above), it follows that d is an element of [c]. From the latter (by definition), it follows that the sentence "c=d" is an element of Γ.
For the reverse direction (if "c=d" is an element of Γ, then [c]=[d]), we will use the fact that the following two propositions, expressing respectively the symmetry and transitivity of the identity relation (for the formal properties of relations, see 3.5 Proof Procedure), are derivable in our proof procedure without premises and thus are derivable from the sentences in Γ (without using them). Since Γ is a complete set of sentences, if any sentences are derivable from it, they are in it.
| ∀x∀y(x=y → y=x) (symmetry of identity) |
| ∀x∀y∀z[(x=y ∧ y=z) → x=z] (transitivity of identity) |
Proofs in the procedure for both:
| 1. ¬∀x∀y(x=y → y=x) assumption |
| 2. ∃x∃y¬(x=y → y=x) 1, relationship between quantifiers |
| 3. ¬(a=b → b=a) 2, EI (twice) |
| 4. a=b ∧ b≠a 3, material implication |
| 5. a=b 4, simplification |
| 6. b≠a 4, commutation and simplification |
| 7. b≠b 5, 6, indiscernibility of identicals |
| 8. b=b law of identity - contradiction with 7 |
| 9. ∀x∀y(x=y → y=x) 1-8, reductio ad absurdum |
| 1. ¬∀x∀y∀z[(x=y ∧ y=z) → x=z] assumption |
| 2. ∃x∃y∃z¬[(x=y ∧ y=z) → x=z] 1, relationship between quantifiers |
| 3. ¬[(a=b ∧ b=c) → a=c] 2, EI (thrice) |
| 4. (a=b ∧ b=c) ∧ a≠c 3, material implication |
| 5. a=b 4, simplification (twice) |
| 6. b=c 4, simplification (twice) and commutation |
| 7. a=c 6, 5, indiscernibility of identicals |
| 8. a≠c 4, commutation and simplification - contradiction with 7 |
| 9. ∀x∀y∀z[(x=y ∧ y=z) → x=z] 1-8, reductio ad absurdum |
The fact that the propositions of symmetry and transitivity of identity are in Γ means that all their specifications with constants are also in Γ, as the latter are derivable from them through universal instantiation. We want to show that if "c=d" is in Γ, then [c]=[d]. Let "c=d" be an element of Γ. Hence "d=c" is also an element of Γ (Γ contains the proposition of symmetry of identity and thus "c=d→d=c", from which "d=c" follows by modus ponens). By definition, for any constant e of L′, the following two conditions are satisfied:
|
e belongs to [c]
iff "c=e" and "e=c" are elements of Γ |
|
e belongs to [d]
iff "d=e" and "e=d" are elements of Γ |
If "c=e" and "e=c" are elements of Γ, then from the fact that "d=c" and "c=e" are elements of Γ, it follows that "d=e" is an element of Γ (the proposition of transitivity of identity is contained in Γ, thus also "(d=c ∧ c=e) → d=e", from which "d=e" follows by conjunction and modus ponens), and from the fact that "e=c" and "c=d" are elements of Γ (again by the same reasoning from the transitivity of identity), it follows that "e=d" is in Γ. Thus, if "c=e" and "e=c" are elements of Γ, then "d=e" and "e=d" are elements of Γ. The reverse (if "d=e" and "e=d" are elements of Γ, then "c=e" and "e=c" are elements of Γ) is shown entirely similarly (the two conditions are symmetric). Thus, we obtain
|
„c=e“ и „e=c“ са елементи на Γ
iff „d=e“ и „e=d“ са елементи на Γ |
Adding this conditional to the above two, we obtain:"
|
e is an element of [c]
iff e is an element of [d] |
Since e was an arbitrary constant, every constant in L′ is an element of [c] if and only if it is an element of [d], meaning [c] and [d] are the same set of constants. We have thus shown that if "c=d" is an element of Γ, then [c]=[d]. End of the proof.
Here is another consequence of defining the universe of А′:
(9) Let X (some set of constants) be an object from the universe of А′. Then for every constant c from L′, it holds that c is an element of X if and only if [c] is X.
Proof:
One direction of the biconditional (if X is [c], then c is an element of X) follows from the fact that c is an element of [c] (see the second consequence above). For the other direction: let c be an element of X. From the definition of the universe of А′, it follows that for some constant d from L′, X is [d]. Therefore, c is an element of [d] and (by definition) "c=d" is an element of Γ. From (8), it follows that [c]=[d], but X=[d], so X=[c]. Thus, if c is an element of X, then X is [c]. End of the proof.
After defining the universe of А′, we need to determine the interpretation of constants and predicate symbols from the lexicon of L′ in А′. First, the interpretation of constants:
If c is a constant from L′, then cA′ (the object denoted by c in А′) is [c].
It is worth noting that from the way we defined the universe of А′ and the just-given interpretation of constants of L′ in А′, it follows that every object from the universe of А′ is denoted in А′ by some constant from L′. This is because the universe consists of the objects [c] for every constant c in L′, and every constant c in L′ denotes [c] (we will use this fact below).
Now, the interpretation of predicate symbols:
If F is an n-ary predicate symbol from L′, and (X1, X2, …, Xn) is an n-tuple of objects from the universe of А′, then (X1, X2, …, Xn) is an element of FA′ (the interpretation of F in А′), if and only if there is a sentence of the form "Fd1…dn" in Γ, where the constant d1 is an element of the set X1, the constant d2 is an element of X2, …, the constant dn is an element of Xn.
With this, the structure А′ is fully defined. Now, we need to show that this structure is a model of Γ, i.e., that all sentences in Γ are true in А′. According to (1), every sentence in the language of a structure is either true or false in it, but not both. Based on the semantic rules, when a sentence is not true in a structure, its negation is true. Therefore, for every sentence φ from L′, it holds that φ or ¬φ is true in А′, but not both. On the other hand, because Γ is a complete and consistent set of sentences, for every sentence φ from L′, either φ or ¬φ is an element of Γ, but not both. Consequently, А′ can only be a model of Γ if Γ is the set of all sentences that are true in А′. Therefore, we will show that А′ is a model of Γ by demonstrating that the seemingly stronger (but actually equivalent in this case) proposition holds:
For every sentence φ in L′, А′ ⊨ φ if and only if φ is an element of Γ.
We will prove this by induction on the complexity of the sentences in L′ (for the complexity of sentences, see the proof of (1)). First, we consider the cases when φ has complexity 0, i.e., when it is an atomic sentence.
Case 1: φ is the sentence d1=d2, where d1 and d2 are constants (not necessarily distinct). Then, it holds:
| А′ ⊨ d1=d2 |
|
iff
(by semantic rules) |
| d1А′=d2А′ |
|
iff
(from the interpretation of constants in А′) |
| [d1]=[d2] |
|
iff
(from (8)) |
| „d1=d2“ is an element of Γ |
It follows that А′ ⊨ φ if and only if φ is an element of Γ.
Case 2, φ is the sentence Fd1…dn, where F is a predicate symbol, and d1, …, dn are constants (not necessarily distinct). Then it holds:
| А′ ⊨ Fd1…dn |
|
iff
(from semantic rules and interpretation of constants) |
| ([d1], …, [dn]) ∈ FA′ |
|
iff
(from interpretation of predicate symbols) |
| There exists a sentence in Γ of the form “Fе1…еn” such that the constant е1 is an element of [d1], …, the constant en is an element of [dn] |
Let the last statement ("There exists a sentence in Γ of the form …") be true. From (9) and the fact that е1 is an element of [d1], …, е1 is an element of [dn], it follows that [е1]=[d1], …, [еn]=[dn], from which based on (8) follows that the sentences “е1=d1”, …, “еn=dn” are in Γ. But “Fе1…еn” is also in Γ. Applying the inference schema of indiscernibility of identicals, we can derive the sentence “Fd1…dn”, which therefore is also an element of Γ. Conversely, let “Fd1…dn” be an element of Γ. Since d1 is an element of [d1], …, dn is an element of [dn], in Γ there exists a sentence “Fе1…еn”, such that the constant е1 is an element of [dn], …, en is an element of [dn] (this is precisely “Fd1…dn”). Thus, we have shown the truth of the following biconditional:
| There exists a sentence in Γ of the form “Fе1…еn”, such that the constant е1 is an element of [d1], …, еn is an element of [dn] |
| iff |
| “Fd1…dn” is an element of Γ |
Combining it with the above biconditionals, we conclude that А′ ⊨ Fd1…dn, if and only if “Fd1…dn” is an element of Γ, which is what we wanted to show.
These were the two possible cases where the sentence φ has complexity 0. Now, we assume that when φ has complexity k, it holds that А′ ⊨ φ, if and only if φ is an element of Γ, and we will show that the same holds when φ has complexity k+1.
Case 3: φ has the form of a negation, i.e., φ is ¬ψ. Then it holds:
| А′ ⊨ ¬ψ |
|
iff
(by semantic rules) |
| А′ ⊭ ψ |
|
iff
(from the induction hypothesis, since ψ has complexity k) |
| ψ is not an element of Γ |
|
iff
(from the completeness and consistency of Γ) |
| ¬ψ is an element of Γ |
We conclude that А′ ⊨ ¬ψ, if and only if ¬ψ is an element of Γ.
Case 4: φ has the form of a conjunction, i.e., φ is ψ1∧ψ2. Then it holds:
| А′ ⊨ ψ1∧ψ2 |
|
iff
(by semantic rules) |
| А′ ⊨ ψ1 and А′ ⊨ ψ2 |
|
iff
(from the induction hypothesis) |
| ψ1 and ψ2 are elements of Γ |
Let the last statement be true (ψ1 and ψ2 are elements of Γ). Using the inference scheme of conjunction, we obtain Γ ⊢ ψ1∧ψ2, which implies that ψ1∧ψ2 is an element of Γ. Conversely, if ψ1∧ψ2 is an element of Γ, using the inference scheme of simplification, we obtain that both ψ1 and ψ2 are derivable from Γ, implying that they are elements of Γ. Thus, we have
| ψ1 and ψ2 are elements of Γ |
| iff |
| ψ1∧ψ2 is an element of Γ |
Combining the last biconditional with the previous two, we conclude that А′ ⊨ ψ1∧ψ2 if and only if ψ1∧ψ2 is an element of Γ.
Case 5: φ takes the form of disjunction, i.e., φ is ψ1∨ψ2. Then it holds:
| А′ ⊨ ψ1∨ψ2 |
|
iff
(according to the semantic rules) |
| А′ ⊨ ψ1 or А′ ⊨ ψ2 |
|
iff
(from the induction hypothesis) |
| ψ1 is an element of Γ or ψ2 is an element of Γ |
Let the last statement be true (ψ1 is an element of Γ or ψ2 is an element of Γ). Using the addition inference scheme, in both cases, we obtain Γ ⊢ ψ1∨ψ2, from which it follows that ψ1∨ψ2 is an element of Γ. Conversely, suppose ψ1∨ψ2 is an element of Γ. Assume neither ψ1 nor ψ2 are elements of Γ. Then (due to the completeness of Γ), both ¬ψ1 and ¬ψ2 are elements of Γ. Using the conjunction inference scheme, we derive ¬ψ1∧¬ψ2, from which we deduce, using De Morgan's laws, ¬(ψ1∨ψ2). Hence, Γ ⊢ ¬(ψ1∨ψ2), which implies that ¬(ψ1∨ψ2) is an element of Γ, contradicting the fact that ψ1∨ψ2 is an element of Γ (since Γ is consistent). Therefore, our assumption is false, meaning that either ψ1 is an element of Γ or ψ2 is an element of Γ. Overall, we conclude that
| ψ1 is an element of Γ or ψ2 is an element of Γ |
| iff |
| ψ1∨ψ2 is an element of Γ |
Combining the last biconditional with the previous two, we conclude that А′ ⊨ ψ1∨ψ2, if and only if ψ1∨ψ2 is an element of Γ.
Case 6: φ has the form of a conditional, meaning φ is ψ1→ψ2. Then it holds:
| А′ ⊨ ψ1→ψ2 |
|
iff
(according to semantic rules) |
| А′ ⊭ ψ1 or А′ ⊨ ψ2 |
|
iff
(from the induction hypothesis) |
| ψ1 is not an element of Γ or ψ2 is an element of Γ |
|
iff
(from the completeness and consistency of Γ22) |
| ¬ψ1 is an element of Γ or ψ2 is an element of Γ |
Let the latter be true (¬ψ1 is an element of Γ or ψ2 is an element of Γ). From either ¬ψ1 or ψ2 being an element of Γ, with addition, we infer ¬ψ1∨ψ2, from which with material implication, we derive ψ1→ψ2. Hence ψ1→ψ2 is an element of Γ. Conversely, let ψ1→ψ2 be an element of Γ. Assume neither ¬ψ1, nor ψ2 are elements of Γ. Then (by the completeness of Γ) ψ1 and ¬ψ2 are elements of Γ. By the conjunction inference schema, we deduce ψ1∧¬ψ2, from which, via material implication, we derive ¬(ψ1→ψ2). Therefore, ¬(ψ1→ψ2) is an element of Γ, which together with ψ1→ψ2 being an element of Γ, contradicts the consistency of Γ. Thus, our assumption is false, meaning ¬ψ1 is an element of Γ or ψ2 is an element of Γ. We have obtained that
| ¬ψ1 is an element of Γ or ψ2 is an element of Γ |
| iff |
| ψ1→ψ2 is an element of Γ |
Adding the latter biconditional to the previous three, we conclude that А′ ⊨ ψ1→ψ2, if and only if ψ1→ψ2 is an element of Γ.
Case 7: φ takes the form of biconditional, i.e., φ is ψ1↔ψ2. Then the following holds:
| А′ ⊨ ψ1↔ψ2 |
|
iff
(according to semantic rules) |
| А′ ⊨ ψ1 and А′ ⊨ ψ2, or А′ ⊭ ψ1 and А′ ⊭ ψ2 |
|
iff
(by the induction hypothesis) |
| ψ1 and ψ2 are elements of Γ, or neither ψ1, nor ψ2 are elements of Γ |
|
iff
(by the completeness and consistency of Γ23) |
| ψ1 and ψ2 are elements of Γ, or ¬ψ1 and ¬ψ2 are elements of Γ |
Let the latter be true (ψ1 and ψ2 are elements of Γ, or ¬ψ1 and ¬ψ2 are elements of Γ). If ψ1 and ψ2 are elements of Γ, by conjunction, we derive ψ1∧ψ2, from which by addition, we derive (ψ1∧ψ2)∨(¬ψ1∧¬ψ2). If ¬ψ1 and ¬ψ2 are elements of Γ, similarly, we derive (ψ1∧ψ2)∨(¬ψ1∧¬ψ2), so in all cases, we derive the latter sentence. From it, by material equivalence, we derive the sentence ψ1↔ψ2, which means it is an element of Γ. Conversely, let ψ1↔ψ2 be an element of Γ. By material equivalence, we derive the sentence (ψ1∧ψ2)∨(¬ψ1∧¬ψ2), which means it is in Γ. Assume neither ψ1∧ψ2, nor ¬ψ1∧¬ψ2 are elements of Γ. Therefore, (by the completeness of Γ) ¬(ψ1∧ψ2) and ¬(¬ψ1∧¬ψ2) are elements of Γ. By conjunction and De Morgan, we derive ¬[(ψ1∧ψ2)∨(¬ψ1∧¬ψ2)], which contradicts the fact that (ψ1∧ψ2)∨(¬ψ1∧¬ψ2) is in Γ. Thus, our assumption is false, i.e., ψ1∧ψ2 is an element of Γ, or ¬ψ1∧¬ψ2 is an element of Γ. In the former case, by simplification, we derive ψ1 and ψ2, and in the latter, ¬ψ1 and ¬ψ2. Therefore, ψ1 and ψ2 are elements of Γ, or ¬ψ1 and ¬ψ2 are elements of Γ. Altogether, we conclude that
| ψ1 and ψ2 are elements of Γ, or ¬ψ1 and ¬ψ2 are elements of Γ |
| iff |
| ψ1↔ψ2 is an element of Γ |
By adding the last biconditional to the three above, we obtain that А′ ⊨ ψ1↔ψ2, if and only if ψ1↔ψ2 is an element of Γ.
Case 8: φ is an existential statement, i.e., φ is ∃xψ(x).
Let А′ ⊨ ∃xψ(x). This means (by semantic rules) for some object X from А′, А′ ⊨ ψ[X]. When defining А′, we noted that each object from the universe of А′ is denoted by some constant from L′. So, there exists a constant c that denotes X in А′. From А′ ⊨ ψ[X] and the fact that c denotes X in А′, it follows that А′ ⊨ ψ(c). From the induction hypothesis (the complexity of ψ(c) is k), it follows that ψ(c) is an element of Γ. From ψ(c), we can derive ∃xψ(x) as follows:
| 1. ψ(c) |
| 2. ¬∃xψ(x) assumption |
| 3. ∀¬xψ(x) 2, relationship between quantifiers |
| 4. ¬ψ(c) 3, UI – contradiction with 1 |
| 5. ∃xψ(x) 2-4, reductio ad absurdum |
Therefore, ∃xψ(x) is in Γ. We have shown that if А′ ⊨ ∃xψ(x), then ∃xψ(x) is an element of Γ.
Conversely, let ∃xψ(x) be an element of Γ. The construction of Γ was such that for every existential sentence ∃xψ(x) in the language L′, Γ contains ∃xψ(x)→ψ(c), for some constant c from {c1, c2, …, cn, …}. Therefore, Γ simultaneously contains ∃xψ(x) and ∃xψ(x)→ψ(c), from which ψ(c) is derived by modus ponens, indicating it is in Γ. From the latter and the induction hypothesis (ψ(c) has complexity k), it follows that A′ ⊨ ψ(c). The constant c denotes some object X from A′, hence from A′ ⊨ ψ(c), it follows that A′ ⊨ ψ[X]. From the latter, by semantic rules, it follows that A′ ⊨ ∃xψ(x). We have also established the reverse direction (if ∃xψ(x) is in Γ, then A′ ⊨ ∃xψ(x)). In conclusion, A′ ⊨ ∃xψ(x) if and only if ∃xψ(x) is an element of Γ.
Case 9: φ is a universal sentence, i.e., φ is ∀xψ(x).
Let A′ ⊨ ∀xψ(x). Suppose that ∀xψ(x) is not an element of Γ. Therefore, ¬∀xψ(x) is an element of Γ. From ¬∀xψ(x), by the relationship between quantifiers, we derive ∃x¬ψ(x). Hence, ∃x¬ψ(x) is in Γ. From the construction of Γ, it follows that Γ contains the sentence ∃x¬ψ(x)→¬ψ(c) (for some c from the added constants), from which and ∃x¬ψ(x), ¬ψ(c) is derived by modus ponens, implying ¬ψ(c) is an element of Γ. Since Γ is consistent, ψ(c) is not in Γ. From the induction hypothesis (the complexity of ψ(c) is k), A′ ⊭ ψ(c). Therefore, for some object X from A′, A′ ⊭ ψ[X], contradicting A′ ⊨ ∀xψ(x). Hence, our assumption is false, and ∀xψ(x) is an element of Γ. We have established that if A′ ⊨ ∀xψ(x), then ∀xψ(x) is an element of Γ.
Conversely, let ∀xψ(x) be an element of Γ. For every constant c in L′, from ∀xψ(x) by universal instantiation, the sentence ψ(c) is derivable, indicating it is an element of Γ. From the latter and the induction hypothesis, it follows that for every constant c in L′, A′ ⊨ ψ(c). Since there is no object in A′ that is not denoted by a constant, for every object X in A′, A′ ⊨ ψ[X]. By semantic rules, A′ ⊨ ∀xψ(x). We have also established the reverse direction (if ∀xψ(x) is in Γ, then A′ ⊨ ∀xψ(x)). In conclusion, A′ ⊨ ∀xψ(x) if and only if ∀xψ(x) is an element of Γ.
With this, the induction is completed. We have shown that for every sentence φ in L′, A′ ⊨ φ if and only if φ is an element of Γ. Therefore, A′ is a model of Γ.
The last step remains to be taken. Δ (the consistent set of sentences we started with) is a subset of Γ, hence A′ is a model of Δ. But Δ is in the language L, where the constants from {c1, c2, …, cn, …} are missing. Therefore, the structure A, which is the reduct of A′ to the language L, will be a model of Δ. Since Δ was an arbitrary consistent set, this shows that every consistent set of sentences has a model, i.e., the proof procedure from 3.5 Proof Procedure is complete.
The proof itself shows something more – that every consistent set has a countable model (the universe of A was a countable set). Adding the consistency we also proved, it follows that any set of sentences that has a model has a countable model (because if it has a model, by consistency, it is consistent, and if it is consistent, by the completeness proof, it has a countable model). This proposition is known as the Lowenheim-Skolem theorem and was proven by (Lowenheim, 1915) and (Skolem, 1920) before the completeness theorem, first proven (for another proof procedure) by Gödel (Gödel, 1930). The presented completeness proof is by Henkin (Henkin, 1949) (for another proof procedure).