{絵|図|絵図}は、{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 など。 証明とは、主張の正しさを保証するものである。その主張に至る過程も含めて…