2
$\begingroup$

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): enter image description here I also have $$ \frac{\begin{align}\Gamma \vdash \phi\\ \Gamma \phi \vdash \psi \end{align}}{\Gamma \vdash \psi} $$

$\endgroup$
3
  • $\begingroup$ 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. $\endgroup$
    – Taroccoesbrocco
    Aug 4, 2021 at 7:03
  • $\begingroup$ @Taroccoesbrocco I wouldn't be surprised at all if Ebbinghaus defined $\wedge$ as a derived connective using $\vee$ and $\neg$. $\endgroup$
    – Z. A. K.
    Aug 4, 2021 at 7:03
  • $\begingroup$ 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)$ $\endgroup$
    – shintuku
    Aug 4, 2021 at 7:04

1 Answer 1

Reset to default
2
$\begingroup$

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.

$\endgroup$
9
  • $\begingroup$ 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? $\endgroup$
    – shintuku
    Aug 4, 2021 at 7:14
  • $\begingroup$ @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$? $\endgroup$
    – S.C.
    Aug 4, 2021 at 7:15
  • $\begingroup$ 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 $\endgroup$
    – shintuku
    Aug 4, 2021 at 7:17
  • $\begingroup$ 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$). $\endgroup$
    – S.C.
    Aug 4, 2021 at 7:19
  • $\begingroup$ $$ \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 $\endgroup$
    – shintuku
    Aug 4, 2021 at 7:24

You must log in to answer this question.

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