predicate logic, predicate calculus, intuitionistic, predicate, embedding, minimal, constructive, calculus, theorem, quantifier, operation, intuitionist, constructive embedding, replacement, substitution

Back to title page

3. Predicate Logic

3.1. Proving Formulas Containing Quantifiers and Implication only

Theorem 3.1.0. [L₁, L₂, L₁₂, L₁₃, MP] |- AxB(x)->ExB(x). What does it mean? It prohibits "empty domains".

Indeed,

Thus, by [L₁, L₂, MP] Deduction Theorem 1, there is a proof of [L₁, L₂, L₁₂, L₁₃, MP] |- AxB(x)->ExB(x).

Theorem 3.1.1. a) [L₁, L₂, L₁₂, L₁₄, MP, Gen] |- Ax(B->C)->(AxB->AxC). What does it mean?

b) [L₁, L₂, L₁₂-L₁₅, MP, Gen] |- Ax(B->C)->(ExB->ExC). What does it mean?

Let us prove (a).

In this proof, Gen is applied only to x, which is not a free variable in Ax(B->C) and AxB. Thus, by [L₁, L₂, L₁₄, MP, Gen] Deduction Theorem 2, there is a proof of [L₁, L₂, L₁₂, L₁₄, MP, Gen] |- Ax(B->C) -> (AxB->AxC).

Let us prove (b).

In this proof, Gen is applied only to x, which is not a free variable in Ax(B->C) and ExB. Thus, by [L₁, L₂, L₁₄, MP, Gen] Deduction Theorem 2, there is a proof of [L₁, L₂, L₁₂-L₁₅, MP, Gen] |- Ax(B->C) -> (ExB->ExC).

Q.E.D.

Theorem 3.1.2. a) [L₁, L₂, L₅, L₁₂, L₁₄, MP, Gen] |- AxAyB(x, y)<->AyAxB(x, y). What does it mean?

b) [L₁, L₂, L₅, L₁₃, L₁₅, MP, Gen] |- ExEyB(x, y)<->EyExB(x, y). What does it mean?

c) [L₁, L₂, L₁₂-L₁₅, MP, Gen] |- ExAyB(x, y)->AyExB(x, y). What does it mean? The converse implication AxEyB(x, y)->EyAxB(x, y) cannot be true. Explain, why.

Let us prove (b).

The proof of the converse implication [L₁, L₂, L₁₃, L₁₅, MP, Gen] |- EyExB(x, y)->ExEyB(x, y) is identical.

Now, by Theorem 2.2.1(a) [L₅]: A, B |- A&B, we obtain the equivalence (b). Q.E.D.

Exercise 3.1.1. Prove (a) and (c) of Theorem 3.1.2.

Exercise 3.1.2. Prove in the constructive logic,

[L₁-L₁₀, L₁₂-L₁₅, MP, Gen] |- Ex(B(x)->C(x)) -> (AxB(x)->ExC(x)).

3.2. Formulas Containing Negations and a Single Quantifier

Attention: non-constructive reasoning! ~AxB -> Ex~B. This formula is accepted in the classical logic: if no x can possess the property B, then there is an x that does not possess B. It represents non-constructive reasoning in its ultimate form: let us assume, all x-s possess the property B, if we succeed in deriving a contradiction from this assumption, then - what? Is this a proof that there is a particular x that does not possess the property B? Does our proof contain a method allowing to build at least one such x? If not, do we have a "real" proof of Ex~B?

How many formulas can be built of the formula B by using negations and a single quantifier?

~~~~~~~~~~Ax~~~~~~~~~~B

~~~~~~~~~~Ex~~~~~~~~~~B

Let us recall Theorem 2.4.5 [L₁-L₉, MP]: |- ~~~A<->~A. I.e., any number of negations can be reduced to zero, one, or two, and thus we obtain 3*2*3 = 18 formulas to be investigated. The following table represents the results of this investigation from

A.Heyting. On weakened quantification. Journal of Symbolic Logic, 1936, vol.11, pp.119-121 (see also Kleene [1952], Section 3.5).

Table 3.2

Legend. a) In the classical logic, within each of the 4 groups all formulas are equivalent, for example, in group III: ~AxB<->Ex~B. Of course, formulas of different groups cannot be equivalent (explain, why).

b) Two formulas within a group are constructively equivalent, iff they have no separating lines between them. For example, in group II: constructively, ~Ax~B<->~~ExB, but not ~Ax~B<->ExB (explain, why). All the formulas of the group IV are constructively equivalent.

c) If two formulas F₁, F₂ within a group (F₁ - above, F₂ - below) are separated by a single line, then: constructively, F₁->F₂, and ~~(F₂->F₁), but not F₂->F₁. For example, in group II: constructively, ExB->~Ax~B, and ~~(~Ax~B->ExB), but not ~Ax~B->ExB (explain, why).

