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](https://mathworld.wolfram.com/GrahamsNumber.html)): $g\_{64}$.


This number is truly [huge](https://plus.maths.org/content/too-big-write-not-too-big-graham), 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](https://www.jstor.org/stable/2269958?seq=1), 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.



The inconsistency of Graham Arithmetics plus $ \forall n, n < g_{64}$
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](https://projecteuclid.org/euclid.pl/1235421926), 3rd ed. Cambridge Univ. Press [2017](https://doi.org/10.1017/9781316717271).


[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](https://doi.org/10.1145/772062.772068).


