A (quantifier-free) is true in standard model of PA ==> PA |- A ??

Question

Is the following statement correct ?

A is a formula in PA without a quantifier and A is true for the standard model of arithmetic, i.e. the model |N = (N,+,×,0,1,<) This means: |N |= A

==>

A is proofable in PA. This means: PA |- A

Example: |N |= (x+y)^2 =x^2 + 2xy + y^2 ===> PA |- (x+y)^2 =x^2 + 2xy + y^2

If this statement is wrong, please give me a counterexample

cu cx

Answer 1

$$ \text{You gave a counterexample: true in N but not PA-provable.} \\ \text{But there are so many examples with: true in N and PA-provable: } \\ \text{I define: } \\ \text{I_N} = \{0,1,2, ...\} \text{ is the set of intuitive natural numbers} \\ \bar 0 \; and \; \bar 1 \text{ are the constants from PA} \\ \oplus and \circ \text{ are the functions in PA} \\ \text{when z is element from I_N, I define:} \\ \bar z := \bar 1 \oplus ... \oplus + \bar 1 \quad \text{n-times} \\ \text{I proofed the following statement "S1"} \\ \text{When n is element from I_N then we have:} \\ PA \vdash \forall x \forall y \; (\bar z = x \oplus y \quad .\rightarrow. \quad \bigvee_{i=0}^z (x=\bar i \land y=\overline{z-i}) \\ \text{I assume, that there are "many" of "similar" statements like S1.} \\ \text{Is it possible to formulate a statement "S", so that "S1" follows from "S" ?} \\ $$

cu cx

Answer 2

EDIT: It looks like I misread your question. There is an important difference between quantifier-free sentences, which is what my original answer (now below the fold) addressed, and quantifier-free formulas. Namely, when you speak of PA proving a formula with free variables (or of a structure satisfying such a formula), you're really asking about PA proving (or a structure satisfying) the universal closure of a quantifier-free formula: e.g. $$PA\vdash (x+y)^2=x^2+2x+y^2$$ is really shorthand for $$PA\vdash\forall x,y((x+y)^2=x^2+2x+y^2).$$

Such statements are no longer provable in PA in general. For example, it's essentially a consequence of the MRDP theorem that there is a Diophantine equation $t_1(x_1,..,x_n)=t_2(x_1,...,x_n)$ which has no solutions but which PA can't prove has no solutions; then the quantifier-free formula $$\neg(t_1(x_1,...,x_n)=t_2(x_1,...,x_n))$$ is true in $\mathbb{N}$ but not PA-provable.

---

What if we don't work with implicit universal quantifiers - that is, we restrict attention to sentences (= formulas with no free variables)? This was the original - incorrect - way I interpreted your question.

Here we get a positive result: PA proves every true $\Sigma_1$ sentence (that is, every sentence of the form $\exists x_1...\exists x_n\varphi(x_1,...,x_n)$, where $\varphi$ uses only bounded quantifiers). This fact ("$\Sigma_1$-completeness") about PA does not depend on PA being consistent - it is provable in PA itself, or indeed much less. The proof is tedious but not hard. Under the further assumption that PA is $\Sigma_1$-sound, this implies that the true $\Sigma_1$-sentences are exactly those which PA proves.

So this exactly delineates PA's power in terms of the coarse arithmetic hierarchy: PA proves exactly the correct $\Sigma_1$ sentences (under a reasonable assumption on PA), but there are correct $\Pi_1$ sentences which PA doesn't prove.