Infeasible inconsistency

[Anton Freund]

> Does anyone know an interesting example of a consistent formal system in
> which
> 1) There is a statement not-P with a proof of infeasible length
> 2) There are statements Q such that P?>Q has a feasible proof, Q does not
> have a feasible proof, and not-Q is not provable
>
> In other words, adding P as an axiom is not known to introduce a feasible
> inconsistency, but does allow feasible proofs of things which were either
> independent or previously had only infeasible proofs.

Write PH(n,N) for the following version of the Paris-Harrington statement:

"For each colouring of the n-tuples from {0,...,N-1} with (say) eight
colours, there is a large homogeneous set with more than n elements."

Take not-P to be the statement "there is an N with PH(n,N)" for some large
n. Then not-P (being Sigma_1) is provable in each fragment I\Sigma_k of
Peano arithmetic, but the proof is infeasible when n is much larger than
k:

Anton Freund: Proof lengths for instances of the Paris–Harrington principle
Annals of Pure and Applied Logic 168:7(2017) 1361-1382.

Also take not-Q to be the Paris-Harrington principle "for every n there is
an N with PH(n,N)". Then P->Q is immediate (as not-P is an instance of
not-Q). However, neither Q nor not-Q are provable in I\Sigma_k.

Note that the proof of not-P is feasible in full PA, as shown e.g. as an
auxiliary lemma in the following:

Anton Freund and Fedor Pakhomov: Short Proofs for Slow Consistency
Notre Dame Journal of Formal Logic 61:1(2020) 31-49.

Maybe this is not quite what you were looking for, as my statement Q is
false in the standard model.