未ログイン ／
ログイン
← ファイル一覧
（保存にはログインが要ります）
0_tutorial/4.book
ヘッダ
行番号
title 高度な表現 author admin import /common/word_logic formel /common/default thmel /common/min
section 高度なword subsection word関数 txt 次のwordも（importした word_logic.book で）紹介されていて、良く使用されます。gramの \({\tt x}\),\({\tt y}\),\({\tt z}\) には s,c,p が入ります。 word {/} lower {/} txt `x {/}= y` の<code>FCL</code>変換は `¬(x = y)` です。txtにおいて{/}と=の間には<b>スペースを入れません</b>。 txt なお `$..p` は2項記号の穴です。 txt ------------ txt 次のThmは引っ掛かりやすいかもしれませんが、きちんと査読が通ります。 thm `⊥` ◀ `x {/}= y` prf `⊥` -| `x {/}= y` p; txt これは一階論理の性質です（sosからは `x {/}= x` が出ます）。 txt 査読は「<b>書いた通り</b>」に行われます。「相異なる2つの x, y」のつもりでもそうはなりません。 br txt あなたが査読器に疑念を抱いたなら、それは正しい姿勢でしょう。その<note>健全性<?>Matheliaは OK を出すとき、「これがあなたの書いたThmです」から始まり、「この段階では、この規則で書き換えられてこうなっています。」の繰り返しを提示できねばなりません。</note>は最重要視されるものです。 txt 上のprfの査読では、査読器が ‘⊥‘ ◁ ‘¬ (x = y)‘ をprover+に投げ、それが<note>コレ<?>formulas(sos).(- (x = y)).end_of_list.formulas(goals).$F.end_of_list.</note>を作ってProver9に投げ、length:2の証明が見つかっています。 subsection [ ] word txt wordを「対象」とする表現があります。`=` についての性質を記述したいときに `[=]` で一つの個体のように扱います。 word :R :T :X lower :R lower :T lower :X br txt `:R&:T` のようなwordは自動で作成されます。 lower :R&:T txt 「`=`は同値関係」ということを表現できます。 thm `[=] :R&:T&:X` ◀ O prf `[=] :R&:T&:X` -| O p; subsection 2項記号の関数化 word {*} lower {*} txt `[?f] {*}= [?g]` は「`?f` と `?g` が恒等的に等しい」と読まれます（?f, ?g は [ ] で囲みます。囲まずに <code>?f {*}= ?g</code> と書くと「wordの引数が不足しています」になります）。 word {**} lower {**} thm `[??p^] :R ⟺ [=] {**}⇒ [??p^]` ◀ O prf goal -| O p; newpage section 定義、定義による展開 subsection 定義を集めた列 \(\mathbb{W.}\) txt 集合論の最初に出てくる記号に次があります。 word ∈ ⊂ txt `⊂` は次の定義を持ちます。一般に 〇. は 〇の定義 という位置づけになります。 prop ⊂. <- `X ⊂ Y ⟺ [ ∀ x ∈ X . x ∈ Y ]` txt `=` にも定義があるという扱いが便利です。\(\Longleftarrow\) は外延性公理と呼ばれることが多いですが。 prop =. <- `X = Y ⟺ ∀ x \, (x ∈ X ⇔ x ∈ Y)` br txt <note>Book内の自動変数<?>査読器はBookを上から読んでいきデータを記憶していきますが、この変数も保持します。</note>が使用されます。 txt \(\mathbb{W}.\) は「〇. (〇 はgramにcを含まない) という形のpropすべての列」です。この段階では ⊂. =. です。 txt \({\tt P}\) ◀ \(\mathbb{W}.\) は「定義から\({\tt P}\)が示される」と読まれます。必要な定義を一々書くのはめんどくさいので、この形が好まれます。 prop/thm =.. ◀ W. prf =.. -| W. p; br txt 一般には、Prover9に投げるときにはsosには必要なものだけを書く方がよいです。 txt 上の <code>prf =.. -| W. p;</code> は、W. の代わりに <code>⊂. ,, =.</code> と書いても同じで、length:37 です。 txt \(\mathbb{W}.\) が無限列になったとき(例えば `\n` を含むwordの定義が与えられたとき)は -| W. p; とはできません。 subsection slash計算 txt / はThmelの2項演算（Riteに作用する）で、\({\tt A}\) / \({\tt P}\) は「\({\tt A}\) を \({\tt P}\) で展開したもの」です。例えば txt =.. / =. … `∀ x \, (x ∈ X ⇔ x ∈ Y) ⟺ [ chain X ⊂ Y ⊂ X ]` br txt 列 \(\Gamma\) に対しても、自然に \({\tt A}\) / \(\Gamma\) は定義されます。 txt 上のThmのprfを新しいものにしてみます。 thm =.. ◀ W. prf =.. / W. -| O p; =.. -| W. h; txt prfの1段目に注目して下さい。Thmelで展開計算を済ませたことにより、Prover9へsos Oで渡せます。goalはかなり長い式になりますが、length:28に減ります。 br txt // W. は / W. / W. になります。 txt 1回の / W. の計算は次の規則です：式を内側の部分式から順に見て、各部分式を<b>1回だけ</b>、その頭の語の定義 〇. で書き換えます（頭が ∈ の所属 <code>t ∈ f(…)</code> なら、右側の語 f の定義を使います。定義の形に合わなければそのまま）。書き換えでできた式は、その回ではもう書き換えません。例えば <code>X ∩ Y ⊂ X</code> / W. では ⊂ が開いて <code>w1 ∈ X ∩ Y</code> が新しく現れますが、これが開くのは次の / です。 txt <code>W.!〇.</code>（空白を入れずに書く）は W. から 〇. を除いた列です。 txt / のすぐ後に数字を書くと、その場所のみを展開します。例えば \({\tt A}\) /1 \({\tt P}\) は「\({\tt A}\) の1番要素のみを \({\tt P}\) で展開したもの」。 txt / W. は goal の中の `=` も =. で書き換えます（`X = Y` が `∀ x (x ∈ X ⇔ x ∈ Y)` になります）。`[⊂] :R&:T` のような [ ] word を含む式にも効きます。 txt 同じThmを <code>-| W. p;</code>（定義を sos に置く）でも <code>/ W. -| O p;</code>（先に展開する）でも示せることが多いです。定義が増えて sos が大きくなると、先に展開する方が有利になります。 txt slash でどう書き換わるかは、証明器に投げずに確かめられます：<code>cd /var/www/test2.atp-research.com && php wp-content/themes/lightning/mathelia/slash_cli.php 0_tutorial/4 '`X = Y ⟹ Y ⊂ X` // W.'</code>。本が最後までに紹介した定義（W.' は本の中で証明した 〇.' も）で計算し、結果を前置記法（<code>[∀ w1 [⇒ …]]</code>）で出します。/ の本数を決めるときに、開かずに残った記号が無いかを見るのに使います（6b.book）。 newpage section Matheliaの高度な機能の例 subsection whole+オプション txt <i>prover+</i> はThmのgoalを、次の規則で<b>断片</b>に割り、断片ごとにProver9に投げます。すべての断片が証明できたとき、そのThmを証明したことになります。 txt \({\tt P}\) and \({\tt Q}\) → \({\tt P}\) と \({\tt Q}\) txt \({\tt P}\) ⇔ \({\tt Q}\) → \({\tt P}\) ⇒ \({\tt Q}\) と \({\tt Q}\) ⇒ \({\tt P}\) txt (\({\tt P}\) or \({\tt Q}\)) ⇒ \({\tt R}\) → \({\tt P}\) ⇒ \({\tt R}\) と \({\tt Q}\) ⇒ \({\tt R}\) txt これらは ⇒ と ∀ の右側にも、割れなくなるまで繰り返し適用されます。例えば次のThmの査読では、Prover9に2つの問題（⊤ と ⊤）が投げられます。 thm `⊤ and ⊤` ◀ O prf `⊤ and ⊤` -| O p; txt 割らずに1つの問題として投げるには、段の末尾の投げ先を <span style="color:brown">p[whole];</span> と書きます。 br txt `\n` の入ったThmも扱えます（prfは有限個のnに対してのみ）。 prop/thm ⇔\n ◀ O at \n=2..5 prf ⇔\n -| O p[whole]; txt 割るとProver9への問題は n=2..5 で34本、割らなければ4本です（n=2..8 だと91本と7本。Thm査読の時間は約4.1秒と約3.3秒）。断片が自明なので、本数だけ起動コストが増えます。 txt ただし一般には割る方が速く（割ると、どの断片が落ちたかまで分かり）、<span style="color:brown">p[whole];</span> は ⇔\({\tt n}\) のように断片が自明な行だけに使います。
表示（保存しません）
保存にはMatheliaへのログインが要ります。