6
$\begingroup$

From Wikipedia

In mathematical logic, a logical theory $T_2$ is a (proof theoretic) conservative extension of a theory $T_1$ if the language of $T_2$ extends the language of $T_1$; every theorem of $T_1$ is a theorem of $T_2$; and any theorem of $T_2$ which is in the language of $T_1$ is already a theorem of $T_1$.

Is a theory, as noted by $T_i$, defined as the set of theorems and axioms of a formal system?

Does a language extending another language means the first language is a superset of the second?

Thanks and regards!

  • 2
    There are several *kinds* of relevant strings, for example terms, formulas, special kinds of formulas such as sentences, strings of sentences, particularly when they are proofs. Strings of sentences are not usually considered part of the language.2012-02-16

1 Answers 1

1

Extensions by definitions are described clearly in Sec.II.15 of Kunnen's "The foundations of mathematics". Definition II.15.1 on p.149 assumes for two lexicons (of non-logical symbols, Definition II.5.2 on p.96) $\mathcal{L}$ and $\mathcal{L'}$ that $\mathcal{L} \subseteq \mathcal{L}'$. Borrowing the example given there, let $\mathcal{L} \triangleq \{ ``\in "\}$ and $\mathcal{L'} \triangleq \{ ``\in", ``\emptyset" \}$. The definition of "language" generated by a lexicon is the same for both $\mathcal{L}$ and $\mathcal{L}'$. So, the language associated to $\mathcal{L}'$ (the formulae) will contain the language associated to $\mathcal{L}$.

Consider a set of sentences $\Sigma$ over $\mathcal{L}$ and a set of sentences $\Sigma'$ over $\mathcal{L}'$ (a formula is a sentence iff no variable is free (Definition II.5.5 on p.98) and the formulae of a lecixon $\mathcal{L}$ are defined inductively (Definition II.5.3 on p.97) using the notion of well-formed expressions of a Polish lexicon (Definition II.4.1 on p.91)).

The set of sentences $\Sigma$ contains the (non-logical) axioms of a formal theory (the proof rules / axioms of the logic constitute the underlying formal system, see Leisenring's excellent book for the distinction between formal system and formal theory).

$\Sigma'$ is an "extension by definitions" of $\Sigma$ iff $\Sigma' = \Sigma \cup \Delta$, where $\Delta$ are extra axioms that have a specific form and define the extra non-logical symbols, i.e., the fresh lexicon symbols in $\mathcal{L'} \setminus \mathcal{L}$. So, the "extension" refers to the axioms, not the theorems.

We can then prove (Theorem II.15.2 on p.149) that: any formula of $\mathcal{L}$ that is provable from the "extended" axioms $\Sigma'$ (the proof may contain formulae of $\mathcal{L}'$) is also provable from the "original" axioms $\Sigma$, using only formulae of $\mathcal{L}$. The opposite holds too. So, what is a theorem and what not is not part of what we define as "extension by definition", but a consequence.