In
mathematical logicMathematical logic is a subfield of mathematics with close connections to computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, a
theory (also called a
formal theory) is a set of
sentenceIn mathematical logic, a sentence of a predicate logic is a well formed formula with no free variables. A sentence is viewed by some as expressing a proposition. It makes an assertion, potentially concerning any structure of L. This assertion has a fixed truth value with respect to the structure...
s in a
formal languageA formal language is a set of words, i.e. finite strings of letters, symbols, or tokens. The set from which these letters are taken is called the alphabet over which the language is defined...
. For example, a
first-order theory is a set of
first-orderFirst-order logic is a formal logic used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, and predicate logic...
sentences. Many authors require that the theory be closed under
logical consequenceLogical consequence is a fundamental concept in logic. It is the relation that holds between a set of sentences and a sentence when the former "entails" the latter...
.
When defining theories for foundational purposes, additional care must be taken and 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.
In
mathematical logicMathematical logic is a subfield of mathematics with close connections to computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, a
theory (also called a
formal theory) is a set of
sentenceIn mathematical logic, a sentence of a predicate logic is a well formed formula with no free variables. A sentence is viewed by some as expressing a proposition. It makes an assertion, potentially concerning any structure of L. This assertion has a fixed truth value with respect to the structure...
s in a
formal languageA formal language is a set of words, i.e. finite strings of letters, symbols, or tokens. The set from which these letters are taken is called the alphabet over which the language is defined...
. For example, a
first-order theory is a set of
first-orderFirst-order logic is a formal logic used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, and predicate logic...
sentences. Many authors require that the theory be closed under
logical consequenceLogical consequence is a fundamental concept in logic. It is the relation that holds between a set of sentences and a sentence when the former "entails" the latter...
.
Theories expressed in formal language generally
When defining theories for foundational purposes, additional care must be taken and 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 which may be derived from them.
A theory is a conceptual class consisting of certain of these elementary statements. The elementary statements which belong to are called the
elementary theorems of and said to be
true. In this way, a theory is a way of designating a subset of which consists entirely of true statements.
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, and not true with respect to another. This is as in ordinary language, where statements such as "He is a terrible person." cannot be judged to be true or false without reference to some interpretation of who "He" is and for that matter what a "terrible person" is under this theory.
Subtheories and extensions
We can define a theory
1 as being a
subtheory of another or as being an
extension or
supertheory of another using the notation of set theory.
1 , and likewise
1
If every elementary theorem of
1 is also one of
Deductive theories
A theory is said to be a
deductive theory if is an inductive class. That is, that its content is based on some
formal deductive systemIn logic, a formal system consists of a formal language together with a deductive system which consists of...
and that some of its elementary statements are taken as axioms. In a deductive theory, any sentence which is a
logical consequenceLogical consequence is a fundamental concept in logic. It is the relation that holds between a set of sentences and a sentence when the former "entails" the latter...
of one or more of the axioms is also a sentence of that theory.
Consistency and completeness
A
syntactically consistent theory is a theory from which not every sentence in the underlying language can be proved (with respect to some
deductive systemA deductive system consists of the axioms and rules of inference that can be used to derive the theorems of the system....
which is usually clear from context). In a deductive system (such as first-order logic) that satisfies the
principle of explosionThe principle of explosion is the law of classical logic and a few other systems according to which "anything follows from a contradiction"; that is, once a contradiction has been asserted, any proposition can be inferred from it...
, this is equivalent to requiring that there is no sentence φ such that both φ and its negation can be proved 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 logicFirst-order logic is a formal logic used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, and predicate logic...
, the most important case, it follows from the
completeness theoremGödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. It was first proved by Kurt Gödel in 1929....
that the two meanings coincide. In other logics, such as
second-order logicIn logic and mathematics second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory....
, there are syntactically consistent theories that are not satisfiable, such as ω-inconsistent theories.
A
complete consistent theoryIn mathematical logic, a theory is complete if it is a maximal consistent set of sentences, i.e., if it is consistent, and none of its proper extensions is consistent...
(or just a
complete theory) is a consistent theory
T such that for every sentence φ in its language, either φ is provable from
T or
T {φ} 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 contensive subject matter when there is a many-to-one correspondence between certain elementary statements of the theory, and certain contensive statements related to the subject matter. If every elementary statement in the theory has a contensive correspondent it is called a
full interpretation, otherwise it is called a
partial interpretation.
Theories associated with a structure
Each
structureIn universal algebra and in model theory, a structure consists of a set along with a collection of finitary functions and relations which are defined on it....
has several associated theories. The
complete theory of a structure
A is the set of all
first-orderFirst-order logic is a formal logic used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, and predicate logic...
sentenceSentence or sentencing may refer to:* Sentence , a grammatical unit of language* Sentence , a formula with no free variables* Sentence , the smallest period in a musical composition...
s over the
signatureA signature is a handwritten depiction of someone's name, nickname or even a simple "X" that a person writes on documents as a proof of identity and intent. The writer of a signature is a signatory...
of
A which 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 σ-sentences 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 which they represent, σ' can be taken to be σ A.) The cardinality of σ' is thus the larger of the cardinality of σ and the cardinality of
A.
The
diagram of
A consists of all atomic or negated atomic σ'-sentences that are satisfied by
A and is denoted by diag
A. The
positive diagram of
A is the set of all atomic σ'-sentences which
A satisfies. It is denoted by diag
+A. The
elementary diagram of
A is the set eldiag
A 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 σ'.
Examples
One way to specify a theory is to define a set of
axiomIn traditional logic, an axiom or postulate is a proposition that is not proved or demonstrated but considered to be either self-evident, or subject to necessary decision...
s 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
structureIn universal algebra and in model theory, a structure consists of a set along with a collection of finitary functions and relations which are defined on it....
and then let the theory be the set of formulas that are satisfied by the structure. This is one method for producing complete theories, described below. Examples of theories of this sort include the sets of true sentences in the structures (
N, +, ×, 0, 1, =) and (
R, +, ×, 0, 1, =), where
N is the set of natural numbers and
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
decidableIn logic, the term decidable refers to the existence of an effective method for determining membership in a set of formulas. Logical systems such as propositional logic are decidable if membership in their set of logically valid formulas can be effectively determined...
; it is the theory of real closed fields.