Flesh out exclusive-or in iset.mm

[jkingdon]

We now have a definition (df-xor) and a number of theorems concerning exclusive or.

I'm tagging this as good first issue since some of it is definitely easy (and the rest probably is, but might involve a little more figuring out what the theorems should be).

Remaining known tasks are:

• bring xorass and xorcom over from set.mm (need new proofs but those should be straightforward)
• figure out what to do with xordi. Does ( ( ph /\ ( ps \/_ ch ) ) <-> ( ( ph /\ ps ) \/_ ( ph /\ ch ) ) ) hold or is this theorem, or some variation thereof, dependent on some propositions being decidable?
• go through xor related theorems in set.mm and see if there are any more which should be brought over, either as-is or with decidability conditions added.

This issue replaces #350 and also builds on #405 (and other xor work to date).

[david-a-wheeler]

I did xorcom. xorass is harder; the approaches that are "obvious" to me don't appear to be valid under intuitionistic logic.

[digama0]

xorass is not true intuitionistically. Suppose it is; then ( ( ph \/_ ph ) \/_ T. ) <-> ( ph \/_ ( ph \/_ T. ) ). But ph \/_ ph is false, so ( ( ph \/_ ph ) \/_ T. ) is true and hence ( ph \/_ ( ph \/_ T. ) ) is true, which implies ph is decidable.

If ph and ch are decidable I think you can prove ( ( ph \/_ ps ) \/_ ch ) <-> ( ph \/_ ( ps \/_ ch ) ).

[digama0]

xordi should be provable with no assumptions.

[david-a-wheeler]

@digama0 : Are you sure xordi is intuitionistically provable? @jkingdon annimdc and xordidc for decidable propositions, but not when there's no guarantee that something is decidable.

[david-a-wheeler]

I'm fiddling with iset.mm in part to try to get my head wrapped around intuitionistic logic, which is decidedly different from classical logic. As such, I'm not going to be the best person to find subtle proofs.

[digama0]

Suppose ( ph /\ ( ps \/_ ch ) ), then ph and one of ps and ch is true, suppose ps is true and ch is false (WLOG). Then ph /\ ps is true, and ph /\ ch is equivalent to ch, so ph /\ ch is false and hence ( ph /\ ps ) \/_ ( ph /\ ch ).

Conversely, suppose ph /\ ps is true and ph /\ ch is false; then since ph, ph /\ ch is equivalent to ch so ch is false. Thus ph and ps \/_ ch.

[digama0]

Reasoning in intutionistic logic is pretty easy for true theorems; you basically only apply introduction rules on the right and elimination on the left, and then the proof will either already be done, or the theorem isn't provable. There is no backtracking or search involved - this is called the "cut-free" proof method since you don't need to invent lemmas (which can be difficult).

[jkingdon]

Hmm, not sure why I was thinking xorass would work. Doesn't seem like it should now.

Been a while since I thought about xordi but maybe I'll take a look.

As for xorcom, you want to make a pull request, @david-a-wheeler ? Might as well get that out of the way.

[david-a-wheeler]

@jkingdon : Oh, I'm way ahead of you :-). Commit 9f958a7830dde8b29dfb4cc49552032374c9d3d3 added xorcom to iset.mm, and it was accepted into "develop" earlier today.

[digama0]

Here's a nicer proof of xordi, without all the case analysis. We use pm5.21nii with ph as the cut theorem. Obviously ( ph /\ ( ps \/_ ch ) ) implies ph, and ( ph /\ ps ) \/_ ( ph /\ ch ) implies ( ph /\ ps ) \/ ( ph /\ ch ) which implies ph by jaoi +simpl or andi + simpl, not sure which is shorter. Then in the presence of ph it is easy to show that both sides are equivalent to ( ps \/_ ch ).

[jkingdon]

I'm going to close this, good work @digama0 and @david-a-wheeler . We have xorcom, xordi is #564 , xorass won't work, and the only other thing was a general "look around set.mm for other things which might hold" which doesn't seem specific enough to be especially useful.