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.


  1. Is Peano arithmetic really necessary in theorem 1?
  2. Am I subtly assuming something without realizing it in theorem 2, (beyond basic rules for dealing with quantifiers)?

1 Answer 1


Very clearly done.

1) Robinson Arithmetic $Q$ is already $\Sigma_1$ complete, so it is enough for $F$ to contain $Q$, no?

2) Looks good as is!

  • 1
    $\begingroup$ Thanks for the answer about Robinson arithmetic! $\endgroup$ Mar 7, 2015 at 20:04

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .