How to ensure a clean conservative extension in general?

Question

Suppose we have a logic $L$ and we have conservative extension $L'$. So, every theorem of $L'$ that can be expressed in $L$ is also a theorem of $L$.

This does not guarantee that $L'$ is "clean". In the sense that it doesn't contain theorems that we normally consider to be false.

For instance if we start with PRA or a logic with $\Pi_2$ sentences and proof strength $I\Sigma_1$ then we can we can make a conservative extension of full first order logic (or even second order logic), if we restrict the induction such that we keep proof strength $I\Sigma_1$.

However, this does not require that the FOL extension contains no sentences we consider to be false. The starting logic can have a standard model, while the conservative extension doesn't.

My question is, are there any precise ways to define a conservative logical extension, such that we keep it "clean"? This must be in a syntactical way, because there is no guarantee that $L$ has a model.

To give my initial thoughts on my own question:

For the answer, you can't just look to the theorems of $L'$ in comparison to $L$. Instead we must look at how $L'$ is constructed, because only then we can ensure that it stays clean.

This leads to the question what we can do in a conservative extension, in case we don't know any properties of $L$ in advance. In concluded that there are basically two constructs:

• If $L \vdash \phi \Rightarrow L \vdash \psi $ then $L' \vdash \phi \rightarrow \psi$, if that can not be expressed by $L$. This can be the case if $L$ allows free variables which can not be explicitly quantified.

EDIT: Given the answer of Andreas Blass, I mean with $L \vdash \phi \Rightarrow L \vdash \psi $ that $\psi$ can be mechanical derived from $\phi$. A correct notation would be $L + \phi \vdash \psi$.

• $L'$ can introduced a new quantifier, which is first introduced as a new variables and later explicit quantification is allowed.

By using only above two concepts we ensure that the conservative extension stays clean.

Is there any prior research in this? Or any other thoughts?

The question is part of my interest in Hilbert's program. The clean conservative extension should then be combined with the $\omega$-rule.

Answer 1

The first of your two constructs doesn't seem to keep things clean in the sense that you described. Suppose, for example, that $L$ is primitive recursive arithmetic, formulated in a way that allows only $\Pi^0_1$ statements. Let $\phi$ be (a traditional $\Pi^0_1$ formalization of) Con(PA), and let $\psi$ be a blatant falsehood like $0=1$. The implication $L\vdash\phi\implies L\vdash\psi$ is true, since its antecedent is false; PRA doesn't prove Con(PA). And $\phi\to\psi$ cannot be expressed in $L$, since it's not a $\Pi^0_1$ statement. So your first construct would let you put $\phi\to\psi$ into $L'$. But $\phi\to\psi$ is false in the standard model of arithmetic, since PA is consistent. So $L'$ would not be clean.