Revisiting Kalmar completeness metaproof

Angélica Olvera Badillo1

Universidad de las Américas,

Sta. Catarina Mártir, Cholula, Puebla, 72820 México
angelica.olverabo@udlap.mx

Abstract In this paper, I present an alternative metaproof of the central

lemma of the Kalmar completeness theorem, shown in Introduction to Mathe-
matical Logic of Elliot Mendelson. It is well-known that the demonstration of a
metamathematical theorem enables us to construct a formal proof. Neverthe-
less, the metaproof shown by Mendelson does not let us to construct entirely
a formal proof if it falls into one case in particular. Based on this observation,
I propose an alternative metaproof with the aim to provide a method that
enable us to construct any formal proof and to allow us to do a recursive
algorithm without falling in some kind of endless loop.
Keywords: propositional calculus, Kalmar, completeness theorem, metamath-
ematics.

1 Introduction

The metaproof1 of the completeness theorem that is reviewed here is due to Kalmar
[2], although it appeared first in Post [6] and then there was another version of Hilbert
and Ackermann [1] in 1928. This metaproof presented here is used by Mendelson [5]
and by Kleene [4] [3].
The completeness theorem states that if a formula A of L2 is a tautology, then
it is a theorem of L. The metaproof of this theorem makes use of a central lemma
and the deduction theorem. The metaproofs of both are constructive, as well as the
whole metaproof of the completeness theorem. This constructive sense is a feature we
expect to find in all the demonstrations of the metamathematical theorems because

“if they have the finitary character which metamathematics is supposed to

have, the demostrations will indicate, at least implicitly, methods for obtain-
ing the formal proofs” [3]

The metaproofs of the deduction theorem and the lemma differ in that the first
one provides an explicit method to construct a proof, while the second one provides
1
The word metaproof is going to be used to refer to a certain sequences of the English
language that serve as an argument to justify the assertions about the language [5] or
formal theory that is being discussed, in this case is the formal theory L that it is presented
in the Background section. It is going to be used the word proof to refer to a certain
sequence of formulas of L
2
L is a formal theory presented by Mendelson [5] and is going to be defined in the Back-
ground section
99
it only implicitly. In fact, Kleene, in [4], clearly illustrates, through an example, that
it is possible to construct entirely a proof using the deduction theorem metaproof.
The reason why the metaproof of the lemma provides a method for constructing
proofs only implicitly is because there is one subcase, within the metaproof, where
there is no more indication as to how to continue building the proof. Therefore, this
method is not as obvious and explicit as the ones provided by most metaproofs as
for example, the metaproof of the deduction theorem. For that aim, I propose an
alternative metaproof in order to provide an explicit method to construct proofs.
This will have at least two benefits, the first one being that teaching the metaproof
will be easier because students just have to follow the metaproof step by step to
construct a proof, and the other one has to do with the area of computer sciences,
because it will be easier to create a recursive algorithm for the automatic construction
of proofs.
This paper is structured as follows. In Section 2, the concepts, definitions and
formal theory that will be used in this paper are introduced, as well as the lemma
and its metaproof provided by Mendelson. In Section 3, the alternative metaproof
that I propose and an example of a proof constructed with the aid of the given
metatheorem are presented. Finally in Section 4, I present some conclusions.

2 Background
In this section, I review some fundamental concepts and definitions following [5] that
will be used throughout this work. I introduce first an axiomatic approach for the
propositional calculus. I also present the central lemma of the Kalmar completeness
theorem provided by Mendelson and an example of a proof which falls into the par-
ticular subcase that is no longer constructive.

2.1 Axiomatic approach for the propositional calculus

In this paper, it is going to be used a formal axiomatic theory for the propositional
calulus which only has only the symbols ¬, →, (,), and the letters Ai with positive
integers i as subscripts: A1 , A2 , A3 , . . .. The symbols ¬ and → are called primitive
connectives, and the letters Ai are called statement letters. A formula is either a
statement letter or a statement form built up from formulae by means of the connec-
tives ¬ and →.
If α, β, and θ are formulas of L, then the following are axioms of L:

(A1) α → (β → α)
(A2) (α → (β → θ)) → ((α → β) → (α → θ))
(A3) (¬β → ¬α) → ((¬β → α) → β)

The only rule of inference of L is modus ponens: β is a direct consequence of α

and (α → β).

For any formulas α and β, the following are theorems of L:

Theorem 1. ` β → ¬¬β
100
Theorem 2. ` ¬α → (α → β)

Theorem 3. ` α → (¬β → ¬(α → β))

The theorems already mentioned are going to be used in the central lemma of the
Kalmar metaproof.

The treatment of logic done so far is called “proof theory”, nevertheless, there is
another way of founding logic called “model theory” where the concept of interpre-
tation arises. An interpretation is an assignment of the truth values true or false to
the statement letters that occur in a formula, under that interpretation, the whole
formula takes the value either true or false. Here, the last ones are going to be denoted
by T or F respectively.

2.2 The central lemma of the Kalmar metaproof

In this section I review a central lemma of the Kalmar completeness theorem of the
propositional logic and its metaproof shown by Elliott Mendelson [5]. The lemma is
the following.

Lemma 1. Let α be a wf, and let B1 , . . . , Bk be the statement letters that occur in
α. For a given assignment of truth values to B1 , . . . , Bk , let Bi0 be Bi if Bi takes the
value T; and let Bi0 be ¬Bi if Bi takes the value F. Let α0 be α if α takes the value T
under the assignment, and let α0 be ¬α if α takes the value F. Then B10 , . . . , Bk0 ` α0 .

