![Theory (mathematical logic)](https://www.english.nina.az/image-resize/1600/900/web/wikipedia.jpg)
In mathematical logic, a theory (also called a formal 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.
General theories (as expressed in formal language)
When defining theories for foundational purposes, additional care must be taken, as normal set-theoretic language may not be appropriate.
The construction of a theory begins by specifying a definite non-empty conceptual class , the elements of which are called statements. These initial statements are often called the primitive elements or elementary statements of the theory—to distinguish them from other statements that may be derived from them.
A theory is a conceptual class consisting of certain of these elementary statements. The elementary statements that belong to
are called the elementary theorems of
and are said to be true. In this way, a theory can be seen as a way of designating a subset of
that only contain statements that are true.
This general way of designating a theory stipulates that the truth of any of its elementary statements is not known without reference to . Thus the same elementary statement may be true with respect to one theory but false with respect to another. This is reminiscent of the case in ordinary language where statements such as "He is an honest person" cannot be judged true or false without interpreting who "he" is, and, for that matter, what an "honest person" is under this theory.
Subtheories and extensions
A theory is a subtheory of a theory
if
is a subset of
. If
is a subset of
then
is called an extension or a supertheory of
Deductive theories
A theory is said to be a deductive theory if is an inductive class, which is to say that its content is based on some formal deductive system and that some of its elementary statements are taken as axioms. In a deductive theory, any sentence that is a logical consequence of one or more of the axioms is also a sentence of that theory. More formally, if
is a Tarski-style consequence relation, then
is closed under
(and so each of its theorems is a logical consequence of its axioms) if and only if, for all sentences
in the language of the theory
, if
, then
; or, equivalently, if
is a finite subset of
(possibly the set of axioms of
in the case of finitely axiomatizable theories) and
, then
, and therefore
.
Consistency and completeness
A syntactically consistent theory is a theory from which not every sentence in the underlying language can be proven (with respect to some deductive system, which is usually clear from context). In a deductive system (such as first-order logic) that satisfies the principle of explosion, this is equivalent to requiring that there is no sentence φ such that both φ and its negation can be proven from the theory.
A satisfiable theory is a theory that has a model. This means there is a structure M that satisfies every sentence in the theory. Any satisfiable theory is syntactically consistent, because the structure satisfying the theory will satisfy exactly one of φ and the negation of φ, for each sentence φ.
A consistent theory is sometimes defined to be a syntactically consistent theory, and sometimes defined to be a satisfiable theory. For first-order logic, the most important case, it follows from the completeness theorem that the two meanings coincide. In other logics, such as second-order logic, there are syntactically consistent theories that are not satisfiable, such as ω-inconsistent theories.
A complete consistent theory (or just a complete theory) is a consistent theory such that for every sentence φ in its language, either φ is provable from
or
{φ} is inconsistent. For theories closed under logical consequence, this means that for every sentence φ, either φ or its negation is contained in the theory. An incomplete theory is a consistent theory that is not complete.
(see also ω-consistent theory for a stronger notion of consistency.)
Interpretation of a theory
An interpretation of a theory is the relationship between a theory and some subject matter when there is a many-to-one correspondence between certain elementary statements of the theory, and certain statements related to the subject matter. If every elementary statement in the theory has a correspondent it is called a full interpretation, otherwise it is called a partial interpretation.
Theories associated with a structure
Each structure has several associated theories. The complete theory of a structure A is the set of all first-order sentences over the signature of A that are satisfied by A. It is denoted by Th(A). More generally, the theory of K, a class of σ-structures, is the set of all first-order that are satisfied by all structures in K, and is denoted by Th(K). Clearly Th(A) = Th({A}). These notions can also be defined with respect to other logics.
For each σ-structure A, there are several associated theories in a larger signature σ' that extends σ by adding one new constant symbol for each element of the domain of A. (If the new constant symbols are identified with the elements of A that they represent, σ' can be taken to be σ A.) The cardinality of σ' is thus the larger of the cardinality of σ and the cardinality of A.[further explanation needed]
The diagram of A consists of all atomic or negated atomic σ'-sentences that are satisfied by A and is denoted by diagA. The positive diagram of A is the set of all atomic σ'-sentences that A satisfies. It is denoted by diag+A. The elementary diagram of A is the set eldiagA of all first-order σ'-sentences that are satisfied by A or, equivalently, the complete (first-order) theory of the natural expansion of A to the signature σ'.
First-order theories
A first-order theory is a set of sentences in a first-order formal language
.
Derivation in a first-order theory
There are many formal derivation ("proof") systems for first-order logic. These include Hilbert-style deductive systems, natural deduction, the sequent calculus, the tableaux method and resolution.
Syntactic consequence in a first-order theory
A formula A is a syntactic consequence of a first-order theory if there is a derivation of A using only formulas in
as non-logical axioms. Such a formula A is also called a theorem of
. The notation "
" indicates A is a theorem of
.
Interpretation of a first-order theory
An interpretation of a first-order theory provides a semantics for the formulas of the theory. An interpretation is said to satisfy a formula if the formula is true according to the interpretation. A model of a first-order theory is an interpretation in which every formula of
is satisfied.
First-order theories with identity
A first-order theory is a first-order theory with identity if
includes the identity relation symbol "=" and the reflexivity and substitution axiom schemes for this symbol.
Topics related to first-order theories
- Compactness theorem
- Consistent set
- Deduction theorem
- Enumeration theorem
- Lindenbaum's lemma
- Löwenheim–Skolem theorem
Examples
One way to specify a theory is to define a set of axioms in a particular language. The theory can be taken to include just those axioms, or their logical or provable consequences, as desired. Theories obtained this way include ZFC and Peano arithmetic.
A second way to specify a theory is to begin with a structure, and let the theory be the set of sentences that are satisfied by the structure. This is a method for producing complete theories through the semantic route, with examples including the set of true sentences under the structure (N, +, ×, 0, 1, =), where N is the set of natural numbers, and the set of true sentences under the structure (R, +, ×, 0, 1, =), where R is the set of real numbers. The first of these, called the theory of true arithmetic, cannot be written as the set of logical consequences of any enumerable set of axioms. The theory of (R, +, ×, 0, 1, =) was shown by Tarski to be decidable; it is the theory of real closed fields (see Decidability of first-order theories of the real numbers for more).
See also
- Axiomatic system
- Interpretability
- List of first-order theories
- Mathematical theory
References
- Haskell Curry, Foundations of Mathematical Logic, 2010.
- Weiss, William; D'Mello, Cherie (2015). "Fundamentals of Model Theory" (PDF). University of Toronto — Department of Mathematics.
- "Completeness (in logic) - Encyclopedia of Mathematics". www.encyclopediaofmath.org. Retrieved 2019-11-01.
- Haskell Curry (1963). Foundations of Mathematical Logic. Mcgraw Hill. Here: p.48
Further reading
- Hodges, Wilfrid (1997). A shorter model theory. Cambridge University Press. ISBN 0-521-58713-1.
In mathematical logic a theory also called a formal 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 ϕ T displaystyle phi in T of a deductively closed theory T displaystyle T is then called a theorem of the theory In many deductive systems there is usually a subset S T displaystyle Sigma subseteq T that is called the set of axioms of the theory T displaystyle T 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 General theories as expressed in formal language When defining theories for foundational purposes additional care must be taken as normal set theoretic language may not be appropriate The construction of a theory begins by specifying a definite non empty conceptual class E displaystyle mathcal E the elements of which are called statements These initial statements are often called the primitive elements or elementary statements of the theory to distinguish them from other statements that may be derived from them A theory T displaystyle mathcal T is a conceptual class consisting of certain of these elementary statements The elementary statements that belong to T displaystyle mathcal T are called the elementary theorems of T displaystyle mathcal T and are said to be true In this way a theory can be seen as a way of designating a subset of E displaystyle mathcal E that only contain statements that are true This general way of designating a theory stipulates that the truth of any of its elementary statements is not known without reference to T displaystyle mathcal T Thus the same elementary statement may be true with respect to one theory but false with respect to another This is reminiscent of the case in ordinary language where statements such as He is an honest person cannot be judged true or false without interpreting who he is and for that matter what an honest person is under this theory Subtheories and extensions A theory S displaystyle mathcal S is a subtheory of a theory T displaystyle mathcal T if S displaystyle mathcal S is a subset of T displaystyle mathcal T If T displaystyle mathcal T is a subset of S displaystyle mathcal S then S displaystyle mathcal S is called an extension or a supertheory of T displaystyle mathcal T Deductive theories A theory is said to be a deductive theory if T displaystyle mathcal T is an inductive class which is to say that its content is based on some formal deductive system and that some of its elementary statements are taken as axioms In a deductive theory any sentence that is a logical consequence of one or more of the axioms is also a sentence of that theory More formally if displaystyle vdash is a Tarski style consequence relation then T displaystyle mathcal T is closed under displaystyle vdash and so each of its theorems is a logical consequence of its axioms if and only if for all sentences ϕ displaystyle phi in the language of the theory T displaystyle mathcal T if T ϕ displaystyle mathcal T vdash phi then ϕ T displaystyle phi in mathcal T or equivalently if T displaystyle mathcal T is a finite subset of T displaystyle mathcal T possibly the set of axioms of T displaystyle mathcal T in the case of finitely axiomatizable theories and T ϕ displaystyle mathcal T vdash phi then ϕ T displaystyle phi in mathcal T and therefore ϕ T displaystyle phi in mathcal T Consistency and completeness A syntactically consistent theory is a theory from which not every sentence in the underlying language can be proven with respect to some deductive system which is usually clear from context In a deductive system such as first order logic that satisfies the principle of explosion this is equivalent to requiring that there is no sentence f such that both f and its negation can be proven from the theory A satisfiable theory is a theory that has a model This means there is a structure M that satisfies every sentence in the theory Any satisfiable theory is syntactically consistent because the structure satisfying the theory will satisfy exactly one of f and the negation of f for each sentence f A consistent theory is sometimes defined to be a syntactically consistent theory and sometimes defined to be a satisfiable theory For first order logic the most important case it follows from the completeness theorem that the two meanings coincide In other logics such as second order logic there are syntactically consistent theories that are not satisfiable such as w inconsistent theories A complete consistent theory or just a complete theory is a consistent theory T displaystyle mathcal T such that for every sentence f in its language either f is provable from T displaystyle mathcal T or T displaystyle mathcal T displaystyle cup f is inconsistent For theories closed under logical consequence this means that for every sentence f either f or its negation is contained in the theory An incomplete theory is a consistent theory that is not complete see also w consistent theory for a stronger notion of consistency Interpretation of a theory An interpretation of a theory is the relationship between a theory and some subject matter when there is a many to one correspondence between certain elementary statements of the theory and certain statements related to the subject matter If every elementary statement in the theory has a correspondent it is called a full interpretation otherwise it is called a partial interpretation Theories associated with a structure Each structure has several associated theories The complete theory of a structure A is the set of all first order sentences over the signature of A that are satisfied by A It is denoted by Th A More generally the theory of K a class of s structures is the set of all first order that are satisfied by all structures in K and is denoted by Th K Clearly Th A Th A These notions can also be defined with respect to other logics For each s structure A there are several associated theories in a larger signature s that extends s by adding one new constant symbol for each element of the domain of A If the new constant symbols are identified with the elements of A that they represent s can be taken to be s displaystyle cup A The cardinality of s is thus the larger of the cardinality of s and the cardinality of A further explanation needed The diagram of A consists of all atomic or negated atomic s sentences that are satisfied by A and is denoted by diagA The positive diagram of A is the set of all atomic s sentences that A satisfies It is denoted by diag A The elementary diagram of A is the set eldiagA of all first order s sentences that are satisfied by A or equivalently the complete first order theory of the natural expansion of A to the signature s First order theoriesA first order theory QS displaystyle mathcal QS is a set of sentences in a first order formal language Q displaystyle mathcal Q Derivation in a first order theory There are many formal derivation proof systems for first order logic These include Hilbert style deductive systems natural deduction the sequent calculus the tableaux method and resolution Syntactic consequence in a first order theory A formula A is a syntactic consequence of a first order theory QS displaystyle mathcal QS if there is a derivation of A using only formulas in QS displaystyle mathcal QS as non logical axioms Such a formula A is also called a theorem of QS displaystyle mathcal QS The notation QS A displaystyle mathcal QS vdash A indicates A is a theorem of QS displaystyle mathcal QS Interpretation of a first order theory An interpretation of a first order theory provides a semantics for the formulas of the theory An interpretation is said to satisfy a formula if the formula is true according to the interpretation A model of a first order theory QS displaystyle mathcal QS is an interpretation in which every formula of QS displaystyle mathcal QS is satisfied First order theories with identity A first order theory QS displaystyle mathcal QS is a first order theory with identity if QS displaystyle mathcal QS includes the identity relation symbol and the reflexivity and substitution axiom schemes for this symbol Topics related to first order theories Compactness theorem Consistent set Deduction theorem Enumeration theorem Lindenbaum s lemma Lowenheim Skolem theoremExamplesOne way to specify a theory is to define a set of axioms in a particular language The theory can be taken to include just those axioms or their logical or provable consequences as desired Theories obtained this way include ZFC and Peano arithmetic A second way to specify a theory is to begin with a structure and let the theory be the set of sentences that are satisfied by the structure This is a method for producing complete theories through the semantic route with examples including the set of true sentences under the structure N 0 1 where N is the set of natural numbers and the set of true sentences under the structure R 0 1 where R is the set of real numbers The first of these called the theory of true arithmetic cannot be written as the set of logical consequences of any enumerable set of axioms The theory of R 0 1 was shown by Tarski to be decidable it is the theory of real closed fields see Decidability of first order theories of the real numbers for more See alsoAxiomatic system Interpretability List of first order theories Mathematical theoryReferencesHaskell Curry Foundations of Mathematical Logic 2010 Weiss William D Mello Cherie 2015 Fundamentals of Model Theory PDF University of Toronto Department of Mathematics Completeness in logic Encyclopedia of Mathematics www encyclopediaofmath org Retrieved 2019 11 01 Haskell Curry 1963 Foundations of Mathematical Logic Mcgraw Hill Here p 48Further readingHodges Wilfrid 1997 A shorter model theory Cambridge University Press ISBN 0 521 58713 1