7
$\begingroup$

I'm trying to write a question about natural dedcution, but I'm not sure what the best/easiest way is to write something similar to this at MSE:

enter image description here

In this post, I tried this:

    • $\lnot (p \lor \lnot p) \quad \quad \quad (H)$
      • $p \quad \quad \quad \quad \quad (H)$
      • $p \lor \lnot p \quad \quad \; \;(\lor \text{I} 2)$
      • $ \bot \quad \quad \quad \quad \;\;(\lnot \text{E}1,3)$
    • $\lnot p \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\; \; (\lnot \text{I}2 - 4)$
    • $p \lor \lnot p \;\;\;\;\;\;\;\;\; \;\;\;\;\;\,(\lor \text{I}5)$
    • $\bot \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\,(\lnot \text{E}1,6)$
  8. $p \lor \lnot p \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\,\;\;\;(\bot \text{E}1-7)$

I think that this solution is not that bad, but using all those \; to align thinks is a little tedious. Does somebody has another/better solution to write natural deduction proofs at MSE ?

$\endgroup$
0
1
$\begingroup$

I just do it all in ascii

(every line starts with 4 spaces)

1 |         ExVyRxy  Premisse 
2 | |____a           Variable
3 | | |__b  VyRby    Assumption
4 | | |     Rba      3 V-Elim
5 | | |     ExRxa    4 E-Intro 
. | | <--------------
6 | |       ExRxa    1, 3-5 E-Elim
. | <----------------   
7 |         VyExRxy  2-6 V- Intro

okay, it uses some wrong symbols but most logicians can follow it

$\endgroup$
2
  • $\begingroup$ You can copy-and-paste these: ∀ ∃. I got them in turn by copying-and-pasting from rendered MathJax output ($\forall, \exists$). $\endgroup$ – user856 Aug 7 '13 at 0:33
  • $\begingroup$ the problem then is that you lose bits of the layout (nice collums and so and i like my collums $\endgroup$ – Willemien Jan 7 '14 at 14:58

You must log in to answer this question.

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