大分類 非形式 形式化データ 備考 計算 対象式 対象式（項） もともと形式化されている 論理 命題 論理式 文字列または構文解析木 論理 推論 推論図 仮定と結論がある 論理 リーズニング リーズニング図 ツリー状ノード・ワイヤー図 すべての形式化データは…

「一貫性」という言葉が曖昧だから整理する。まず、律子〈rator〉は法則を与える2-射（あるいはもっと高次の射）のこと。律子が満たす等式を制約等式〈constraint equation〉または等式的制約〈equational constraint〉または単に制約〈constraint〉と呼ぶ。…

ずーーっと、用語法の整理、使える用語／使えない用語の選別をしている。酷い状況であることはもちろん承知はしていたが、作業してみると、その酷さをまざまざと実感する。命題を表す変数を「命題変数」と呼びたいが、「命題変数」は命題論理 -- コンテキス…

推論のストリング図をテキストで表したものがシーケントだと解釈すると、通常のシーケント記法はダメなことがわかる。シーケント矢印が 推論のスパイダーを表す矢印 ケーブリングを表す矢印 の区別ができないと、ストリング図を書き写すことができない。次の…

演繹システムのパート分類（モジュラー／レイヤード設計・実装のため）： 分野固有パート 論理パート（分野によらない共通パート） 分野固有パートは： 個体レベル 型レベル 論理パート 命題レベル 推論レベル システムが単ソート〈single{- | }sort{ed}?〉…

メタ(形容詞)＝我々が生きている現実世界の … 対象(形容詞)＝我々が調査と考察の対象（目的物）とする数学的モデル（対象演繹システム）内の … 例： メタ記号 vs. 対象記号 メタ変数 vs. 対象変数 メタ命題 vs. 対象命題 メタ定理 vs. 対象定理 メタ側がモヤ…

推論を次のように規定する。 推論には必ずプロファイルがある。 プロファイルは仮定命題リストと結論命題リストからなる。 推論はラベル付きのときもあれば、ラベル無しのときもある。 推論は組み込みのときもあれば、ユーザー定義のときもある。 組み込み推…

名詞 動詞能動態 形容詞-済み 形容詞-可能 証明 × × ○ 推論は- ○ 推論は-、命題は- 推論 ○ △ 仮定が結論を- × × リーズニング ○ ○ 上式が下式を- ○ 推論は- ○ 推論は- 言い方の候補： Γ infers Δ Γ concludes Δ Γ derives Δ Γ entailes Δ ξ reasons η ξ conc…

マルチスクリーンムービー ムービーフィルム フレーム（のコンテンツ） 絵コンテ〈ストーリーボード〉 {絵コンテの{コマ | シート} | {ストーリー}?シート} シーン {アクション}?コマンド スクリプト（ActionScriptは固有名詞） スクリプトのユーザー定義関…

なんかもう、ひたすら単語の選択と（必要なら）造語をしている。いいかげんウンザリはしている。全般的に、用語法において、関数と関数を表す式と関数値の区別が付いてない／付けてないことが分かる。これは普遍的（どこでも見いだせる）な現象だ。関数まわ…

思い付いたことを順不同にダダーっと箇条書きにする。後で整理する。まだごった煮。先に意味領域： 集合の集合がある。小さい具象圏の対象集合 ＝ Type ＝ |Sem| 0, 1 はType内にある。0, 1∈Type 型がAの個体〈individual〉とは、1からのAへの射のこと。 関…

{絵|図|絵図}は、{figure | picture | diagram | drawing | painting | illustration | visual object} などがあるが、図＝diagram とする。ムービーのフレームのあいだのトランジションの制作には、図コンビネータ〈diagram combinator〉のコマンドを使う。…

オリジナルのゲンツェンLKでは、 公理は一種類（1パターン） 推論規則は左右それぞれ10種で合計20種 Cutが一種 合計で21種の推論規則 LK改では、 id:A ↔ A !:A → T π[1]:A, B → A π[2]:A, B → B Δ:A ↔ A, A α:A, B, C ↔ A, B, C （注記参照） λ:T, A ↔ A ρ:A…

ホントに酷い、腐っているとしか言いようがない。整理を試みれば試みるほどに酷さを痛感する。 「証明」は無理だ。使用しない。 「推論」を使う。ただし、「推論」と「リーズニング」はまったく別。 「定理」は使える。[追記]いや、使えないわ。[/追記] 絵図…

