# 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. Commented 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$. Commented 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)$ Commented 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? Commented 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.
Commented 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 Commented 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.
Commented 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 Commented Aug 4, 2021 at 7:24