Is it possible to construct proof systems that look consistent for short proofs, but are actually inconsistent?

Question

What's the shortest axiom you can add to a system like ZFC to make it inconsistent such that the shortest proof of a contradiction has length n? Is the length of the axiom lower-bounded by Ω(n), or is it possible to do better?

Are there any known examples of systems which are inconsistent, but the length of the shortest proof of a contradiction is exponential in the length of the axioms?

Is there a standard terminology for systems that "look consistent" when only considering short proofs, but fail to be consistent for longer proofs?

Answer 1

Reproducing my comment as an answer on suggestion.

---

The classic example, due to the man himself, is a sentence $G_n$ which says (via the standard diagonalization trick)

I am not provable from $T$ in fewer than n symbols

where $T$ is some consistent, c.e., $\Sigma_1$-complete theory.

If $G_n$ were provable in $T$ by fewer than $n$ symbols, $T$ would be able to prove this, and hence refute $G_n$ and be inconsistent, so the sentence is true. But then, just by checking all proofs of length less than $n,$ $T$ will be able to prove $G_n$. So $G_n$ is provable, but the proof requires more than $n$ symbols. Thus, $T + \{\lnot G_n\}$ is an inconsistent system with no proof of inconsistency shorter than $n.$

How slowly the size of the shortest possible implementation of $G_n$ scales with $n$ is only limited by how much $T$ is capable of compressing $n$. Note that this is the only point at which the strength of $T$ (beyond $\Sigma_1$-completeness) becomes relevant.

Answer 2

Take the formula $p \to \neg \neg p$ in a Hilbert-style axiom system with only inference rule Modus Ponens and axioms

• $\varphi \to (\psi \to \varphi)$ (I1)
• $(\varphi\to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi))$ (I2)
• $\neg \varphi \to (\varphi \to \psi)$ (I3)
• $(\varphi \to \neg \varphi) \to \neg \varphi$ (I4)

Next, add in the ZF axioms and define

• $\xi:=(\neg \neg p \to p)$
• $\phi_0:=((\xi \to p) \to \neg \neg p)$
• $\phi_{n+1}:=((\phi_n \to \neg \neg p) \to p)$

Take a sufficiently large $n$ and add the axiom $\neg \phi_n$.

I honestly have no idea how to calculate how long it would take to prove a contradiction without allowing assumptions/Deduction Theorem, meta-theorems, or meta-axioms/lemmas. However, it’s clear that the number of symbols increases by only $10$ between each $\phi_n$ and $\phi_{n+1}$.