TITLE: Can meta-languages disagree over what an object language proves?
QUESTION [4 upvotes]: Suppose we have a language/theory $\mathcal{L}$ in First Order Logic, and we look at what it proves. Is it possible that there are two meta-languages/theories, say $\mathcal{L_1}$ and $\mathcal{L_2}$, that take $\mathcal{L}$ as an object language/theory (the symbols of $\mathcal{L}$ constitute the constants of $\mathcal{L_{1,2}}$) and they disagree over what $\mathcal{L}$ can prove?
For example, $\mathcal{L_1} \vdash (\mathcal{L} \vdash p )$ and $ \mathcal{L_2} \vdash (\mathcal{L} \vdash \neg p )$ 
or  $\mathcal{L_1} \vdash (\mathcal{L} \vdash p) $ and $\mathcal{L_2} \vdash (\mathcal{L} \not\vdash p )$ ?
I realize that $\vdash$ might mean different things in the above sentences, but I am confused, is my question well-defined and if so, is there any work on this problem that you know of?

REPLY [2 votes]: Yes, it is clearly possible - as in the comments, for example $A$ might prove $\lnot \text{Con}(\text{ZFC})$ and $B$ might prove $\text{Con}(\text{ZFC})$. 
But, in some sense, this is only kind of example. Assume that $A$ and $B$ are consistent theories each of which is strong enough to work with the same formalized provability predicate $\text{Pr}_C$ for some effective theory $C$, so $\text{Pr}_C$ is the same in the language of $A$ and the language of $B$. 
Also assume that  $A \vdash \text{Pr}_C(\phi)$ and $B \vdash \lnot \text{Pr}_C(\phi)$ for some sentence $\phi$ in the language of $C$. 
Then $A \cup B  \vdash \text{Pr}_C(\phi) \land \lnot \text{Pr}_C(\phi)$, so 
$A\cup B$ is inconsistent. This means that there is a finite subset $A'$ of $A$ and a finite subset $B'$ of $B$ so that $A' \cup B'$ is inconsistent, so $A' \vdash \lnot \bigwedge B'$.  Hence, if the situation above happens, there are particular axioms of $A$ that are incompatible with particular axioms of $B$. 
This means, in particular, that the situation will never happen with the usual hierarchy of foundational theories, because these are all compatible with each other. 
Now, continue with the assumptions in the second paragraph. Because $\psi \equiv \text{Pr}_C(\phi)$ is a $\Sigma^0_1$ statement, then if it is true then it is true in every model of arithmetic, even nonstandard models. This means that, if $\psi$ is true then the only way for $B \vdash \lnot \psi$ to happen is for $B$ to be inconsistent. We assumed otherwise, so $\psi$ is false. This means that, for the situation in the second paragraph to happen, $\phi$ is not provable in $C$. Thus $\psi$ is false in every $\omega$-model of arithmetic, and so $A$ has no $\omega$-models.  
That is exactly the kind of situation we get from the example in the first paragraph, where $\text{Con}(\text{ZFC})$ holds in every $\omega$-model and a theory that proves $\lnot \text{Con}(\text{ZFC})$ has no $\omega$-models.
{"set_name": "stack_exchange", "score": 4, "question_id": 2952475}