定理$BOOLE'25$

以下は

$$(\forall x)(not (x \in X) \Leftrightarrow (x \in Y \Leftrightarrow x \in Z)) \Leftarrow X = Y \oplus Z$$

の証明です。

theorem :: BOOLE'25:
  (for x holds not x in X iff (x in Y iff x in Z))   implies X = Y \+\ Z
proof
  assume A1: not x in X iff (x in Y iff x in Z);
  now let x;
    x in X iff x in Y & not x in Z or x in Z & not x in Y by A1;
    then x in X iff x in Y \ Z or x in Z \ Y by Def4;
    then x in X iff x in (Y \ Z) \/ (Z \ Y) by Def2;
    hence x in X iff x in Y \+\ Z by Def6;
  end;
  hence thesis by TARSKI:2;
end;

$$A1:not (x \in X) \Leftrightarrow (x \in Y \Leftrightarrow x \in Z))$$

を仮定すると, 任意の$x$について,$A1$から,

$$(x \in X) \Leftrightarrow ( (x \in Y \ and \ not \ x \in Z) \ or \ (x \in Z \ and \ not \ x \in Y))$$

が成り立ち,これと$Def4$から

$$x \in X \Leftrightarrow (x \in Y \setminus Z \ or \ x \in Z \setminus Y )$$

が成り立ち,さらに,$Def2$により,

$$x \in X \Leftrightarrow x \in (Y \setminus Z) \cup (Z \setminus Y)$$

が成り立ち,これから$TARSKI:2$によって証明終了です。