In most scenarios a deductive system is first understood from context, after which an element
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.
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
is a conceptual class consisting of certain of these elementary statements.
This general way of designating a theory stipulates that the truth of any of its elementary statements is not known without reference to
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.
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.
(and so each of its theorems is a logical consequence of its axioms) if and only if, for all sentences
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.
This means there is a structure M that satisfies every sentence in the theory.
For first-order logic, the most important case, it follows from the completeness theorem that the two meanings coincide.
For theories closed under logical consequence, this means that for every sentence φ, either φ or its negation is contained in the theory.
(see also ω-consistent theory for a stronger notion of consistency.)
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.
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).
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.
[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.
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 σ'.
is a set of sentences in a first-order formal language
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.
A formula A is a syntactic consequence of a first-order theory
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.
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.