5
$\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!

  • 1
    Almost, and yes. A [theory](http://en.wikipedia.org/wiki/Theory_%28mathematical_logic%29) is simply a set of sentences in a formal language. Here, though, that set is taken to contain all of its logical consequences, so in effect your understanding is correct.2012-02-16
  • 0
    @BrianM.Scott: Thanks! (1) Is a theory a set of all wff of a formal language, or a set of all axioms and theorems of a formal system? Is a theory a concept for a formal language or for a formal system? (2) Does a language extending another language means the first language is a superset of the second?2012-02-16
  • 0
    (2) Yes. (1) No, a theory in a language is simply a set of well-formed sentences (= formulas with no free variables) in that language.2012-02-16
  • 0
    @Brian: Thanks! (1) Is a theory a concept for a formal language only, or for a formal system? (2) is it correct that an element of a language called well-formed formula? (3) What elements of a language are not sentences? For example, Words? (4) Are well formed sentences and well formed formulas the same concept?2012-02-16
  • 2
    Hard to know what you mean by elements of a language. But for example, the logical and non-logical symbols are not sentences. Neither are the terms. A well-formed sentence has no free occurrences of variable symbols, a well-formed formula can and usually does.2012-02-16
  • 0
    @AndréNicolas: Thanks! I view a language as a set of finite length strings over some alphabet. So "an element of a language" is by viewing the language as a set. Hope this make my last comment clear.2012-02-16
  • 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

0

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.