# Suppose A is a set of premises of an argument and B the conclusion of that argument. Prove that if A U {¬B} ⊢ ⊥, then A ⊢ B

Suppose A is a set of premises of an argument and B the conclusion of that argument. Prove that if A U {¬B} ⊢ ⊥, then A ⊢ B. (Use Fitch)

I have no idea where to start, can someone help?

• The operator symbol you use for A (op) B does not render on my Android cellphone. Can you rewrite? Second, $\cup$ is not a logical symbol. Do you mean $A\land\not B$? – user20153 Apr 30 '16 at 21:19
• @mobileink - A is a set of premises (but to use a different type of symbols - like Γ - would be better...); thus Γ U {¬B} is correct: it means the "enlarged" set of premises "made of" all the formulae in Γ plus ¬B. – Mauro ALLEGRANZA May 1 '16 at 8:07
• @MauroALLEGRANZA: understood, my nitpicky point is that FOL is not set theory. $\Gamma, A\vdash B$ is not necessarily synonymous with $\Gamma\cup A\vdash B$. (Sorry I can't get Latex markup to work.) – user20153 May 1 '16 at 14:38
• It is written that way in many textbooks... See e.g. van Dalen, Lemma 2.4.3 (g), page 35. – Mauro ALLEGRANZA May 1 '16 at 14:53
• OP: is your question about how Fitch style proofs work? – user20153 May 1 '16 at 21:13

Assume A U {¬B} ⊢ ⊥

Now we need to show that A ⊢ B:

Assume ¬B, get a contradiction from premise A and from A U {¬B} ⊢ ⊥, and then conclude B. (You should fill here the natural deduction steps.) That's it.

I agree with Eliran H's answer.

Here are specific steps using a Fitch-style proof checker without assuming "¬B".

The proof uses disjunction introduction (∨I), conditional elimination (→E), explosion (X) and conditional introduction (→I). Further information on these rules may be found in forall x: Calgary Remix. References

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/