Three_Way_Exclusive_Or_and_Equivalence

Disproved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

logicproofwikipropositional-logic

Let $p \iff q$ be the biconditional operator, and $p \oplus q$ be the exclusive or operator. Then $p \iff q \iff r \dashv \vdash p \oplus q \oplus r$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Three_Way_Exclusive_Or_and_Equivalence (p q r : Prop) [Decidable p] [Decidable q] [Decidable r] : (Xor' (Xor' p q) r) ↔ ¬((p ↔ q) ↔ r) := by sorry

Source

https://proofwiki.org/wiki/Three-Way_Exclusive_Or_and_Equivalence

View graph