In this paper, I present an alternative metaproof of the central lemma of the Kalmar completeness theorem, shown in Introduction to Mathematical Logic of Elliot Mendelson. It is well-known that the demonstration of a metamathematical theorem enables us to construct a formal proof. Nevertheless, 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.
The metaproof1 of the completeness theorem that is reviewed here is due to Kalmar
[
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 nd in all the demonstrations of the metamathematical theorems because
\if they have the nitary character which metamathematics is supposed to
have, the demostrations will indicate, at least implicitly, methods for
obtaining the formal proofs" [
The metaproofs of the deduction theorem and the lemma di er in that the rst
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 [
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 bene ts, the rst 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, de nitions 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
In this section, I review some fundamental concepts and de nitions following [
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 connectives : 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 : and ( ! ). is a direct consequence of For any formulas
and , the following are theorems of L:
! :: Theorem 2. ` : ! ( ! )
! (:
! :( ! ))
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 interpretation 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 [
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 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.
Proof. :A; B ` (z(A ! B) !}| A) ! | {z }
A{ |{z} This is the case 2a where
takes the value F. So, 1::((A ! B) ! A) 2::((A ! B) ! A) ! (((A ! B) ! A) ! A) 3:((A ! B) ! A) ! A
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. *to prove :A; B ` z:((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 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 :
Subcase 1a. is : . Hence 0 is :: . Given that takes the value T. Then 0 is So, takes the value F, then
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 ` 2: B10; : : : ; Bk0 ` : 3: B10; : : : ; Bk0 ` ! (: ! :( ! 4: B10; : : : ; Bk0 ` : ! :( ! ) 5: B10; : : : ; Bk0 ` :( ! ) by inductive hypothesis.
by inductive hypothesis )) theorem 3 modus ponens from 1 and 3 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 ` : 2: B10; : : : ; Bk0 ` : 3: B10; : : : ; Bk0 ` ! (
! ) ! by inductive hypothesis theorem 2 modus ponens from 1 and 2 But, !
is 0 Subcase 2b. takes the value T. Then 0 is . So, 1: B10; : : : ; Bk0 ` 2: B10; : : : ; Bk0 ` 3: B10; : : : ; Bk0 ` ! ( ! ! ) by inductive hypothesis.
Axiom schema (A1) 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 Proof. :A; B ` (z(A ! B) !}| A) ! A{
| {z } |{z} This is the subcase 2a where 1::((A ! B) ! A) 2::((A ! B) ! A) ! (((A ! B) ! A) ! A) 3:((A ! B) ! A) ! A 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 **to prove: :A; B ` zA !}| B {
|{z} |{z} This is the subcase 2a where
takes the value F. So, 1::A 2::A ! (A ! B) 3:A ! B assumption formula theorem 2 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 2::A ! (A ! B) 3:(A ! B) 4:(A ! B) ! (:A ! :((A ! B) ! A)) 5::A ! :((A ! B) ! A) 6::((A ! B) ! A) 7::((A ! B) ! A) ! (((A ! B) ! A) ! A) 8:((A ! B) ! A) ! A assumption formula theorem 2 modus ponens from 1 and 2 theorem 3 modus ponens from 3 and 4 modus ponens from 1 and 5 theorem 2 modus ponens from 6 and 7
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 bene ts of the my proposal, already mentioned, are at least two, the rst 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.