d) If two formulas F₁, F₂ within a group (F₁ - above, F₂ - below) are separated by a double line, then: constructively, F₁->F₂, but not F₂->F₁, and even not ~~(F₂->F₁). For example, in group III: constructively, Ex~B->~AxB, but not ~AxB->Ex~B, and even not ~~(~AxB->Ex~B) (try to explain, why). Thus, the implication ~AxB->Ex~B could be qualified as super-non-constructive.

Now, let us prove the implications necessary for the positive part of the above legend to be true.

Group I

I-1. Constructively, [L₁, L₂, L₉, MP]: |- AxB->~~AxB

Immediately, by Theorem 2.4.4 [L₁, L₂, L₉, MP]: |- A->~~A.

I-2. Constructively, [L₁-L₉, L₁₂, L₁₄, MP, Gen]: |- ~~AxB->Ax~~B

I-3. Constructively, [L₁, L₂, L₉, MP]: |- Ax~~B->~~Ax~~B

Immediately, by Theorem 2.4.4 [L₁, L₂, L₉, MP]: |- A->~~A.

I-4. Constructively, [L₁, L₂, L₉, L₁₂, L₁₅, MP, Gen] |- ~~Ax~~B->~Ex~B

I-5. In the classical logic, [L₁-L₁₁, L₁₃, L₁₄, MP, Gen]: |- ~Ex~B->AxB

Thus, we have proved that in Group I, constructively, F₁->F₂->F₃->F₄->F₅, and, in the classical logic, F₅->F₁. I.e. we have proved that in Group I: a) in the classical logic, all the formulas are equivalent, and b) constructively, upper formulas imply lower formulas.

I-6. Constructively, [L₁, L₂, L₉, L₁₃, L₁₄, MP, Gen]: |- ~Ex~B->Ax~~B

Thus, we have proved that in Group I, constructively, [L₁, L₂, L₉, L₁₂ -L₁₅, MP, Gen]: F₃->F₄->F₅->F₃, i.e. that formulas F₃, F₄, F₅ are constructively equivalent.

For Group I, it remains to prove

I-7. Constructively, [L₁-L₁₀, MP] |- ~~(~~AxB->AxB)

Immediately, by Theorem 2.5.2(d) [L₁-L₁₀, MP] |- ~~(~~A->A).

Group II

II-1. Constructively, [L₁, L₂, L₉, L₁₂-L₁₅, MP, Gen] |- ExB->Ex~~B

II-2. Constructively, [L₁-L₉, L₁₂-L₁₅, MP, Gen] |-Ex~~B->~~ExB

II-3. Constructively, [L₁-L₉, L₁₂-L₁₅, MP, Gen] |- ~~ExB->~~Ex~~B

Immediately from II-1, by From (1), by Theorem 2.4.7(a) [L₁-L₉, MP]: |- (A->B)->(~~A->~~B).

II-4. Constructively, [L₁-L₉, L₁₂, L₁₅, MP, Gen] |- ~~Ex~~B->~Ax~B

II-5. In the classical logic, [L₁-L₁₁, L₁₃, L₁₄, MP, Gen]: |- ~Ax~B->ExB

Thus, we have proved that in Group II, constructively, F₁->F₂->F₃->F₄->F₅, and, in the classical logic, F₅->F₁. I.e. we have proved that in Group II: a) in the classical logic, all the formulas are equivalent, and b) constructively, upper formulas imply lower formulas.

II-6. Constructively, [L₁, L₂, L₉, L₁₃, L₁₄, MP, Gen] |- ~Ax~B->~~ExB

Thus, we have proved that in Group II, constructively, [L₁-L₉, L₁₂-L₁₅, MP, Gen]: F₃->F₄->F₅->F₃, i.e. that formulas F₃, F₄, F₅ are constructively equivalent.

II-7. Constructively, [L₁-L₁₀, MP]: |- ~~(~~ExB->ExB)

Immediately, by Theorem 2.5.2 [L₁-L₁₀, MP]: |- ~~(~~A->A).

Thus, constructively, ~~(F₃->F₁), and F₁->F₂->F₃->F₄->F₅->F₃. By Theorem 2.4.7(d), [L₁-L₉, MP] ~~(A->B), ~~(B->C) |- ~~(A->C). Thus, in fact, we have proved that in Group II, for all i, j, constructively, ~~(F_i->F_j) (a kind of "weak equivalence").

Group III

III-1. Constructively, [L₁, L₂, L₉, MP]: |- Ex~B->~~Ex~B

