True arithmetic

Last updated

In mathematical logic, true arithmetic is the set of all true first-order statements about the arithmetic of natural numbers. [1] This is the theory associated with the standard model of the Peano axioms in the language 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.

Contents

Definition

The signature of Peano arithmetic 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.

The structure is defined to be a model of Peano arithmetic as follows.

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 Th(). This set is, equivalently, the (complete) theory of the structure . [2]

Arithmetic undefinability

The central result on true arithmetic is the undefinability theorem of Alfred Tarski (1936). It states that the set Th() 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 is a sharper version of the undefinability theorem that shows a relationship between the definability of Th() and the Turing degrees, using the arithmetical hierarchy. For each natural number n, let Thn() be the subset of Th() consisting of only sentences that are or lower in the arithmetical hierarchy. Post's theorem shows that, for each n, Thn() is arithmetically definable, but only by a formula of complexity higher than . Thus no single formula can define Th(), because

but no single formula can define Thn() for arbitrarily large n.

Computability properties

As discussed above, Th() is not arithmetically definable, by Tarski's theorem. A corollary of Post's theorem establishes that the Turing degree of Th() is 0(ω), and so Th() is not decidable nor recursively enumerable.

Th() is closely related to the theory Th() of the recursively enumerable Turing degrees, in the signature of partial orders. [3] In particular, there are computable functions S and T such that:

Model-theoretic properties

True arithmetic is an unstable theory, and so has models for each uncountable cardinal . As there are continuum many types over the empty set, true arithmetic also has countable models. Since the theory is complete, all of its models are elementarily equivalent.

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 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, Th(), is a subset of the true theory of second-order arithmetic, and Th() is definable in second-order arithmetic. However, the generalization of Post's theorem to the analytical hierarchy shows that the true theory of second-order arithmetic is not definable by any single formula in second-order arithmetic.

Simpson (1977) has shown that the true theory of second-order arithmetic is computably interpretable with the theory of the partial order of all Turing degrees, in the signature of partial orders, and vice versa.

Notes

  1. Boolos, Burgess & Jeffrey 2002 , p. 295
  2. see theories associated with a structure
  3. Shore 2011 , p. 184

Related Research Articles

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 quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.

In mathematical logic, model theory is the study of the relationship between formal theories, and their models. The aspects investigated include the number and size of models of a theory, the relationship of different models to each other, and their interaction with the formal language itself. In particular, model theorists also investigate the sets that can be defined in a model of a theory, and the relationship of such definable sets to each other. As a separate discipline, model theory goes back to Alfred Tarski, who first used the term "Theory of Models" in publication in 1954. Since the 1970s, the subject has been shaped decisively by Saharon Shelah's stability theory.

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 unchanged in a number of metamathematical investigations, including research into fundamental questions of whether number theory is consistent and complete.

In classical deductive logic, a consistent theory is one that does not lead to a logical contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent if it has a model, i.e., there exists an interpretation under which all formulas in the theory are true. This is the sense used in traditional Aristotelian logic, although in contemporary mathematical logic the term satisfiable is used instead. The syntactic definition states a theory is consistent if there is no formula such that both and its negation are elements of the set of consequences of . Let be a set of closed sentences and the set of closed sentences provable from under some formal deductive system. The set of axioms is consistent when for no formula .

In mathematical logic, the compactness theorem states that a set of first-order sentences has a model if and only if every finite subset of it has a model. This theorem is an important tool in model theory, as it provides a useful method for constructing models of any set of sentences that is finitely consistent.

<span class="mw-page-title-main">Arithmetical hierarchy</span> Hierarchy of complexity classes for formulas defining sets

In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them. Any set that receives a classification is called arithmetical. The arithmetical hierarchy was invented independently by Kleene (1943) and Mostowski (1946).

In mathematical logic, the Löwenheim–Skolem theorem is a theorem on the existence and cardinality of models, named after Leopold Löwenheim and Thoralf Skolem.

In mathematical logic, the diagonal lemma establishes the existence of self-referential sentences in certain formal theories of the natural numbers—specifically those theories that are strong enough to represent all computable functions. The sentences whose existence is secured by the diagonal lemma can then, in turn, be used to prove fundamental limitative results such as Gödel's incompleteness theorems and Tarski's undefinability theorem.

Tarski's undefinability theorem, stated and proved by Alfred Tarski in 1933, is an important limitative result in mathematical logic, the foundations of mathematics, and in formal semantics. Informally, the theorem states that "arithmetical truth cannot be defined in arithmetic".

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.

In computability theory, the Turing jump or Turing jump operator, named for Alan Turing, is an operation that assigns to each decision problem X a successively harder decision problem X with the property that X is not decidable by an oracle machine with an oracle for X.

Independence-friendly logic is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form and , where is a finite set of variables. The intended reading of is "there is a which is functionally independent from the variables in ". IF logic allows one to express more general patterns of dependence between variables than those which are implicit in first-order logic. This greater level of generality leads to an actual increase in expressive power; the set of IF sentences can characterize the same classes of structures as existential second-order logic.

In mathematical logic, an arithmetical set is a set of natural numbers that can be defined by a formula of first-order Peano arithmetic. The arithmetical sets are classified by the arithmetical hierarchy.

In mathematical logic, a theory is a set of sentences in a formal language. In most scenarios a deductive system is first understood from context, after which an element of a deductively closed theory is then called a theorem of the theory. In many deductive systems there is usually a subset that is called "the set of axioms" of the theory , in which case the deductive system is also called an "axiomatic system". By definition, every axiom is automatically a theorem. A first-order theory is a set of first-order sentences (theorems) recursively obtained by the inference rules of the system applied to the set of axioms.

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.

In model theory and related areas of mathematics, a type is an object that describes how a element or finite collection of elements in a mathematical structure might behave. More precisely, it is a set of first-order formulas in a language L with free variables x1, x2,..., xn that are true of a set of n-tuples of an L-structure . Depending on the context, types can be complete or partial and they may use a fixed set of constants, A, from the structure . The question of which types represent actual elements of leads to the ideas of saturated models and omitting types.

In mathematical logic, an ω-consistenttheory is a theory that is not only (syntactically) consistent, but also avoids proving certain infinite combinations of sentences that are intuitively contradictory. The name is due to Kurt Gödel, who introduced the concept in the course of proving the incompleteness theorem.

In logic, finite model theory, and computability theory, Trakhtenbrot's theorem states that the problem of validity in first-order logic on the class of all finite models is undecidable. In fact, the class of valid sentences over finite models is not recursively enumerable.

In the mathematical discipline of set theory, there are many ways of describing specific countable ordinals. The smallest ones can be usefully and non-circularly expressed in terms of their Cantor normal forms. Beyond that, many ordinals of relevance to proof theory still have computable ordinal notations. However, it is not possible to decide effectively whether a given putative ordinal notation is a notation or not ; various more-concrete ways of defining ordinals that definitely have notations are available.

In recursion theory, hyperarithmetic theory is a generalization of Turing computability. It has close connections with definability in second-order arithmetic and with weak systems of set theory such as Kripke–Platek set theory. It is an important tool in effective descriptive set theory.

References