Zulip Chat Archive

Stream: general

Topic: iff.assoc


view this post on Zulip Kevin Buzzard (Jul 25 2018 at 18:48):

Chris asked today if iff was associative and a room full of mathematicians had no clue between them :-) We proved it by checking all 8 cases in Lean :-)

import tactic.finish
open classical
example (P Q R : Prop) : ((P  Q)  R)  (P  (Q  R)) :=
begin cases (em P);cases (em Q);cases (em R);finish
end

I was surprised that finish didn't do it alone:

-- example (P Q R : Prop) : ((P ↔ Q) ↔ R) ↔ (P ↔ (Q ↔ R)) := by finish -- fails

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 18:50):

I later found a better proof: if we break with convention and define true = 0 and false = 1 then iff is addition mod 2, and addition mod 2 is associative.

Is it true constructively? I struggled, but then again I am certainly no expert.

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

Here's one place I get stuck:

P Q R : Prop,
HQPQ : Q → (P ↔ Q),
HPQQ : (P ↔ Q) → Q,
H : Q → P,
HP : P
⊢ Q

I eliminated R (WLOG I believe) and I can't see how to do this. I am now minded to look for a counterexample. @Kenny Lau to prove it's not constructively provable it would suffice to find some topological space with three subsets such that some random statement in topology is false, right?

view this post on Zulip Simon Hudon (Jul 25 2018 at 18:58):

I think tauto should manage to prove it

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 18:59):

done tactic failed, there are unsolved goals
state:
P Q R : Prop,
a : P ↔ Q ↔ R,
a_1 : P,
a_2 : Q
⊢ R

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 18:59):

Is tauto constructive?

view this post on Zulip Patrick Massot (Jul 25 2018 at 18:59):

Kevin, don't you have serious math to formalize?

view this post on Zulip Kenny Lau (Jul 25 2018 at 18:59):

I think so

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 19:00):

Blame Chris. He pointed out that when a mathematician writes A iff B iff C, they mean A iff B, and B iff C, so A iff C, i.e. iff.trans. iff.assoc is a different question entirely :-) It's like the 1 <= k <= n thing.

view this post on Zulip Simon Hudon (Jul 25 2018 at 19:01):

Yes, I believe it sticks to classical lemmas and if your propositions are decidable, it can prove more

view this post on Zulip Patrick Massot (Jul 25 2018 at 19:04):

The original question is perfectly legit, it's the constructivist deviance that I frown upon.

view this post on Zulip Johan Commelin (Jul 25 2018 at 19:05):

I later found a better proof: if we break with convention and define true = 0 and false = 1 then iff is addition mod 2, and addition mod 2 is associative.

That sounds like a proof by transport of structure (-;

view this post on Zulip Chris Hughes (Jul 25 2018 at 19:53):

lemma em_of_iff_assoc : ( p q r : Prop, ((p  q)  r)  (p  (q  r)))   p, p  ¬p :=
λ h p, ((h (p  ¬p) false false).1
⟨λ h, h.1 (or.inr (λ hp, h.1 (or.inl hp))), λ h, h.elim).2 iff.rfl

#print axioms em_of_iff_assoc

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 19:53):

[no axioms]

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 19:53):

Aah yes that's another way of resolving this

view this post on Zulip Mario Carneiro (Jul 26 2018 at 01:23):

I recall having this exact conversation with Kenny a while ago (prove LEM from iff assoc)

view this post on Zulip Kenny Lau (Jul 26 2018 at 05:36):

it was xor assoc

view this post on Zulip Chris Hughes (Jul 26 2018 at 05:45):

Did you prove XOR assoc -> em?

view this post on Zulip Kenny Lau (Jul 26 2018 at 05:45):

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

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/xor.20is.20not.20associative/near/125266318

view this post on Zulip Kenny Lau (Jul 26 2018 at 05:46):

by Mario

view this post on Zulip Kevin Buzzard (Jul 26 2018 at 07:45):

xor is associative because if you label false as 0 and true as 1 then it's addition mod 2. I thought it was funny that iff could be proved associative with the other labelling. It's almost like this is a proof strat and then you make all labellings and find out what each labelling proves :-)

view this post on Zulip Kenny Lau (Jul 26 2018 at 07:46):

can we create a Kripke frame where ((p ↔ q) ↔ r) but not (p ↔ (q ↔ r))?

view this post on Zulip Kevin Buzzard (Jul 26 2018 at 07:52):

and is associative because multiplication is associative, and or is associative because multiplication is associative. nand is not associative (however it is commutative, answering a question which an UG asked me last Oct -- "does commutative imply associative?")

view this post on Zulip Kevin Buzzard (Jul 26 2018 at 07:52):

Is a Kripke frame just a fancy name for a topological space in this context?

view this post on Zulip Kenny Lau (Jul 26 2018 at 07:53):

Kripke frame is a semantics for constructive logic

view this post on Zulip Kenny Lau (Jul 26 2018 at 07:53):

I think topological space is another semantics

view this post on Zulip Patrick Massot (Jul 26 2018 at 07:53):

topos!


Last updated: May 12 2021 at 22:15 UTC