2

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?

Improve this question
5
  • 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
  • 1
    @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
    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.
    – Mauro ALLEGRANZA
    Commented May 1, 2016 at 14:53
  • OP: is your question about how Fitch style proofs work?
    – user20153
    Commented May 1, 2016 at 21:13

2 Answers 2

Reset to default
1

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.

Improve this answer
0

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.

enter image description here

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/

Improve this answer

You must log in to answer this question.

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