4 基本記号②

4.1 一意量化子

abbr … \(! x P\) ≈ \(\forall y , z \in \{ x \mid P \} . y = z\)
abbr … \(\exists! x P\) ≈ \(\exists x P , ! x P\)
abbr … \(! x \mathop{{\sf A}} . P\) ≈ \(! x ( x \mathop{{\sf A}} , ( P ) )\)
abbr … \(\exists! x \mathop{{\sf A}} . P\) ≈ \(\exists! x ( x \mathop{{\sf A}} , ( P ) )\)

4.2 集合となるクラス

word(c,p) … \(\dot\exists\)
Exi. … \(\dot\exists C \Longleftrightarrow \exists X \, ( X = C )\)

word(,c) … \(\mathbb{V}_0\)
𝕍0. … \(\mathbb{V}_0 = \{ x \mid x \notin x \}\)
\(\neg \dot\exists \mathbb{V}_0\) \(\blacktriangleleft\) O

置換公理
schema ax_r(??p^;x,y;C_) := \(\forall x \, ! y \, x \mathbin{p} y \Longrightarrow \forall X \, \dot\exists \{ y \mid \exists x \in X . x \mathbin{p} y \}\)
分出公理
ax_s … \(\exists X \, C \subset X \Longrightarrow \dot\exists C\) \(\blacktriangleleft\) ax_r
\(\neg \dot\exists \mathbb{V}\) \(\blacktriangleleft\) ax_s

4.3 内包記法の拡張

abbr … \(\{ T \mid P \}\) ≈ \(\{ x \mid \exists \mathop{{\sf X}} ( ( P ) , x = T ) \}\)
abbr … \(\{ T \mathop{{\sf A}} \mid P \}\) ≈ \(\{ x \mid x \mathop{{\sf A}} , \exists \mathop{{\sf X}} ( ( P ) , x = T ) \}\)
abbr … \(_{ P } T\) ≈ \(\{ T \mid P \}\)
\(X = \bigcup _{ x \in X } \{ x \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

4.4 関数の像

word+(s,s→s,c) … \(\text{^}\)
lower … \(\stackrel{\text{^}}{\mathbin{{\sf f}}} A\) ≃ \(\{ \mathbin{{\sf f}} a \mid a \in A \}\)
word+(ss,s→ss,c) … \(\text{^*}\)  \(\text{*^}\)  \(\text{^^}\)
lower … \(A \stackrel{\text{^*}}{\mathbin{{\sf f}}} b\) ≃ \(\{ a \mathbin{{\sf f}} b \mid a \in A \}\)
lower … \(a \stackrel{\text{*^}}{\mathbin{{\sf f}}} B\) ≃ \(\{ a \mathbin{{\sf f}} b \mid b \in B \}\)
lower … \(A \stackrel{\text{^^}}{\mathbin{{\sf f}}} B\) ≃ \(\{ a \mathbin{{\sf f}} b \mid a \in A , b \in B \}\)