## Stream: maths

### Topic: xor is not associative

#### Kenny Lau (Apr 18 2018 at 15:27):

Could someone prove that xor is not associative constructively, perhaps by constructing a Kripke model where this fails?

#### Kenny Lau (Apr 18 2018 at 15:27):

here xor is defined as Lean defines it: p xor q := (p and not q) or (not p and q)

#### Kenny Lau (Apr 18 2018 at 15:28):

or maybe show that xor is associative implies LEM

#### Kevin Buzzard (Apr 18 2018 at 15:32):

if you defined xor' as (p or q) and (not p or not q) then can you constructively prove that this is the same as xor?

#### Kevin Buzzard (Apr 18 2018 at 15:32):

I can't believe I'm thinking about such nonsense

#### Kenny Lau (Apr 18 2018 at 15:33):

let's say you can. and then?

#### Kenny Lau (Apr 18 2018 at 15:34):

I've convinced myself that you can

#### Kevin Buzzard (Apr 18 2018 at 15:35):

I guess distributivity is all fine constructively

#### Patrick Massot (Apr 18 2018 at 15:35):

I can't believe I'm thinking about such nonsense

Kevin, I'm very disappointed

#### Kevin Buzzard (Apr 18 2018 at 15:35):

I'm trying to finish this affine scheme thing and he keeps pestering me!

#### Patrick Massot (Apr 18 2018 at 15:36):

He should work on mechanics each time he is tempted by constructivist non-sense

#### Patrick Massot (Apr 18 2018 at 15:36):

mechanics is super constructive

#### Kenny Lau (Apr 18 2018 at 15:36):

you bunch are horrible people

#### Kevin Buzzard (Apr 18 2018 at 15:36):

with spanners and everything

#### Patrick Massot (Apr 18 2018 at 15:39):

you bunch are horrible people

We are working on saving your soul

:(

#### Kevin Buzzard (Apr 18 2018 at 15:40):

Kenny, the only technique I know for this sort of thing is to imagine Prop is some topological space

#### Kenny Lau (Apr 18 2018 at 15:40):

that's one interpretation

#### Kevin Buzzard (Apr 18 2018 at 15:40):

and then there's something with open sets

#### Kenny Lau (Apr 18 2018 at 15:40):

but I like Kripke model more

#### Patrick Massot (Apr 18 2018 at 15:40):

Imagining Prop is a topological space saves souls??

#### Kenny Lau (Apr 18 2018 at 15:40):

since it's morally what's going on behind constructivism

#### Kevin Buzzard (Apr 18 2018 at 15:40):

where not p is something like the interior of the complement of p

#### Kenny Lau (Apr 18 2018 at 15:40):

@Patrick Massot he's unsaving me

#### Kevin Buzzard (Apr 18 2018 at 15:41):

All I'm saying is that the one time in my life when I thought about this was a few months ago, when I proved that not not p implies p was not provable constructively

#### Kevin Buzzard (Apr 18 2018 at 15:41):

by making some trivial observation about topological spaces

#### Kenny Lau (Apr 18 2018 at 15:41):

right, but the connection is not trivial at all :-)

#### Patrick Massot (Apr 18 2018 at 15:41):

soon they will be using toposes...

#### Kevin Buzzard (Apr 18 2018 at 15:41):

and it seems to me that your question might yield to the same strategy

#### Mario Carneiro (Apr 18 2018 at 18:24):

here is a simpler problem: if not (p xor q), is p decidable?

#### Mario Carneiro (Apr 18 2018 at 18:30):

ah, of course not: if p <-> q then not (p xor q) but then p may be some arbitrary nondecidable proposition

#### Kenny Lau (Apr 18 2018 at 18:40):

use non-well-founded recursion to prove that p is decidable :P @Mario Carneiro

using p <-> q

#### Gabriel Ebner (Apr 18 2018 at 18:50):

Maybe a better problem: if xor p q, is p decidable?

#### Gabriel Ebner (Apr 18 2018 at 18:50):

BTW, this is a nice puzzle! Thanks, @Kenny Lau

no problem

#### Kenny Lau (Apr 18 2018 at 18:51):

here's what inspired me

#### Kenny Lau (Apr 18 2018 at 18:51):

I wanted to prove that Prop is a group under xor

#### Kenny Lau (Apr 18 2018 at 18:51):

but if this is possible, then it would imply double negation elimination

#### Kenny Lau (Apr 18 2018 at 18:51):

so one of the group axioms must go wrong

#### Kenny Lau (Apr 18 2018 at 18:51):

who can possibly know that it is the associativity

#### Kenny Lau (Apr 18 2018 at 18:51):

(well I eliminated the other trivial axioms though)

#### Kenny Lau (Apr 18 2018 at 18:52):

Maybe a better problem: if xor p q, is p decidable?

technically, even p or not p doesn't mean p is decidable

#### Kevin Buzzard (Apr 18 2018 at 18:53):

Kenny did you try the topological space approach?

#### Gabriel Ebner (Apr 18 2018 at 18:53):

Ah, you're right of course.

#### Kenny Lau (Apr 18 2018 at 18:54):

Kenny did you try the topological space approach?

I'm busy getting free group to work

#### Kevin Buzzard (Apr 18 2018 at 18:54):

You need to check p xor not p is provable :-)

#### Kevin Buzzard (Apr 18 2018 at 18:55):

OK let me just spend a few minutes doing the top space thing in case it clarifies anything

#### Kevin Buzzard (Apr 18 2018 at 18:55):

I don't remember the details

#### Kevin Buzzard (Apr 18 2018 at 18:55):

but is the idea somehow that we can think of a prop as being an open set in a topological space

right

#### Kenny Lau (Apr 18 2018 at 18:55):

not = exterior, or = union, and = intersection

not is what?

exterior

#### Kevin Buzzard (Apr 18 2018 at 18:55):

Do I take the interior of the complement?

right

#### Kevin Buzzard (Apr 18 2018 at 18:56):

Is that what exterior means? I've never heard that

yes

#### Kenny Lau (Apr 18 2018 at 18:56):

interior + boundary + exterior = whole space

#### Kenny Lau (Apr 18 2018 at 18:56):

interior + boundary = closure

#### Kevin Buzzard (Apr 18 2018 at 18:56):

So are we 100 percent fixed on definition of xor?

#### Kenny Lau (Apr 18 2018 at 18:56):

what is xor here?

#### Kenny Lau (Apr 18 2018 at 18:56):

oh right, we already have everything

yes then

#### Mario Carneiro (Apr 18 2018 at 18:56):

so here is a proof of LEM from xor assoc:

example (h : ∀ p q r, xor p (xor q r) ↔ xor (xor p q) r) {p} : p ∨ ¬ p :=
have ¬ xor p p, from λ h, h.elim (λ ⟨hp, np⟩, np hp) (λ ⟨hp, np⟩, np hp),
have xor p (xor p true), from (h p p true).2 (or.inr ⟨trivial, this⟩),
this.imp and.left and.right


#### Kevin Buzzard (Apr 18 2018 at 18:57):

great, Mario just saved me a job :-)

#### Kenny Lau (Apr 18 2018 at 18:57):

@Mario Carneiro muito obrigado

#### Andrew Ashworth (Apr 18 2018 at 18:58):

this is random but related to xor: has anyone seen a definition of one-hot encoding?

#### Kevin Buzzard (Apr 18 2018 at 18:58):

now the other way!

#### Kevin Buzzard (Apr 18 2018 at 18:58):

Oh the other way is trivial, right?

Just do cases

right

#### Kevin Buzzard (Apr 18 2018 at 18:58):

so this is another way of formulating LEM :-)

#### Kevin Buzzard (Apr 18 2018 at 18:58):

that Prop is a group :-)

right

#### Kenny Lau (Apr 18 2018 at 19:03):

and people won't guess that it is associativity that fails

#### Kevin Buzzard (Apr 18 2018 at 19:03):

I'll put it on next year's Christmas Quiz

#### Mario Carneiro (Apr 18 2018 at 19:04):

I wonder if there is any group structure on Prop?

#### Gabriel Ebner (Apr 18 2018 at 19:04):

The double-negation translation of xor should do the job.

rofl

#### Kevin Buzzard (Apr 18 2018 at 19:05):

I am not so sure life is so easy

#### Mario Carneiro (Apr 18 2018 at 19:05):

I don't think that will satisfy the cancellation laws on nondecidable props

#### Kevin Buzzard (Apr 18 2018 at 19:05):

I am not sure this has inverses.

#### Kevin Buzzard (Apr 18 2018 at 19:06):

This question is related to putting a group structure on the set of open sets in a topological space I guess

#### Gabriel Ebner (Apr 18 2018 at 19:06):

Mmh, the double-negation translation turns classical theorems into intuitionistic theorems. So if xor is associative, etc., classicaly then xor^N should be intuitionistically associative, etc.

#### Mario Carneiro (Apr 18 2018 at 19:07):

true, but the group has to include all props, not just the negative props

#### Kevin Buzzard (Apr 18 2018 at 19:08):

in my language, consider open sets which are dense. Their negation is empty

#### Kevin Buzzard (Apr 18 2018 at 19:08):

so you have lost information which is never coming back, and that's bad for groups

#### Kevin Buzzard (Apr 18 2018 at 19:09):

Does the following make sense:

#### Kevin Buzzard (Apr 18 2018 at 19:09):

there is a two-point space with one point open

#### Kevin Buzzard (Apr 18 2018 at 19:09):

and this space has three open sets

#### Kevin Buzzard (Apr 18 2018 at 19:10):

and so if it were a group it would be cyclic of order 3

#### Kevin Buzzard (Apr 18 2018 at 19:10):

and now I want to write down a map from bool to this set or from this set to bool

#### Kevin Buzzard (Apr 18 2018 at 19:10):

and argue that if Prop had a group structure it would have to be a group homomorphism

#### Kevin Buzzard (Apr 18 2018 at 19:10):

but things don't add up

#### Mario Carneiro (Apr 18 2018 at 19:11):

Ah, how about this: every (definable in intuitionistic logic) one-arg operator is noninjective on some topological space or is the identity

#### Kevin Buzzard (Apr 18 2018 at 19:11):

because I am hoping I am writing down two incompatible "interpretations" of Prop somehow

#### Gabriel Ebner (Apr 18 2018 at 19:11):

Ah yes, everything goes through except xor p false <-> p...

#### Kenny Lau (Apr 18 2018 at 19:12):

Ah yes, everything goes through except xor p false <-> p...

what do you mean?

#### Kenny Lau (Apr 18 2018 at 19:13):

isn't that intuitionistically valid

#### Mario Carneiro (Apr 18 2018 at 19:13):

xor implies both its arguments are decidable

#### Mario Carneiro (Apr 18 2018 at 19:13):

(in the LEM sense)

does it?

right, it does

#### Kenny Lau (Apr 18 2018 at 19:14):

something is wrong with me

#### Gabriel Ebner (Apr 18 2018 at 19:15):

xor p false <-> p fails for the double-negation translation. It is true in the official version, though.

#### Peter Jipsen (Apr 24 2018 at 15:04):

Can't one just check associativity of xor in Heyting algebras? It fails in the 3-element Heyting algebra where 0<1<2: (2 xor 2) xor 1 \ne 2 xor (2 xor 1) (assuming a xor b is defined as (a or b) and not (a and b)). Of course this would require quite some background work defining Heyting algebras etc.

#### Kenny Lau (Apr 24 2018 at 15:04):

Is it the same thing as Kripke frames?

#### Peter Jipsen (Apr 24 2018 at 15:05):

Yes, it's the algebraic version

aha

#### Kenny Lau (Apr 24 2018 at 15:05):

a xor b is defined as (a and not b) or (not a and b)

#### Kenny Lau (Apr 24 2018 at 15:05):

would knowing about Kripke frames and boolean algebra make Heyting algebra easy to learn? if so, do you mind teaching me?

#### Andrew Ashworth (Apr 24 2018 at 15:06):

http://www.cri.ensmp.fr/classement/doc/E-372.pdf

#### Kenny Lau (Apr 24 2018 at 15:08):

:o infinite logic?

#### Andrew Ashworth (Apr 24 2018 at 15:09):

the paper is a little hard to read without a little more background

#### Andrew Ashworth (Apr 24 2018 at 15:09):

but the coq code is nice

#### Andrew Ashworth (Apr 24 2018 at 15:09):

https://github.com/SkySkimmer/NormalisationByCompleteness

#### Peter Jipsen (Apr 24 2018 at 15:34):

The definition (a and not b) or (not a and b) has the same counterexample.
The equivalence between finite Heyting algebras and finite partially ordered Kripke frames is similar to the equivalence between finite Boolean algebras and finite sets, so you have all the necessary background. (In the general case Esakia spaces are a categorical dual of Heyting algebras.) Propositional intuitionistic logic is decidable, so questions like this can be answered algorithmically by a tableau prover or Gentzen's sequent calculus LJ.

thanks

#### Peter Jipsen (Apr 24 2018 at 16:03):

A interesting test problem is to decide if the two definitions of xor are intuitionistically equivalent. I would like to understand how one would use Lean to help prove or refute it. E.g. is there a tactic that implements tableau?

Last updated: May 19 2021 at 00:40 UTC