# 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?

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

-
I'm not sure I understand the question you're asking, but one difficulty that arises immediately is that second-order logic has no good proof system; what does "a second-order logic proof" mean to you? (I also don't think the notion of a proof reduction is quite clear.) –  Noah S Apr 8 '12 at 19:09
Noah, thanks for reading my question. With 'proof' I mean the whole derivation tree of a theorem. For second order logic, I mean a logic where I can quantify over functions or predicates. I don't know what you mean that second-order logic has no good proof system. At least I can say, in informal mathematics, a proof that requires quantification over functions or predicates. For the proof reduction, it is difficult to be more clear, because I failed to make the precise algorithm. It is an attempt to automate the things I can do manually, but I want to understand better, why I failed. –  Lucas K. Apr 8 '12 at 21:02
Derivation tree with what axioms and rules? There isn't a canonical answer for second-order logic; "full" second order logic, where the range of quantification is understood to be all sets and predicates fails compactness, and therefore doesn't have any conventional proof system. The usual alternative is a first-order formulation where functions and predicates are just objects of a different sort, together with comprehension principles (as in reverse math or ZFC); but this is actually first-order logic. –  Henry Towsner Apr 8 '12 at 21:34
Henry, thanks for pointing this out. I mean second order logic as in reverse math. So, where functions and predicates are just objects and with full comprehension principle. For my question it is only relevant, that we have a stronger logic that FOL + PA, that is capable of proving the consistency of FOL + PA. As far I know (but I could be wrong), second order logic in the sense of reverse math, is capable of that. For any consistent system that is capable of proving consistency of FOL + PA, it is not possible to prove relative consistency in that system. So, why does that proof fail? –  Lucas K. Apr 10 '12 at 20:37

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.

-
Neil, thanks for answer. I have learned some HOL-light. HOL, Isabelle and Coq (I don't know Agda), are type theory, I thought it would be simpler to restrict it to second order logic. If I indeed want to make such algorithm, then you are right that I need to be more specific. However, in general I can say, that such algorithm won't work, because it would ultimo mean that the logic could prove it's own consistency if it can prove the termination of the algorithm. Since, I can do these things manually, I don't understand which cases are intrinsically hard. I think these cases are in all sys. –  Lucas K. Apr 8 '12 at 21:18

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.

-
"in ZFC, you have a concept of functions and relations as first order objects." What do you mean by that? The only first order objects in ZFC are the sets and nothing else. –  Guillaume Brunerie Apr 9 '12 at 11:36
@Guillaume: In ZFC, one usually defines functions and relations as sets (of ordered pairs). That won't give you class-sized "functions" (for example, ones whose domain is the whole universe), but it (more than) suffices to give you all the functions from integers to integers, and these are what's relevant to second-order arithmetic. –  Andreas Blass Apr 9 '12 at 13:13
Schoppenhauer, thanks for the answer. But this is not exactly what I was looking for. You extend the second order logic with additional axioms. But, I just want, without extending the logic, a theorem in second order logic, for which the proof does not reduce to a trivial first order logic theorem, when all variables are filled in. As I explained in my question, I think such theorem must exists, because if it does not exist the logic could prove its own consistency. –  Lucas K. Apr 10 '12 at 20:32