Immediately, by Theorem 2.4.4 [L₁, L₂, L₉, MP]: |- A->~~A.

III-2. Constructively, [L₁, L₂, L₉, L₁₂, L₁₅, MP, Gen]: |- ~~Ex~B->~Ax~~B

III-3. Constructively, [L₁-L₉, L₁₂, L₁₄, MP, Gen]: |- ~Ax~~B->~AxB

III-4. In the classical logic, [L₁-L₁₁, L₁₃, L₁₄, MP, Gen]: |- ~AxB->Ex~B

Thus, we have proved that in Group III, constructively, F₁->F₂->F₃->F₄, and, in the classical logic, F₄->F₁. I.e. we have proved that in Group III: a) in the classical logic, all the formulas are equivalent, and b) constructively, upper formulas imply lower formulas.

III-4. Constructively, [L₁, L₂, L₉, L₁₃, L₁₄, MP, Gen]: |- ~Ax~~B->~~Ex~B

Thus, we have proved that in Group III, constructively, F₂->F₃->F₂, i.e. that formulas F₂, F₃ are constructively equivalent.

III-5. Constructively, [L₁-L₁₀, MP]: |- ~~(~~Ex~B->Ex~B)

Immediately, by Theorem 2.5.2 [L₁-L₁₀, MP]: |- ~~(~~A->A).

Group IV

IV-1. Constructively, [L₁, L₂, L₉, MP]: |- Ax~B->~~Ax~B

Immediately, by Theorem 2.4.4 [L₁, L₂, L₉, MP]: |- A->~~A.

IV-2. Constructively, [L₁-L₉, L₁₂-L₁₅, MP, Gen]: |- ~~Ax~B->~Ex~~B

IV-3. Constructively, [L₁, L₂, L₉, L₁₂-L₁₅, MP, Gen]: |- ~Ex~~B->~ExB

IV-4. Constructively, [L₁, L₂, L₉, L₁₃, L₁₄, MP, Gen]: |- ~ExB->Ax~B

Thus, we have proved that in Group IV all the formulas are constructively equivalent.

And thus, we have proved the positive part of the legend of Table 3.2. The negative part of the legend asserts that the following (classically provable) formulas cannot be proved constructively:

We will prove these facts in Section 4.5 (see Exercise 4.5.1).

Still, the most striking (classically provable) non-constructive quantifier implications correspond to existence proofs via reductio ad absurdum:

3.3. Proving Formulas Containing Conjunction and Disjunction

Theorem 3.3.1. a) [L₁-L₅, L₁₂, L₁₄, MP, Gen]: |- Ax(B&C) <-> AxB & AxC.

b) [L₁, L₂, L₆-L₈, L₁₄, MP, Gen]: |- AxB v AxC -> Ax(BvC). The converse formula Ax(BvC)->AxB v AxC cannot be true. Explain, why.

Exercise 3.3.1. Prove [L₃-L₅, L₁₂, MP, Gen]: Ax(B&C) |- AxB & AxC and [L₃-L₅, L₁₂, MP, Gen]: AxB & AxC |- Ax(B&C).

Since, in your first proof, Gen has been applied only to x, which is not a free variable in Ax(B&C), then, by Deduction theorem 2 [L₁, L₂, L₁₄, MP, Gen] we obtain that [L₁- L₅, L₁₂, L₁₄, MP, Gen]: |- Ax(B&C)->AxB & AxC.

Similarly, in your second proof, Gen has been applied only to x, which is not a free variable in AxB & AxC, then, by Deduction theorem 2 [L₁, L₂, L₁₄, MP, Gen] we obtain that [L₁- L₅, L₁₂, L₁₄, MP, Gen]: |- AxB & AxC ->Ax(B&C).

Now, by Theorem 2.2.1(a) [L₅]: A, B |- A&B, we obtain the equivalence (a).

Let us prove (b): |- AxB v AxC -> Ax(BvC).

The summary is [L₁, L₂, L₆-L₈, L₁₂, L₁₄, MP, Gen].

Q.E.D.

Theorem 3.3.2. a) [L₁-L₈, L₁₂-L₁₅, MP, Gen]: |- Ex(BvC) <-> ExB v ExC

b) [L₁-L₅, L₁₃, L₁₅, MP, Gen]: |- Ex(B&C) -> ExB & ExC. The converse implication ExB & ExC -> Ex(B&C) cannot be true. Explain, why.

First, let us prove Ex(BvC) -> ExB v ExC.

The summary is [L₁, L₂, L₆-L₈, L₁₃, L₁₅, MP, Gen].

Let us prove ExB v ExC -> Ex(BvC).

The summary is [L₁, L₂, L₆-L₈, L₁₂-L₁₅, MP, Gen].

