12
$\begingroup$

As you all know, Ronald Graham just passed away. He is famous for many fabulous contributions to finite combinatorics, and much much more, but perhaps none of them is as popular as the infamous Graham number (see here): $g_{64}$.

This number is truly huge, though in more recent times it has been dwarfed by several other "finite inaccessible numbers" (allow me to call them that way), such as Friedman's TREE(3) .

Anyway, it is big enough to play the role of "infinite number" in what follows.

Now, start with Robinson's arithmetics $Q$ and "beef it up" so that it contains all the recursive definitions necessary to talk about $g_{64}$ (for instance, all equations to define upper arrow notation).

As a tribute to Graham, let us call this theory GRAHAM.

Define T as GRAHAM + $ \forall n, n < g_{64}$

Clearly, T is classically inconsistent. But: just like Parikh's feasible arithmetics, there are, as far as I see, no short proofs of its inconsistency without appealing to induction. Now the question:

assuming a fixed proof system (say Gentzen), can we give a measure of the shortest induction-free proof that T is not consistent?

NOTE: I have mentioned Parikh's aritmetics, because obviously T and Parikh system share some common features.

But in his case, he keeps some induction and augments arithmetics with an additional unary predicate expressing feasibility for which induction does not apply , whereas here there is no such predicate, but on the other hand there is no induction whatsoever.

$\endgroup$
11
  • 5
    $\begingroup$ As a practice try two simpler theories first, using the Paseman theory (all numbers are less than 7) and the Mannucci theory (less than 2401), and see how proof length grows. My guess is the lengths are super exponential and that it will be challenging to estimate this length for the Mannucci theory. Gerhard "Remember, Baby Steps At First" Paseman, 2020.07.11. $\endgroup$ Jul 11, 2020 at 19:46
  • 2
    $\begingroup$ LOL. Good take. Yes, Gerhard, but in Mannucci's theory (as I mentioned several years ago on MO) even 5 is inaccessible, why bothering with such a huge number ? I can barely count beyond 2. Anyway, jokes aside, good guess, but I need an exact gauge (I have something in mind..) $\endgroup$ Jul 11, 2020 at 19:49
  • $\begingroup$ @EmilJeřábek thanks! 1) would love if you (at your leisure ) expanded this comments into a full blown answer (looks like I have to do many nested cuts to make room for iterated tetartion.... ). 2) also, any useful ref you can think of is appreciated ( probably Pudlak has something along these lines) $\endgroup$ Jul 12, 2020 at 11:08
  • 1
    $\begingroup$ I will try to write it up, but I’m not sure when I will be able to get to it. $\endgroup$ Jul 12, 2020 at 18:53
  • 3
    $\begingroup$ As much as it is honorific to put someone's name to a concept, I don't know that I'd like someone to tie my name to an inconsistent system that I never studied. $\endgroup$ Jul 13, 2020 at 17:51

2 Answers 2

11
$\begingroup$

At the request of the OP, I’m writing a lengthy nonanswer showing that there are short proofs of inconsistency of similar theories where the “big number” is given by a term in the usual language of arithmetic $L_{PA}=\{0,S,+,\cdot\}$, possibly expanded by the exponential function. The argument does not work for languages including faster growing functions such as tetration, let alone the Ackermann function needed to succinctly represent the Graham number.

Let $|t|$ denote the size (= number of symbols) of a syntactic object $t$ (a term, a formula, etc.).

Theorem 1: For any closed $L_{PA}$-term $t$, there is a proof of $t\nless t$ in $Q$ (and therefore a proof of inconsistency in $Q+\forall x\,x<t$) with $O(|t|)$ lines, each of size $O(|t|)$.