Proof. The proof is by induction on the number n of ocurrences of ¬ and → in α. If

n = 0, α is just a statement letter B1 , and then the lemma reduces to B1 ` B1 and
¬B1 ` ¬B1 . Assume now that the lemma holds for all j < n.

– Case 1. α is ¬β. Then β has fewer than n occurrences of ¬ and →.

• Subcase 1a. Let β take the value T under the given truth value assignment.
Then α takes the value F. So, β 0 is β and α0 is ¬α. By the inductive hypothesis
applied to β, B10 , . . . , Bk0 ` β. Then, by theorem 1 and MP, B10 , . . . , Bk0 ` ¬¬β.
But, ¬¬β is α0 .
• Subcase 1b. Let β take the value F. Then β 0 is ¬β and α0 is α. By inductive
hypothesis, B10 , . . . , Bk0 ` ¬β. But, ¬β is α0 .
– Case 2. α is β → θ. Then β and θ have fewer occurrences of ¬ and → than α. So,
by inductive hypothesis, B10 , . . . , Bk0 ` β 0 and B10 , . . . , Bk0 ` θ0 .
– Case 2a. β takes the value F. Hence, α takes the value T. Then β 0 is ¬β and α0
is α. So, B10 , . . . , Bk0 ` ¬β. By theorem 2, B10 , . . . , Bk0 ` β → θ. But, β → θ is α0 .
– Case 2b. θ takes the value T. Hence α takes the value T. Then θ0 is θ and α0 is
α. Now, B10 , . . . , Bk0 ` θ. Then, by axiom schema (A1), B10 , . . . , Bk0 ` β → θ. But,
β → θ is α0 .
– Case 2c. β takes the value T and θ takes the value F. Then α takes the value F.
β 0 is β, θ0 is ¬θ, and α0 is ¬α. Now, B10 , . . . , Bk0 ` β and B10 , . . . , Bk0 ` ¬θ. So, by
theorem 3, B10 , . . . , Bk0 ` ¬(β → θ). But ¬(β → θ) is α0
101
Example 1. Lets take the well known pierce formula: (((A → B) → A) → A) and let
the assignment of truth values to the statement letters as follows: A takes the value
F and B takes the value T. So the metaproof just given is supposed to enable us to
construct the proof of ¬A, B ` ((A → B) → A) → A.

In order to make more clear the way it is going to follow the metaproof to construct
the proof, I use horizontal brackets indicating the formula α and their subformulas β
and θ when needed.
α
z }| {
Proof. ¬A, B ` ((A → B) → A) → |{z}
A
| {z }
β θ
This is the case 2a where β takes the value F. So,

1.¬((A → B) → A) by inductive hypothesis (*to prove)

2.¬((A → B) → A) → (((A → B) → A) → A) theorem 2
3.((A → B) → A) → A modus ponens from 1 and 2.

