Extension by new constant and function names

In mathematical logic, a theory can be extended with new constants or function names under certain conditions with assurance that the extension will introduce no contradiction. Extension by definitions is perhaps the best-known approach, but it requires unique existence of an object with the desired property. Addition of new names can also be done safely without uniqueness.

Suppose that a closed formula

\exists x_{1}\ldots \exists x_{m}\,\varphi (x_{1},\ldots ,x_{m})

is a theorem of a first-order theory $T$ . Let $T_{1}$ be a theory obtained from $T$ by extending its language with new constants

a_{1},\ldots ,a_{m}

and adding a new axiom

\varphi (a_{1},\ldots ,a_{m})

Then $T_{1}$ is a conservative extension of $T$ , which means that the theory $T_{1}$ has the same set of theorems in the original language (i.e., without constants $a_{i}$ ) as the theory $T$ .

Such a theory can also be conservatively extended by introducing a new functional symbol:^[1]

Suppose that a closed formula $\forall {\vec {x}}\,\exists y\,\!\,\varphi (y,{\vec {x}})$ is a theorem of a first-order theory $T$ , where we denote ${\vec {x}}:=(x_{1},\ldots ,x_{n})$ . Let $T_{1}$ be a theory obtained from $T$ by extending its language with a new functional symbol $f$ (of arity $n$ ) and adding a new axiom $\forall {\vec {x}}\,\varphi (f({\vec {x}}),{\vec {x}})$ . Then $T_{1}$ is a conservative extension of $T$ , i.e. the theories $T$ and $T_{1}$ prove the same theorems not involving the functional symbol $f$ ).

Shoenfield states the theorem in the form for a new function name, and constants are the same as functions of zero arguments. In formal systems that admit ordered tuples, extension by multiple constants as shown here can be accomplished by addition of a new constant tuple and the new constant names having the values of elements of the tuple.

References

^ Shoenfield, Joseph (1967). Mathematical Logic. Addison-Wesley. pp. 55–56.

Mathematical logic

General

Axiom
- list
Cardinality
First-order logic
Formal proof
Formal semantics
Foundations of mathematics
Information theory
Lemma
Logical consequence
Model
Theorem
Theory
Type theory

Theorems (list)
and paradoxes

Gödel's completeness and incompleteness theorems
Tarski's undefinability
Banach–Tarski paradox
Cantor's theorem, paradox and diagonal argument
Compactness
Halting problem
Lindström's
Löwenheim–Skolem
Russell's paradox

Logics

Traditional	Classical logic Logical truth Tautology Proposition Inference Logical equivalence Consistency Equiconsistency Argument Soundness Validity Syllogism Square of opposition Venn diagram
Propositional	Boolean algebra Boolean functions Logical connectives Propositional calculus Propositional formula Truth tables Many-valued logic 3 finite ∞
Predicate	First-order list Second-order Monadic Higher-order Fixed-point Free Quantifiers Predicate Monadic predicate calculus

Set theory

Set hereditary Class (Ur-)Element Ordinal number Extensionality Forcing Relation equivalence partition Set operations: intersection union complement Cartesian product power set identities
Types of sets	Countable Uncountable Empty Inhabited Singleton Finite Infinite Transitive Ultrafilter Recursive Fuzzy Universal Universe constructible Grothendieck Von Neumann
Maps and cardinality	Function/Map domain codomain image In/Sur/Bi-jection Schröder–Bernstein theorem Isomorphism Gödel numbering Enumeration Large cardinal inaccessible Aleph number Operation binary
Set theories	Zermelo–Fraenkel axiom of choice continuum hypothesis General Kripke–Platek Morse–Kelley Naive New Foundations Tarski–Grothendieck Von Neumann–Bernays–Gödel Ackermann Constructive

Formal systems (list),
language and syntax

Alphabet Arity Automata Axiom schema Expression ground Extension by definition conservative Relation Formation rule Grammar Formula atomic closed ground open Free/bound variable Language Metalanguage Logical connective ¬ ∨ ∧ → ↔ = Predicate functional variable propositional variable Proof Quantifier ∃ ! ∀ rank Sentence atomic spectrum Signature String Substitution Symbol function logical/constant non-logical variable Term Theory list
Example axiomatic systems (list)	of arithmetic: Peano second-order elementary function primitive recursive Robinson Skolem of the real numbers Tarski's axiomatization of Boolean algebras canonical minimal axioms of geometry: Euclidean: Elements Hilbert's Tarski's non-Euclidean Principia Mathematica