Now, by Theorem 2.2.1(a) [L₅]: A, B |- A&B, we obtain the equivalence (a). Q.E.D.

Exercise 3.3.2. Prove (b) of Theorem 3.3.2. (Hint: first, assume B&C, derive ExB & ExC, and apply Deduction Theorem 1). The converse implication ExB & ExC -> Ex(B&C) cannot be true. Explain, why.

3.4. Replacement Theorems

In this section we will prove meta-theorems that will allow replacing sub-formulas by equivalent formulas. For example, if have proved the formula ExB->D, and we know that |- B<->C, then we can replace B by C, obtaining the formula ExC->D. Until now, we could not use this very natural mathematical argument.

We will prove also that the meaning of a formula does not depend on the names of bound variables used in it. For example, |- (ExB(x)->C)<->(EyB(y)->C).

Note. To prove all these replacement theorems we will need only the minimal logic [L₁-L₉, L₁₂-L₁₅, MP, Gen].

Replacement Lemma 1. In the minimal logic, [L₁-L₉, MP]:

Case (a). We will first prove that [L₁, L₂, L₄, MP]: A<->B |- (A->C)->(B->C).

Thus, by [L₁, L₂, MP] Deduction Theorem 1, [L₁, L₂, L₄, MP]: A<->B |- (A->C)->(B->C).

As the second step, we will prove that , [L₁, L₂, L₃, MP]: A<->B |- (B->C)->(A->C).

Thus, by [L₁, L₂, MP] Deduction Theorem 1, [L₁, L₂, L₃, MP]: A<->B |- (B->C)->(A->C).

Now, by Theorem 2.2.1(a) [L₅]: A, B |- A&B, we obtain (a).

Q.E.D.

Exercise 3.4.1. Prove (b, c, d ) of Replacement Lemma 1.

Case (e): A<->B |- AvC<->BvC. We will first prove that [L₁, L₂, L₃-L₈, MP]: A<->B |- AvC->BvC.

Thus, by [L₁, L₂, MP] Deduction Theorem 1, [L₁-L₈, MP]: A<->B |- AvC->BvC.

As the second step, we will prove that , [L₁-L₈, MP]: A<->B |- BvC->AvC.

Thus, by [L₁, L₂, MP] Deduction Theorem 1, [L₁-L₈, MP]: A<->B |- BvC->AvC.

Now, by Theorem 2.2.1(a) [L₅, MP]: A, B |- A&B, we obtain (e).

Exercise 3.4.2. Prove (f ) of Replacement Lemma 1.

Case (g). We will first prove that [L₁-L₉, MP]: A<->B |- ~A->~B.

Thus, by [L₁, L₂, MP] Deduction Theorem 1, [L₁-L₉, MP]: A<->B |- ~A->~B.

As the second step, we will prove that [L₁-L₉, MP]: A<->B |- ~B->~A.

Thus, by [L₁, L₂, MP] Deduction Theorem 1, [L₁-L₉, MP]: A<->B |- ~A->~B.

Now, by Theorem 2.2.1(a) [L₅]: A, B |- A&B, we obtain (g).

This completes our proof of the Replacement Lemma 1.

Replacement Theorem 1. Let us consider three formulas: B, B', C, where B is a sub-formula of C, and o(B) is a propositional occurrence of B in C (i.e. no quantifiers stand over o(B)). Let us denote by C' the formula obtained from C by replacing o(B) by B' . Then, in the minimal logic, [L₁-L₉, MP]: B<->B' |- C<->C'.

Proof. Induction by the "depth" of the propositional occurrence o(B).

Induction base: depth = 0. Then C is B, and C' is B'. The conclusion is obvious.

Induction step. If C is not B, then one of the following holds:

a) C is F->G, and o(B) is in F.

b) C is F->G, and o(B) is in G.

c) C is F&G, and o(B) is in F.

d) C is F&G, and o(B) is in G.

e) C is FvG, and o(B) is in F.

f) C is FvG, and o(B) is in G.

g) C is ~F, and o(B) is in F.

Case (a). By induction assumption, [L₁-L₉, MP]: B<->B' |- F<->F'. By Replacement Lemma 1(a), [L₁-L₉, MP]: F<->F' |- (F->G)<->(F'->G). Thus, [L₁-L₉, MP]: B<->B' |- C<->C'.

Exercise 3.4.3. Repeat the above argument for the remaining cases (b, c, d, e, f, g).

Q.E.D.

Now, we can use the replacement argument mentioned at at the beginning of this section - at least, for propositional occurrences of equivalent sub-formulas.

Replacement Lemma 2. In the minimal logic, [L₁-L₉, L₁₂-L₁₅, MP, Gen]:

