Sigma-0 soundness (source code)

= Sigma-0 soundness
{c}
{title2=$\Sigma_0\text{-soundness}$}

A <first-order theory> is Sigma-0 <sound> when every <arithmetic> <bounded arithmetic sentence> it proves is true in the standard <natural numbers>. For a <first-order theory> proving every true <bounded arithmetic sentence>, this is equivalent to <first-order consistency>: a false bounded theorem would have a provable bounded <negation>, and an inconsistent <first-order theory> proves the false <bounded arithmetic sentence> $0=1$.