絵図形式 左に a を入れるの省略。 f f η| | ∩| | ||| ≡ | |∪ | |ε | f f 自然演繹形式 (1)から(6)の番号は絵との対応を取るためのもの。 snake::: (a.η*f);(a.f*ε) ≡> a.f^ {(a.η*f);(a.f*ε) :: True ⇒ a.f≦a.f True ==================================[du…

Title: A comparison of the mathematical proof languages Mizar and Isar Markus Wenzel, Freek Wiedijk Pages: 24p URL: http://www4.in.tum.de/~wenzelm/papers/romantic.pdf P.24からの引用（画面ショット） 証明している定理は： for every number n t…

*1*2 *1:記事： https://kotobank.jp/word/%E4%B8%8A%E8%85%95-533810 画像： https://kotobank.jp/image/dictionary/daijisen/media/112911.jpg ローカル： human-arm_112911.jpg *2:記事： https://kotobank.jp/word/%E8%85%95-34946 画像： https://kotob…

*1*2*3*4バックホーとユンボの違い（習慣的用法）については： https://detail.chiebukuro.yahoo.co.jp/qa/question_detail/q1013051685 *1:記事： http://www.cranenet.or.jp/tisiki/syoberu.html 画像： http://www.cranenet.or.jp/tisiki/images/syoberu0…

いくつかの事例、シーケント推論図の形式： [Γ→Δ],[Π→Σ]⇒Γ,Π→Δ,Σ Γ→Δ Π→Σ ===============(×) Γ,Π→Δ,Σ [Γ→Δ,A], [A,Π→Σ]⇒[Γ,Π→Δ,Σ] (A has ↓) Γ→Δ,A A,Π→Σ ====================(＼↓A) Γ,Π→Δ,Σ [Γ→Δ,A],[Π→A*,Σ]⇒[Γ,Π→Δ,Σ] (A has ↓) Γ→Δ,A Π→A*,Σ =========…

自然演繹の欠点を克服したい。 自然演繹とシーケント計算を別々に扱うのではなくて、融合・統合して一体として扱いたい。 証明オブジェクトと証明オブジェクトの操作であるリーズニングを区別したい。そして、曖昧性を排除したい。 人間が通常行っている混合…

用語法を注意しないといけない。 証明： 順方向証明か逆方向証明か曖昧 証明： 証明オブジェクトかリーズニングか曖昧 証明図： 自然演繹の証明図かシーケント計算の証明図か曖昧 自然演繹の証明図： テキスト証明図かピクチャー証明図か曖昧 基本的に証明は…

推論（正確にはリーズニング）に関して次の4分類をする。 正しい 間違っている 受け入れやすい 問題なし 誤用（アブダクション） 受け入れにくい 難解 問題なし 推論を順推論（通常の推論）と逆推論（バックワードリーズニングの原子ステップ）に分ける。問…

1. 連言 ∧ A B A∧B ------ ------ A∧B A - A∧B -A -------(分割統治) --------(過剰責務) -A -B - A∧(B) 2. 選言 ∨ A A∨B [A |- C, B |- C] ------- ------------------------- A∨(B) C - A∨B -C -------(投機) ----------------------------- -A - (A)∨(B) …

Isarのbyはボディがない証明（proof eqd）の略記。byの直後は証明メソッド。 Mizarは推論規則の適用とスキーマの適用をby, fromで区別するが、Isarは高階論理なのでbyだけ。 Isarの前置fromはMizarのfromとは別。Mizarのby相当らしいが要チェック。 Isarの前…

証明は、複合証明 proof ... qed か、自動証明 by ... のどちらか。 自動証明の根拠と複合証明のヘッダ部には証明メソッドが書かれる。 複合証明の本体（ボディ）部は、文（ステートメント）の列。 文（ステートメント）は次の種類： fix文 自由変数の宣言 a…

論理式（formula）は極性（ポラリティ polarity, 符号 sign）を持つとする、正負号（positive sign）と負符号（negative sign）。正負号は省略してもよい。（書き方は後で）正（極性が正）の論理式の集まりを論理資産（logical asset(s)）、負の論理式の集ま…

2018年封切り予定の映画『Proud Mary』 http://www.imdb.com/title/tt6421110/ はアクション映画。アクションが主体かどうかは分からないが、アクション要素はあるはず。ヒロインを演じるのはタラジ・P・ヘンソン（Taraji Penda Henson）、1970年9月11日生ま…

前提（premise; プレミス）は次のもの達の総称する。 公理（axiom） 定理（theorem） 仮説（hypothesis, 複数形 -ses） 仮定（assumption） 公理と定理はどちらも論理式またはシーケントで、表現形式上の差はなくて（Mizarでは公理と定理の区別はない）、定…

集合のド・モルガンの法則の証明（順証明、フォワード証明）http://d.hatena.ne.jp/m-hiyama-memo/20170810/1502363526 の最後のほうは、 // SerND (x∈X)∧¬(x∈A) ∨ (x∈X)∧¬(x∈B) contract $.1, $.2 by (集合の差) (x∈X＼A) ∨ (x∈X＼B) contract by (集合の合…

記号的には、 [x1:t1, ..., xk:tk | A1, ..., An |- B] 最初はk個の変数型宣言。型理論で言う型環境。 次にn個の前提（仮説）論理式。 1個の結論論理式。 出現するすべての変数は型環境で型付けされている。 自然言語風の記述は： for x1:t1, ..., xk:tk giv…

オペラッドの射をオペ射と呼ぶ。オペラッドのホムセットをオペホムセットと呼ぶ。オペホムセットを O(A, B⇒C) のように書く。⇒の左が空なら終対象を置き、右が空なら始対象を置く。ニ様なシーケント（http://d.hatena.ne.jp/m-hiyama-memo/20161026/14774513…

環境として、論理環境（logical environment）と応用固有環境（application-specific environment）がある。論理環境は、論理定理データベースと論理推論規則データベースからなる。応用固有環境は、応用固有定理データベースと応用固有推論規則データベース…

"Preface: Twenty Years of the QED Manifes" というPDF文書がある。これはアクセスするとダウンロードされてしまう2ページの文書。ここで要約しておく。QEDマニフェストとワークショップが1994,5,6あたりに行われたので、2014,5,6あたりで20周年になる。当…

Natural Deduction Mizar SerND → introduction assume assume + use → elimination – apply ∧ introduction thus concat ∧ elimination – select ∨ introduction – add ∨ elimination per cases cases ∀ introduction let for ∀ elimination – instantiate …

逆像のf-1 を f^* と書く。 // SerND 共通部分の逆像 target f^*(C)∩f^*(D) = f^*(C∩D) proof target f^*(C)∩f^*(D) ⊆ f^*(C∩D) proof assume x∈(f^*(C)∩f^*(D)) ---(ass) expand by (集合の共通部分) x∈f^*(C) ∧ x∈f^*(D) expand $.1, $.2 by (写像の逆像) …

// SerND 集合のド・モルガンの法則target X＼(A∩B) = (X＼A)∪(X＼B) proof target X＼(A∩B) ⊆ (X＼A)∪(X＼B) proof assume x∈X＼(A∩B) ---(ass) expand by (集合の差) x∈X ∧ ¬(x∈A∩B) expand $.2.1 by (集合の共通部分) x∈X ∧ ¬(x∈A ∧ x∈B) rewrite $.2 by …

名前の管理が甘い、名前空間が粗末 ユニコードを考慮してない。アスキー偏重。 Mizar以外は、スクリプト言語またはそのシンタックスシュガー。 ブロック構造を意識してないか曖昧。 文書構造を意識してないか粗末 型クラスがあと付けで歪んでいたり問題を抱…

キーワード 意味 備考 target 目標は…である。 proof end （これから）証明しよう。 set …と置く。 by the way ところで リーフの開始 remark …であることを注意しておく。 concat …との連言を作る。 ∧導入 select …を抜き出すと、 ∧除去 add …との選言を作…

Mizar Isar let fix assume assume set let set def consider ... such that obtain ... where take (no equivalent) per cases ... proof ... qed suppose next assume (no keyword) have thus show hence then show thesis (?thesis) proof ... end proof …

wired ワイヤード weird ウィアード 異様な、不気味な

αを名前を表すメタメタ変数として： 項メタ変数 %α 命題メタ変数 _α 式パスメタ変数 @α 自然言語（英語）としての自然さよりは、人工言語としての整合性を重視する。使う前置詞： by with to of from byとwithは区別しない。by/withはどちらでもいいことを示…

次を示す。 f(A)＼f(P) ⊆ f(A＼P) 下に、清書したフォワードプルーフ。作業的にはバックワード探索をしている。使う（一部未使用）定義、論理法則、推論規則： DefSetInc: A⊆B :⇔ ∀x.(x∈A ⇒ x∈B) DefSetDiff: X = A＼B :⇔ ∀x.(x∈X ⇔ (x∈A ∧ ¬(x∈B))) DefSetD…

円周の対蹠点の同一視*1交差させて縫合*2クロスキャップ*3 *1:記事： https://topologia.wordpress.com/2008/12/25/5-el-plano-proyectivo-y-la-cinta-de-mobius/ 画像： https://topologia.files.wordpress.com/2008/12/plano-proyectivo.gif?w=480 ファイ…

僕が失敗した最近の例 r2 = x2 + y2 (x, y, r ≧ 0) 両辺の平方根を“取って” r = √(x2 + y2) この「取って」がマズかった。なぜなら、「取ってないで付けているじゃないか」と。こういうのは一種のジャーゴンかもしれない。 K“上の”ベクトル空間V A“上の”同値…