Add intuitionistic exclusive-or to iset.mm

[jkingdon]

The discussion so far has been in #316 and #349 but neither one is exactly about the project of adding intuitionistic exclusive-or. I'm tagging this as good first issue because I think some of it is pretty simple although I'm not sure I have a full understanding of which parts are easier or harder.

Basic definitions of xor are now merged (see for example #351 and #357 ). The parts remaining are:

• bring excxor over from set.mm and find an intuitionistic proof
• bring xorass and xorcom over from set.mm (need new proofs but those should be straightforward)
• go over the classical exclusive-or section near the end of iset.mm . Figure out what, if anything, can be intuitionized and bring that into the intuitionistic logic section. Revise the comments for the parts which remain classical to refer to the intuitionistic theorems. Bring it into closer resemblence to current set.mm (use the exclusive-or symbol, for example).
• see what else is in set.mm which might work in iset.mm

[digama0]

By the way, here are some more facts about intuitionistic xor that I'm sure have no set.mm analogue:

• ph \/_ ps implies that ph and ps are decidable. (Should there be a notation for this concept?)
• Therefore, ph \/_ ps implies every other classically equivalent form of xor, like ph <-> -. ps and -. (ph <-> ps)

There should probably be classical theorems in the intuitionistic section given appropriate decidability assumptions. For example, ( ph -> ( ps \/ ch ) ) <-> ( ( ph -> ps ) /\ ( ph -> ch ) ) if any of ph, ps or ch are decidable. This is somewhat similar to the practice of having choice-free proofs of obvious choice-requiring theorems, like Zorn's lemma, under some "local" choice assumption, because often one can prove that a certain proposition is decidable without using EM, and then you get classical theorems for the price of intuitionistic logic.

[jkingdon]

@digama0 Meaning something like df-decidable $a |- decidable ph <-> ( ph \/ -. ph ) ? (notation to be determined). I guess that makes sense (either with a notation or just writing it as ph \/ -. ph). I'm not really qualified to say whether there are any tricky issues with free variables or anything else, in terms of using it for things like proofs of xor theorems.

[digama0]

Yes, that's exactly what I mean. One option I was considering was LEM ph, but anything along those lines would do the trick. There aren't any issues with bound variables; this is just a unary propositional connective. (And bound variables aren't even going to come up in the propositional fragment.) An example of mixing in free variables might be the theorem that natural number equality is decidable:

|- ( ( A e. NN /\ B e. NN ) -> LEM A = B )

[jkingdon]

I've moved the discussion of a decidability notation to a separate issue at #362 (which I probably should have done as soon as the topic came up, but better late than never). Over at that issue I have some proposed changes to iset.mm and some questions that are open for discussion.

[jkingdon]

This is done except for the parts which I moved over to #406.