Pi-1 soundness (source code)

= Pi-1 soundness
{c}
{title2=$\Pi_1\text{-soundness}$}

<Pi-1 soundness> means that every closed <Pi-1 formula>[Pi-1] theorem is true in the standard <natural numbers>. <consistent first-order theory>[Consistency] plus <bounded completeness of an arithmetic theory>[bounded completeness] implies it, since a false universal bounded statement has a standard counterexample whose arithmetic verification is provable. It is weaker than full soundness and does not prevent a <consistent first-order theory>[consistent] <first-order theory>[arithmetic theory] from proving a false <Sigma-1 formula>[Sigma-1] sentence.