Stickynotes

公理的集合論上で分出公理を用いて上記の $A$ が存在しないことを示す。

分出公理: $\forall A \exists B \forall x (x \in B ⟺ x \in A \land φ (x))$

※ $φ$ は $x$ と $A$ を含む論理式である。とくに FOL で考えているため、これを量化することはしない。

$φ$ ごとに分出公理が成り立つので、以下も成り立つ。

\forall A \exists B \forall x (x \in B ⟺ x \in A \land x \in x)

$A$ として $\forall x . x \in A$ を満すような集合をとってくる。

公理から次のような集合が存在することが導かれる。

B = {x \in A ∣ x \in x}

もし $B \in B$ だったとき、 $φ$ の定義から $B \notin B$ となり矛盾。もし $B \notin B$ だったとき、 $φ$ の定義から $B \in B$ となり矛盾。

したがって、以上の議論のどこかに矛盾がある。

以上より、どんな $x$ も含む集合 $A$ は存在しない。■

2023年4月に仙台にて学生から質問を受けてこの問題を解きました。解くにあたって Yudai Suzuki 氏にも助言をもらいました。お二人ともありがとうございます。

Date: 2023-05-12T00:00:00.000Z

適当なシーケント計算の体系 (たとえば $G3cp$ ) において、その体系が無矛盾であることを導くことを考える。

体系が無矛盾であることは $\Rightarrow ⊥$ が導かれないことである。背理法を用いて、 $\Rightarrow ⊥$ が導かれると仮定する。

現在の体系でカット除去定理が成り立つならば、このシーケントもカット以外の推論規則で証明できるはずである。

ところが、このシーケントに至るまでに、直前に適用されたと考える推論規則はカットのみである(※体系依存)。なぜなら、 $⊥$ 以外の項がシーケントに含まれていないからである。

したがって、このシーケントがカットを用いずに証明できないことから、仮定が否定されるため、体系は無矛盾であることが示される。■

Leuven に滞在中の 2024 年 8 月に Marianna Girlando 氏にこの証明のアイデアを教えていただきました。ありがとうございます。

Date: 2024-08-09T00:00:00.000Z