Simplify rules

[catrincm]

Some rules are repetitions of others. That makes memorising the rules harder. It also perhaps makes learning strategies for how to use the different rules harder. I've been trying to simplify the rules. That'll generally make proofs using them one line longer, but I don't think any more difficult.

• rule for biconditional can be simplified to simply allow moving between the biconditional and the conjunction of the two conditionals. Then rules for conditionals can be applied.
• rule TND by Law of Excluded middle: you can always write Av¬A.

I've already edited this in my version, but that's not up on GitHub because I haven't properly worked out how to use GitHub. https://uob-my.sharepoint.com/personal/cc15682_bristol_ac_uk/_layouts/15/guestaccess.aspx?docid=0ed0ef9e829a14fcebcc7b253346a8d66&authkey=ATuzcf6W48MgwwLACcjyjYM&expiration=2017-12-01T00%3a00%3a00.000Z

[rzach]

Do you want to get rid of the LEM rule in favor of an LEM axiom, or have both?

It'll be hard to teach the proof checker to have ambiguous rule labels. The LEM axiom would be the only axiom in the system. The <->E rule that goes from A <-> to (A -> B) & (B -> A) [and perhaps a similar second <->I rule] would be complicated. I'm also not sure how often it will be useful. Perhaps it would be better to have these shortcuts not as official rules but just as examples: show students how to easily get from one to the other in a few simple steps. That would actually also be useful for the inferences B |- A -> B and ~A |- A -> B.

Deriving A v ~A using the LEM rule is now an exercise in the derived rules chapter. There could be a chapter on "Other useful inference" where we show them some tricks of that sort, but not introduce new official rules.

I would prefer to keep the basic rules simple and standard, and also not proliferate the derived rules too much.

[catrincm]

The idea was to replace the rule by the axiom. The thought being that it's more basic and is easy to remember and motivate, whereas the motivation for the current version seems to simultaneously motivate Av¬A and the argument structure for vE. Here's how the proposed modifications look: forallxbris.pdf

Anyway with your change to the Prawitz system this discussion isn't necessary as then there's no LEM axiom or rule at all, it's just derived.

The thought for simplifying the <--> rule is similar. It's not something that's terribly important because <--> isn't really a primitive symbol and I could quickly pass by this rule by just saying it allows you to move between <--> and the two conditionals. The current rules essentially do this move but also straight away plug in the way one should deal with & and ->. I was thinking it'd be better to separate these, so all the complicated stuff goes in the action of ->. I don't know anything about your proof checker and why that would be difficult. But fair enough, that might be a reason to stick to the current rules.