3
$\begingroup$

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.

$\endgroup$

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.