0
$\begingroup$

I am wanting to show that $(A\cup B)-B\subseteq A$ by using Fitch Notation. I think it would be as follows. Would this be correct? I am unsure as to to label the assumption step and conditional introduction. $$\def\ftc#1#2{\quad\begin{array}{|l}#1\\\hline #2\end{array}}\ftc{}{\vdots\\\ftc{1.~(x\in A\lor x\in B)\land x\notin B\hspace{11ex}\textsf{Assumption}}{2.~(x\in A\lor x\in B)\hspace{20ex}\textsf{1, Simplification}\\3.~x\notin B\hspace{30.5ex}\textsf{1, Simplification}\\4.~x\in A\hspace{30.5ex}\textsf{2, 3, Disjunctive Sylogism}}\\5.~((x\in A\lor x\in B)\land x\notin B)\to x\in A\hspace{3.5ex}\textsf{1-4, Conditional Introduction}}$$

$\endgroup$
  • $\begingroup$ Yes, that all looks correct! $\endgroup$ – Bram28 May 31 '17 at 17:47
  • $\begingroup$ Is the assumption fine with the scope line without any preceding premises? That was one thing I was worried about. I apologize that it is a picture and not coded out. I would code it out, but those lines are hard to code. $\endgroup$ – W. G. May 31 '17 at 17:50
  • $\begingroup$ @Bram28 I appreciate you looking at it! $\endgroup$ – W. G. May 31 '17 at 17:52
  • $\begingroup$ Yes, you can start a proof with a subproof, that's fine. ... So you created this picture by hand, and not with a prover? In fact, Fitch systems typically only have INtroduction and Elimination rules, so do you have Disjunctive Syllogism available as a 1-step rule? $\endgroup$ – Bram28 May 31 '17 at 17:56
  • $\begingroup$ Yes, it is a pain. What is that? As for disjunctive syllogism as a one step rule, I just use this site en.wikipedia.org/wiki/List_of_rules_of_inference $\endgroup$ – W. G. May 31 '17 at 17:57
3
$\begingroup$

I coded it up in the Fitch prover I like to use:

enter image description here

I used variables $y$ and $z$ instead of $A$ and $B$, so this proves it for any sets $A$ and $B$, but otherwise it is exactly your proof (and, as you can see by the checkmarks, the system accepted the proof!). The $DS 2$ is Disjunctive Syllogism, proven elsewhere:

enter image description here

Please note though that different proof systems have different rules, so in a different system than the one I use here, the proof may look slightly different (e.g. not every system uses the explicit contradiction symbol $\bot$)

$\endgroup$
  • $\begingroup$ Whats the name of that prover? If its free I wouldn't mind downloading it myself. $\endgroup$ – user400188 Jun 1 '17 at 4:26
  • $\begingroup$ @user400188 It's aptly named 'Fitch', but it's not free. It comes with the commercial book and software package called 'Language, Proof, and Logic'. $\endgroup$ – Bram28 Jun 1 '17 at 16:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.