# Undo a weakened statement in sequent calculus later in the inferences

I'm working on an answer to (b) of Mathematical Logic, Ebbinghaus et. al. 1984 p. 64

Consider the following inference: \frac{\begin{align}\Gamma \vdash A\\ \Gamma \vdash B\end{align}}{\Gamma \vdash A\land B} I show it is a valid inference, the question only allowing a restricted set of rules, using Weakening, Contraposition, and the $$\lor$$-Antecedent rules. But I'm stuck on the last part:

$$Γ\vdash A$$

$$Γ\vdash B$$

$$Γ \, \neg C \vdash A$$

$$Γ \, \neg C \vdash B$$

$$Γ \, \neg A \vdash C$$

$$Γ \, \neg B \vdash C$$

$$Γ \, (\neg A\lor \neg B) \vdash C$$

$$Γ \, \neg C \vdash \neg(\neg A\lor\neg B)$$

How would I get rid of the $$\neg C$$ I acquired from weakening? I have access to explosion, Contraposition, Modus ponens, and these (the last formula on each line is made true by the ones before it): I also have \frac{\begin{align}\Gamma \vdash \phi\\ \Gamma \phi \vdash \psi \end{align}}{\Gamma \vdash \psi}

• Is the list of rules you provided complete? For instance, can you use de Morgan's laws? They're not listed, but you use it in your last step. Aug 4, 2021 at 7:03
• @Taroccoesbrocco I wouldn't be surprised at all if Ebbinghaus defined $\wedge$ as a derived connective using $\vee$ and $\neg$. Aug 4, 2021 at 7:03
• Yep, $\land$ is not primitive, and the rules listed are all those available (except the quantification rules). The last line relies on defining $A\land B$ as $\neg(\neg A \lor \neg B)$ Aug 4, 2021 at 7:04

Follow the same proof using $$\neg C$$ in place of $$C$$, concluding $$\Gamma, \neg \neg C \vdash A \land B$$. Together with the original proof of $$\Gamma, \neg C \vdash A \land B$$, we can use the rule PC to eliminate $$C$$ entirely and conclude $$\Gamma \vdash A \land B$$.

$$C$$ seems to just be a placeholder which is needed to apply some of the rules. So there really isn't much that changes in the proof if we replace $$C$$ by something else.

• I fixed a mistake: the proof ends without $A \land B$, staying at $\neg(\neg A \lor \neg B)$, since it wasn't available. I don't think we can use this approach in that case, no? Aug 4, 2021 at 7:14
• @shintuku Are you saying you weren't able to prove $\Gamma, \neg C \vdash A \land B$? What is the exact definition of $A \land B$?
– S.C.
Aug 4, 2021 at 7:15
• In this case, it is $\neg ( \neg A \lor \neg B)$ (and this, without $\neg C$, is what we want). But I'm not seeing how we can apply PC in this case, given that we would only have, upon following your instructions $\Gamma C \vdash \neg(\neg A \lor \neg B)$. I may very well be misunderstanding your comment however Aug 4, 2021 at 7:17
• If $A \land B$ equals $\neg (\neg A \lor \neg B)$ by definition then it doesn't matter which one you have. In any case, my answer suffices to eliminate C. In PC, $\varphi$ would just have to be $\neg (\neg A \lor \neg B)$ (and $\psi$ would be $\neg C$).
– S.C.
Aug 4, 2021 at 7:19
• \frac{\begin{align}\Gamma C \vdash \neg ( \neg A \lor \neg B)\\ \Gamma \neg C \vdash \neg(\neg A \lor \neg B) \end{align}}{\Gamma \vdash \neg ( \neg A \lor \neg B)} If I understand you correctly, we would be getting the above, but supposing we begin using $\neg C$ instead of $C$, where would you get the second line in order to perform PC? Truly sorry if I'm misunderstanding you Aug 4, 2021 at 7:24