New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Proof rules for negation #11

Closed
wyleyr opened this Issue Jun 15, 2017 · 9 comments

Comments

Projects
None yet
3 participants
@wyleyr

wyleyr commented Jun 15, 2017

Via email, I said:

Mainly the problem here is that the text calls '\bot Introduction' the rule that I think of as '\neg Elimination'; there is no '\neg Elimination' rule. This breaks the nice symmetry of having two I/E rules which define each connective. I also gave students a problem about explaining why we can define '\neg P' as 'P \eif \bot'. This problem would make more sense if the insight they were expected to get was: the I/E rules for negation just become instances of the rules for the conditional.

Richard Zach said:

I agree. This shouldn't be too hard to fix: rename all the rules in
existing proofs, and rewrite 15.7 and 15.8 (probably also: reverse them)?

(I'm also not sure about using the TND rule as opposed to the classical
absurdity rule.)

@catrincm

This comment has been minimized.

Show comment
Hide comment
@catrincm

catrincm Sep 27, 2017

So your suggestion is to have the current-botI as new-¬E, and have botE and ¬I as they currently are. Then the new system would have no botI rule, and you still need TND as a rule (eg to derive LEM) so that doesn't then fit in.

A nicer alternative would maybe to keep bot rules as they are and replace TND with
||¬A (assume)
||bot
|A

(That's then the proof system used in Halbach's logic manual. But a consequence of that change is that proving LEM from it is a massive task! So perhaps that's not so useful, although it's more pleasing on the eye, as it were).

catrincm commented Sep 27, 2017

So your suggestion is to have the current-botI as new-¬E, and have botE and ¬I as they currently are. Then the new system would have no botI rule, and you still need TND as a rule (eg to derive LEM) so that doesn't then fit in.

A nicer alternative would maybe to keep bot rules as they are and replace TND with
||¬A (assume)
||bot
|A

(That's then the proof system used in Halbach's logic manual. But a consequence of that change is that proving LEM from it is a massive task! So perhaps that's not so useful, although it's more pleasing on the eye, as it were).

@rzach

This comment has been minimized.

Show comment
Hide comment
@rzach

rzach Sep 27, 2017

Owner

That is the solution I favor. It's hat prawitz calls the classical absurdity rule; I propose we call it Indirect proof (IP). TND would become a derived rule. (Tricky to derive, but not so massive! Or, not more massive than DeM).

Instead of \bot E, I think we should call it ECQ (ex contradictione quodlibet). What do you think?

