居住セット

数学では、集合に 要素が存在する場合、その集合には要素が存在します。 ${\displaystyle A}$${\displaystyle a\in A}$

古典数学では、人が住んでいるという性質は空でないということと同義です。しかし、この同値性は構成的論理や直観主義論理では有効ではないため、この別の用語は主に構成的数学の集合論で使用されます。

一階述語論理の形式言語では、集合が占有されているという性質を持つのは、 ${\displaystyle A}$

${\displaystyle \exists z.(z\in A).}$

集合 は、の場合、または同等にの場合、空であるという特性を持ちます。ここで は否定 を表します。 ${\displaystyle A}$${\displaystyle \forall z.(z\notin A)}$${\displaystyle \neg \exists z.(z\in A)}$${\displaystyle z\notin A}$${\displaystyle \neg (z\in A)}$

集合が空でないと判断されるのは、それが空でない場合、つまり の場合、または同等の の場合です。 ${\displaystyle A}$${\displaystyle \neg \forall z.(z\notin A)}$${\displaystyle \neg \neg \exists z.(z\in A)}$

モーダスポネンスはを意味し、 について任意の偽の命題を取ることでが常に有効であることを確立します。したがって、任意の有人集合は空でないことも証明できます。 ${\displaystyle P\to ((P\to Q)\to Q)}$${\displaystyle Q}$${\displaystyle P\to \neg \neg P}$

構成的数学では、二重否定除去原理は自動的には有効ではありません。特に、存在ステートメントは一般にその二重否定形式よりも強力です。後者は、一貫して否定できないという強い意味で、存在を除外できないことを単に表現しています。構成的な読み方では、何らかの式に対して が成り立つためには、を満たすの特定の値が構築されるか既知である必要があります。同様に、全称量化ステートメントの否定は一般に、否定ステートメントの存在量化よりも弱いです。逆に、集合が空でないことは証明できますが、そこに存在することを証明することはできません。 ${\displaystyle \exists z.\phi (z)}$ ${\displaystyle \phi}$${\displaystyle z}$${\displaystyle \phi}$

またはのような集合には、例えば によって証明されるように、人が存在します。集合は空であり、したがって人が存在しません。したがって、当然、例のセクションでは、人が存在していることが証明されていない空でない集合に焦点を当てています。 ${\displaystyle \{2,3,4,7\}}$${\displaystyle \mathbb {Q} }$${\displaystyle 3\in \{2,3,4,7\}}$${\displaystyle \{\}}$

分離公理を使用すると、このような例を簡単に挙げることができます。分離公理を使用すると、論理ステートメントを常に集合論的なステートメントに変換できるからです。たとえば、サブセットが と定義されている場合、命題は常に と同等に述べることができます。特定のプロパティを持つエンティティの二重否定の存在主張は、そのプロパティを持つエンティティの集合が空でないと述べることで表現できます。 ${\displaystyle S\subset \{0\}}$${\displaystyle S:=\{n\in \{0\}\mid P\}}$${\displaystyle P}$${\displaystyle 0\in S}$

サブセットを定義するには ${\displaystyle A\subset \{0,1\}}$

${\displaystyle A:=\{n\in \{0,1\}\mid (P\land n=0)\lor (\neg P\land n=1)\}}$

明らかに、そしてであり、無矛盾の原理から、結論はこうなります。さらに、そして、 ${\displaystyle P\leftrightarrow 0\in A}$${\displaystyle (\neg P)\leftrightarrow 1\in A}$${\displaystyle \neg (0\in A\land 1\in A)}$${\displaystyle (P\lor \neg P)\leftrightarrow (0\in A\lor 1\in A)}$

${\displaystyle (P\lor \neg P)\to \exists !(n\in \{0,1\}).n\in A}$

