← ファイル一覧
（保存にはログインが要ります）
1_basis/4_NBG.book
ヘッダ
行番号
title 論理と集合・クラス author admin import 2_class
section クラスの量化 word ∀_ ∃_ txt 例えば `∀_ X_ P^` はp-Formになります。 txt これは「単ソート翻訳」はできません。単ソート翻訳では、ものは1種類しかなく、クラスは cvt規則 で溶けてしまいます。 !txt 溶けたクラスは走るものが無いので、クラスを走る変数は量化できません。`∀_ X_ P^` を単ソート翻訳へ送ると、理由を付けて断られます。 !txt <code>Prover9 cannot emit class quantification (TFL is single-sorted)</code> br txt 「多ソート翻訳」という翻訳があります。 !txt ここでは、その中でも「s,cをソートする翻訳」を紹介します。 txt 「s,cをソートする翻訳」では、s(集合) と c(クラス) を<strong>別のソート</strong>として持ちます。クラスは溶けずに「もの」のまま残るので、`∀_ X_ P^` はその c を走る量化になります。 !txt 現在のソートは s と c と f(写像) の3つです。ソートの本数は綴りに出しません。使わないソートがあっても、書いた式の意味は変わりません。 br txt -| が単ソート翻訳、--| が多ソート翻訳での導出を表します。表示はどちらも ◀ です。 !txt どの証明器に投げるかは prf の接頭辞(p-| v--| h--| など)が決めます。 txt prfのチェックにおいて、多ソート翻訳のthmはVampireに投げられことが多く、v--| と記載されます。 txt その際の「仮定」には \(\mathbb{W}_+.\) が追加されます。 txt \(\mathbb{W}_+.\) は「〇. (〇はその行に出てくる\(\mathbb{W}_+\)) という形のpropすべての列」です。この本の\(\mathbb{W}_+\)は ∈_ =_ \cls の3つなので、実際に添えられるのは =_. だけです。 txt \(\mathbb{W}_+\) の語は、単ソート翻訳では cvt規則 が定義を使い切ってしまいますが、多ソート翻訳では記号として残ります。だから定義が要ります。 txt \(\mathbb{W}_+.\) は \(\mathbb{W}.\) と違って ◀ の右には書きません。書きませんが、仮定に入ります。 txt `∈_` `\cls` `\fn` も \(\mathbb{W}_+\) ですが、定義propを持たない(意味を運ぶのは翻訳そのものです)ので \(\mathbb{W}_+.\) には関与しません。 txt なお、添えた定義の中に出てくる\(\mathbb{W}_+\)の語の定義は、添えられません。word family(\n を含むword)があると定義が無限個になるからです。その語は解釈されない記号のまま残ります。 txt 単ソート翻訳で示したことを多ソート翻訳の行で使うときは、関係をまたぐので「持ち上げ」が要ります。持ち上げてよいかは機械が確かめます。 section NBG のクラス存在公理 txt- NBG では下の B1〜B5 は<strong>公理</strong>として置かれます。ここでは内包記法 `\{ cls x | $P \}` の定義から<strong>定理として</strong>出ます。<br>各行の左辺に現れる内包項が、NBG が「存在する」と要請するクラスそのものです。<br> prop/thm NBG-B2 := `∃_ X_ ∀ x \, (x ∈_ X_ ⟺ x ∈_ A_ and x ∈_ B_)` --| O prf `∀ x \, (x ∈_ \{ cls y | y ∈_ A_ and y ∈_ B_ \} ⇔ (x ∈_ A_ and x ∈_ B_))` p-| O; NBG-B2 h--| O; txt B2（交わり） !txt ∃_ X_ ∀ x \, (x ∈_ X_ ⟺ x ∈_ A_ and x ∈_ B_) !let B2 := `∀ x \, (x ∈_ \{ cls y | y ∈_ A_ and y ∈_ B_ \} ⇔ (x ∈_ A_ and x ∈_ B_))` thm B2 -| O prf B2 p-| O; txt B3（補クラス） !let B3 := `∀ x \, (x ∈_ \{ cls y | y {/}∈_ A_ \} ⇔ x {/}∈_ A_)` thm B3 -| O prf B3 p-| O; !txt 順序対（B1・B4・B5 で使う） word \pr abbr pr txt B4（定義域） !let B4 := `∀ x \, (x ∈_ \{ cls y | ∃ z \, (\< pr y ; z \> ∈_ A_) \} ⇔ ∃ z \, (\< pr x ; z \> ∈_ A_))` thm B4 -| O prf B4 p-| O; txt B1（所属関係のクラス） !let B1 := `∀ x \, ∀ y \, (\< pr x ; y \> ∈_ \{ cls w | ∃ u \, ∃ v \, (w = \< pr u ; v \> and u ∈ v) \} ⇔ ∃ u \, ∃ v \, (\< pr x ; y \> = \< pr u ; v \> and u ∈ v))` thm B1 -| O prf B1 p-| O;
表示（保存しません）
保存にはMatheliaへのログインが要ります。