Is there a natural example of a second order proof that does not reduce to a first order proof in a straight forward way, if all variables are filled in?

Question

Dear all,

This is a retry of question Would Wiles proof of Fermat theorem reduce if you fill in the variables?. I stated that question badly, but my intention are genuine and hope do to a better job here.

First of all, with proof reduction I mean that there is a set of reduction rules (algorithm) that simplifies or alters a proof written in a formal logic. In such way, that the adapted proof will have a certain property after executing, for instance no higher order theorems, or no induction.

A normal mathematical proof is not likely to be reduced, because the mathematician did his best to have a minimum proof. However, if certain variables of the end theorem of the proof are replaced by constants, and this is substituted back over the proof, then a reduction algorithm may simplify such proof. Still, there is no guarantee that significant simplification can be performed on the proof.

Things get a little different when all variables of the end theorem are instantiated to constants, such that the end theorem is a quantifier free theorem. In that situation, ones hopes that the proof collapses and reduces to a trivial proof. This gives the mathematician confidence, that the end theorem is indeed correct (paradoxes have the property that they do not reduce).

If you do such reduction manually, then it often turns out not to be difficult. In case of induction, it can be unrolled if the n is known. However, to do this automated with an algorithm, is far from trivial. There is sequent calculus and cut-elimination and this is not simple.

Suppose there is a second order logic proof and the variables of the end theorem are replaced by constants and substituted back over the proof. For that, it would be nice to have an algorithm that reduces to proof to a trivial first order logic (+PA) proof.

However, it is impossible that we can prove in second order logic that such algorithm is guaranteed to give result. Because, falsum is a quantifier free formula, and by proving that the algorithm halts and gives result, we actually proof the relative consistency of second order logic to first order logic. Since, second order logic can prove the consistency of first order logic, it would mean that second order logic would prove its own consistency, which is not possible, unless it is inconsistent.

Still, the algorithm could exist (and in fact, if second order logic is consistent, it exists, by just searching for the theorem in first order logic), but you need a logic stronger than second order logic, to prove that the algorithm actually works.

Given above I expect (and maybe I am wrong here), that there are second order logical proof that do not reduce straight forward in a first order trivial proof, if all variables are filled in.

I am curious how those proofs look like and if there is a simple natural example (so, that is my question). Also if there is any literature in this area (in case I see it all wrong :-)

Regards,

Lucas

Answer 1

First let me give an example of what I think you mean. We can write a general proof of Wilson's theorem, that $(p-1)!=-1\pmod{p}$ for any prime $p$. We can then change the symbol $p$ in the proof to $19$, and somehow mix in a proof of the fact that $19$ is prime, to get a proof that $18!=-1\pmod{19}$. This will involve a proof that $(\mathbb{Z}/19)\setminus\{0\}$ is a group, and quantification over the elements of that group. Alternatively, we can write a simpler (and quantifier-free) proof where we just calculate that $18!+1=19\times336967037143579$. I think that you are asking for an algorithm that converts the first kind of proof to the second kind of proof.

I think it is possible to ask well-defined and interesting questions along these lines, but that you would need to specify your foundations in much more detail. If you want to pursue this I would suggest that you investigate software like Agda, Coq or Isabelle. In Agda, for example, you can enter proofs in a formal language and get the computer to check them. Moreover, proofs are represented as mathematical objects that can be manipulated, so it makes sense to substitute $p=19$ in a proof of Wilson's theorem and see what you get. Unfortunately, these systems have a fairly steep learning curve.

Answer 2

Firstly, when using natural deduction rather than a sequent calculus, it is fairly straightforward to algorithmically replace an induction step for a given $n$ by the actual proof for this special $n$.

Secondly, an easy way of embedding the relevant parts of second order logic into first order logic is ZFC, and ZFC is the System which is currently mostly used in Mathematics, and in ZFC, you have a concept of functions and relations as first order objects. The advantage of first order logic lies in the fact that it actually has a complete calculus, while second order logic as such does not.

That being said, an example to what I think you wanted to ask: Take second order arithmetic, that is, Peano Arithmetic with second order induction, add a constant $c$ and for this constant, add the infinitely many axioms $c>1$, $c>1+1$, $c>1+1+1$, $\ldots$. As any two Peano-structures are isomorphic, from this follows the falsum $\bot$, obviously. However, by the compactness theorem, this is not the case for first-order Peano Arithmetic. So such a proof cannot exist.