すでに極小論理によって、任意の排中命題に対する二重否定 が証明されています。これはここでは と同等です。したがって、前の含意に対して 2 つの対偶を実行すると が確立されます。言葉で言うと、と のどちらか 1 つが に存在することを一貫して排除することはできません。特に、後者は に弱めることができ、 は空でないことが証明されます。 ${\displaystyle \neg \neg (P\lor \neg P)}$${\displaystyle \neg (0\notin A\land 1\notin A)}$${\displaystyle \neg \neg \exists !(n\in \{0,1\}).n\in A}$${\displaystyle 0}$${\displaystyle 1}$${\displaystyle A}$${\displaystyle \neg \neg \exists n.n\in A}$${\displaystyle A}$

のステートメントの例として、連続体仮説、手元にある健全な理論の一貫性、または非公式には過去や未来についての知ることのできない主張など、理論に依存しないことが証明されている悪名高いステートメントを考えてみましょう。意図的に、これらは証明不可能となるように選択されています。これの変形は、単にまだ確立されていない数学的な命題を考えることです。Brouwerian 反例 も参照してください。または の有効性に関する知識は、上記のに関する知識と同等であり、取得できません。理論でもも証明できない場合、特定の数が存在することも証明されません。さらに、選言プロパティを持つ構成的フレームワークでは、どちらも証明できません。 、 、 の証拠はなく、それらの選言の構成的証明不可能性はこれを反映しています。それでも、排中律を排除することは常に矛盾することが証明されているため、が空でないことも確立されています。古典論理は を公理的に採用し、構成的な読みを台無しにします。 ${\displaystyle P}$${\displaystyle 0\in A}$${\displaystyle 1\in A}$${\displaystyle P}$${\displaystyle P}$${\displaystyle \neg P}$${\displaystyle A}$${\displaystyle P\lor \neg P}$${\displaystyle 0\in A}$${\displaystyle 1\in A}$${\displaystyle A}$${\displaystyle P\lor \neg P}$

では存在が証明できないが、完全な選択公理によって存在すると暗示される、特徴付けが容易な集合が様々あります。したがって、その公理自体は から独立しています。実際、それは集合論の他の潜在的な公理と矛盾します。さらに、集合論のコンテキストでは、それは確かに構成原理 とも矛盾します。排中律を許可しない理論は、関数存在原理 も検証しません。 ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle {\mathrm {AC} }}$${\displaystyle {\mathsf {ZF}}}$${\displaystyle {\mathrm {AC} }}$

では、 は、すべてのベクトル空間に対して基底が存在するという命題と同等です。したがって、より具体的には、有理数上の実数のハメル基底の存在の問題を考えてみましょう。このオブジェクトは、その存在を否定したり有効にしたりするさまざまなモデルが存在するという意味で、とらえどころのないものです。したがって、ここでは存在を否定できないと仮定することも、一貫して否定できないという意味で、一貫しています。また、その公理は、そのようなハメル基底の集合は空ではないと言うことで表現できます。構成的理論では、そのような公理は単純な存在公理よりも弱いですが、（意図的に）ハメル基底が存在しないことを意味するすべての命題を否定するのに十分強いです。 ${\displaystyle {\mathsf {ZF}}}$${\displaystyle {\mathrm {AC} }}$ ${\displaystyle {\mathsf {ZF}}}$

古典論理では、存在する集合は空でない集合と同じであるため、空でない集合を含みながら「存在する」という条件を満たさない古典的な意味でのモデルを生成することはできません。 ${\displaystyle X}$${\displaystyle X}$

しかし、2 つの概念を区別するKripke モデルを 構築することは可能です。すべての Kripke モデルにおいて、直観主義論理で証明可能な場合にのみ含意が真となるため、これは実際に、「空でない」が「人が居住している」を意味することを直観的に証明することはできないことを確立します。 ${\displaystyle M}$${\displaystyle X}$${\displaystyle X}$

• 交差（集合論）  – いくつかの集合のすべてに共通する要素の集合
• 無 – 何も存在しないこと。すべての反対
• 型理論における型の居住。

• D. ブリッジズと F. リッチマン。1987 年。構成的数学の変種。オックスフォード大学出版局。ISBN 978-0-521-31802-0 

この記事には、 PlanetMathの Inhabited セットの資料が組み込まれており、これはCreative Commons Attribution-Share-Alike Licenseに基づいてライセンスされています。