Understanding definition of conservative extension of a theory

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!

1 Answer

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.