Editing Peano axioms (section)

=== Undecidability and incompleteness ===

According to [[Gödel's incompleteness theorems]], the theory of '''PA''' (if consistent) is incomplete. Consequently, there are sentences of [[first-order logic]] (FOL) that are true in the standard model of '''PA''' but are not a consequence of the FOL axiomatization. Essential incompleteness already arises for theories with weaker axioms, such as [[Robinson arithmetic]]. 

Closely related to the above incompleteness result (via [[Gödel's completeness theorem]] for FOL) it follows that there is no [[algorithm]] for deciding whether a given FOL sentence is a consequence of a first-order axiomatization of Peano arithmetic or not. Hence, '''PA''' is an example of an [[Decidability_(logic)#Decidability_of_a_theory|undecidable theory]]. Undecidability arises already for the existential sentences of '''PA''', due to the negative answer to [[Hilbert's tenth problem]], whose proof implies that all [[computably enumerable]] sets are [[diophantine set]]s, and thus definable by existentially quantified formulas (with free variables) of '''PA'''. Formulas of '''PA''' with higher [[quantifier rank]] (more quantifier alternations) than existential formulas are more expressive, and define sets in the higher levels of the [[arithmetical hierarchy]].