False Σ1-sound theories I was wondering how Σ1-sound theories in the language of first-order arithmetic can go wrong.  As far as I can tell, they cannot prove false claims about consistency, since such claims (e.g., that there is a proof of 0=1" from the axioms) are  equivalent (in weak theories of arithmetic) to Σ1 sentences.  Can they prove that a sequence is finite when it is really infinite?  It would be helpful to hear about some concrete Σ1-sound theories that prove blatantly false things.  Thanks!

Basically, soundness at one level of the arithmetical hierarchy doesn't prevent errors higher up.
For example, let $PA_n$ be PA + all true $\Pi_n$ sentences (incidentally, note that every true $\Sigma_{n+1}$ sentence is a theorem of $PA_n$). Then we can form the Godel-Rosser sentence for $PA_n$:

$(*)_n$: "For every proof of me from $PA_n$, there is a shorter disproof of me from $PA_n$."

The usual arguments show that $(*)_n$ is independent of $PA_n$ and true (in particular, $PA_n$ is fully sound and $PA_n$ can decide whether something is a valid $PA_n$ proof); so $PA_n+(*)_n$ is $\Pi_n$-complete and hence $\Sigma_n$-sound, but not fully sound.
As a cautionary tale, note that Godel's second incompleteness theorem breaks down when we try to push it beyond computably axiomatizable theories: there is an arithmetically definable theory which proves its own consistency, in fact it's just an unusual arithmetic description of PA itself! I believe this is folklore, but see e.g. here.

For a more non-constructive but simpler argument, note that $Thm(PA_n)$ has Turing degree ${\bf 0^{(n+1)}}$ but $Th(\mathbb{N})$ is not arithmetic, so we must have $Thm(PA_n)\subsetneq Th(\mathbb{N})$ for all $n$. Pick $\sigma\in Th(\mathbb{N})\setminus Thm(PA_n)$, and consider $PA_n+\neg\sigma$.
(I'm writing "$Thm(S)$" for the deductive closure of $S$ here.)