Case (a). We will first prove that [L₁, L₂, L₃, L₁₂, L₁₄, MP, Gen]: B<->C |- AxB->AxC.

Thus, we have proved that [L₃, L₁₂, MP, Gen]: B<->C, AxB |- AxC. Since Gen has been applied only to x, which is not a free variable in AxB, then, by Deduction Theorem 2 [L₁, L₂, L₁₄, MP, Gen] we obtain that [L₁, L₂, L₃, L₁₂, L₁₄, MP, Gen]: B<->C |- AxB->AxC.

In a similar way (with L₄ instead of L₃), [L₁, L₂, L₄, L₁₂, L₁₄, MP, Gen]: B<->C |- AxC->AxB.

Now, by Theorem 2.2.1(a) [L₅]: A, B |- A&B, we obtain (a).

Case (b). We will first prove that [L₁, L₂, L₃, L₁₂, L₁₄, MP, Gen]: B<->C |- ExB->ExC.

Thus, we have proved that [L₁, L₂, L₃, L₁₃, L₁₅, MP, Gen]: B<->C, ExB|- ExC. Since Gen has been applied only to x, which is not a free variable in ExB, then, by Deduction Theorem 2 [L₁, L₂, L₁₄, MP, Gen] we obtain that [L₁, L₂, L₃, L₁₂-L₁₅, MP, Gen]: B<->C |- ExB->ExC.

In a similar way (with L₄ instead of L₃), [L₁, L₂, L₄, L₁₂-L₁₅, MP, Gen]: B<->C |- ExC->ExB.

Now, by Theorem 2.2.1(a) [L₅, MP]: A, B |- A&B, we obtain (b).

Q.E.D.

Replacement Theorem 2. Let us consider three formulas: B, B', C, where B is a sub-formula of C, and o(B) is any occurrence of B in C. Let us denote by C' the formula obtained from C by replacing o(B) by B' . Then, in the minimal logic, [L₁-L₉, L₁₂-L₁₅, MP, Gen]: B<->B' |- C<->C'.

Proof. Induction by the "depth" of the occurrence o(B).

Induction base: depth = 0. Then C is B, and C' is B'. The conclusion is obvious.

Induction step. If C is not B, then one of the following holds:

a) - g) - as in the proof of Replacement Theorem 1.

h) C is AxF, and o(B) is in F.

i) C is ExF, and o(B) is in F.

Case (h). By induction assumption, [L₁-L₉, L₁₂-L₁₅, MP, Gen]: B<->B' |- F<->F'. By Replacement Lemma 2(a), [L₁-L₉, L₁₂-L₁₅, MP, Gen]: F<->F' |- AxF<->AxF'. Thus, [L₁-L₉, L₁₂-L₁₅, MP, Gen]: B<->B' |- C<->C'.

Case (i). By induction assumption, [L₁-L₉, L₁₂-L₁₅, MP, Gen]: B<->B' |- F<->F'. By Replacement Lemma 2(b), [L₁-L₉, L₁₂-L₁₅, MP, Gen]: F<->F' |- ExF<->ExF'. Thus, [L₁-L₉, L₁₂-L₁₅, MP, Gen]: B<->B' |- C<->C'.

Q.E.D.

Now (only now!) , we may use in our proofs the replacement argument mentioned at at the beginning of this section for any equivalent sub-formulas.

Finally, let us prove that the meaning of a formula does not depend on the names of bound variables used in it. Intuitively, it "must be so", but now we can prove this intuition as a meta-theorem.

Replacement Lemma 3. If the formula B does not contain the variable y, then (in the minimal logic):

a) [L₅, L₁₂, L₁₄, MP, Gen]: |- AxB(x)<->AyB(y)

b) [L₅, L₁₃, L₁₅, MP, Gen]: |- ExB(x)<->EyB(y).

First, let us prove [L₁₂, L₁₄, MP, Gen]: |- AxB(x)->AyB(y).

Now, let us prove [L₁₂, L₁₄, MP, Gen(x)]: |- AyB(y)->AxB(x).

Now, by Theorem 2.2.1(a) [L₅]: A, B |- A&B, we obtain (a).

To prove (b), first, let us prove [L₁₃, L₁₅, MP, Gen(y)]: |- EyB(y)->ExB(x).

Now, let us prove [L₁₃, L₁₅, MP, Gen(x)]: |- ExB(x)->EyB(y).

Now, by Theorem 2.2.1(a) [L₅]: A, B |- A&B, we obtain (b).

Q.E.D.

Replacement Theorem 3. Let y be a variable that does not occur in a formula F, containing an occurrence of a quantifier Ax (or Ex). Let us replace by y all occurrences of the variable x bound by this particular quantifier occurrence. Let us denote the resulting formula by F'. Then, in the minimal logic, [L₁-L₉, L₁₂-L₁₅, MP, Gen]: |- F<->F'.

