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

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

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.

• Thank you for your feedback. I tried to proof my statement, but I could not do it. My idee: every term represent as a polynom. Please can you give me a link to the proof of my statement. cu cx – user508589 Jan 29 at 21:29
• @user508589 Looking at your question again, I misread it (the issue being "formula" versus "sentence" and the implicit universal quantifier when we talk about proving/satisfying the former). I've edited. – Noah Schweber Jan 29 at 22:35

$$\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