Infinite number of Proofs in Propositional Calculus?

Question

Reading over a book on computability, it asserts that in P.C., if A is a theorem, then A has arbitrarily many proofs. I can't see how that would work, would you do an infinite loop in the sequence of well-formed-formulae?

Answer 1

A proof is a sequence of steps that leads to desired conclusion at the end. Nobody says that all these steps have to be relevant. For instance, just before concluding the proof you can put lots of logical tautologies. For a human reader, they will obviously be irrelevant to the proof, but nevertheless, the new proof, the bigger part of which is pointless, will still be a correct proof.

For instance, here's a proof that all numbers divisible by 4 are also divisible by 2:

Let $n$ be a number divisible by $4$. It means there's some $k$ such that $n = 4k$. But $4k = 2\cdot 2k$. Putting $l = 2k$, we have $n = 2l$. Thus $n$ is divisble by 2.

Here's another proof.

Let $n$ be a number divisible by $4$. It means there's some $k$ such that $n = 4k$. But $4k = 2\cdot 2k$. Putting $l = 2k$, we have $n = 2l$. We see that $n = 2l$. We also have $4k = 2 \cdot 2k$. We know that $n$ is divisible by $4$. We see that $n = 2l$. Thus $n$ is divisble by 2.

We obviously can make even longer (or arbitrarily long) proof.

Answer 2

There exist several ways to indicate this. I'll consider classical logical systems which only have detachment and universal substitution as primitive inference rules. I use Polish notation. Classical logic has CpCqp as a theorem. So, if "a" is a theorem, and "b" is a theorem we can prove "a" as follows:

Substitute p with a, q with b in CpCqp, abbreviated CpCqp p/a, q/b. The "*" symbol separates the left hand side from the right hand side.

1 CaCba

1*Ca-2

This says that formula 1 comes as equiform to CaCba, with "a" as the antecedent, and 2 as the consequent, and we will detach 2.

2 Cba

2*Cb-3

3 a

Since b comes as arbitrary, and classical logic has an arbitrary "number" of theorems, it follows that we can prove "a" in an arbitrary "number" of ways.

We also have CNNpp and CpNNp as theorems. So, if "a" is a theorem, then we can obtain NNa as a theorem, NNNNa as a theorem, and so on. Then we can prove "a" by using CNNpp and making appropriate substitutions.