Proof. Thus, the formula F contains a sub-formula AxB(x) (or ExB(x)), and we wish to replace it by Ay(B(y) (or EyB(y)), where y does not occur in F. By Replacement Lemma 3, in the minimal logic, |- AxB(x)<->AyB(y), and |- ExB(x)<->EyB(y). Hence, by Replacement Lemma 2, in the minimal logic, |- F<->F'. Q.E.D.

3.5. Constructive Embedding

Glivenko's Theorem (see Section 2.7) provides a simple "constructive embedding" for the classical propositional logic: any classically provable formula can be "proved" in the constructive logic, if you put two negations before it. This theorem does not hold for the predicate logic. For example (see Section 3.2),

II-5. In the classical logic, [L₁-L₁₁, L₁₃, L₁₄, MP, Gen]: |- ~Ax~B->ExB.

The double negation of this formula, i.e. the formula ~~(~Ax~B->ExB) cannot be proved in the constructive predicate logic (see Section 4.5). Thus, instead of simply ~~F, we must search for a more complicated embedding operation.

However,

Exercise 3.5.0 (for smart students). Verify that a formula F is provable in the classical predicate logic, iff ~~F is provable in the constructive predicate logic plus the following axiom: Ax~~B->~~AxB (the so-called Double Negation Shift schema, see Intuitionistic Logic by Joan Moschovakis in Stanford Encyclopedia of Philosophy.

The first such embedding operation was introduced by Andrey Nikolaevich Kolmogorov (1903-1987) in

A.N.Kolmogorov. On the principle tertium non datur. Matem. sbornik, 1925, vol.32, pp.646-667 (in Russian).

A quote from A Short Biography of A.N. Kolmogorov by Paul M.B. Vitanyi follows:

"K. got interested in mathematical logic, and in 1925 published a paper in Mathematicheskii Sbornik on the law of the excluded middle, which has been a continuous source for later work in mathematical logic. This was the first Soviet publication on mathematical logic containing (very substantial) new results, and the first systematic research in the world on intuitionistic logic. K. anticipated to a large extent A. Heyting 's formalization of intuitionistic reasoning, and made a more definite correlation between classical and intuitionistic mathematics. K. defined an operation for `embedding' one logical theory in another. Using this - historically the first such operation, now called the `Kolmogorov operation' - to embed classical logic in intuitionistic logic, he proved that application of the law of the excluded middle in itself cannot lead to a contradiction. In 1932 K. published a second paper on intuitionistic logic, in which for the first time a semantics was proposed (for this logic), free from the philosophical aims of intuitionism. This paper made it possible to treat intuitionistic logic as constructive logic."

See also Kolmogorov Centennial.

We will investigate the following version of an embedding operation: to obtain O(F), in a formula F, put two negations before: a) every atomic formula, b) every disjunction, c) every existential quantifier. More precisely, let us define the following embedding operation O (you may wish to compare it with some other versions possessing similar properties):

(^*) By Theorem 2.4.5, [L₁-L₉, MP]: |- ~~~K(F)<->~K(F).

For example, let us take the above formula ~Ax~B->ExB. If B is an atomic formula, then

O(~Ax~B->ExB) is ~Ax~~~B->~~Ex~~B, i.e. ~Ax~B->~~Ex~~B

The latter formula is constructively provable (see Section 3.2, Group II).

Lemma 3.5.1. For any formula F, in the classical logic, |- F<->O(F).

Proof. By induction. Let us recall Theorem 2.6.1: [L₁-L₁₁, MP] |- ~~A <-> A.

1. Induction base: F is an atomic formula. Then O(F) is ~~F. By Theorem 2.6.1, [L₁-L₁₁, MP] |- ~~F<->F, hence, in the classical logic, |- O(F)<->F.

2. Induction step.

Case 2a: F is BvC. Then O(F) is ~~(O(B)vO(C)).

Case 2b: F is ExB. Then O(F) is ~~ExO(B).

Case 2c: F is B->C.
Case 2d: F is B&C.
Case 2e: F is ~B.
Case 2f: F is AxB.

Exercise 3.5.1.Prove (c, d, e, f).

Q.E.D.

Still, the key feature of the formulas having the form O(F) is given in

Lemma 3.5.2. For any formula F, there is a proof [L₁-L₉, L₁₂, L₁₄, MP,Gen]: |- ~~O(F)<->O(F). I.e., in the minimal logic, we may drop the double negation before O(F) (before an arbitrary formula, we can do this only in the classical logic).

