Sigma-1 soundness (source code)

= Sigma-1 soundness
{title2=$\Sigma_1\text{-soundness}$}

A theory has Sigma-1 soundness if every <Sigma-1 formula> that is a closed theorem is true in the standard natural-number structure. It is weaker than full <arithmetic soundness>. Under bounded completeness it is equivalent to <one-consistency>. The standard interpretation matters: an existential statement can have a witness in a nonstandard model while having no standard witness.