Here are two theorems about formal proof systems I have attempted to prove, and for which I would like to check my understanding and clarify any missing details or loose ends.
Theorem 1. If a formal proof system is $\omega$-consistent and contains Peano arithmetic, then it is $\Sigma_2$-sound.
Proof. We shall assume that a formal proof system $F$ contains Peano arithmetic and prove the contrapositive. To that end, suppose $F$ contains Peano arithmetic but is $\Sigma_2$-unsound. Then there is some false sentence of the form $\exists x \forall y P(x,y)$, where $P(x,y)$ is rudimentary (expressible with only bounded quantifiers), that is provable in $F$. But it is in fact true that $\forall x \exists y \lnot P(x,y)$, and thus for every substitution of the variable $x$, $\exists y \lnot P(x,y)$ is provable in $F$, since $F$ contains Peano arithmetic and thus can prove every true $\Sigma_1$ sentence. Therefore if $Q(x)\equiv \exists y \lnot P(x,y)$, then all of $\exists x \lnot Q(x)$, $Q(1)$, $Q(2)$, $Q(3)$, ... are provable in $F$ and thus $F$ is $\omega$-inconsistent. Q.E.D.
Theorem 2. For any $k\in \mathbb N$, $\Sigma_k$-soundness is equivalent to $\Pi_{k+1}$-soundness.
Proof. It seems acknowledged as obvious that $\Pi_{k+1}$-soundness implies $\Sigma_k$-soundness, (use the $\forall$-introduction rule.) For the other implication, suppose a formal proof system $F$ is $\Sigma_k$-sound. Further suppose that some $\Pi_{k+1}$ sentence is provable in $F$. Then this sentence can be expressed as $\forall x P(x)$, where $P(x)$ is a $\Sigma_k$ formula with one free variable. Since $\forall x P(x)$ is provable, $P(x)$ is provable for every substitution of the variable $x$, by the $\forall$-elimination rule. But since $F$ is $\Sigma_k$-sound, $P(x)$ must be true for every substitution of the variable $x$ — in other words, $\forall x P(x)$. But this was an arbitrary provable $\Pi_{k+1}$ sentence that was shown to be true provided that the proof system $F$ is $\Sigma_k$-sound. Thus if $F$ is $\Sigma_k$-sound, then $F$ is also $\Pi_{k+1}$-sound. Q.E.D.
Questions:
- Is Peano arithmetic really necessary in theorem 1?
- Am I subtly assuming something without realizing it in theorem 2, (beyond basic rules for dealing with quantifiers)?