論理とギリシャ語順のトリビア - 言語ゲーム
伝統的に、ギリシャ三段論法はこんな風に書きます。 大前提: 全ての人間は死にます。(全ての B は A) 小前提: ソクラテスは人間です。(全ての C は B) 結論: ソクラテスは死にます。(全ての C は A) なんか違和感ありませんか？なんか順番がちぐはぐですね。なぜもっと自然に 全ての A は B 全ての B は C ゆえに全ての A は C と書かないのでしょうか？伝統的な論理学にはプログラミングで使う論理学とは微妙に違う考え方が出てきます。この語順についても、昔の人はバカだからわざわざ難しい書き方をしたのだと思っていました。ところが何と、これにはちゃんとした理由があったのです。なんでも、これはギリシャ語で書いたときに自然な語順になっているそうです。 ギリシア語では、主語と述語の論理の記述が逆だそうです。この語順を無理やり当てはめるとこんな風になります。 大前提: 死ぬものの中に
オンラインで入手できる数理論理学・数学基礎論のテキスト
オンラインで入手できる数理論理学・数学基礎論のテキスト 数理論理学、数学基礎論の教科書的に使えるテキスト（講義ノート、サーヴェイ、モノグラフ等）のうち、オンラインで入手できるものを集めました。 入門的概説 論理一般 高階論理と型理論 直観主義論理 コンビネータとラムダ計算 時相論理および時制論理 様相論理 適切さの論理 自然言語の論理 空間論理 モデル理論 安定性理論 無限論理 計算可能性理論および再帰理論 集合論 pcf理論 記述集合論 実数の集合論 選択公理 強制法と内部モデル 連続体仮説 NF 証明論と構成的数学 順序数解析 算術の体系と不完全性 証明可能性論理 線形論理 構成的数学 代数的論理と圏論 ブール代数 普遍代数 量子論理 圏論 歴史 入門的概説 [▲] 加茂静夫，「数理論理学（命題論理と述語論理）」．[PDF] 嘉田勝，「数理論理学 講義ノート（2013年度版）」． St
Perspective in Logics, Lecture Notes in Logic 無料化 - あいまいな本日の私 blog
id:nuhsnuh さん経由。知っている人は知っている話でしょうが。 ASLで編集され、Springerから出版されていた ”Perspective in logics"シリーズが、なんと Project Euclid で無料公開されていました。ページはこちら。内訳は Computability in Analysis and Physics; Marian B. Pour-El, J. Ian Richards (1989) Higher Recursion Theory; Gerald E. Sacks (1990) Metamathematics of First-Order Arithmetic; Petr Hájek, Pavel Pudlák (1998) Essential Stability Theory; Steven Buechler (1996) Proper an
ProofWeb - kururu_goedel’s diary
ProofWeb 知らなかった。CoqとかIsabelleとかのような定理証明器をウェブ上で動かせます。インストールがいらないのでちょっと遊んでみるのに便利ですね。まあ、操作性では劣りますが。
閉圏、弱いラムダ計算、弱い論理 - 檜山正幸のキマイラ飼育記 (はてなBlog)
「モノイド圏、豊饒圏、閉圏と内部ホム」は自分用メモと思って書いたら、トラックバック／コメント欄で色々とやりとりがあって面白かったです。お相手してくださった皆様、ありがとうございます。 でまー、またゴニュゴニョ続けるのですけど、このての話（って、まだ話してないが）は、ランベック（J. Lambek）とかケリー（G. M. Kelly）あたりが大昔にやっていそうで気が引けますが、まー、練習問題ということで。 “そとの人”と“なかの人” 例え話で、閉圏（閉じた対称モノイド圏のこと）のなかに棲む生物を出したのですが、比喩だからピンとこない人もいるでしょう。でも、この比喩に共感できる人は、強烈で具体的なイメージを持てると思います。「そと」とか「なか」が何を意味するか、もう少し説明しましょう。 まず、“そとの人”は、神様のつもりになった我々人間。圏に対して何でもできます（つうか、そういう幻想を抱いてい
The Mercury Project: Comparing Mercury and Haskell
Home News Information Documentation Tutorial Reference Manual  Version 0.13.1  Snapshot User's Guide Version 0.13.1 Snapshot Library Reference Version 0.13.1 Snapshot cf. Prolog Version 0.13.1 Snapshot cf. Haskell FAQ  Version 0.13.1  Snapshot Mailing Lists Back-ends Download Related Contact Search Bug Database Comparing Mercury with Haskell Mercury has a lo
A declarative logic programming system
A declarative applicative logic programming system KANREN is a declarative logic programming system with first-class relations, embedded in a pure functional subset of Scheme. The system has a set-theoretical semantics, true unions, fair scheduling, first-class relations, lexically-scoped logical variables, depth-first and iterative deepening strategies. The system achieves high performance and ex
The Haskell Road to Logic, Maths and Programming
Sample from the book (table of contents plus first chapter): compressed postscript Addendum to Chapter 9 of the Book: Direct Computation of Polynomial Representations for Sequences: PolAddendum.pdf PolAddendum.hs Errata A list of errata is here. Software Getting Started: GS.hs Talking about Mathematical Objects: TAMO.hs The Use of Logic: Proof: TUOLP.hs Sets, Types and Lists: STAL.hs Database used
Wadler: History of logic and programming languages
Philip Wadler Papers we love: John Reynolds, Definitional Interpreters for Higher-Order Programming Languages Papers We Love, Skills Matter, London, 7 June 2016 Certain papers change your life. McCarthy's 'Recursive Functions of Symbolic Expressions and their Computation by Machine (Part I)' (1960) changed mine, and so did Landin's 'The Next 700 Programming Languages' (1966). And I remember the mo
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20090708
ヒビルテ
Amazon.co.jp: ロジカル・ディレンマ ゲーデルの生涯と不完全性定理: ジョン・W・ドーソンJr (著), 村上祐子 (翻訳), 塩谷賢 (翻訳): 本
monad.me.uk
The S combinator and 99 Prolog problems