Proof: We will use the fact that there are $Q$-definable cuts that interpret fragments of arithmetic such as $I\Delta_0$, see [1,§V.5(c)]. Specifically, there exists a formula $I(x)$ such that $Q$ proves $$\begin{align} &I(0),\\ &\forall x\,\forall y\:\bigl(I(x)\land I(y)\to I(S(x))\land I(x+y)\land I(x\cdot y)\bigr),\\ &\forall x\,\forall y\:\bigl(I(x)\land y<x\to I(y)\bigr),\\ &\forall x\:\bigl(I(x)\to x\nless x\bigr). \end{align}$$ Let us fix $I$ and a $Q$-proof of the above. Then we prove $$I(t)$$ by (meta)induction on the complexity of a closed term $t$: if, say $t$ is $t_0+t_1$, we instantiate one of the formulas above to obtain $$I(t_0)\land I(t_1)\to I(t_0+t_1),$$ and we conclude $I(t_0+t_1)$ using the induction hypothesis and modus ponens. This argument involves $O(1)$ proof lines for each subterm of $t$, where each line has size $O(|t|)$. QED

In fact, the same argument shows more: since every $\Pi_1$ sentence $\psi$ provable in $I\Delta_0+\exp$ is interpretable on a cut in $Q$ by [1,Thm. V.5.26], we can take the cut $I$ above to satisfy $\psi$, and obtain

Theorem 2: Let $\theta(x)$ be a fixed $\Delta_0$ formula such that $I\Delta_0+\exp\vdash\forall x\,\theta(x)$. Then given a closed $L_{PA}$ term $t$, we can construct a $Q$-proof of $\theta(t)$ with $O(|t|)$ lines, each of size $O(|t|)$.

In order to adapt the argument to exponentiation, we need more work, as there are no definable cuts in $Q$ closed under exponentiation. Let $Q(\exp)$ be the theory in language $L_{\exp}=L_{PA}\cup\{x^y\}$ axiomatized by $Q$ and $$\begin{align} x^0&=1,\\ x^{S(y)}&=x^y\cdot x. \end{align}$$

Theorem 3: Let $\theta(x)$ be a fixed $\Delta_0$ formula such that $I\Delta_0+\exp\vdash\forall x\,\theta(x)$. Then given a closed $L_{\exp}$ term $t$, we can construct a $Q(\exp)$-proof of $\theta(t)$ with $O(|t|)$ lines, each of size $O(|t|)$.

In particular, we can construct a proof of inconsistency in $Q(\exp)+\forall x\,x<t$ with such parameters.

Proof: As above, we fix a definable cut $I_0(x)$ that, provably in $Q(\exp)$, is closed under $+$ and $\cdot$, and satisfies $\mathrm{PA}^-$ and $\forall x\,\bigl(I_0(x)\to\theta(x)\bigr)$. Moreover, we can make sure $Q(\exp)$ proves $$\begin{align} \forall x\,\forall y\,\forall z\:\bigl(I_0(x)\land I_0(y)\land I_0(z)\to x^{y+z}&=x^y\cdot x^z\bigr),\\ \forall x\,\forall y\,\forall z\:\bigl(I_0(x)\land I_0(y)\land I_0(z)\to\:\, x^{y\cdot z}&=(x^y)^z\bigr). \end{align}$$ We now define a sequence of shorter and shorter cuts by $$I_{k+1}(x)\iff I_k(x)\land\forall y\:\bigl(I_k(y)\to I_k(y^x)\bigr).$$ Using the properties of $I_0$, it is easy to construct by metainduction on $k$ $Q(\exp)$ proofs that $I_k$ is a cut closed under $+$ and $\cdot$, using $O(1)$ proof lines for each $I_k$, i.e., $O(k)$ lines in total to prove the properties for $I_0,\dots,I_k$. Each line has size $O(|I_k|)$.

As defined, $I_{k+1}$ involves two occurrences of $I_k$, hence $|I_k|=O(2^k)$. Pretend for the moment that we can rewrite the definition of $I_{k+1}$ so that it only refers to $I_k$ once. Then $|I_k|=O(k)$, hence the proof so far has $O(k)$ lines, each of size $O(k)$.

