12
$\begingroup$

Hilbert's program is popularly understood as an attempt to justify infinitary mathematics with a finitary consistency proof. Godel's Second Theorem is usually considered as showing this is not possible.

Question (to be made precise below): Can finitary mathematics be justified with a ultrafinitistic consistency proof?

Consider FPA, a multi-sorted first-order theory, with lower-case or small letters (for numbers) and upper-case or big letters for relations of n-arity (n >= 1). (Practically, I think one can limit the theory to relations where n = 1, 2, or 3.)

Full comprehension is assumed.

FPA has a constant symbol 0, a 1-ary relationship N (natural number), and a 2-ary relationship symbol S (successoring).

In this context the Peano Axioms can be written:

(PA1) N0
(PA2) $\forall$n (Nn $\Rightarrow$ $\exists$m (Nm & Sn,m))
(PA3) $\forall$n$\forall$m$\forall$m' (Nn & Nm & Nm' & Sn,m & Sn,m' $\Rightarrow$ m = m')
(PA4) $\forall$n$\forall$m$\forall$n' (Nn & Nm & Nn' & Sn,m & Sn',m $\Rightarrow$ n = n')
(PA5) $\forall$n (Nn $\Rightarrow$ $\neg$ Sn,0)
(PA6) $\forall$P (P0 & $\forall$n$\forall$m(Pn & Sn,m $\Rightarrow$ Pm) $\Rightarrow$ $\forall$n(Nn $\Rightarrow$ Pn))

FPA assumes all the Peano Axioms except (PA2), that is, everything except the totality of the successor relationship. It has as its standard models all the initial segments as well as the standard model of the natural numbers. {0} is a model. It is therefore agnostic as to whether the natural numbers go on and on. Let's call it "ultrafinitistic" even if it's not always clear to me what "ultrafinitistic" means.

Now an ultrafinitistic Hilbert's Program might be the following. Let E(n) be the wff
$\exists x_1 \exists x_2 ... \exists x_n$(N$x_1$ & S0,$x_1$ & N$x_2$ & S$x_1,x_2$ & ... & S$x_{n-1},x_n$)
i.e. the assertion that the number n exists. The ultrafinitistic hope would be that FPA can prove the consistency of FPA + E(n) for any n, or even (this would be magical) prove the assertion
$\forall$n Cons(FPA + E(n)).

Now in one sense of consistency, where like Godel one uses numbers to represent sequences, one can actually get started on this. Restricting the arities of the upper-case letters to no more than 3 (which is sufficient to develop the appropriate apparatus), it seems that FPA can prove the Godel consistency of FPA + E(1) and FPA + E(2).

However, the proof works with a certain cheat; Godel numbering uses numbers so big that the assumption that there is a proof leading to a contradiction implies the existence of a truly big number, which provides enough space for creating a model of true-in-{0,1} or true-in-{0,1,2} for propositions whose length are <= the length of the longest proposition appearing in the proof of contradiction. A more appropriate manner of representing consistency would surely be to use the upper-case letters, since then a sequence of length n only implies the existence of n, which is obviously much smaller than the Godel number. Let RCons(FPA) and the like represent this notion of consistency.

According to Can FPA really prove its consistency? whether FPA can prove RCons(FPA) is equivalent to a well-known open problem which is conjectured to be false. Obviously, this does not bode well for FPA proving stronger systems to be RCons consistent. Still, "open" brings hope, so my questions are:

(1) Can it be shown, for any n, that FPA does not prove RCons(FPA + E(n))?
(2) If so what is the smallest n?
(3) If not can it be shown that FPA cannot prove $\forall$n Cons(FPA + E(n)) ?

If something significant can be said with a different formula asserting the existence of a number other than E(n) (e.g. defined using an exponential), that would obviously be of interest. (EDITED ADDITION: The restriction of upper-case letters to arity 3 or less is welcome, especially if a "yes" answer plays on unbounded arity.)

Since this is my third question about this theory, I would also like here to refer to this question/answer, where the models (and other details) of FPA are described: Provability in Second-Order Arithmetic without the Successor Axiom so with one search I can later find everything.

