Timeline for Predicate Logic - Natural Deduction; Assumptions about exists-elimination
Current License: CC BY-SA 4.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 8, 2018 at 19:33 | vote | accept | Robert | ||
| Aug 8, 2018 at 14:54 | comment | added | Caleb Stanford | @RobertK You're welcome, and I hope the answer helps when you return. | |
| Aug 8, 2018 at 7:52 | comment | added | Robert | Sorry i have not been able to engage more in this post, i have not had the time to study further since i posted this question (busy at my summer job). This answer does seem to be the correct one; i will sit down tonight and try to solve this task and come back to mark this as accepted :-) Thanks for engaging in my problem, to both of you. @6005 and Thomas Klimpel. | |
| Aug 8, 2018 at 7:24 | comment | added | Thomas Klimpel | OK, now I see. You are right, sorry. Probably I was lead in the wrong direction by my comment "I believe your answer is not strictly wrong, but ..." on mcg256's answer (and your comment on Free Logic, which I used to justify an incorrect step in my "own imagined" proof). | |
| Aug 7, 2018 at 23:16 | comment | added | Caleb Stanford | @ThomasKlimpel I think we're on the same page about the definitions: I'm fine with the definition in the notes you linked. I am honestly just trying to figure out why you disagree that this is a valid natural deduction proof. Do you just disagree with the phrase "prove as a lemma"? If so, this should be perfectly compatible with natural deduction. Whether writing the proof out as a tree or as a sequence of lines, you simply deduce $S \lor \lnot S$ from no premises, then prove the conclusion from each of $S$ and $\lnot S$, and finish with $\lor$ elimination. | |
| Aug 7, 2018 at 20:19 | comment | added | Thomas Klimpel | The question basically used cs.uwaterloo.ca/~plragde/cs245old/02-propnd.pdf as reference for the proof system. It is a real "natural deduction" system. However, see my first comment, where I reformulated the message from page 13 to express my doubts whether a beginners course should use it. Since you are way beyond beginners level, take a look at cs.cmu.edu/~fp/courses/atp/handouts.html to learn the real meaning of "natural deduction" and "sequent calculus". Those strange meta-theorems and proof-terms are what is important to me, and they work too for the classical variant. | |
| Aug 7, 2018 at 19:20 | comment | added | Caleb Stanford | @ThomasKlimpel We will have to agree to disagree. Of course I am aware of the various formal meanings of these terms. I suppose you object to my claim that law of excluded middle can be proven in natural deduction. Well, there are intuitionistic and classical variants, but in introductory logic courses in the US, usually one includes double-negation-elimination and therefore classical inference. I don't know what you consider the "real meaning" but to me there are multiple possibilities, with the classical one being more likely. | |
| Aug 7, 2018 at 18:18 | comment | added | Thomas Klimpel | Both "natural deduction" and "sequent calculus" (and also "analytic tableau") have a certain core technical meaning beyond specific representations of the calculus. Your suggestion "Try first proving, as a lemma, the law of the excluded middle" seems to me to be incompatible with that core technical meaning. There are good reasons for authors to use some simpler less strict calculus for an introduction to logic. But even if they would name such a simplified calculus "natural deduction" or "sequent calculus", it would still not change the real meaning of those terms. | |
| Aug 7, 2018 at 15:49 | comment | added | Caleb Stanford | @ThomasKlimpel I don't agree it doesn't describe a natural deduction proof. "Natural deduction" means different things to different authors -- I have seen a basic variant of the sequent calculus described as natural deduction, but more common is the system where you introduce and discharge premises via introduction and elimination rules. The elimination rule for implication requires that we have $S$ before we can get to $\exists x Q(x)$. Perhaps your natural deduction system is not the one I am using here? | |
| Aug 7, 2018 at 8:05 | comment | added | Thomas Klimpel | Your answer definitely does not describe a "natural deduction proof", but it is basically right otherwise. The "natural deduction" proof systems allows you to (temporarily) eliminate the annoying implication without assuming the law of excluded middle. The problem with using "natural deduction" in a beginners course is that this system has desirable technical qualities beyond the scope of a beginners course. This makes it hard to explain why things have to be done in the way prescribed by the system. | |
| Aug 7, 2018 at 5:35 | history | answered | Caleb Stanford | CC BY-SA 4.0 |