11

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 synonym of a constructive proof?

311411
  • 3,537
  • 9
  • 19
  • 36
Alessandro Codenotti
  • 12,285
  • 3
    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
  • 2
    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 01 '14 at 02:45
  • 1
    @CarlMummert Some examples would be helpful then, if only an ontological definition is possible. – DanielV Oct 21 '16 at 19:41
  • 1
    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 00: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 02:46

4 Answers4

2

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

Abdelrhman Fawzy
  • 456
2

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.

Mikhail Katz
  • 42,112
  • 3
  • 66
  • 131
0

I was recently puzzled by this as well, and things clarified a bit after reading (parts of) [1]. In the introduction, a distinction is made between three types of formulae, which the author claims to be relevant to understanding the difference between finitist and non-finitist:

  1. Formulae without variables, e.g. $2 + 2 = 4$;
  2. Formulae with only free variables for individuals and computable functions: e.g. $2 \times x = f(y)$;
  3. Formulae with bound variables: e.g. $\forall x \exists y (x < y)$.

The first two types are considered "decidable" in the sense that type 1 formulae can be mechanically verified and closed instances of type 2 formulae become type 1 and thus can also be verified. The role of type 2 formulae being that they serve as schemata for generating type 1 formulae. Finally, the author puts forward the thesis that an argument is not considered finitist if it contains formulas with bound variables (type 3).

Overall, I don't think there is a concrete definition of what a finitist argument is, and it certainly has a large overlap with constructiveness. But the way it is employed in Shoenfield's book seems consistent with this interpretation, especially when considering section 4.3 on the Consistency Theorem.

[1] Kreisel, G. (1951). On the interpretation of non-finitist proofs—Part I. Journal of Symbolic Logic, 16(4), 241-267. doi:10.1017/S0022481200100581

0

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

Rene Schipperus
  • 39,526
  • 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
  • Then I think our wires are crossed. Did you mean to say "We can not prove the Fermat last theorem"? (In case that's the case, I'm removing my downvote.) – Semiclassical Jul 31 '14 at 17:19
  • 1
    @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
  • 1
    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
  • 3
    @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