0
$\begingroup$

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.

$\endgroup$
10
  • $\begingroup$ Yes, you can. By the principal of explosion. $\endgroup$ Commented Mar 15, 2023 at 12:59
  • $\begingroup$ 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. $\endgroup$
    – Hypatius
    Commented Mar 15, 2023 at 13:14
  • $\begingroup$ If you are just adding one statement that is false, then by explosion you get that every statement is derivable. $\endgroup$ Commented Mar 15, 2023 at 13:19
  • $\begingroup$ 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. $\endgroup$
    – Hypatius
    Commented Mar 15, 2023 at 13:26
  • $\begingroup$ 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. $\endgroup$ Commented Mar 15, 2023 at 14:08

2 Answers 2

2
$\begingroup$

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$.

$\endgroup$
4
  • 1
    $\begingroup$ @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$ $\endgroup$
    – Bram28
    Commented Mar 15, 2023 at 14:22
  • 1
    $\begingroup$ @Hypatius I just rewrote my Answer too as my earlier Answer was clearly misinterpreting your question :P $\endgroup$
    – Bram28
    Commented Mar 15, 2023 at 14:32
  • 1
    $\begingroup$ 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. $\endgroup$
    – Hypatius
    Commented Mar 15, 2023 at 19:21
  • 1
    $\begingroup$ @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) $\endgroup$
    – Bram28
    Commented Mar 15, 2023 at 19:49
1
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .