※この記事は「記事9 問題集7」単一の論理式〈形式化された命題〉だけではなくて、論理式のリストを徹底的に使い倒した最初の人はおそらくゲンツェンだろう。プログラミングで言えば、単一タプル引数（パックされた多引数）、単一タプル戻り値（パックされた…

※この記事は「記事8 問題集6」2018-12-02: 冒頭に、スコット・ブラケット＝真理集合の役割の説明を追記。与えられた論理式〈形式化された命題〉に対して、そのスコット・ブラケットを実際に計算する練習。スコット・ブラケット（の値）と真理集合は同じもの…

※この記事は「記事7」（問題集ではない）演繹を遂行できる人工的なシステムである演繹システムを（少なくとも1つは）実際に構成して、その演繹システムの性質を調べるのが我々に課せられたタスクである。その演繹システムの論理パートを、仕様として定義する…

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

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

演繹システムのパート分類（モジュラー／レイヤード設計・実装のため）： 分野固有パート 論理パート（分野によらない共通パート） 分野固有パートは： 個体レベル 型レベル 論理パート 命題レベル 推論レベル システムが単ソート〈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ではない。対になるべき語がうま…

証明ストリング図のノードラベルが、メタ変数でラベルしているのか、システム内のラベルでラベルしているのが分からないという問題があった。ラベルのテキストで区別するのは現実的ではないが、ノード形状で区別ならなんとかなる。まず、ノード種別を インラ…

絵を中心に考えるしかないだろう。で、絵のノードだが、誤解を招きそうな気がしてきた。ノード → スパイダーと改名したほうがいいかも知れない。グラフ理論の頂点とは違って、むしろ近傍部分グラフみたいなものだから。スパイダーは脚を持つ。脚の付け根をピ…

メタ変数、メタ論理、メタ数学 とかの奇妙な言葉。メタ変数は実質的に困難をもたらす。 変数集合V上を走る変数 x, y 。で、V = {x, y, ... } だったりする。 状況としては、 日本語と共通の単語が多くあり、意味が同じだったり違っていたりという外国語があ…

フントニモウ、ムカムカムカムカ、ムッキー！！ 矢鱈に同義語があったりする（例：論理AND、論理積、連言、合接、コンジャンクション）のに、肝心なモノ・コトに言葉がなかったり、曖昧過ぎて使いものにならなかったり。むっかー！ 定理 証明 公理と推論 定…

比喩： 具体素子 基本リーズニング 証明図（スチル） ムービー 料理 食材 基本調理法 料理のスナップショット 料理動画 回路工作 素子とワイヤー 基本組み立て法 回路のスナップショット 工作動画 ピクチャーパズル ピース 基本組み立て法 ピクチャーのスナ…

fA→B これではバラエティが足りないのでもっと描き足すつもり。それと、題材は f:A, B→C にする。

関連しそうな自分のエントリー。ウヘー、我ながらいっぱいあるなー。ざっと読んでいこう。読んだら、感想を一言ずつ書いていこう。 述語論理とインデックス付き圏と限量随伴性 20170824 テンソル積の作り方 20160829 中学レベル代入計算からカリー／ハワード…

無名変数 ハイフンまたはアンダースコア〈アンダーバー | アンダーライン〉 セクション記法 関数のプロファイル（多変数・多値のカンマ区切りもあり） maps-to記法 |→ 関数適用〈引数渡し | 関数呼び出し〉の中置記法 関数が右からの関数適用 ラムダ記法 コ…

リーズナー〈reasoner〉は、{定理|証明}コンビネータのこと。 ; （二項） （二項） （二項） ◇ （任意項） □ （任意項） Λ （単項） p, qが{定理|証明}で、Pが{定理|証明}のインデックス族とするときの適用結果は： p;q pq pq ◇P □P Λp ただし、は'∧'に輪（…

意味結び付きを切り替える儀式として 記憶を助けるヒントとして ← コジツケでもいい

論理AND、合接、論理積、連言、コンジャンクション 論理OR、離接、論理和、選言、ディスジャンクション 論理NOT、否定、{ニ | ネ}ゲーション 含意、条件{法}?、インプリケーション 多義語： 矛盾： 矛盾命題＝偽命題＝偽的命題〈falsy prop.〉、演繹システム…

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