$\DeclareMathOperator\ed{ed}$For any closed term $t$, we define the exponentiation nesting depth $\ed(t)$ by $$\begin{align} \ed(0)&=0,\\ \ed(S(t))&=\ed(t),\\ \ed(t\circ u)&=\max\{\ed(t),\ed(u)\},\qquad\circ\in\{+,\cdot\},\\ \ed(t^u)&=\max\{\ed(t),1+\ed(u)\}. \end{align}$$ Then we construct $Q(\exp)$ proofs of $$I_{k-\ed(t)}(t)$$ by induction on the complexity of a closed term $t$ such that $\ed(t)\le k$, using the properties of $I_0,\dots,I_k$ above. We use $O(1)$ proof lines for each $t$ on top of the induction hypothesis, hence $O(|t|+k)$ lines in total, each of size $O(|t|+k)$. Choosing $k=\ed(t)\le|t|$, we obtain a proof of $$I_0(t),$$ and therefore of $\theta(t)$, with $O(|t|)$ lines, each of size $O(|t|)$.

It remains to show how to present the definition of $I_k$ so that it has size only $O(k)$. The basic idea is to use the equivalences $$\begin{align} \psi(x)\lor\psi(y)&\iff\exists z\:\bigl((z=x\lor z=y)\land\psi(z)\bigr),\\ \psi(x)\land\psi(y)&\iff\forall z\:\bigl((z=x\lor z=y)\to\psi(z)\bigr), \end{align}$$ however, the definition of $I_{k+1}$ involves both a positive and a negative occurrence of $I_k$, and these cannot be contracted directly. To fix this, we encompass both polarities in a single predicate $$J_k(x,a)\iff(a=0\land I_k(x))\lor(a\ne0\land\neg I_k(x)).$$ In order to make the notation manageable, let me write $$\def\?{\mathrel?}(\phi\?\psi_0:\psi_1)\iff\bigl((\phi\land\psi_0)\lor(\neg\phi\land\psi_1)\bigr).$$ We can express $J_{k+1}$ in terms of $J_k$ as $$\begin{align} J_{k+1}(x,a)&\iff\bigl[a=0\?\forall y\,(J_k(y,1)\lor J_k(y^x,0)):\exists z\,(J_k(z,0)\land J_k(z^x,1))\bigr]\\ &\iff\begin{aligned}[t] \bigl[a=0&\?\forall y\,\exists u,v\:\bigl((v=0\?u=y^x:u=y)\land J_k(u,v)\bigr)\\ &\,:\exists z\,(J_k(z,0)\land J_k(z^x,1))\bigr] \end{aligned}\\ &\iff\begin{aligned}[t] \forall y\,\exists z,u,v\:\bigl[a=0&\?(v=0\?u=y^x:u=y)\land J_k(u,v)\\ &\,:J_k(z,0)\land J_k(z^x,1)\bigr] \end{aligned}\\ &\iff\forall y\,\exists z,u,v\:\bigl[\bigl(a=0\to(v=0\?u=y^x:u=y)\bigr)\\\ &\qquad\qquad{}\land\forall u',v'\:\bigl[\bigl(a=0\?u'=u\land v'=v:(v'=0\?u'=z:u'=z^x)\bigr)\\ &\qquad\qquad\qquad\qquad\qquad\qquad\qquad\to J_k(u',v')\bigr]\bigr]. \end{align}$$ Notice that even though the last expression looks complicated, it contains only one occurrence of $J_k$ (even if we expand the abbreviations), hence we use it as the definition of $J_{k+1}$. This way, we define formulas $J_k$ of size $O(k)$, and we put $I_k(x)\iff J_k(x,0)$.

Let me point out that a general method how to eliminate such nested definitions of predicates is given by Avigad [2].

References:

[1] Petr Hájek, Pavel Pudlák: Metamathematics of first-order arithmetic, Springer, 1994, 2nd ed. 1998, 3rd ed. Cambridge Univ. Press 2017.

[2] Jeremy Avigad: Eliminating definitions and Skolem functions in first-order logic, ACM Transactions on Computational Logic 4 (2003), no. 3, pp. 402–415, doi: 10.1145/772062.772068.

$\endgroup$
9
  • 1
    $\begingroup$ You're welcome. (The missing part is really a boring technicality.) $\endgroup$ Jul 13, 2020 at 18:12
  • 1
    $\begingroup$ You are thinking about it the wrong way. You don’t get cuts closed under various functions by exploiting functions total in the theory, but by exploiting inner stuctural properties of the cuts. Functions of the ambient theory are basically irrelevant. I suggest you study §V.5(c) in Hájek–Pudlák in more detail to see how it works. But basically, recall that the very first step is that I need a cut satisfying $\forall x\,x\nless x$ (this is where the contradiction ultimately derives from). Now, this is obtained by taking an instance of induction for a $\Delta_0$ formula $\theta(x)$ that ... $\endgroup$ Jul 14, 2020 at 14:02
  • 1
    $\begingroup$ ... implies the property I want, and consider the definable set $I_0=\{u:\theta(0)\land\forall x\,(\theta(x)\to\theta(x+1))\to\theta(u)\}$. Pure logic proves that this is an inductive set, i.e., it is closed under $S$, but no matter how much functions I have in the ambient theory, there is no reason for $I_0$ to be closed under anything else than $S$. At this point you lost all the extra functions, and you are never going to get them back. There is a general method where you take a cut closed under $S$ and define inside it a cut closed under $+$, then inside that a cut closed under $\cdot$,... $\endgroup$ Jul 14, 2020 at 14:06
  • 1
    $\begingroup$ ... and you can carry on to get closure under the $\omega_k$ functions, but that’s it. You can’t get cuts closed under faster growing functions such as exponentiation. $\endgroup$ Jul 14, 2020 at 14:06
  • 1
    $\begingroup$ Let me add one more illustration. Let $T$ be an arbitrarily strong finitely axiomatized sequential theory, such as $I\Sigma_n$, or even NGB. Then there is a definable cut $I$ such that $T$ proves $I\Delta_0$ + cut-free consistency $CFCon(T)$ on $I$. Assuming $T$ is consistent, there is no definable cut $J$ inside $I$ that is $T$-provably closed under exponentiation (because then $T$ would interpret $I\Delta_0+\exp+CFCon(T)$, contradicting Gödel’s theorem, as $I\Delta_0+\exp$ proves the standard derivability conditions for cut-free provability). There is also no cut $J$ such that ... $\endgroup$ Jul 14, 2020 at 14:12
7
$\begingroup$

The length of the least proof of contradiction in $\mathsf{Graham}+\forall n (n<g_{64})$ should be inbetween $(\log_2^*(g_{64}))^{1/N}$ and $(\ln^*(g_{64}))^{N}$, where $\ln^*(x)=\min\{n\mid \log_2^n(x)<0\}$ and $N$ is some reasonable small integer (which could be figured out by a careful examination of the proof).

So let me first spell out what exactly I take as $\mathsf{Graham}$. Namely I'll assume that $\mathsf{Graham}$ is $\mathsf{Q}$ with additional function $x\uparrow^{y}z$ and axioms

  1. $x\uparrow^z0=x$
  2. $x\uparrow^0S(y)=x(x\uparrow^0y)$
  3. $x\uparrow^{S(z)}S(y)=x\uparrow^z(x\uparrow^{S(z)}y)$

Note that here $x\uparrow^{y}z$ should corresponds to $x\underbrace{\uparrow\ldots\uparrow}\limits_{y+1\;\text{arrows}}z+1$ rather than $x\underbrace{\uparrow\ldots\uparrow}\limits_{y\;\text{arrows}}z$. This change of notations is due to the fact that in $\mathsf{Q}$ we start naturals with $0$ rather than $1$.

Numbers $g_{n}$ thus would be denoted by the terms

  1. $g_1=\underline{3}\uparrow^{\underline{3}}\underline{2}$
  2. $g_{n+1}=\underline{3}\uparrow^{g_n}\underline{2}$

Proof of the upper bound essentially follows from Emil's answer. Using axioms of $\mathsf{Graham}$ by polynomial in $\log_2^*(g_{64})$ proof we would show that $g_{64}=\underline{3}\uparrow^{\underline{1}} \underline{b}$, for appropriate $b<\log_2^*(g_{64})$. Next,since $\uparrow^0$ is exponentiation operation we could apply Emil's analysis to show by a polynomial in $\log_2^*(g_{64})$ proof in $\mathsf{Graham}$ that $\lnot\underline{3}\uparrow^{\underline{1}} \underline{b}<\underline{3}\uparrow^{\underline{1}} \underline{b}$. This gives an upper bound for the length of the proof of contradiction.

I'll sketch how to give the lower bound using fulfillment sequences see [1].

I'll assume that we use the variant of first-order language with $\forall,\exists,\land,\lor$ and negations that could be only used with atomic formulas; for non-atomic $\varphi$ we denote as $\lnot\varphi$ the formula that is obtained from $\varphi$ by replacing $\forall$ with $\exists$, $\land$ with $\lor$, non-negated atomic $\psi$, with $\lnot \psi$ and vice versa.

Let $\tau=\langle \tau_i\mid i\le n\rangle$ be a sequence of non-decreasings subsets of some model $\mathfrak{M}_{\tau}$ of the language $L(\mathsf{Graham})$. We call $\tau$ of this form fulfulment sequences. We define fulfilment relation $\tau, i\Vdash \varphi$, for $i\le n$ and $L(\mathsf{Graham})$ formulas $\varphi$ with parameters from $\tau_i$:

  1. $\tau,i\Vdash \varphi\iff \mathfrak{M}\models \varphi$, if $\varphi$ is atomic or negation of atomic
  2. $\tau,i\Vdash \varphi\land \psi \iff \tau,i\Vdash \varphi\text{ and }\tau,i\Vdash \psi$
  3. $\tau,i\Vdash \varphi\lor \psi \iff \tau,i\Vdash \varphi\text{ or }\tau,i\Vdash \psi$
  4. $\tau,i\Vdash \forall x\;\varphi(x) \iff \text{for all $i\le j\le n$ and $a\in \tau_j$ we have }\tau,j\Vdash \varphi(a)$
  5. $\tau,i\Vdash \exists x\;\varphi(x) \iff \text{either $i=n$ or for some $a\in \tau_{i+1}$ we have }\tau,i+1\Vdash \varphi(a)$

Note that for $i\ge j$ we have $\tau, j\Vdash \varphi\Rightarrow \tau,i\Vdash \varphi$. And note that for a formula $\varphi$ of logical depth $l$ and $i\le \mathsf{len}(\tau)-l$ we couldn't have $\tau,i\Vdash \varphi$ and $\tau,i\Vdash \lnot \varphi$ at the same time.

Essential idea here is that a fulfillment sequence is a finite approximation for a first-order model.

Let us say that a fulfulment sequence $\tau$ supports set of formulas $\Gamma$ if the following holds:

  1. For any $\varphi(\vec{x})$ that is a subformula of formula from $\Gamma$, any $i\le \mathsf{len}(\tau)$, and $\vec{a}\in \tau_i$ we have $i\Vdash \varphi(\vec{a})\lor\lnot\varphi(\vec{a})$.
  2. We have $t(\vec{a})\in \tau_{i+1}$, for any term $t(\vec{x})$ appearing in $\Gamma$, any $i< \mathsf{len}(\tau)$, and $\vec{a}\in \tau_i$.

The following lemma connects finite deductions with fulfilement sequences:

Lemma 1. Suppose $\Gamma(x)$ is a sequent of logical depth $l$, $P$ is a deduction of $\Gamma$ in Tait calculus (with cuts) of the depth $k$, and $\tau$ is a fulfilment sequence that supports formulas appearing in $P$. Then for any $i$ between $k$ and $\mathsf{len}(\tau)-l$ and $\vec{a}\in\tau_i$ we have $\tau,i\Vdash \bigvee\Gamma(\vec{a})$

Proof. By induction on structure of $P$.

Suppose we have some finite sets of formulas $\Gamma\subseteq \Delta$ that are closed under subformulas. And suppose that we have some long enough fulfilment sequence $\tau$ that supports $\Gamma$. The key construction that we need is the construction of a shorter $\tau'$ such that $\tau'$ supports $\Delta$, $\mathfrak{M}_\tau=\mathfrak{M}_{\tau'}$, and for some function $f\colon \{0,..,\mathsf{len}(\tau')\}\to \{0,..,\mathsf{len}(\tau)\}$ we have

  1. $\tau'_i\subseteq \tau_{f(i)}$,
  2. $\tau',i\Vdash \varphi(\vec{a})\iff \tau,f(i)\Vdash \varphi(\vec{a})$, for any $\varphi(\vec{x})\in \Gamma$ and $\vec{a}\in \tau'_i$.

Let $s$ be the sum of lengthes of formulas from $\Delta$ and $k$ be the least number such that for any $\varphi\in \Delta$ and it's depth $k$ subformula $\psi$ we have $\psi\in \Gamma$. It would be always possible to construct $\tau'$ of the length $n$ as long as $\tau$ had the length $\ge P(n,s)\uparrow \uparrow k+1$, for some polynomial $P$. I'll skip technical details of construction of $\tau'$ from $\tau$.

Now our goal would be to construct long enough fulfulment sequence $\tau$ that would fulfill and support the set of all axioms of $T=\mathsf{Graham}+\forall x (x<g_{64})$. Let us construct finite sets of naturals $A_0=\{0\}$ and $$A_{i+1}=A_i\cup \{\max(0,a-1)\mid a\in A_i\}\cup \{\min(t(\vec{a}),g_{64})\mid \vec{a}\in \tau_i\text{ and }t(\vec{x}) \text{ occurs in axioms of $T$}\}.$$ Let $n$ be the last step so that $A_{n}\ne [0,g_{64}]$ and let $s$ be the least so that $[s,g_{64}]\subseteq A_n$. The model $\mathfrak{M}_\tau$ is the model with the domain $[0,s]$ that is obtained from $\mathbb{N}$ by collapsing all numbers $>s$ to $s$. We put $\mathsf{len}(\tau)=n$ and $\tau_i=(A_i\cap [0,s))\cup\{s\}$. It is easy to see that

  1. $\tau$ supports the set of axioms of $T$
  2. $\tau,i\Vdash \varphi$, for any $i\le \mathsf{len}(\tau)$ and axiom $\varphi$ of $T$
  3. $\mathsf{len}(\tau)>\log_2(\log_2(g_{64}))$.

Finally assume for a contradiction that $P$ is a proof of the sequent $\lnot \mathsf{Graham},\exists x \lnot(x<g_{64})$ of the length $k$, where $k\le(\log_2^*(g_{64}))^{1/N}$. Then from $\tau$ constructed above we construct $\tau'$ so that

  1. $\tau'$ supports the set of all formulas occuring in $P$
  2. $\tau',i\Vdash \varphi$, for any $i\le \mathsf{len}(\tau)$ and axiom $\varphi$ of $T$
  3. $\mathsf{len}(\tau')\ge k+l$, where $l$ is the logical depth of $\bigvee \lnot \mathsf{Graham}\lor \exists x \lnot(x<g_{64})$.

We get to a contradiction since from Lemma 1 should have that $\tau',k\Vdash \bigvee \lnot \mathsf{Graham}\lor \exists x \lnot(x<g_{64})$ but at the same time from 2. we have $\tau',k\Vdash \bigwedge \mathsf{Graham}\land \forall x (x<g_{64})$. And the latter is impossible since $k$ is too far away from the end of the sequence $\tau'$.

[1] J.E. Quinsey, "Some problems in logic: Applications of Kripke's Notion of Fulfilment", PhD thesis, St. Catherine's College, Oxford, 1980, https://arxiv.org/abs/1904.10540

$\endgroup$
2
  • 1
    $\begingroup$ Fedor, simply fantastic! Technically, you should have the green, but I have already given it to Emil. Truth is, you both deserve it. I am proud that there are folks like Emil and you here, not only knowledgeable, but willing to share. Follow up question: looks to me that the same methods would do for essentially any other beast as for instance TREE(n), mutatis mutandis (gotta add the recursive definitions, etc). Thoughts? $\endgroup$ Jul 14, 2020 at 13:33
  • 2
    $\begingroup$ @MircoA.Mannucci Yes the construction haven't relied on on any special properties of $g_{64}$. If you would add to $\mathsf{Q}$ axioms for recursive definitions of some other functions and instead of $g_{64}$ would take some other very large number based on this functions this would still work. $\endgroup$ Jul 14, 2020 at 13:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.