Definitional Extensions and Interpretations

Definitional Extensions

Let %$T$% be a theory in a in a language (set of constant, predicate, and function symbols) %$\mathcal{L}$%. Let %$T^+$% be a theory in a language %$\mathcal{L}^+$% such that %$\mathcal{L}\subseteq\mathcal{L}^+$% and let %$\mathcal{E}$% be %$\mathcal{L}^{+}-\mathcal{L}$%. We call %$\mathcal{E}$% the set of new symbols.

• Definition. %$T^+$% is a definitional extension of %$T$% if there is a set of sentences %$A$% such that
  • %$T^+$% is the closure of %$T\cup A$% under logical consequence.
  • Each new constant, predicate, or function symbol occurs in exactly one one sentence in %$A$%.
  • If %$c$% is a new constant symbol, then there is a formula %$\phi (x)$% with one free variable, %$x$%, in the language %$\mathcal{L}$% such that
    • %$(\exists x)(\phi (x)\land (\forall y)(\phi (y)\rightarrow y=x))$% is a theorem of %$T$%. (That is, %$T$% proves that there is exactly one %$x$% such that %$\phi (x)$%.)
    • The sentence %$(\forall x)(x=c\leftrightarrow\phi (x))$% is in %$A$%.
  • If %$P$% is a new %$n$%-ary relation symbol, then there is a formula %$\phi (x_{1},\ldots ,x_{n})$%, with free variables among %$x_{1},\ldots ,x_{n}$% , in the language %$\mathcal{L}$% such that
    • The sentence %$(\forall x_{1})\cdots (\forall x_{n})(P(x_{1},\ldots ,x_{n})\leftrightarrow \phi (x_{1},\ldots ,x_{n}))$% is in %$A$%.
  • If %$f$% is a new %$n$%-ary function symbol, then there is a formula %$\phi (x_{1},\ldots ,x_{n},y)$%, with free variables among %$x_{1},\ldots ,x_{n},y$% , in the language %$\mathcal{L}$% such that
    • %$(\forall x_{1})\cdots (\forall x_{n})(\exists y)(\phi (x_{1},\ldots ,x_{n},y)\land (\forall z)(\phi (x_{1},\ldots ,x_{n},z)\rightarrow z=y))$% is a theorem of %$T$%. (That is, %$T$% proves that %$\phi (x_{1},\ldots ,x_{n},y)$% defines an %$n$%-placed function.)
    • The sentence %$(\forall x_{1})\cdots (\forall x_{n})(\forall y)(y=f(x_{1},\ldots ,x_{n})\leftrightarrow\phi (x_{1},\ldots ,x_{n},y))$% is in %$A$%.

• Theorem. Suppose %$T^+$% is a definitional extension of %$T$%. If %$\mathfrak{A}$% is a model of %$T$%, then there is exactly one expansion of %$\mathfrak{A}$% to a model of %$T^+$%.

• Theorem. Suppose %$T^+$% is a definitional extension of %$T$%. There is a recursive relation that pairs every sentence of the language %$\mathcal{L}^+$% with a sentence of the language %$T$% in such a way that
  • If %$\phi ^+$% is paired with %$\phi$%, then it is a theorem of %$T^+$% that %$\phi ^{+}\leftrightarrow\phi$%.

Sketch of proof. Pair each sentence of %$\phi ^+$% with a sentence obtained by replacing the new symbols by their definitions.

• Corollary. If %$T^+$% is a definitional extension of %$T$%, then every theorem of %$T^+$% in which none of the new symbols occur is a theorem of %$T$%.

Example. The theory obtained from Peano arithmetic by adding the new symbol %$\le$% with the axiom %\[(\forall x)(\forall y)(x\le y\leftrightarrow (\exists z)y=x+z)\]% is a definitional extension of Peano arithmetic.

Interpretations

So far, we have only considered adding new symbols to a theory without changing the domain of discourse. That won't do when embedding arithmetic into set theory, for example.

• Definition. Let %$\phi$% be a formula with one free variable, and let %$\psi$% be an arbitrary formula. The formula %$\psi^{[\phi ]}$%, %$\psi$% bounded by %$\phi$%, is the formula obtained as follows: Let %$\phi ^*$% be a formula just like %$\phi$% except that the bound variable have been changed so that no variable that occurs in %$\psi$% occurs in %$\phi$%. Then %$\psi^{[\phi ]}$% is the formula obtained from %$\psi$% by recursively replacing every subformula of %$\psi$% of the form %$(\forall y)\theta$% by the formula %$(\forall y)(\phi ^{*}(y)\rightarrow\theta^{[\phi ]})$% and every subformula of %$\psi$% of the form %$(\exists y)\theta$% by the formula %$(\exists y)(\phi ^{*}(y)\land\theta^{[\phi ]})$%.