Note. In some other textbooks, if ~~G<->G can be proved in the constructive logic, then G is called a stable formula. Thus, the embedding O(F) is a stable formula for any F.

Proof. By Theorem 2.4.4, [L₁, L₂, L₉, MP]: |- A->~~A. Thus, it remains to prove |- ~~O(F)->O(F). Let us proceed by induction.

1. Induction base: F is an atomic formula. Then O(F) is ~~F, and ~~O(F)->O(F) is ~~~~F->~~F. Let us recall Theorem 2.4.5: [L₁-L₉, MP] |- ~~~A<->~A. Hence, by taking A = ~F: [L₁-L₉, MP] |- ~~~~F->~~F, i.e. [L₁-L₉, MP] |- ~~O(F)->O(F).

2. Induction step.

Case 2a: F is BvC, or ExB, or ~B. Then O(F) is ~~(O(B)vO(C)), or ~~ExO(B), or ~O(B). Hence, ~~O(F)->O(F) is ~~~G->~G, where G is ~(O(B) v O(C)), or ~ExO(B), or O(B). Let us recall Theorem 2.4.5: [L₁-L₉, MP] |- ~~~A<->~A. Hence, [L₁-L₉, MP] |- ~~~G->~G, i.e. [L₁-L₉, MP] |- ~~O(F)->O(F).

Case 2b: F is B->C. Then O(F) is O(B)->O(C). By induction assumption, [L₁, L₂, L₁₂, L₁₄, MP, Gen]: |- ~~O(B)->O(B), and |- ~~O(C)->O(C).

Hence, since Gen is not applied here at all, by Deduction Theorem 1 [L₁, L₂, MP] we obtain that [L₁-L₉, L₁₂, L₁₄, MP, Gen] |- ~~O(F)->O(F).

Case 2c: F is B&C. Then O(F) is O(B)&O(C). By induction assumption, [L₁, L₂, L₁₂, L₁₄, MP, Gen]: |- ~~O(B)->O(B), and |- ~~O(C)->O(C).

Hence, since Gen is not applied here at all, by Deduction Theorem 1 [L₁, L₂, MP] we obtain that [L₁-L₉, L₁₂, L₁₄, MP, Gen] |- ~~O(F)->O(F).

Case 2d: F is AxB. Then O(F) is AxO(B). By induction assumption, [L₁-L₉, L₁₂, L₁₄, MP, Gen]: |- ~~O(B)->O(B). We must prove that |- ~~AxO(B)->AxO(B).

Q.E.D.

Lemma 3.5.3. If F is one of the (classical) axioms L₁-L₁₁, L₁₂-L₁₅, then, in the constructive logic, [L₁-L₁₀, L₁₂-L₁₅, MP, Gen]: |- O(F).

Note. The axiom L₁₀ will be used in the proof of Lemma 3.5.3 only once - to prove that O(L₁₀) is provable in the constructive logic. But, of course, O(L₁₀) cannot be proved in the minimal logic, hence, in the Lemma 3.5.3, the constructive logic cannot be replaced by the minimal one.

Proof.

Case 1. F (as an axiom schema) does not contain disjunctions and existential quantifiers, i.e. if F is L₁, L₂, L₃, L₄, L₅, L₉, L₁₀, L₁₂, or L₁₄., then O(F) is an instance of the same axiom as F, i.e. [F]: |- O(F). For example, if F is L₁, i.e. B->(C->B), then O(F) is O(B)->(O(C)->O(B)), i.e. O(F) is an instance of the same axiom L₁.

