Zulip Chat Archive

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 :-)

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

having just read some Wikipedia article about this sort of thing

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

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

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

Kenny Lau (Apr 18 2018 at 18:50):

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

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

right

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

not = exterior, or = union, and = intersection

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

not is what?

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

exterior

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

Do I take the interior of the complement?

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

right

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

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

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

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

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

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?

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

Just do cases

Kenny Lau (Apr 18 2018 at 18:58):

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 :-)

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

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.

Kevin Buzzard (Apr 18 2018 at 19:04):

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)

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

does it?

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

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

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

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.

Kenny Lau (Apr 24 2018 at 15:34):

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: Dec 20 2023 at 11:08 UTC