# Finitary Proofs in Mathematical Logic

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 wiki sheds some light. – Mason Nov 28 '18 at 23:28
• I don't know Schoenfield's book and I can't justify his statements out of context. However, the whole idea behind mathematical logic is to model mathematical proofs and the formulas that appear in them as mathematical objects in their own right (as strings of symbols, or what are called "syntax trees" in computer science) so that we can reason about them. In the vast majority of the literature (but not all), proofs are expected to be finite objects. In that sense, we expect proofs and the syntactic objects in them (not the mathematical abstractions those objects represent) to be very concrete. – Rob Arthan Nov 28 '18 at 23:51
• @Rob Arthan: I totally get the notion of the language of a formal system as a purely syntactical object, with a set of rules that can determine for each expression whether it is a formula. And yes, we formalize the rules of deduction in this formal (syntactical) system so that they apply to all theories, regardless of particular meanings given to them in particular models. When we prove a theorem in Topology, or Analysis, everyone knows the rules of deduction (most of the time) and the syntactical objects you talk about take on particular meanings depending on the theory and model. – marcus66502 Nov 29 '18 at 1:39
• @ Rob Arthan: What I still don't get is what makes a proof finitary when I look at it, say if I'm looking at a proof of Liouville's Theorem in Analysis. – marcus66502 Nov 29 '18 at 1:40
• The proof of Liouville's theorem involves a finite number of symbols. You'd spot an infinitary proof straight away if one was presented to you. – Rob Arthan Nov 29 '18 at 2:15

## 1 Answer

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.