Ytukyg

I have been reading the famous Joseph Schoenfield's text "Mathematical Logic" and this may sound naïve but I can't make sense of his comments about finitary proofs. Can someone please explain to me what a "finitary" proof is?

To quote from Schoenfield's text:

"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;"

What exactly is this supposed to mean? I can't think of a proof in mathematics that deals with concrete objects. All objects that are dealt with in mathematical proofs are abstract in nature. We're not talking about the notion of proof as used in a court room, where the objects in question are actual events and/or tangible evidence.

There is another question here which asks the same thing but the answers don't seem to help me. Instead, the answers suggest that if I can't think of a proof as an object in itself, then the above-quoted paragraph will not make sense. Again, I don't know how I'm supposed to look at a written proof as an "object in itself", and what exactly that is to accomplish.

If this suggests that my experience with proofs is lacking, that's a suggestion I absolutely reject. I hold a Master's of Science degree in pure mathematics and I've seen hundreds of proofs in lectures and textbooks. I know what a proof is, say, in analysis, but I couldn't tell you whether it's finitary according to Schoenfield's notion, or whether I'm looking at a written proof as an "object in itself" and what that is supposed to accomplish. Can someone shed light?

The context is the debate about the Foundations of mathematics of the 1930s.

Some lines above, the author says :

An axiom (or theorem) may be viewed in two ways. It may be viewed as a sentence, i.e., as the object which appears on paper when we write down the axiom, or as the meaning of a sentence, i.e., the fact which is expressed by the axiom.

The distinction between "sentence" and its "meaning" is at the core of the well-known Gödel's Incompleteness Theorems :

(under suitable conditions) there are true [this is the "meaning" side] formulas of formal arithmetic that are not provable (from the axioms of the system).

Thus, mathematical logic studies formal systems (the concrete objects) whose meaning are very abstract : number, sets, etc.

The statement :

there is no value in studying concrete (rather than abstract) objects unless we approach them in a concrete or constructive manner. For example, when we wish to prove that a concrete object with a certain property exists, we should actually construct such an object, not merely show that the nonexistence of such an object would lead to a contradiction.

refers to of Hilbert's Program :

In the early 1920s, the German mathematician David Hilbert (1862–1943) put forward a new proposal for the foundation of classical mathematics which has come to be known as Hilbert's Program. It calls for a formalization of all of mathematics in axiomatic form, together with a proof that this axiomatization of mathematics is consistent. The consistency proof itself was to be carried out using only what Hilbert called “finitary” methods.

See also page 3 : "Hilbert, who first instituted this study, felt that only finitary mathematics was immediately justified by our intuition."

In a nutshell, in meta-mathematics [the mathematical study of the properties of "concrete" objects : formal theories], we have to restrict the allowed methods of proof to constructive existence proofs, avoiding non-constructive ones [i.e. existence proofs based on reductio ad absurdum.