5
$\begingroup$

Let $HA$ denote the theory of Heyting Arithmetic, referring to the intuitionistic fragment of $PA$. Is there some infinite set of formulas $\Gamma$ such that both $HA \vdash \Gamma$ and $PA \vdash \Gamma$, yet the length of the shortest cut-free $HA$-proof of some formula $\phi \in \Gamma$ grows asymptotically faster than its shortest cut-free proof in $PA$?

In particular, are there sets of only $\Sigma_0$- or $\Sigma_1$-formulas such that this condition holds? Quantifier-free formulas can be ruled out, I think, since $HA$ decides equality on naturals and thus is equivalent to $PA$ on these formulas with only a multiplicative slowdown.

$\endgroup$

1 Answer 1

2
$\begingroup$

I'm not sure if this is exactly what you want, but there's a fairly short argument along those lines. Given a natural number $n$, you can produce by Gödel style diagonalisation a sentence $\varphi$ that says "$\varphi$ is not provable by a derivation of length less than $n$". I believe this ends up being $\Delta_0$. By the usual diagonal tricks $\varphi$ is provable in $\mathbf{HA}$, but it is also true, and so has no derivation shorter than $n$. Then $\varphi \vee \neg \varphi$ is also provable in $\mathbf{HA}$ by first proving $\varphi$ and then applying $\vee$-introduction. Moreover, in cut free intuitionistic sequent calculus that is the only possible way to derive $\varphi \vee \neg \varphi$. On the other hand, in $\mathbf{PA}$ $\varphi \vee \neg \varphi$ is simply an instance of excluded middle and so has a trivial proof. For example, in the formulation of classical sequent calculus $\mathbf{LK}$ on the wikipedia page this can be done in 4 steps using $(I)$, $(\vee R_1)$, $(\vee R_2)$, and finally the right hand contraction rule, $(CR)$.

You might worried about the length of the formula $\varphi$, since it increases at least linearly with $n$. In that case you can instead consider $\varphi$ stating "$\varphi$ is not provable by a derivation of length less than $F(n)$" where $F$ is any primitive recursive function. That can ensure the shortest possible proof grows faster than the length of $\varphi$. I think this would make $\varphi$ a $\Sigma_1$ sentence.

$\endgroup$
5
  • $\begingroup$ Thanks! I think one does need to invoke $\Sigma_1$ sentences: Let $\phi(n)$ be "$\phi(n)$ is not provable in less than $2^n$ steps", where exponentiation is only used externally as a product with $n$ factors. Then, of course, the shortest $HA$-proof of $ \phi(n) \vee \neg\phi(n) $ has at least length $2^n$. $\endgroup$
    – univalence
    Commented Mar 12, 2021 at 10:38
  • $\begingroup$ Did you mean to say "does not need to invoke"? In that case it looks like your proof works, modulo checking the details with the Gödel argument, which should be fine as far as I can remember. $\endgroup$
    – aws
    Commented Mar 12, 2021 at 15:58
  • $\begingroup$ Oh, yeah, of course. However, I'm not quite sure whether any of these $\phi(n)$ are $\Delta_0$ without adding exp - aren't there exponentially many derivations of a given length? At least they aren't uniformly so, I think $\endgroup$
    – univalence
    Commented Mar 12, 2021 at 17:16
  • $\begingroup$ Yes, you could be right about that. $\endgroup$
    – aws
    Commented Mar 12, 2021 at 17:56
  • $\begingroup$ Nevermind, we know about $n$ externally and thus can calculate an upper bound that can be expressed in $\phi(n)$, but the set of these $\phi(n)$ itself might not be $\Delta_0$ within the arithmetic. $\endgroup$
    – univalence
    Commented Mar 12, 2021 at 18:07

You must log in to answer this question.

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