In the end, the I/E rules make up minimal logic, add ECQ for intuitionistic logic, add IP for classical. (Not that we'd have to discuss that, but it would make it easier to tie in our system to a discussion of minimal and intuitionistic logic in a future chapter or another course.)

Owner

rzach commented Sep 27, 2017

That is the solution I favor. It's hat prawitz calls the classical absurdity rule; I propose we call it Indirect proof (IP). TND would become a derived rule. (Tricky to derive, but not so massive! Or, not more massive than DeM).

Instead of \bot E, I think we should call it ECQ (ex contradictione quodlibet). What do you think?

In the end, the I/E rules make up minimal logic, add ECQ for intuitionistic logic, add IP for classical. (Not that we'd have to discuss that, but it would make it easier to tie in our system to a discussion of minimal and intuitionistic logic in a future chapter or another course.)

@rzach

This comment has been minimized.

Show comment
Hide comment
@rzach

rzach Sep 27, 2017

Owner

PS: One thing that's holding this up is that I want the proof checker to not break, but I've now gotten it to work and it should not be hard to make those changes.

Owner

rzach commented Sep 27, 2017

PS: One thing that's holding this up is that I want the proof checker to not break, but I've now gotten it to work and it should not be hard to make those changes.

@rzach

This comment has been minimized.

Show comment
Hide comment
@rzach

rzach Sep 30, 2017

Owner

I've drafted the necessary changes. They're in branch https://github.com/rzach/forallx-yyc/tree/issue11

See CH 15, 19 and Appendix B.

forallxyyc.pdf

Owner

rzach commented Sep 30, 2017

I've drafted the necessary changes. They're in branch https://github.com/rzach/forallx-yyc/tree/issue11

See CH 15, 19 and Appendix B.

forallxyyc.pdf

@rzach

This comment has been minimized.

Show comment
Hide comment
@rzach

rzach Oct 1, 2017

Owner

Aaaand the rules are working in the proof checker OpenLogicProject/fitch-checker#2

Owner

rzach commented Oct 1, 2017

Aaaand the rules are working in the proof checker OpenLogicProject/fitch-checker#2

@catrincm

This comment has been minimized.

Show comment
Hide comment
@catrincm

catrincm Oct 1, 2017

Thanks! I'm still working out how to use GitHub properly. One thing, though is that I prefer the name Explosion to ECQ. Mostly because of trying to avoid latin which I think needlessly puts students off.

catrincm commented Oct 1, 2017

Thanks! I'm still working out how to use GitHub properly. One thing, though is that I prefer the name Explosion to ECQ. Mostly because of trying to avoid latin which I think needlessly puts students off.

@rzach

This comment has been minimized.

Show comment
Hide comment
@rzach

rzach Oct 1, 2017

Owner

Changed rule names to "less pretentious." Also in proof checker.

PDF of new version: forallxyyc.pdf

Owner

rzach commented Oct 1, 2017

Changed rule names to "less pretentious." Also in proof checker.

PDF of new version: forallxyyc.pdf

@wyleyr

This comment has been minimized.

Show comment
Hide comment
@wyleyr

wyleyr Oct 2, 2017

This is great; thanks for making these changes! One nitpick: now that \bot-Introduction has been renamed to \neg-Elimination, wouldn't it make sense to switch the order of the lines in the citation? That is, as with the other elimination rules, the premise containing the eliminated connective should be cited first.

Would it make sense to start converting proofs in the solutions manual to use the new rules?

wyleyr commented Oct 2, 2017

This is great; thanks for making these changes! One nitpick: now that \bot-Introduction has been renamed to \neg-Elimination, wouldn't it make sense to switch the order of the lines in the citation? That is, as with the other elimination rules, the premise containing the eliminated connective should be cited first.

Would it make sense to start converting proofs in the solutions manual to use the new rules?

@rzach

This comment has been minimized.

Show comment
Hide comment
@rzach

rzach Oct 2, 2017

Owner

Ah, good point, yes. [fixed it!] So ~E and _|_I are actually different rules then. So I'll have to go through it and change all the \ri's to \ne's which is probably cleaner anyway. (Are we supposed to be sticklers about the order of the justifications? The solution to the second problem of 15.A suggests yes, but I didn't see a statement explicitly anywhere. The proof checker doesn't care.)

If you're volunteering to go through the solutions manual, sure! I fear we might have to actually move some exercises around -- with TND it was not too big of a deal to prove 15.C.7, but this is in the chapter on basic rules, and it'll be a lot harder with IP -- so probably move that into chapter 16 which needs examples of TND/LEM anyway. 15.C.12 will be easier with IP (just the second subproof), but we'll need a few more examples of IP in use/as exercises. I also added a few exercises already. Must keep track somewhere so we can make a list of what's changed for the next edition. [see #18 ]

Owner

rzach commented Oct 2, 2017

Ah, good point, yes. [fixed it!] So ~E and _|_I are actually different rules then. So I'll have to go through it and change all the \ri's to \ne's which is probably cleaner anyway. (Are we supposed to be sticklers about the order of the justifications? The solution to the second problem of 15.A suggests yes, but I didn't see a statement explicitly anywhere. The proof checker doesn't care.)

If you're volunteering to go through the solutions manual, sure! I fear we might have to actually move some exercises around -- with TND it was not too big of a deal to prove 15.C.7, but this is in the chapter on basic rules, and it'll be a lot harder with IP -- so probably move that into chapter 16 which needs examples of TND/LEM anyway. 15.C.12 will be easier with IP (just the second subproof), but we'll need a few more examples of IP in use/as exercises. I also added a few exercises already. Must keep track somewhere so we can make a list of what's changed for the next edition. [see #18 ]

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment