The inconsistency of Graham Arithmetics plus $ forall n, n < g_{64}$

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{nmid 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 $xuparrow^{y}z$ and axioms

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

Note that here $xuparrow^{y}z$ should corresponds to $xunderbrace{uparrowldotsuparrow}limits_{y+1;text{arrows}}z+1$ rather than $xunderbrace{uparrowldotsuparrow}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 $lnotunderline{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 $lnotvarphi$ 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_imid ile nrangle$ 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, iVdash varphi$, for $ile n$ and $L(mathsf{Graham})$ formulas $varphi$ with parameters from $tau_i$:

1. $tau,iVdash varphiiff mathfrak{M}models varphi$, if $varphi$ is atomic or negation of atomic
2. $tau,iVdash varphiland psi iff tau,iVdash varphitext{ and }tau,iVdash psi$
3. $tau,iVdash varphilor psi iff tau,iVdash varphitext{ or }tau,iVdash psi$
4. $tau,iVdash forall x;varphi(x) iff text{for all $ile jle n$ and $ain tau_j$ we have }tau,jVdash varphi(a)$
5. $tau,iVdash exists x;varphi(x) iff text{either $i=n$ or for some $ain tau_{i+1}$ we have }tau,i+1Vdash varphi(a)$

Note that for $ige j$ we have $tau, jVdash varphiRightarrow tau,iVdash varphi$. And note that for a formula $varphi$ of logical depth $l$ and $ile mathsf{len}(tau)-l$ we couldn't have $tau,iVdash varphi$ and $tau,iVdash 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 $ile mathsf{len}(tau)$, and $vec{a}in tau_i$ we have $iVdash varphi(vec{a})lorlnotvarphi(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}intau_i$ we have $tau,iVdash bigveeGamma(vec{a})$

Proof. By induction on structure of $P$.

Suppose we have some finite sets of formulas $Gammasubseteq 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 $fcolon {0,..,mathsf{len}(tau')}to {0,..,mathsf{len}(tau)}$ we have

1. $tau'_isubseteq tau_{f(i)}$,
2. $tau',iVdash 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 $varphiin Delta$ and it's depth $k$ subformula $psi$ we have $psiin 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_icup {max(0,a-1)mid ain A_i}cup {min(t(vec{a}),g_{64})mid vec{a}in tau_itext{ 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_icap [0,s))cup{s}$. It is easy to see that

1. $tau$ supports the set of axioms of $T$
2. $tau,iVdash varphi$, for any $ile 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 $kle(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',iVdash varphi$, for any $ile 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',kVdash bigvee lnot mathsf{Graham}lor exists x lnot(x<g_{64})$ but at the same time from 2. we have $tau',kVdash 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

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 $tnless 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 $IDelta_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(xcdot y)bigr),\ &forall x,forall y:bigl(I(x)land y<xto I(y)bigr),\ &forall x:bigl(I(x)to xnless xbigr). 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 $IDelta_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 $IDelta_0+expvdashforall 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^ycdot x. end{align}$$

Theorem 3: Let $theta(x)$ be a fixed $Delta_0$ formula such that $IDelta_0+expvdashforall 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)totheta(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^ycdot x^zbigr),\ forall x,forall y,forall z:bigl(I_0(x)land I_0(y)land I_0(z)to:, x^{ycdot z}&=(x^y)^zbigr). end{align}$$ We now define a sequence of shorter and shorter cuts by $$I_{k+1}(x)iff I_k(x)landforall 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)$.

$DeclareMathOperatored{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(tcirc u)&=max{ed(t),ed(u)},qquadcircin{+,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)lorpsi(y)&iffexists z:bigl((z=xlor z=y)landpsi(z)bigr),\ psi(x)landpsi(y)&iffforall z:bigl((z=xlor z=y)topsi(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=0land I_k(x))lor(ane0landneg I_k(x)).$$ In order to make the notation manageable, let me write $$def?{mathrel?}(phi?psi_0:psi_1)iffbigl((philandpsi_0)lor(negphilandpsi_1)bigr).$$ We can express $J_{k+1}$ in terms of $J_k$ as $$begin{align} J_{k+1}(x,a)&iffbigl[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]\ &iffbegin{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}\ &iffbegin{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}\ &iffforall y,exists z,u,v:bigl[bigl(a=0to(v=0?u=y^x:u=y)bigr)\ &qquadqquad{}landforall u',v':bigl[bigl(a=0?u'=uland v'=v:(v'=0?u'=z:u'=z^x)bigr)\ &qquadqquadqquadqquadqquadqquadqquadto 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.