語源、由来、謂れ、いわく、物語、逸話 とかを要求されると困るのだが、人々はそれを求めるので、書いておく。 記号 由来 ! たぶん唯一性から ∃! と同じ由来 π projectionのp ι injectionのi Δ diagonalのd、それと形状の類似 λ leftのl ρ rightのr（rh） α …

以下の文章（引用ではない）内の「証明」「主張」は専門用語ではない。非形式的に使用している言葉。主張は assertion, declaration, claim, statement, judgement, thesis など。 証明とは、主張の正しさを保証するものである。その主張に至る過程も含めて…

展開＝マクロ展開＝expand で、いいと思う。展開の逆だが、 contraction, collapsing がある。contraction〈縮約〉はthinning〈水増し〉と対にもなる。水増しは複製〈duplication〉でもある。複製の逆は併合〈merge〉、unionではない。対になるべき語がうま…

言語・習慣・文化のせいで、せっかくの原則がうまく使えない例がカリー／ハワード対応。なんとかしてキレイに整理する。演繹システムでは不明瞭で、プログラミング・システムでは明瞭な概念： システム組み込み vs ユーザー定義 ライブラリによるシステムの…

http://d.hatena.ne.jp/m-hiyama-memo/20181102/1541141733の最後の余談を敷衍する。domain of discourse の訳語に論域を使う。すると、命題関数の域は論域となる。「論域＝命題関数の域」で事情が少しハッキリする。シーケントにおける自由変数の指定は、論…

記法バイアスと記法独立な把握： 順序随伴を例として - 檜山正幸のキマイラ飼育記では、 標準的テキスト記法の強烈なバイアスに支配されている、あるいは記法の獄舎に投獄されているからです。 自ら「記法の獄舎」に閉じこもりたい傾向（思考、指向、嗜好）…

一言でいうと節約原理。 ページ節約： 紙面とインクを使わない。リソース・コストの節約。 絵図排除： 絵図（イラスト・ピクチャー）を避けて活字組版で処理したい。人件費と時間の節約。 コピー排除： 手書きのとき、コピー（転記）を避けたい。手間の節約…

次の3つは区別されるべき。 計算指示としての式 例：算術式 計算結果としの値 例：自然数値＝算術値 計算する行為 計算をオペレーションと言い直すと： オペレーション指示としての式 オペレーション結果としの値 オペレーションする行為 値はオペレーション…

function strange-func(x:Func1Code):Void := if (halt(x, x)) then forever() else done() ; predicate strange-pred(x:Pred1Code) := ¬provable(x, x)Godはゲーデル符号化だとして、次の述語を考える。 halt(God(strange-func), God(strange-func)) : Bool…

基本的に2つの“世界”がある。構文世界〈syntactic {world | realm}〉と意味世界〈semantic {world | realm}〉。補助的にシステムの世界〈{world | realm} of systems | system {world | realm}〉があるとする。システムの世界に自立性はなく、各システムは、…

コミュニケーションの精度向上のため 命題のデータ化のため コミュニケーション精度向上のほうは、やることが望ましいが、必須ではない。がんばれば、自然言語でも伝わる。それに100%の形式はどうせ無理。常に必然的に宿命的に中途半端である。一方、命題の…

レイヤーは次元kでインデックスされる。kが動く範囲を次元範囲〈dimension range〉と呼ぶ。次元範囲Dとすると、D⊆Z で、Dは区間の形をしている。D = x..y の形で書く。次元範囲に渡るレイヤーの集まりをタワーと呼ぶ。レイヤーは横方向のスライスだが、縦方…

n-セオリーの立場からは、次は、次元や具体的状況が違うだけで同義になる。 変数状態 値割り当て 評価環境 リテラル（定数）解釈 データベース状態 データベースインスタンス 代数セオリーのモデル＝代数 基本命題の真偽値割り当て なんらかの意味のモデルイ…

Unicode A 𝔸 𝔸 C ℂ ℂ T 𝕋 𝕋 ℂ𝔸𝕋 s2-ℂ𝔸𝕋 Tex A \mathbb{A} C \mathbb{C} T \mathbb{T} , s2- TeXのほうがいいな。

予備知識／能力として、原始組み合わせ幾何〈primitive combinatrial geometry〉を仮定する。有限点や有向線分などを理解している、とする。n-箙、特に有限n-箙は原始組み合わせ幾何の概念で直観で理解可能だとする。参照→ マテリアル計算 - 檜山正幸のキマ…

writhe のたくる、のたうつ tortile ねじれた、よじれた twist ひねった、捻り yank ひっぱり tangle からむ