4

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?

marcus66502
  • 79
  • 2
  • 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 01: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 01: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 02:15
  • @ Rob Arthan: So what you're saying is that finitary proofs are precisely those that involve a finite number of symbols. If this is what you're saying and if it's true then it's a step forward in answering my question. Infinitary proofs (by which I assume you mean proofs that are NOT finitary?) would be those involving an infinite number of symbols? Can you give me an example of this? – marcus66502 Nov 29 '18 at 02:43
  • See Constructive Mathematics and Hilbert's Program. – Mauro ALLEGRANZA Nov 29 '18 at 07:16
  • See also W.W. Tait, Remarks on finitism. – Mauro ALLEGRANZA Nov 29 '18 at 07:17
  • @marcus66502 As Rob suggested, to discuss proofs in the context of mathematical logic, first we formalize them in some language. Finitary proofs require finitely many symbols of this language and satisfy fairly stringent requirements. They do not quite look like standard proofs in natural language, but the point is that just about any proof in the natural sense of the word "can (at least in theory) be rewritten as one of these formal counterparts. On the other hand, there may be infinitary proofs that do not adhere to these patterns. For instance: – Andrés E. Caicedo Nov 29 '18 at 20:19
  • To be concrete, consider a theory of natural numbers (such as first-order Peano arithmetic). It could be that, working in your favorite (reasonable, decently strong) theory, you can prove of some statement $P(x)$ that $P(0)$ holds, $P(1)$ holds, $P(2)$ holds, etc. These are infinitely many different proofs, one for each natural $n$. However, it may well be that your theory is not strong enough to prove $\forall x,P(x)$. Nevertheless, if you proved each $P(n)$, it would be reasonable to conclude this sentence as well. An example of an infinitary system allows this $\omega$-rule: – Andrés E. Caicedo Nov 29 '18 at 20:22
  • From the infinitely many statements $P(n)$, $n\in\mathbb N$, it follows that $\forall x,P(x)$. Proofs with this rule are not quite finitary objects. Of course, it could be that any such proof can be reformatted as a finitary one, but this is in general not the case, at least with our current notion of finitary proof. There are many other possibilities. For instance, the completeness theorem tells us that a statement $\phi$ is provable (in the strict finitary sense) in a theory $T$ if and only if any model of $T$ (in the sense of model theory) is also a model of $\phi$. Ok. Now, ... – Andrés E. Caicedo Nov 29 '18 at 20:26
  • It may well be that one is not interested in all models of $T$ but only in certain "well-behaved" ones. We could then introduce a new rule, that says that $\phi$ is "provable" from $T$ if it holds in all well-behaved models of $T$. These are usually infinitary proofs in he sense that do not have any reasonable finitary counterpart. These "proofs" are actually used in practice, by the way. In set theory, for example, many times we only care about so-called transitive models of set theory rather than all models, and there are many properties that hold in all these models but are not ... – Andrés E. Caicedo Nov 29 '18 at 20:29
  • provable in set theory (in the finitary sense). Now, you could object that these are (or at least might be) finitary proofs, only not in set theory but in some variant theory. Sure. But you see how these examples open the door to many other options: Proofs of variable infinite length (say, indexed by ordinals), proofs involving arbitrary collections of models (for which there may not be a reasonable finitary description) and so on. – Andrés E. Caicedo Nov 29 '18 at 20:31
  • (Nice question, by the way.) – Andrés E. Caicedo Nov 29 '18 at 20:32
  • @ Andres E. Caicedo : Thank you for your comments. They certainly helped elucidate the concept. Since you were talking about proofs in natural languages, I just wanted to add that when we state a proof in a natural language in, say Fourier Analysis, we do so for pure convenience, with the clear understanding that we can rewrite any such proof in a formal language (although first we'd have to agree on the formal language and the logical and nonlogical axioms of the ambient theory). Just like defined symbols are NOT symbols of the formal language. They're symbols added for convenience. – marcus66502 Nov 29 '18 at 21:28
  • @ Andres E. Caicedo : …. and any formula written with these defined symbols can be rewritten using only the symbols of the formal language. Anyway my point is that ALL mathematics can be done within formal systems, no matter what the theory is, because we only follow formal rules of deduction. A proof that fails to do so is no proof at all. And so this is what I was trying to get at with my original question, how can we determine when we look at a proof whether it's finitary or not. – marcus66502 Nov 29 '18 at 21:31
  • @marcus66502: Rob's wrong about what "finitary" means. It is a philosophical notion that different logicians have different views on. A common view is that any arithmetical statement (i.e. sentence over PA) is finitary, and that any finitary proof can be translated to a proof over ACA. See this post about ACA. – user21820 Apr 11 '20 at 03:59

1 Answers1

3

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.

Mauro ALLEGRANZA
  • 94,169