Thanks for your time.

Improve this question
$\endgroup$
6
  • 3
    $\begingroup$ I also have work to do, so I’m not going to write a detailed answer this time. Any finite model can be simulated by quantified propositional logic, hence if you restrict arities to be constant, RCons(FPA+E(n)) again reduces to the consistency of $G$. If the arities are arbitrary, then adding $E(1)$ makes the consistency strength stronger (as satisfiability of second-order formulas in a model with two-element universe is complete for $\mathrm{ALTTIME}(n^{O(1)},2^{O(n)})$, I believe), but having $E(n)$ with larger (but constant) $n$ should not make any further difference. ... $\endgroup$
    – Emil Jeřábek
    Commented Jan 30, 2013 at 12:15
  • 3
    $\begingroup$ ... I guess that with arbitrary arities, (1) is true (and some sort of diagonalization should work), (2) n = 1. As for (3), I’d expect FPA cannot prove the formula, but showing it might be difficult. If you restrict arities, then as mentioned, the provability of (1) in unrestricted FPA is an open problem. There is a chance that its provability in restricted FPA may be refuted unconditionally, because this breaks the connection to $I\Delta_0+\Omega_1$. $\endgroup$
    – Emil Jeřábek
    Commented Jan 30, 2013 at 12:29
  • 3
    $\begingroup$ I realized that I read (1) as “... FPA does not prove RCons(FPA + E(n))”, and similarly for (3). If this was not intended, i.e., you really ask about provability of the consistency of RCons(FPA + E(n)), you need to specify what kind of consistency, and how one should understand the consistency of the bare formula RCons(FPA + E(n)) without a background theory (i.e., should it really be the consistency of FPA + RCons(FPA + E(n)), or something else). $\endgroup$
    – Emil Jeřábek
    Commented Jan 30, 2013 at 12:34
  • 3
    $\begingroup$ With all respect I would also suggest that since the theories you are interested in turn out to be a variant of bounded arithmetic in disguise, it would be more efficient if you studied some bounded arithmetic first before making further questions about provability in such theories. Classical introductions to the subject are Chap. V of Hájek and Pudlák’s book, Krajíček’s “Bounded arithmetic, propositional logic, and complexity theory”, Buss’s Chap. II in the “Handbook of Proof Theory”, and his thesis (available on his webpage). ... $\endgroup$
    – Emil Jeřábek
    Commented Jan 30, 2013 at 12:43
  • 2
    $\begingroup$ ... The new book “Logical foundations of proof complexity” by Cook and Nguyen may be easier to read as it works with second-order theories closer to your setup than the traditional first-order systems, but on the other hand it also concentrates more on computational complexity and especially small complexity classes like $TC^0$. $\endgroup$
    – Emil Jeřábek
    Commented Jan 30, 2013 at 12:47

1 Answer 1

Reset to default
6
$\begingroup$

Ulrich Kohlenbach with his coworkers in proof mining has perhaps the best modern nonfatalist position about Hilbert program. Rather than stressing over Gödel's demolition of Hilbert's ideal, we can analyze the extent to which "non-finitary" methods play a role. This has lead to some very nice results and applications of proof theory. Lecture 1 of Ulrich's notes on "Proof mining" provides a quick but more careful explanation of the idea that proof mining is the natural outcome of Hilbert's program.

Improve this answer
$\endgroup$
3
  • $\begingroup$ I guess the question in my subject was badly chosen. I wasn't actually asking whether there are possible ways to redo a Hilbert program, but whether one specific way was possible. In any case, thank you for the information, I'll take a look. $\endgroup$
    – abo
    Commented Jan 30, 2013 at 19:07
  • 3
    $\begingroup$ Yes, I understand that you asked about FPA, but I thought nontheless there is no harm in answering the question is a slightly broader sense. $\endgroup$
    – Andrej Bauer
    Commented Jan 30, 2013 at 20:45
  • 1
    $\begingroup$ Link is broken, I think the paper is this one but I am not sure, so I did not edit. $\endgroup$
    – durum
    Commented Mar 22, 2018 at 14:12

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .