Zulip Chat Archive

Stream: maths

Topic: xor is not associative


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Apr 18 2018 at 15:28):

or maybe show that xor is associative implies LEM

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:32):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 15:33):

let's say you can. and then?

view this post on Zulip Kenny Lau (Apr 18 2018 at 15:34):

I've convinced myself that you can

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:35):

I guess distributivity is all fine constructively

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:35):

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

Kevin, I'm very disappointed

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:35):

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

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:36):

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

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:36):

mechanics is super constructive

view this post on Zulip Kenny Lau (Apr 18 2018 at 15:36):

you bunch are horrible people

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:36):

with spanners and everything

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:39):

you bunch are horrible people

We are working on saving your soul

view this post on Zulip Kenny Lau (Apr 18 2018 at 15:39):

:(

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 18 2018 at 15:40):

that's one interpretation

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:40):

and then there's something with open sets

view this post on Zulip Kenny Lau (Apr 18 2018 at 15:40):

but I like Kripke model more

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:40):

Imagining Prop is a topological space saves souls??

view this post on Zulip Kenny Lau (Apr 18 2018 at 15:40):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:40):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 15:40):

@Patrick Massot he's unsaving me

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:41):

by making some trivial observation about topological spaces

view this post on Zulip Kenny Lau (Apr 18 2018 at 15:41):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:41):

having just read some Wikipedia article about this sort of thing

view this post on Zulip Patrick Massot (Apr 18 2018 at 15:41):

soon they will be using toposes...

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 15:41):

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 18:24):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:40):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:40):

using p <-> q

view this post on Zulip Gabriel Ebner (Apr 18 2018 at 18:50):

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

view this post on Zulip Gabriel Ebner (Apr 18 2018 at 18:50):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:50):

no problem

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:51):

here's what inspired me

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:51):

I wanted to prove that Prop is a group under xor

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:51):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:51):

so one of the group axioms must go wrong

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:51):

who can possibly know that it is the associativity

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:51):

(well I eliminated the other trivial axioms though)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 18:53):

Kenny did you try the topological space approach?

view this post on Zulip Gabriel Ebner (Apr 18 2018 at 18:53):

Ah, you're right of course.

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:54):

Kenny did you try the topological space approach?

I'm busy getting free group to work

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 18:54):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 18:55):

I don't remember the details

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:55):

right

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:55):

not = exterior, or = union, and = intersection

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 18:55):

not is what?

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:55):

exterior

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 18:55):

Do I take the interior of the complement?

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:56):

right

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 18:56):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:56):

yes

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:56):

interior + boundary + exterior = whole space

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:56):

interior + boundary = closure

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 18:56):

So are we 100 percent fixed on definition of xor?

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:56):

what is xor here?

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:56):

oh right, we already have everything

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:56):

yes then

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 18:57):

great, Mario just saved me a job :-)

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:57):

@Mario Carneiro muito obrigado

view this post on Zulip Andrew Ashworth (Apr 18 2018 at 18:58):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 18:58):

now the other way!

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 18:58):

Oh the other way is trivial, right?

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 18:58):

Just do cases

view this post on Zulip Kenny Lau (Apr 18 2018 at 18:58):

right

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 18:58):

so this is another way of formulating LEM :-)

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 18:58):

that Prop is a group :-)

view this post on Zulip Kenny Lau (Apr 18 2018 at 19:03):

right

view this post on Zulip Kenny Lau (Apr 18 2018 at 19:03):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 19:03):

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

view this post on Zulip Mario Carneiro (Apr 18 2018 at 19:04):

I wonder if there is any group structure on Prop?

view this post on Zulip Gabriel Ebner (Apr 18 2018 at 19:04):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 19:04):

rofl

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 19:05):

I am not so sure life is so easy

view this post on Zulip Mario Carneiro (Apr 18 2018 at 19:05):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 19:05):

I am not sure this has inverses.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 18 2018 at 19:07):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 19:08):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 19:08):

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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 19:09):

Does the following make sense:

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 19:09):

there is a two-point space with one point open

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 19:09):

and this space has three open sets

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 19:10):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 19:10):

but things don't add up

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 18 2018 at 19:11):

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

view this post on Zulip Gabriel Ebner (Apr 18 2018 at 19:11):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 19:12):

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

what do you mean?

view this post on Zulip Kenny Lau (Apr 18 2018 at 19:13):

isn't that intuitionistically valid

view this post on Zulip Mario Carneiro (Apr 18 2018 at 19:13):

xor implies both its arguments are decidable

view this post on Zulip Mario Carneiro (Apr 18 2018 at 19:13):

(in the LEM sense)

view this post on Zulip Kenny Lau (Apr 18 2018 at 19:13):

does it?

view this post on Zulip Kenny Lau (Apr 18 2018 at 19:14):

right, it does

view this post on Zulip Kenny Lau (Apr 18 2018 at 19:14):

something is wrong with me

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 24 2018 at 15:04):

Is it the same thing as Kripke frames?

view this post on Zulip Peter Jipsen (Apr 24 2018 at 15:05):

Yes, it's the algebraic version

view this post on Zulip Kenny Lau (Apr 24 2018 at 15:05):

aha

view this post on Zulip Kenny Lau (Apr 24 2018 at 15:05):

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

view this post on Zulip 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?

view this post on Zulip Andrew Ashworth (Apr 24 2018 at 15:06):

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

view this post on Zulip Kenny Lau (Apr 24 2018 at 15:08):

:o infinite logic?

view this post on Zulip Andrew Ashworth (Apr 24 2018 at 15:09):

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

view this post on Zulip Andrew Ashworth (Apr 24 2018 at 15:09):

but the coq code is nice

view this post on Zulip Andrew Ashworth (Apr 24 2018 at 15:09):

https://github.com/SkySkimmer/NormalisationByCompleteness

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 24 2018 at 15:34):

thanks

view this post on Zulip 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