Soundness for first order

59 Views Asked by At

While reading the book by Peter Smith I came across two different definitions of soundness, the general definition

A theory $T$ is sound iff its axioms are true (on the interpretation built into T’s language), and its proof system is truth-preserving, so all its theorems are true.

and for theory with a standard first-order theory $T$

$T \vdash \phi$ only if $T \models \phi$

where $T \models \phi$ means any way of (re) interpreting the non-logical vocabulary that makes all the axioms of $T$ true makes $\phi$ true.

The author shows $Q$ (Robinson arithmetic) cannot prove $\forall x (0+x=x)$, by showing a (re) interpretation $I$ that satisfies all axioms of $Q$ but where $\forall x (0+x=x)$ is false (and then invokes first-order soundness mentioned above). Next, the author introduces Peano arithmetic $P$ by adding axioms of type (for capturing induction) to $Q$

$$ (\phi(0) \wedge \forall x (\phi(x) \to \phi(Sx)) \to \forall x \phi(x) $$ where $S$ denotes the successor function. And shows that $\forall x (0+x=x)$ can be proved in $P$. The author also explains the (re) interpretation $I$ used earlier in $Q$ cannot be used here as $I$ had "numerals" which were successors of themself, but in $P$ one can prove $\forall x (x \not = Sx)$, and thus can rule out such (re) interpretations.

My doubt

Does $T \models \phi$ mean any way of (re) interpreting the non-logical vocabulary that makes all the theorems of $T$ true makes $\phi$ true? If not it is not clear to me why $I$ cannot be used to show $P$ cannot prove $\forall x (0+x=x)$, as $I$ violates $\forall x (x \not = Sx)$ which is a theorem not an axiom of $P$.