In
mathematical logic
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal ...
, true arithmetic is the set of all true
first-order statements about the
arithmetic
Arithmetic () is an elementary part of mathematics that consists of the study of the properties of the traditional operations on numbers—addition, subtraction, multiplication, division, exponentiation, and extraction of roots. In the 19th c ...
of
natural number
In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country").
Numbers used for counting are called '' cardinal ...
s. This is the theory
associated with the
standard model
The Standard Model of particle physics is the theory describing three of the four known fundamental forces ( electromagnetic, weak and strong interactions - excluding gravity) in the universe and classifying all known elementary particles. I ...
of the
Peano axioms
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly ...
in the
language
Language is a structured system of communication. The structure of a language is its grammar and the free components are its vocabulary. Languages are the primary means by which humans communicate, and may be conveyed through a variety of ...
of the first-order Peano axioms.
True arithmetic is occasionally called Skolem arithmetic, though this term usually refers to the different theory of natural numbers with multiplication.
Definition
The
signature
A signature (; from la, signare, "to sign") is a Handwriting, handwritten (and often Stylization, stylized) depiction of someone's name, nickname, or even a simple "X" or other mark that a person writes on documents as a proof of identity and ...
of
Peano arithmetic
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly ...
includes the addition, multiplication, and successor function symbols, the equality and less-than relation symbols, and a constant symbol for 0. The (well-formed) formulas of the language of first-order arithmetic are built up from these symbols together with the logical symbols in the usual manner of
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quanti ...
.
The
structure is defined to be a model of Peano arithmetic as follows.
* The
domain of discourse
In the formal sciences, the domain of discourse, also called the universe of discourse, universal set, or simply universe, is the set of entities over which certain variables of interest in some formal treatment may range.
Overview
The dom ...
is the set
of natural numbers,
* The symbol 0 is interpreted as the number 0,
* The function symbols are interpreted as the usual arithmetical operations on
,
* The equality and less-than relation symbols are interpreted as the usual equality and order relation on
.
This structure is known as the
standard model or
intended interpretation of first-order arithmetic.
A
sentence in the language of first-order arithmetic is said to be true in
if it is true in the structure just defined. The notation
is used to indicate that the sentence
is true in
True arithmetic is defined to be the set of all sentences in the language of first-order arithmetic that are true in
, written . This set is, equivalently, the (complete) theory of the structure
.
Arithmetic undefinability
The central result on true arithmetic is the
undefinability theorem of
Alfred Tarski
Alfred Tarski (, born Alfred Teitelbaum;School of Mathematics and Statistics, University of St Andrews ''School of Mathematics and Statistics, University of St Andrews''. January 14, 1901 – October 26, 1983) was a Polish-American logician ...
(1936). It states that
the set is not arithmetically definable. This means that there is no formula
in the language of first-order arithmetic such that, for every sentence ''θ'' in this language,
:
Here
is the numeral of the canonical
Gödel number of the sentence ''θ''.
Post's theorem In computability theory Post's theorem, named after Emil Post, describes the connection between the arithmetical hierarchy and the Turing degrees.
Background
The statement of Post's theorem uses several concepts relating to definability and re ...
is a sharper version of the undefinability theorem that shows a relationship between the definability of and the
Turing degree
In computer science and mathematical logic the Turing degree (named after Alan Turing) or degree of unsolvability of a set of natural numbers measures the level of algorithmic unsolvability of the set.
Overview
The concept of Turing degree is fund ...
s, using the
arithmetical hierarchy
In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy (after mathematicians Stephen Cole Kleene and Andrzej Mostowski) classifies certain sets based on the complexity of formulas that define th ...
. For each natural number ''n'', let be the subset of consisting of only sentences that are
or lower in the arithmetical hierarchy. Post's theorem shows that, for each ''n'', is arithmetically definable, but only by a formula of complexity higher than
. Thus no single formula can define , because
:
but no single formula can define for arbitrarily large ''n''.
Computability properties
As discussed above, is not arithmetically definable, by Tarski's theorem. A corollary of Post's theorem establishes that the
Turing degree
In computer science and mathematical logic the Turing degree (named after Alan Turing) or degree of unsolvability of a set of natural numbers measures the level of algorithmic unsolvability of the set.
Overview
The concept of Turing degree is fund ...
of is 0
(ω), and so is not
decidable nor
recursively enumerable
In computability theory, a set ''S'' of natural numbers is called computably enumerable (c.e.), recursively enumerable (r.e.), semidecidable, partially decidable, listable, provable or Turing-recognizable if:
*There is an algorithm such that the ...
.
is closely related to the theory of the
recursively enumerable Turing degrees, in the signature of
partial order
In mathematics, especially order theory, a partially ordered set (also poset) formalizes and generalizes the intuitive concept of an ordering, sequencing, or arrangement of the elements of a set. A poset consists of a set together with a binary ...
s.
In particular, there are computable functions ''S'' and ''T'' such that:
* For each sentence ''φ'' in the signature of first-order arithmetic, ''φ'' is in if and only if ''S''(''φ'') is in .
* For each sentence ''ψ'' in the signature of partial orders, ''ψ'' is in if and only if ''T''(''ψ'') is in .
Model-theoretic properties
True arithmetic is an
unstable theory, and so has
models for each uncountable cardinal
. As there are
continuum many
type
Type may refer to:
Science and technology Computing
* Typing, producing text via a keyboard, typewriter, etc.
* Data type, collection of values used for computations.
* File type
* TYPE (DOS command), a command to display contents of a file.
* Ty ...
s over the empty set, true arithmetic also has
countable models. Since the theory is
complete
Complete may refer to:
Logic
* Completeness (logic)
* Completeness of a theory, the property of a theory that every formula in the theory's language or its negation is provable
Mathematics
* The completeness of the real numbers, which implies ...
, all of its models are
elementarily equivalent In model theory, a branch of mathematical logic, two structures ''M'' and ''N'' of the same signature ''σ'' are called elementarily equivalent if they satisfy the same first-order ''σ''-sentences.
If ''N'' is a substructure of ''M'', one ofte ...
.
True theory of second-order arithmetic
The true theory of second-order arithmetic consists of all the sentences in the language of
second-order arithmetic
In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics.
A precu ...
that are satisfied by the standard model of second-order arithmetic, whose first-order part is the structure
and whose second-order part consists of every subset of
.
The true theory of first-order arithmetic, , is a subset of the true theory of second-order arithmetic, and is definable in second-order arithmetic. However, the generalization of Post's theorem to the
analytical hierarchy
In mathematical logic and descriptive set theory, the analytical hierarchy is an extension of the arithmetical hierarchy. The analytical hierarchy of formulas includes formulas in the language of second-order arithmetic, which can have quantifiers ...
shows that the true theory of second-order arithmetic is not definable by any single formula in second-order arithmetic.
has shown that the true theory of second-order arithmetic is computably interpretable with the theory of the partial order of all
Turing degree
In computer science and mathematical logic the Turing degree (named after Alan Turing) or degree of unsolvability of a set of natural numbers measures the level of algorithmic unsolvability of the set.
Overview
The concept of Turing degree is fund ...
s, in the signature of partial orders, and ''vice versa''.
Notes
References
* .
* .
* .
*
*
Tarski, Alfred (1936), "Der Wahrheitsbegriff in den formalisierten Sprachen". An English translation "The Concept of Truth in Formalized Languages" appears in
External links
*
*
*{{MathWorld, title=Tarski's Theorem, urlname=TarskisTheorem
Model theory
Formal theories of arithmetic