The semantic tableaux version of the second incompleteness theorem extends almost to Robinson's arithmetic Q

Dan Willard

We will generalize the Second Incompleteness Theorem almost to the level of Robinson's System Q. We will prove there exists a P₁ sentence V, such that if a is any finite consistent extension of Q+V then a will be unable to prove its Semantic Tableaux consistency.