# Strongest tools to detect unsoundness

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.