In the earlier proof, note that I wrote the formula ¬((A → B) → A) by inductive
hypothesis, this means that we take it as already demostrated and provable. But to
construct the whole proof of the pierce formula we have to construct the proof of
those formulas too. I shall use “*” to indicate those formulas that need to be proved.
α
z }| {
*to prove ¬A, B ` ¬((A → B) → A)
| {z }
β
This is the case 1b where β takes the value F. Note that the metaproof says this is
already proved and does not indicate how to construct the proof when it falls into this
case. Hence, it does not allow us to construct the whole pierce formula. This example
shows how this metaproof, although it is correct, loses some of the constructive sense
the metaproofs are supposed to have.

In the next section, I propose an alternative metaproof with the aim to enable the
complete construction of proofs.

3 The alternative metaproof

The alternative metaproof of the lemma 1 that I propose is the following.

Proof. The proof is by induction on the number n of ocurrences of ¬ and → in α0 .

If n ≤ 1, α0 is B1 or ¬B1 where B1 is just a statement letter, and then the lemma
reduces to B1 ` B1 and ¬B1 ` ¬B1 Assume now that the lemma holds for all j < n.

– Case 1. α0 is ¬β
102
 • Subcase 1a. β is ¬θ. Hence α0 is ¬¬θ. Given that β takes the value F, then θ
takes the value T. Then θ0 is θ So,

1. B10 , . . . , Bk0 ` θ by inductive hypothesis.

2. B10 , . . . , Bk0 ` θ → ¬¬θ theorem 1
3. B10 , . . . , Bk0 ` ¬¬θ modus ponens from 1 and 2.
But, ¬¬θ is α0

• Subcase 1b. β is θ → γ. Hence α0 is ¬(θ → γ). Given that β takes the value F,
then θ takes the value T and γ takes the value F. Then θ0 is θ and γ 0 is ¬γ. So,

1. B10 , . . . , Bk0 `θ by inductive hypothesis.

2. B10 , . . . , Bk0 ` ¬γ by inductive hypothesis
3. B10 , . . . , Bk0 ` θ → (¬γ → ¬(θ → γ)) theorem 3
4. B10 , . . . , Bk0 ` ¬γ → ¬(θ → γ) modus ponens from 1 and 3
5. B10 , . . . , Bk0 ` ¬(θ → γ) modus ponens from 2 and 4
But, ¬(θ → γ) is α0

– Case 2. α0 is β → θ
• Subcase 2a. β takes the value F. Then β 0 is ¬β. So,

1. B10 , . . . , Bk0 ` ¬β by inductive hypothesis

2. B10 , . . . , Bk0 ` ¬β → (β → θ) theorem 2
3. B10 , . . . , Bk0 ` β → θ modus ponens from 1 and 2
But, β → θ is α0

• Subcase 2b. θ takes the value T. Then θ0 is θ. So,

1. B10 , . . . , Bk0 ` θ by inductive hypothesis.

2. B10 , . . . , Bk0 ` θ → (β → θ) Axiom schema (A1)
3. B10 , . . . , Bk0 ` β → θ modus ponens from 1 and 2.
But β → θ is α0

Example 2. Lets take the same example 1 (((A → B) → A) → A) with the same
assignment of truth values to the statement letters: A takes the value F and B
takes the value T. So, the metaproof just given enable us to construct the proof
of ¬A, B ` (((A → B) → A) → A)

As in the example 1, it is going to use the horizontal brackets to indicate the

formula α0 and their subformulas β, θ and γ when needed, in order to make the
construction of the proof more clear to the reader.
α0
z }| {
Proof. ¬A, B ` ((A → B) → A) → |{z}
A
| {z }
β θ

103
 This is the subcase 2a where β takes the value F. So,

1.¬((A → B) → A) by inductive hypothesis (*to prove)

2.¬((A → B) → A) → (((A → B) → A) → A) theorem 2
3.((A → B) → A) → A modus ponens from 1 and 2.

α0
z }| {
*to prove: ¬A, B ` ¬ ((A → B) → |{z}
A )
| {z }
θ γ
| {z }
β
This is the subcase 1b where β is θ → γ. So,

1.A → B by inductive hypothesis (**to prove)

2.¬A assumption formula
3.(A → B) → (¬A → ¬((A → B) → A)) theorem 3
4.¬A → ¬((A → B) → A) modus ponens from 1 and 3
5.¬((A → B) → A) modus ponens from 2 and 4

α0
z }| {
**to prove: ¬A, B ` |{z}
A → |{z}
B
β θ
This is the subcase 2a where β takes the value F. So,

1.¬A assumption formula

2.¬A → (A → B) theorem 2
3.A → B modus ponens from 1 and 2

Now, there is not another formula that needs to be proved, so the proof is complete,
built following the metaproof that I propose.

The complete proof of the pierce formula is the following.

Proof. ¬A, B ` (((A → B) → A) → A)

1.¬A assumption formula

2.¬A → (A → B) theorem 2
3.(A → B) modus ponens from 1 and 2
4.(A → B) → (¬A → ¬((A → B) → A)) theorem 3
5.¬A → ¬((A → B) → A) modus ponens from 3 and 4
6.¬((A → B) → A) modus ponens from 1 and 5
7.¬((A → B) → A) → (((A → B) → A) → A) theorem 2
8.((A → B) → A) → A modus ponens from 6 and 7

104
4 Conclusions

In this work I reviewed the Kalmar completeness theorem and the lemma that it
uses. I also mentioned the problem we have to deal with if we follows the metaproof
of the lemma provided by Mendelson to construct a formal proof. So it is proposed
an alternative metaproof of the lemma, in order to indicate explicitly a method for
obtaining a formal proof and it is illustrated, through an example, how this this
is possible just following the proposed metaproof. The benefits of the my proposal,
already mentioned, are at least two, the first one being that teaching the metaproof
will be easier because students just have to follow the metaproof step by step to
construct a proof, and the other one has to do with the area of computer sciences,
because it will be easier to create a recursive algorithm for the automatic construction
of proofs.

References
1. D. Hilbert and Acker. Grundzüge der theorethischen Logik. Springer, Berlin, first edition,
1928.
2. L. Kalmár. Über die axiomatisierbarkeit des aussagenkalküls. Acta scientiarum mathe-
maticarum (Szeged), 7:222–243, 1935.
3. S. C. Kleene. Introduction To Metamathematics. American Elsevier Publishing Company,
Inc., New York, N.Y., first edition, 1974.
4. S. C. Kleene. Mathematical Logic. Dover, Mineola, N.Y., first edition, 2002.
5. E. Mendelson. Introduction to Mathematical Logic. Wadsworth, Belmont, CA, third
edition, 1987.
6. E. L. Post. Introduction to a general theory of elementary propositions. Amer. jour.
math., 43:163–185, 1921.

105
106