## Stream: general

### Topic: iff.assoc

#### 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


#### 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.

#### 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?

#### Simon Hudon (Jul 25 2018 at 18:58):

I think tauto should manage to prove it

#### 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


#### Kevin Buzzard (Jul 25 2018 at 18:59):

Is tauto constructive?

#### Patrick Massot (Jul 25 2018 at 18:59):

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

I think so

#### 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.

#### 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

#### Patrick Massot (Jul 25 2018 at 19:04):

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

#### 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 (-;

#### 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


[no axioms]

#### Kevin Buzzard (Jul 25 2018 at 19:53):

Aah yes that's another way of resolving this

#### Mario Carneiro (Jul 26 2018 at 01:23):

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

it was xor assoc

#### Chris Hughes (Jul 26 2018 at 05:45):

Did you prove XOR assoc -> em?

#### 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

by Mario

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

#### Kenny Lau (Jul 26 2018 at 07:46):

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

#### 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?")

#### Kevin Buzzard (Jul 26 2018 at 07:52):

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

#### Kenny Lau (Jul 26 2018 at 07:53):

Kripke frame is a semantics for constructive logic

#### Kenny Lau (Jul 26 2018 at 07:53):

I think topological space is another semantics

#### Patrick Massot (Jul 26 2018 at 07:53):

topos!

Last updated: Dec 20 2023 at 11:08 UTC