0

On Wikipedia it says:

"... the Gödel sentence of Peano arithmetic, is not provable nor disprovable in Peano arithmetic."

When talking about proving something in Peano Arithmetic, are we talking about just using the axioms of Peano Arithmetic (or maybe some model of them), or are we also allowed to use some other logic to make proofs? For example, in the first case, we would not be able to use modus ponens.

So in the first case, we could show that $succ(succ(0))$ is a natural number. But we could not show that $x = 0 \land y = succ(0) \implies y = succ(0)$ because ($\land$) and ($\implies$) just are not symbols of the language of peano arithmetic.

johannesCmayer
  • 1
  • The language of Peano arithmetic does include the ordinary symbols of first-order logic, and its axioms include the usual logical axioms. – MJD Oct 06 '21 at 16:42
  • 1
    When we talk about proving something in a theory, we are allowed to also use the basic inference rules of the logic of that theory as well. It's on this level that modus ponens lives. – Noah Schweber Oct 06 '21 at 17:45
  • 2
    @MJD Depending on the source the OP is reading that's not quite right: the "language" of a theory is often defined to be the set of non-logical symbols appearing in it, and the logical axioms are usually not included in the $\mathsf{PA}$ axioms. – Noah Schweber Oct 06 '21 at 17:46
  • 1
    In this context, we probably mean with Peano Arithmetic the corresponding first-order theory. In this case we have the resources of uderlying logic available: axioms + rules (e.g. Modus Ponens). – Mauro ALLEGRANZA Oct 11 '21 at 12:26
  • See First-order theory of arithmetic: "All of the Peano axioms except the ninth axiom (the induction axiom) are statements in first-order logic." Thus, $\land$ and $\to$ (see 2nd axioms) as well as the quantifiers "are symbols of the language of Peano arithmetic." – Mauro ALLEGRANZA Oct 12 '21 at 08:18

0 Answers0