Case 2a. F is L₆: B->BvC. Then O(F) is O(B)->~~(O(B)vO(C)), and [[L₁, L₂, L₆, L₉, MP] |- O(F). Indeed:

Case 2b. F is L₇: C->BvC. Then O(F) is O(C)->~~(O(B)vO(C)), and [[L₁, L₂, L₇, L₉, MP] |- O(F). Proof is similar to Case 2a.

Case 2c. F is L₈: (B->D)->((C->D)->(BvC->D)). Then O(F) is

(O(B)->O(D))->((O(C)->O(D))->(~~(O(B)vO(C))->O(D))).

Hence, since Gen is not applied after hypotheses appear in the proof, by Deduction Theorem 2A [L₁, L₂, L₁₄, MP, Gen] we obtain that [L₁-L₉, L₁₂, L₁₄, MP,Gen] |- O(F).

Case 2d. F is L₁₁: Bv~B. Then O(F) is ~~(O(B)v~O(B)). Let us recall Theorem 2.4.6(b): [L₁-L₉, MP] |- ~~(Av~A). Hence, [L₁-L₉, MP] |- O(F).

Case 2e. F is L₁₃: F(t)->ExF(x). Then O(F) is O(F(t))->~~ExO(F(x))), and [[L₁, L₂, L₉, L₁₃, MP] |- O(F). Indeed:

Case 2f. F is L₁₅: Ax(F(x)->G)->(ExF(x)->G). Then O(F) is

Ax(O(F(x))->O(G))->(~~ExO(F(x))->O(G)).

Hence, since Gen is not applied after hypotheses appear in the proof, by Deduction Theorem 2A [L₁, L₂, L₁₄, MP, Gen] we obtain that [L₁-L₉, L₁₂, L₁₄, L₁₅, MP,Gen] |- O(F).

Q.E.D.

Theorem 3.5.4. In the classical logic, [L₁-L₁₁, L₁₂-L₁₅, MP, Gen]: B₁, B₂, ..., B_n |- C, iff, in the constructive logic, [L₁-L₁₀, L₁₂-L₁₅, MP, Gen]: O(B₁), O(B₂), ..., O(B_n) |- O(C). In particular, a formula F is provable in the classical logic, iff the formula O(F) is provable in the constructive logic.

Proof.

1. Let [L₁-L₁₁, L₁₂-L₁₅, MP, Gen]: B₁, B₂, ..., B_n |- C. Induction by the length of the shortest proof.

Induction base. If C is an axiom, then, by Lemma 3.5.3, in the constructive logic, |- O(C). If C is B_i, then O(B_i) |- O(C) in any logic.

Induction step.

If C is derived by MP from B and B->C, then, by induction assumption, in the constructive logic: O(B₁), O(B₂), ..., O(B_n) |- O(B), and O(B₁), O(B₂), ..., O(B_n) |- O(B->C). Let us merge these two proofs. Since O(B->C) is O(B)->O(C), then, by MP, in the constructive logic: O(B₁), O(B₂), ..., O(B_n) |- O(C).

If C is AxB(x), and is derived by Gen from B(x), then, by induction assumption, in the constructive logic: O(B₁), O(B₂), ..., O(B_n) |- O(B(x)). Hence, by Gen, in the constructive logic: O(B₁), O(B₂), ..., O(B_n) |- AxO(B(x)), i.e. O(B₁), O(B₂), ..., O(B_n)|- O(F).

Q.E.D.

2. Let in the constructive logic: |- O(B₁), O(B₂), ..., O(B_n) |- O(C). By Lemma 3.5.1, in the classical logic, |- B_i->O(B_i) for all i, and |- O(C)->C. Hence, in the classical logic, B₁, B₂, ..., B_n |- C.

Q.E.D.

Corollary 3.5.5. If, in the classical logic, B₁, B₂, ..., B_n |- C&~C, then, in the constructive logic, O(B₁), O(B₂), ..., O(B_n) |- O(C)&~O(C). I.e., if the postulates B₁, B₂, ..., B_n are inconsistent in the classical logic, then the postulates O(B₁), O(B₂), ..., O(B_n) are inconsistent in the constructive logic. Or: if the postulates O(B₁), O(B₂), ..., O(B_n) are consistent in the constructive logic, then the postulates B₁, B₂, ..., B_n are consistent in the classical logic.

Corollary 3.5.6. If, for some first order language, the classical logic is inconsistent, then so is the constructive logic. Or: if, for some first order language, the constructive logic is consistent, then so is the classical logic (Goedel [1933], Gentzen [1936]).

Warning! Corollary 3.5.6 does not extend immediately to first order theories, having their own specific non-logical axioms. It must be verified separately for each theory! For example,

Exercise 3.5.2 (for smart students). Verify that, if the constructive first order arithmetic is consistent, then so is the classical first order arithmetic (Goedel [1933], Gentzen [1936]). Thus, the non-constructivity does not add contradictions (at least) to arithmetic. If it would, then we could derive "constructive" arithmetical contradictions as well. (Hint: verify that, a) atomic formulas of arithmetic are stable - this is the hard part of the proof, b) if F is an axiom of arithmetic, then so is O(F).)

K.Goedel. Zur intuitionistischen Arithmetik und Zahlentheorie. Ergebnisse eines mathematischen Kolloquiums, 1933, Vol. 4, pp. 34-38.

Gerhard Gentzen. Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen, 1936, Vol. 112, pp. 493-565.

About constructive embedding operations as a general notion see

Nikolai A.Shanin. Embedding the classical logical-arithmetical calculus into the constructive logical-arithmetical calculus. SSSR, 1954, vol. 94, N2, pp.193-196 (in Russian).Dokladi AN

Back to title page

predicate logic, predicate calculus, intuitionistic, predicate, embedding, minimal, constructive, calculus, theorem, quantifier, operation, intuitionist, constructive embedding, replacement, substitution