• Definition. Let %$T$% and %$T'$% be distinct theories in disjoint languages %$\mathcal{L}$% and %$\mathcal{L}'$%. The theory %$T'$% is interpretable in the theory %$T$% if there is a definitional extension %$T^+$% of %$T$% to the language %$\mathcal{L}\cup\mathcal{L}'$% and a formula %$\phi$% in the language %$\mathcal{L}$% with one free variable %$x$% such that
  • %$(\exists x)\phi$% is a theorem of %$T$%
  • A sentence %$\psi$% in the language %$\mathcal{L}'$% is a theorem of %$T'$% only if %$\psi^{[\phi ]}$% is a theorem of %$T^+$%.

Example. Peano arithmetic is interpretable in the language of set theory. One might show that, for example, by defining 0 to be %$\varnothing$%, %$S$% to be such that %$(\forall x)(\forall y)(y=Sx\leftrightarrow y=x\cup\{x\})$% (that is, take the ordinals to be the von Neumann ordinals, the ones Ernie learns in Benacerraf's article), and define + and %$\times$% in a suitable corresponding manner and let %$\phi$% be a formula that defines the set of finite von Neumann ordinals. (This isn't a course in set theory, so it probably won't be obvious, but the following will work: %$x$% is linearly ordered by %$\in$%, every subset of %$x$% has a least element in that order, every subset of %$x$% is a member of %$x$%, and every member %$y$% of %$x$% is either 0 or such that for some %$z$% in %$x$% %$y=Sz$%.) As Benacerraf in effect observed, the theorems of Peano arithmetic are true of the finite von Neumann ordinals when 0, %$S$%, and so forth are defined as I have indicated. To say that the theorems of Peano arithmetic are true of the finite von Neumann ordinals (as opposed to true of all the sets) just means that we take the quantifiers in those theorems to range only over the finite von Neumann ordinals, not over all sets. But that is just to say that %$psi$% is a theorem of Peano arithmetic if and only if %$\psi^{[\phi ]}$% is a theorem of the definitional extension just described.

• Theorem. Every definitional extension of a theory is interpretable in the theory.

Indication of proof. Let %$\phi (x)$% be %$x=x$%. The result is trivial, but it is convenient because it means that every theorem about interpretations is also a theorem about definitional extensions, which saves having to say many things twice.

• Theorem. Suppose %$T'$% is interpretable in %$T$% using a definitional extension %$T^+$% and a bounding formula %$\phi$%. There is a recursive relation that pairs every sentence of the language of %$T'$% with a sentence of the language of %$T$% in such a way that
  • If %$\psi '$% is paired with %$\psi$%, then it is a theorem of %$T^+$% that %$\psi\rightarrow\psi '^{[\phi ]}$%.
• Corollary. Suppose %$T'$% is interpretable in %$T$%. Then if %$T$% is decidable, so is %$T'$%.
• Corollary. Suppose %$T'$% is interpretable in %$T$%. Then if %$T$% is consistent, so is %$T'$%.
• Theorem. Suppose %$T'$% is interpretable in %$T$% and that %$T$% is consistent. If %$T'$% is essentially undecidable, so is %$T$%.

Thus, for example, since Peano arithmetic is essentially undecidable and interpretable in a standard axiomatization of set theory, it follows that a standard axiomatization of set theory is essentially undecidable.

Gödel's second incompleteness theorem for a theory %$T$% involves a particular sentence %$\mathrm{Con}_T$%, which says, using the particular number theoretic coding we introduced, that %$T$% is consistent. Thus, our method of extending the theorem to new theories via interpretations will involve the same sentence, which, since the new theory may make no explicit mention of numbers, may be a bit awkward.

• Theorem. Let %$T$% be a consistent axiomatizable theory. Suppose that a sufficiently strong theory %$P$% is interpretable in %$T$% using a definitional extension %$T^+$% and a bounding formula %$\phi$%, where "sufficiently strong" means sufficiently strong to prove Gödel's second incompleteness theorem in it. Then %$\mathrm{Con}_{T}^{[\phi ]}$% is not provable in %$T^+$%.

• Example. Since Peano arithmetic is interpretable in a standard axiomatizable theory of sets, if that theory of sets is consistent, then the number-theoretic sentence that asserts the consistency of that theory of sets, interpreted as a sentence about the von Neumann ordinals, is not provable in that theory. There will be more natural and direct ways to express that the theory is consistent in the theory, ones that use "Gödel sets" instead of Gödel numbers. It will turn out that standard such sentences expressing the consistency of the theory of sets will be provably equivalent to the number-theoretic sentence that asserts the consistency of that theory of sets, interpreted as a sentence about the von Neumann ordinals, and so less artificial versions of Gödel's second incompleteness theorem will follow from the one obtained using the interpretability result.

Several of the results on this page have proofs that are rather subtle. Details and related results may be found in Shoenfield67, 62–63, 134–136, 139–140, 233–234.

-- ShaughanLavine - 05 Nov 2006

• #Set DENSITY = 232