Adding $\tfrac{}{\Gamma \varphi}$ (for a fixed non-correct $\Gamma \varphi$) to the rules of the sequent calculus, can one now derive every sequent?

One knows that the sequent calculus over the set of sequents $$\Gamma \varphi$$ is correct and complete, meaning that the derivable sequents are precisely the correct ones.

However, adding just one axiom $$\tfrac{}{\Gamma \varphi}$$ (where $$\Gamma \varphi$$ is not correct) to the rules of the sequent calculus, can one now derive every sequent?

To prove or disprove this, it might be important to know that I am talking about the specific sequent calculus introduced in "Mathematical Logic" by Ebbinghaus, Thomas and Flum.

• Yes, you can. By the principal of explosion. Commented Mar 15, 2023 at 12:59
• This would mean that one can start with $\Gamma \phi$ and by some clever use of inference rules from the sequent calculus arrive at $\Delta \psi$, where $\Delta \psi$ is an arbitrary sequent. Can anyone give me some hints? I suppose that by principle of explosion you mean the use of the contradiction rule or some variant of it. I have already tried to combine that and other rules for a while and have not yet been succesful. Commented Mar 15, 2023 at 13:14
• If you are just adding one statement that is false, then by explosion you get that every statement is derivable. Commented Mar 15, 2023 at 13:19
• Thank you Shinrin, but the sequent calculus I am talking about does not have a rule that allows one to do this in one step. It has to be some combination of rules. Commented Mar 15, 2023 at 13:26
• Note: Ebbinghaus' proof system (see page 58) has the Assumption rule: $\dfrac { }{ \Gamma \ \varphi}$, provided that $\varphi$ is a memeber of $\Gamma$. If you discard the proviso, the rule is unsound. Commented Mar 15, 2023 at 14:08

Not in general, no.

Consider adding the sequent $$\{ \} P$$ where $$P$$ is a specific logic statement that is not a contradiction.

Then all statements that you can derive (as a sequent $$\{ \} \phi$$) are going to be either tautologies, or statements that are logically implied by $$\phi$$... which means you cannot derive the sequent $$\{ \} \neg P$$

The only time that adding a specific sequent would allow you to infer all sequents is when the sequent you add is equivalent to a contradiction, e.g. if you add the sequent $$\{ \} P \land \neg P$$ for some specific $$P$$.

• @Hypatius OK, got it now. Sorry for slow understanding! :P Anyway, no, this would not allow you to derive any sequent. Take my example of adding $\{ A \} B$. This can get you $\{ \} A \to B$, but unless you can also get to $\{ \} \neg (A \to B)$, you can;t try and use explosion to get anything. Even more general, we could add sequent $\{ \} P$ where $P$ is a specific logic statement. Then all statements that tyou can derive are going to be either tautologies, or statements that are equivalent to $P$... which means you cannot get to $\neg P$ ... i.e. you can't derive the sequent $\{ \} \neg P$ Commented Mar 15, 2023 at 14:22
• @Hypatius I just rewrote my Answer too as my earlier Answer was clearly misinterpreting your question :P Commented Mar 15, 2023 at 14:32
• Hey Bram, thanks again for your answers. There is a problem with the reasoning however: Starting with let us say {}$\phi$, one could immediately derive {}$(\phi\lor\psi)$ using rule ($\lor$S) from Ebbinghaus, and $\phi$ need not be equivalent to $(\phi\lor\psi)$. One entails the other however, which gave me an idea to fix your proof. I was succesful and posted the (I believe) answer to my question. Commented Mar 15, 2023 at 19:21
• @Hypatius Ah yes, good point! What is true is that any statement that you can infer is logically implied by $\phi$. Put differently: you can infer any statement that is equivalent to $\phi$, or weaker than $\phi$ (which includes all the tautologies that you can infer using the original system, and anything 'in between'), but you can't derive anything not implied by $\phi$ itself (which includes, for example, statements that are strictly stronger than $\phi$, such as any contradiction) Commented Mar 15, 2023 at 19:49

The answer to my question is: not in general. Thanks to Bram28 for giving me an idea in his answer.

Assuming $$\Gamma \varphi$$ only contains sentences (!), one can proof the following by induction over the enlarged sequent calculus: If $$\Delta \psi$$ can be derived in the enlarged calculus, then for all interpretations ℑ: If (If ℑ$$\models \Gamma$$, then ℑ$$\models \varphi$$), then (If ℑ$$\models \Delta$$, then ℑ$$\models \psi$$). The proof is analogous to the one showing correctness of the sequent calculus. $$\Gamma \varphi$$ only containing sentences is needed to avoid problems with free variables while dealing with the rule ($$\exists$$A) (see Ebbinghaus for the rule).

Now we use a counterexample similarly to Bram28's approach: Take $$\Gamma=\emptyset$$ and a sentence $$\varphi$$ that is not valid (making the sequent $$\Gamma \varphi$$ not correct), but let it also be satisfiable. For example, use $$\varphi=\exists x \exists y \lnot x \equiv y$$ where $$x$$ and $$y$$ are different variables (i.e. "the universe contains at least two elements", which is not always true, but it can be).

If the sequent $$\Delta\psi=\emptyset\lnot\varphi$$ was derivable, the above result yields: For all interpretations ℑ: If (ℑ$$\models\varphi$$), then (ℑ$$\models\lnot\varphi$$), i.e. $$\varphi\models\lnot\varphi$$. This is false because $$\varphi$$ is satisfiable.