I am curious about the strongest methods we currently know of that can allow us to discover (arithmetical) unsoundness or nonstandardness in a foundational system $S$ that interprets at least ACA (such as Z). Detecting (arithmetical) inconsistency is 'easy'; $S$ is inconsistent iff $S$ proves (the translation of) $0=1$, so it suffices to look for such a proof. This is a $Σ_1$-quest. But detecting unsoundness (or nonstandardness) is harder. More precisely: $ \def\con{\text{Con}} $

What are the best $Σ_1$-methods currently known for detecting (arithmetical) unsoundness of a (computable) formal system $S$ that interprets ACA, where the "$Σ_1$" means that the method can be (ideally) implemented as a computer program whose termination indicates detection of unsoundness? Ideally, if the method yields a positive detection, then $S$ must be unsound. But I would also be satisfied if a positive detection only implies nonstandardness (i.e. $S$ has no ω-model).

For example, here are three possible methods (where "$⬜Q$" is the arithmetic sentence that captures "$S$ proves $Q$"):

  1. Search for a proof of $(¬Q∧⬜Q)$ over every arithmetical sentence $Q$. If such a proof is found, then $S$ cannot be $Σ_1$-sound, otherwise $S$ would prove $Q$ and hence a contradiction. Note that $PA' := PA+¬\con(PA)$ is consistent but proves $¬\con(PA')$, so $S$ can be consistent and yet prove $⬜{⊥}$. Indeed, this method finds that $PA'$ proves $(¬{⊥}∧⬜{⊥})$, so it successfully identifies it as $Σ_1$-unsound. But it fails to discover $Σ_1$-sound systems that are $Σ_2$-unsound.

  2. Search for a proof of $∃\overline{Q}(Σ_n(Q)∧¬T_n(Q)∧⬜Q)$, where $T_n$ is a truth-predicate over $S$ for $Σ_n$-sentences (i.e. $S$ proves $(Q⇔T_n(Q))$ for every $Σ_n$-sentence $Q$), over every (standard) natural $n$. Note that this method subsumes the previous one, because if $S$ proves $(¬A∧⬜A)$ for some arithmetical sentence $A$, then $A$ is a $Σ_k$-sentence for some natural $k$ and is coded by some numeral $c$, so $S$ proves $(Σ_k(A)∧¬T_k(A)∧⬜A)$ in which $A$ is represented by the term $c$, and hence also proves $∃\overline{Q}(Σ_n(Q)∧¬T_n(Q)∧⬜Q)$.

  3. Search for a proof of ( $S$ is arithmetically unsound ). Unlike the previous methods, which can be used for formal systems that interpret just PA, this method needs a bit more (which is why I stated ACA in my question). We can express ( $Q$ is a true arithmetical sentence ) as ( there is winning strategy for Verifier against Falsifier on $Q$ under game semantics ), where a strategy is a mapping from game states to a move for the current player in that state, and a winning strategy for Verifier is a strategy such that every game play in which Verifier follows the strategy ends in a win for Verifier. I believe that this method subsumes the previous ones, but it seems to detect not just unsoundness but also even systems with no ω-model. Specifically, all I know is that $S$ proves its own unsoundness then it cannot have an ω-model otherwise the witnessing strategy in an ω-model can be used to verify that $S$ proves a sentence false in $ω$.

But are there even stronger methods possible?

I also have some side questions:

(A) Is there a (computable) formal system that interprets ACA and is (arithmetically) unsound but is not detected by method 2 (i.e. fails to proves its own $Σ_n$-unsoundness for any standard numeral $n$).

(B) Is there a (computable) formal system that interprets ACA and is (arithmetically) sound but is detected by method 3 (i.e. proves its own unsoundness)?

I think the answer to both side questions is yes, but I do not know how to go about constructing such systems.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.