Extension by definitions

In mathematical logic, more specifically in the proof theory of first-order theories, extensions by definitions formalize the introduction of new symbols by means of a definition. For example, it is common in naive set theory to introduce a symbol ∅ {displaystyle emptyset } for the set which has no member. In the formal setting of first-order theories, this can be done by adding to the theory a new constant ∅ {displaystyle emptyset } and the new axiom ∀ x ( x ∉ ∅ ) {displaystyle forall x(x otin emptyset )} , meaning 'for all x, x is not a member of ∅ {displaystyle emptyset } '. It can then be proved that doing so adds essentially nothing to the old theory, as should be expected from a definition. More precisely, the new theory is a conservative extension of the old one. In mathematical logic, more specifically in the proof theory of first-order theories, extensions by definitions formalize the introduction of new symbols by means of a definition. For example, it is common in naive set theory to introduce a symbol ∅ {displaystyle emptyset } for the set which has no member. In the formal setting of first-order theories, this can be done by adding to the theory a new constant ∅ {displaystyle emptyset } and the new axiom ∀ x ( x ∉ ∅ ) {displaystyle forall x(x otin emptyset )} , meaning 'for all x, x is not a member of ∅ {displaystyle emptyset } '. It can then be proved that doing so adds essentially nothing to the old theory, as should be expected from a definition. More precisely, the new theory is a conservative extension of the old one. Let T {displaystyle T} be a first-order theory and ϕ ( x 1 , … , x n ) {displaystyle phi (x_{1},dots ,x_{n})} a formula of T {displaystyle T} such that x 1 {displaystyle x_{1}} , ..., x n {displaystyle x_{n}} are distinct and include the variables free in ϕ ( x 1 , … , x n ) {displaystyle phi (x_{1},dots ,x_{n})} . Form a new first-order theory T ′ {displaystyle T'} from T {displaystyle T} by adding a new n {displaystyle n} -ary relation symbol R {displaystyle R} , the logical axioms featuring the symbol R {displaystyle R} and the new axiom called the defining axiom of R {displaystyle R} . If ψ {displaystyle psi } is a formula of T ′ {displaystyle T'} , let ψ ∗ {displaystyle psi ^{ast }} be the formula of T {displaystyle T} obtained from ψ {displaystyle psi } by replacing any occurrence of R ( t 1 , … , t n ) {displaystyle R(t_{1},dots ,t_{n})} by ϕ ( t 1 , … , t n ) {displaystyle phi (t_{1},dots ,t_{n})} (changing the bound variables in ϕ {displaystyle phi } if necessary so that the variables occurring in the t i {displaystyle t_{i}} are not bound in ϕ ( t 1 , … , t n ) {displaystyle phi (t_{1},dots ,t_{n})} ). Then the following hold: The fact that T ′ {displaystyle T'} is a conservative extension of T {displaystyle T} shows that the defining axiom of R {displaystyle R} cannot be used to prove new theorems. The formula ψ ∗ {displaystyle psi ^{ast }} is called a translation of ψ {displaystyle psi } into T {displaystyle T} . Semantically, the formula ψ ∗ {displaystyle psi ^{ast }} has the same meaning as ψ {displaystyle psi } , but the defined symbol R {displaystyle R} has been eliminated. Let T {displaystyle T} be a first-order theory (with equality) and ϕ ( y , x 1 , … , x n ) {displaystyle phi (y,x_{1},dots ,x_{n})} a formula of T {displaystyle T} such that y {displaystyle y} , x 1 {displaystyle x_{1}} , ..., x n {displaystyle x_{n}} are distinct and include the variables free in ϕ ( y , x 1 , … , x n ) {displaystyle phi (y,x_{1},dots ,x_{n})} . Assume that we can prove in T {displaystyle T} , i.e. for all x 1 {displaystyle x_{1}} , ..., x n {displaystyle x_{n}} , there exists a unique y such that ϕ ( y , x 1 , … , x n ) {displaystyle phi (y,x_{1},dots ,x_{n})} . Form a new first-order theory T ′ {displaystyle T'} from T {displaystyle T} by adding a new n {displaystyle n} -ary function symbol f {displaystyle f} , the logical axioms featuring the symbol f {displaystyle f} and the new axiom called the defining axiom of f {displaystyle f} . Let ψ {displaystyle psi } be any formula of T ′ {displaystyle T'} . We define formula ψ ∗ {displaystyle psi ^{ast }} of T {displaystyle T} recursively as follows. If the new symbol f {displaystyle f} does not occur in ψ {displaystyle psi } , let ψ ∗ {displaystyle psi ^{ast }} be ψ {displaystyle psi } . Otherwise, choose an occurrence of f ( t 1 , … , t n ) {displaystyle f(t_{1},dots ,t_{n})} in ψ {displaystyle psi } such that f {displaystyle f} does not occur in the terms t i {displaystyle t_{i}} , and let χ {displaystyle chi } be obtained from ψ {displaystyle psi } by replacing that occurrence by a new variable z {displaystyle z} . Then since f {displaystyle f} occurs in χ {displaystyle chi } one less time than in ψ {displaystyle psi } , the formula χ ∗ {displaystyle chi ^{ast }} has already been defined, and we let ψ ∗ {displaystyle psi ^{ast }} be