まずは、言葉の問題。同義語らしきもの。 agent, player, voter, member, stake holder, participant alternative, candidate, (political) option, policy, social status agreement, consensus permutation, ordering, ranking rule, method, algorithm es…

Pは変数を持つ命題だとする。 Pを事実だと認識する。 Pを信じる。 同じだろうか？ Pの具体例（変数への代入例）を確認する能力／手段がある。 Pのすべての具体例を確認する能力／手段がある。 変数の領域が無限なら、すべての確認はできない。だから、無限領…

宗教や政治とは離れて、論理として信念体系〈belief system〉を考える。述語論理の体系Lを固定して、命題とはLの論理式のことだとする。命題と述語は区別せずに、命題＝述語の全体はPredとする。ただし、議論域があるので、X上の命題はPred[X]とする。Pred[-…

up-to-isoの話をするとき、up-to-isoで決まる性質は、個体に貼り付いているというよりは、全体構造のなかで個体に与えられた役割と解釈すべき -- という話を僕はするのだが、個体の属性と役割の区別は難しい。N君が、距離空間の勉強をしていて、距離空間XとA…

変数 実体 変数名 実体名 変数の値 実体の集合 変数の型 実体の型 値の集合 集合の集合 変数の型＝変数の値の集合 実体の型＝実体の集合の集合＝実体の可能的全体集合 文字実体の場合だと、次の多義性がある。 文字実体＝実体'文字'＝'文字'という名前の実体…

図のテキスト表現 符号化ERA図 { 実体 学生; 属性 学年:学生→int; 符号化 番号:学生→int; } 符号化ER図 { 実体 学生, コース; 関連 履修(学生, コース); 符号化 <氏名, 生年月日>:学生→string×date, コース名:コース→string; } 符号化ER図 { 実体 学生, コー…

方言識別マーカー 長い名前 代替語の使用 同義語併記 異義語併記 方言識別マーカー 特定分野の方言はそれと分かるようにマークする。例： 《タプル》 《リレーション》 長い名前 多義語の片方（あるいは両方）を形容詞・副詞で修飾する。 線グラフと関数グラ…

型＝データ型＝集合 基本型＝基本データ型＝基本集合 直積型構成子 直積型＝直積データ型＝直積集合 直積型＝タプル型 ペア型⊆タプル型 ベキ集合型構成子＝ベキ型構成子 { {ベキ集合}{型 | データ型} | {ベキ}{型 | データ型 | 集合} } {制約 | 制限}{_ | 条…

int = Int を許容するリーズニング（アブダクション） S('int') = Int --------------------------------[アブダクション] let int = S('int') int = Int S('檜山') = (生きている人間・檜山) ---------------------------------[アブダクション] let 檜山 =…

「バベルの塔」問題 「アブダクション」問題 バベルの塔 - Wikipedia 神は降臨してこの塔を見「人間は言葉が同じなため、このようなことを始めた。人々の言語を乱し、通じない違う言葉を話させるようにしよう」と言った。このため、人間たちは混乱し、塔の建…

一般的な有限性は： 典型的有限集合 {1, ..., n} と同型 自分自身への単射で同型でないものが存在しない（自身自身への単射は常に同型） とかで定義する。自然数内の有限集合に関しては、上界の存在で定義できる。これはけっこう使いみちがある。例えば、集…

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

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

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

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

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 …との選言を作…

αを名前を表すメタメタ変数として： 項メタ変数 %α 命題メタ変数 _α 式パスメタ変数 @α 自然言語（英語）としての自然さよりは、人工言語としての整合性を重視する。使う前置詞： 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“上の”同値…

一般的な状況に探りを入れるために、特殊ケースを考えるのは有効だ。例えば： 一般にRnだが、n = 1, 2, 3を考える。 一般に集合Xだが、Xが有限集合のときを考える。 一般に多様体Mだが、S2, T2（トーラス）のときを考える。 だが、勝手に特殊な条件や仮定を…

忘れられない、捨てられない。 「蓄積された知識」を忘れられない オーバーロード、型クラス、 「複雑な思い」を忘れられない 感情を伴う関係を外延として捉える 「出会った頃」を忘れられない。ベクトルの矢印、集合は大文字。集合の集合で困難。 「ニュア…

3次元方向記述とその実現 - 檜山正幸のキマイラ飼育記 メモ編, 姿勢記述の色々 - 檜山正幸のキマイラ飼育記 メモ編 のオマケ／追加。*1 *1:記事： http://reset.etsii.upm.es/en/projects/robotic-arm/ 画像： http://reset.etsii.upm.es/en/uploads/pool__p…

特に文言がなくても、「示せ」。 半群Sで、単位元があるなら一意。 モノイドMで、x∈M の逆元があるなら一意。 Gは群。HがGの部分群であることは、x, y∈H ⇒ xy-1∈H とも言える。 クラインの四元群（four-group）Fを自分自身F上の置換群として表現せよ。 クラ…

HがGの部分群のとき、y-1x∈H で定義される同値関係を左同値と呼ぶようだ。左同値関係の同値類を左コセットと呼ぶ。ところが、左コセットは右作用の軌道なのだ。H左コセットをH[x]と書くと： H[x] = xH なぜなら：y∈H[x] ⇔ x H〜 y ⇔ x-1y∈H ⇔ y∈xH 。最後は…