証明シェル
A1, ..., Anを仮定（assume）してBを結論（conclude, entail, result, produce, show）する証明があるとき、その証明内で使っている暗黙の知識がある。これを証明の文脈とか環境と呼ぶ。で、文脈とは正確には何か？ が大問題。それと、トンネル論法（コンパ…
ざっと調べたが、雑でイイカゲンで未完成である。一般的な概念 モジュールとパッケージ：モジュールを集めてパッケージ パッケージマネージャ グローバルインストールとローカルインストール プロジェクト： 作業をするための環境 パッケージのメタ情報 パッ…
こんな感じかな。 theorem 定理の名前 require モジュール1, モジュール2 using 定義, 定理1, 定理2, 規則 for 宣言1, 宣言2 given 命題1, 命題2 holds 命題 proof 証明 end end考慮点は カンマの代わりにandか？ for given の繰り返しを許すか holdsの前にf…
タイトルが、 「影響を及ぼし合わない物的事象と心的事象がともにあるとする発言は経験的に真なる発言ではあり得ない」ことの証明。 物的事象がPhysicalのPで、心的事象がMentalのMかな？ 事象が未定義でアトミックなナニカだとすると、∀x.P(x)∨M(x) で M(x)…
たまたまみた http://sets.cocolog-nifty.com/blog/2017/11/post-ee0f.html に次のような"証明”(?)があった。 （前提1）すべての事象は、特性Ｐと特性Mのいずれか、または、両者を持つ。つまり、すべての事象は、特性Ｐのみを持つＰ事象か、特性Mのみを持つM…
最初の案： 暫定版 証明図シリアル化構文 - 檜山正幸のキマイラ飼育記 メモ編 その後の変更： 証明図シリアル化構文 キーワードの現状 - 檜山正幸のキマイラ飼育記 メモ編 BLKと書いてあるのはブロック、そうでなければコマンド。 論理記号 導入 削除 ∧ make…
x is P ⇔ P(x) x1, ..., xn are P ⇔ P(x1, ..., xn) A equals B ⇔ A = B x in A ⇔ x∈A A on/within X ⇔ A⊆X x = y over X ⇔ x, y∈X ∧ x =X y
人と人とのコミュニケーションを目的にするので、機械可読ではない。特に、新しい変数（fresh variable）が登場したら、適当な変域の自由変数（または全称束縛変数）と解釈する。 前提 次は前提（既に知っているもの）とする。':⇔' は '⇔' と同じだが、定義…
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…
いくつかの事例、シーケント推論図の形式： [Γ→Δ],[Π→Σ]⇒Γ,Π→Δ,Σ Γ→Δ Π→Σ ===============(×) Γ,Π→Δ,Σ [Γ→Δ,A], [A,Π→Σ]⇒[Γ,Π→Δ,Σ] (A has ↓) Γ→Δ,A A,Π→Σ ====================(＼↓A) Γ,Π→Δ,Σ [Γ→Δ,A],[Π→A*,Σ]⇒[Γ,Π→Δ,Σ] (A has ↓) Γ→Δ,A Π→A*,Σ =========…
自然演繹の欠点を克服したい。 自然演繹とシーケント計算を別々に扱うのではなくて、融合・統合して一体として扱いたい。 証明オブジェクトと証明オブジェクトの操作であるリーズニングを区別したい。そして、曖昧性を排除したい。 人間が通常行っている混合…
用語法を注意しないといけない。 証明： 順方向証明か逆方向証明か曖昧 証明： 証明オブジェクトかリーズニングか曖昧 証明図： 自然演繹の証明図かシーケント計算の証明図か曖昧 自然演繹の証明図： テキスト証明図かピクチャー証明図か曖昧 基本的に証明は…
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) …
論理式（formula）は極性（ポラリティ polarity, 符号 sign）を持つとする、正負号（positive sign）と負符号（negative sign）。正負号は省略してもよい。（書き方は後で）正（極性が正）の論理式の集まりを論理資産（logical asset(s)）、負の論理式の集ま…
前提（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 …
キーワード 意味 備考 target 目標は…である。 proof end （これから）証明しよう。 set …と置く。 by the way ところで リーフの開始 remark …であることを注意しておく。 concat …との連言を作る。 ∧導入 select …を抜き出すと、 ∧除去 add …との選言を作…
αを名前を表すメタメタ変数として： 項メタ変数 %α 命題メタ変数 _α 式パスメタ変数 @α 自然言語（英語）としての自然さよりは、人工言語としての整合性を重視する。使う前置詞： 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…
