# 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
Commented Apr 30, 2016 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. Commented May 1, 2016 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
Commented May 1, 2016 at 14:38
• It is written that way in many textbooks... See e.g. van Dalen, Lemma 2.4.3 (g), page 35. Commented May 1, 2016 at 14:53
– user20153
Commented May 1, 2016 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/