最小元 ∃a.∀x.a≦x 準備 Γ |-? ∃a.∀x.∃z.(a + z = x) 証明 証明要求： Γ |-? ∃a.∀x.a≦x BEGIN ∀-BOX var u 0 + u = u --[●∃導入 t:←左辺のu] ∃t.0 + t = u 0 ≦ u --[●∀導入 x:←u] ∀x.(0 ≦ x) END ∀x.(0 ≦ x) --[●∃導入 a:←0] ∃a.∀x.(a ≦ x) 最大元 ない。 足…

困った事と対策： aはbの約数である（bはaの倍数である）ことを表す（広く合意された）記号がない。 縦棒 | を使うことがあるが、使い勝手が悪い！ Unicode一覧を見ると、⊑（U+2291） と ⊒（U+2292） がある。 これを使おう。 定義： aはbの約数である ⇔ a⊑b…

参考： 引き算と無限個の足し算は両立しない - 檜山正幸のキマイラ飼育記 モノイドや半環は、群や環とはかけ離れている - 檜山正幸のキマイラ飼育記 定義 集合Lの定義 L := {(x, y)∈N2 | x≦y } (x, y)∈L ⇔ ∃z.(x + z = y) 関数subtの定義 function subt := λ…

x ≦ x 準備 Γ |-? ∀x∈N.(x ≦ x) ---------------------------------- Γ |-? ∀x∈N.∃z∈N.( x + z = x) ---------------------------------- Γ, x∈N |-? ∃z∈N.( x + z = x)証明 証明要求： Γ, x∈N |-? ∃z∈N.(x + z = x) x + 0 = x ---(1) -----------------[●∃…

Even(n) :⇔ ∃p.(n = 2p) のもとで、 ∀n.(n%2 = 1 ⇔ ¬∃p.(n = 2p)) を示す。 Γ |-? ∀n.(n%2 = 1 ⇔ ¬∃p.(n = 2p)) -------------------------------------------------- Γ, n∈<b>Z</b> |-? n%2 = 1 ⇔ ¬∃p.(n = 2p) -------------------------------------------------…

定義 Even(n) :⇔ ∃p.(n = 2p) Odd1(n) :⇔ ¬Even(n) Odd2(n) :⇔ ∃p.(n = 2p + 1) Odd3(n) :⇔ ∃p.(n = 2p - 1) Odd4(n) :⇔ n%2 = 1 問題 Odd1, Odd2, Odd3, Odd4は同値であることを示せ。

全称記号の導入 x∈X は任意とする。 ： P(x) xは任意だったから、 ∀x.P(x)含意導入 Pと仮定する。 ： Q Pを仮定していたから、 P⇒Q存在命題からの言い回しが難しい。 ∃x.P これを満たすxをaとする。 ： Q例題 定義 Even(n) :⇔ ∃p.(n = 2p) ターゲット Even(n…

奇数とは、2で割って1余る数 偶数とは、2で割り切れる数 奇数とは、偶数でない数 偶数とは、2n と書ける数 奇数とは、2n + 1 と書ける数 奇数とは、2n - 1 と書ける数 「とは、」の前も文になる。文には主語が必要。主語は、日本語なら「は」「が」の前に置…

beliefの訳語は信念だが、どうしても宗教／政治／人生とかの雰囲気がするので、確信にする。確信の表現とは、命題の集合へのマーキング（マーク付け）だと言える。 ○ … 確信を持って真（ほんと、正しい） × … 確信を持って偽（うそ、間違い） ? … どちらか確…

Mizarは（潜在的には）イプシロン記号で関数を定義している。同じ方法で定義するとして、 関数 部分関数 スコーレム関数 定義形式は仮にだが、 function foo:X->Y := λx∈X.εy∈Y.P(x, y) partial function foo:X->Y := λx∈X.εy∈Y.P(x, y) Skolem function foo…

次の命題を考える。 ターゲット命題： fが各点で連続ならば連続 通常は無意識に使っている選択公理の使い所が分かるように書いたので、証明が長くなった。記号の乱用記号の乱用をして、位相空間とその台集合を同じ記号で表す、つまり、X = (X, OX) のように…

途中までだ。A⊆N が、次の3つの性質を持つとする。 Aは空ではない ---(1) n∈A ⇒ -n∈A ---(2) n, m∈A ⇒ n+m∈A ---(3) このとき、非負整数kがあって、 n∈A ⇔ nはkの倍数 ---(4) 上のパラグラフをまとめると、 $(1)∧$(2)∧$(3) ⇒ ∃k st 非負整数.$(4) しかし、条…

とりあえず、分かりやすいのだけ列挙する。⇒導入 Aと仮定する。 ： Bである。 以上により、したがって、 A⇒B である。∧導入 Aである。 ： Bである。 $(A)だったので、したがって、 A∧Bである。∨除去 A∨Bである。 場合分けをしよう。 Aの場合： : Cである。 B…

以前、次のようなことを書いた。 哲学的(?)議論の形式化 - 檜山正幸のキマイラ飼育記 メモ編 哲学的(?)議論の形式化 2 - 檜山正幸のキマイラ飼育記 メモ編 結局、用語の定義も推論に使っている論理もよく分からないので、言ってることも意味不明ということだ…

集合と論理の練習問題： ツリー状の集合族 - 檜山正幸のキマイラ飼育記

目標設定文〈ターゲティング文〉：証明すべきターゲット命題を明らかにする。ターゲティングの時点では、ターゲット命題はもちろん証明されてない。 結論付け文〈コンクルーディング文〉：ローカルであれグローバルであれ、ターゲットが証明されて、定理にな…

ド・ラーム・コホモロジーとホッジ分解のオモチャ (2/2) - 檜山正幸のキマイラ飼育記の証明部分（枠内）は、半形式的になるように意識したのだが、そのとき感じた雑多なこと。 任意のxを選ぶ。 xを任意とする。 任意のxに対して 以上は同義で、自由変数xを含…

次の区別は曖昧。 …により …から …を使って 「により」と「から」は同義だと思っていいが、「使って」は例えば証明シェマ（マクロ）を使うことに限定するとかの用法もある。ただし、「定理命題を使う」と「証明シェマを使う」の境界も実はあいまい。 A∈Γ | B…

自分が使っている言葉をとりあえず列挙する。メタな言明 …（命題）が言える。 行為の予告 …を計算する。 …を示す。 …を示そう。 行為と結果 …（行為する）と、 文と文のあいだの接続詞 …（命題）(に)?より、 …（命題）から、 …（命題）なので、 …（命題）(だ…

カリー／ハワード対応を信じるなら、関数の記述と定理の証明はまったく同じはず。だったら同じ書き方ができるはず。 // f:X×Y→Z function f given x:X, y:Y ensures Z begin ... end // t:A∧B→C theorem t given a:A, b:B ensures C begin ... end関数定義に…

定理記述 - 檜山正幸のキマイラ飼育記 メモ編の続き。少し変える。 theorem 定理の名前 import モジュール1, モジュール2 for 宣言1, 宣言2 given 命題1, 命題2 ensures 命題 begin 証明 end endproofという語は避けた。 圏論 論理 始対象 False 終対象 True…

コマンドは、先頭が動詞原型または動詞過去分詞形、それに続いてキーワード目的語名詞が続いてもいい。apply, make conjunction, found inconsistency など。「命題 by 根拠名詞 引数並び」でも証明が書けるとする。以下、根拠名詞とコマンド動詞の対応表。 …

命題、証明、規則をそれぞれ0-射、1-射、2-射の意味で使う。 公理 公理証明 ax_A : * -> A * ----[ax A] AAx⊆|C| なので、Axは命題の集合として与えられるが、それはデカルト閉圏の特殊事情で、一般には、 a : X -> A X ---[a] Aつまり、Ax⊆Mor(C)。Axはどん…

こんな感じかな。 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）が登場したら、適当な変域の自由変数（または全称束縛変数）と解釈する。 前提 次は前提（既に知っているもの）とする。':⇔' は '⇔' と同じだが、定義…

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) …