# What is a finitary proof?

I started reading "mathematical logic", by J.R.Shoenfield, but I cannot quite understand a sentence in the very first chapter:

Proofs which deal with concrete objects in a constructive manner are said to be finitary. Another description, suggested by Kreisel, is this: a proof is finitary if we can visualize the proof. Of course neither description is very precise;

I cannot understand what exactly is a finitary proof, is it a synonimous of a constructive proof?

• Neither description is precise. Keep reading. When you are done, reread. If you have never thought about proofs as mathematical entities on their own, the paragraph won't make sense at this point. – Andrés E. Caicedo Jul 31 '14 at 17:40
• Nobody understands "exactly" what is a finitary proof. We know that some proofs are, and some are not, but the dividing line is not so clear. – Carl Mummert Aug 1 '14 at 2:45
• @CarlMummert Some examples would be helpful then, if only an ontological definition is possible. – DanielV Oct 21 '16 at 19:41
• Probably almost everyone would agree that the proof that every natural number greater than $1$ can be factored into primes is finitary. On the other hand, probably very few believe that Gentzen's consistency proof of Peano Arithmetic is finitary. Some people draw an arbitrary line that proofs in PRA are finitary, and most people accept PRA as a finitary theory, but whether that is the upper limit of finitistic proof is not universally accepted. @DanielV – Carl Mummert Oct 22 '16 at 0:11
• @CarlMummert That sort of makes sense....I tend to see finitary used in the context of "this could be demonstrated with a formal program", like "proposition logic is complete because here is a program that decides it", although sometimes I just see that called constructive. Hard for me to distinguish between constructive and finitary. – DanielV Oct 22 '16 at 2:46

I wonder if Schoenfield has the Hilbert-Bernays metamathematical finitism program in mind. If so, the "finitary" bit is meant at the syntactic level (formalisation of proofs), whereas the semantic content could be anything, including classical (nonconstructive) mathematics.

I 'm reading this book and i don't understand this statement but i found this in wiki Finitary

A finitary argument is one which can be translated into a finite set of symbolic propositions starting from a finite1 set of axioms. In other words, it is a proof (including all assumptions) that can be written on a large enough sheet of paper.

And i think this what kreisel meant by : a proof is finitary if we can visualize the proof

For example we can prove the Fermat last theorem by writing down every instance and checking it numerically. This is not finitary.

• This seems quite wrong: One can provide a finitary proof by computation that any particular 'example' is in fact false. But one cannot do a finitary proof by computation that every such example fails. (The proof via algebraic geometry, on the other hand, would be finitary.) – Semiclassical Jul 31 '14 at 17:17
• @Semiclassical did you see that I said it was NOT finitary ? – Rene Schipperus Jul 31 '14 at 17:18
• @Semiclassical What I am saying is there are proof systems that allow infinite deductions, like checking each case (even if there are an infinite number of them). This is not the kind of proof we would normally accept, and does not fall under Schoenfield's designation as finitary. – Rene Schipperus Jul 31 '14 at 17:24
• Ok. I think it was simply said a bit too quickly for me to follow. To confirm that I follow: "In principle, one could prove Fermat's last theorem by checking every single possible example. Such a proof, however, would certainly not be a finitary one!) – Semiclassical Jul 31 '14 at 17:26
• @Semiclassical Yes. That's right. Obviously such a proof cannot exist in the real world, but as a theoretical construct it can be useful. – Rene Schipperus Jul 31 '14 at 17:30