Asinus's blog

西牟田祐樹のブログです。

数理論理学

もうひとつの自然演繹: Jaśkowski, Theory of deduction based on the method of suppositionを読む

Jaśkowskiの自然演繹についての概要 自然演繹といえばゲンツェンがシーケント計算と共に考案したことで有名だが、ちょうど同年の1934年にヤスコフスキ(Jaśkowski)も自然演繹についての論文を発表した。 ゲンツェン流とヤスコフスキ流の大きな違いは、ゲンツ…

射としての含意: Paul Herz, "Über Axiomensysteme für beliebige Satzsystem"を読む

ゲンツェンとの関係 あまり知られていないがシーケント計算や自然演繹を考え出したゲンツェンの最初の論文はパウル・ヘルツの体系に関する結果である1。ヘルツは特にシーケント、カット規則、弱化規則に関してゲンツェンに影響を与えている。 この記事ではヘ…

グリベンコからハイティングへの手紙 (7)

はじめに 前回の記事はこちら グリベンコからハイティングへの手紙 (6) - Asinus's blog 今回の記事でグリベンコの手紙に関しては完結です。 翻訳 モスクワ 1933年10月24日 ハイティング様、 発音について教えていただきありがとうございました。私にとって…

グリベンコからハイティングへの手紙 (6)

はじめに 前回の記事はこちら グリベンコからハイティングへの手紙 (5) - Asinus's blog 翻訳 モスクワ 1933年10月12日 ハイティング様、 論理学についてのあなたのノートを受け取りました。しかもそれはよいタイミングでした。なぜならほぼ四年前から私はこ…

グリベンコからハイティングへの手紙 (5)

はじめに 前回の記事はこちら。 https://incognito0.hatenablog.com/entry/2021/05/18/193546 翻訳 モスクワ 1928年11月13日 ハイティング様、 あなたの記念論文とは独立に私の結果を発表しようと思います。それはこの結果がほとんど自明なリマークに過ぎな…

グリベンコからハイティングへの手紙 (4)

はじめに 前回の記事はこちら。 https://incognito0.hatenablog.com/entry/2021/05/18/183327 翻訳 モスクワ 1928年10月30日 ハイティング様、 私が最近の手紙であなたにお伝えした結果をベルギー王立アカデミーの『年報』("Bulletins" de l'Académie Royale…

グリベンコからハイティングへの手紙 (3)

はじめに 前回の記事はこちら。 https://incognito0.hatenablog.com/entry/2021/04/02/183020 翻訳 モスクワ、1928年10月18日 ハイティング様、 偶然にも10月13日に私の手紙で述べられていた質問への答えが書かれていた10月7日のあなたからの手紙を昨日受け…

グリベンコからハイティングへの手紙 (2)

はじめに 前回の記事はこちら。前の手紙から約3ヶ月が経過している。 https://incognito0.hatenablog.com/entry/2021/04/02/183020 翻訳 モスクワ、1928年10月13日 ハイティング様、 まずはあなたの論文の抜粋をご教示いただいたことに感謝いたします。この…

Lensを通して見るゲーデル

Haskell等で使われるLens(の一般形)1は実は論理学とも深い関係がある。Lensの構造に関する研究の(おそらく)最も最初のものはゲーデルのディアレクティカ解釈の研究である2。 ゲーデルのディアレクティカ解釈とは直観主義算術から量化子なしの有限型算術 Tへ…

早すぎたアイデア: W. Kneale & M. Kneale, "The Development of Logic"を読む

W. Kneale & M. Knealeのアイデア W.Kneale & M. Kneale, The development of Logic, Clarendon Press, 1962という論理学史の本についてほとんど知られていないであろう内容を書き記しておく1。 この本は古代ギリシアからヒルベルト辺りまでを詳細にカバーし…

グリベンコからハイティングへの手紙 (1)

はじめに グリベンコの定理1でお馴染みのグリベンコの手紙をいくつか翻訳する。 テキストはA. S. Troestra, On the Early History of Intuitionisitc Logic, In Mathematical Logic, Springer, pp.3-17 (1990) を使用した。 以下でも読むことができる。 http…

ローレンツェンのゲーム意味論への転回

ドイツの論理学者・哲学者であるポール・ローレンツェン(Paul Lorenzen 1915~1994)の仕事はざっくり大きく二つの時期に分けられる1。一つはゲーム意味論に取り組む前の"Einführung in die operative Logik und Mathematik", 1955を主要な成果とするような操…

排他的選言の推論規則

日常言語での接続詞の用法や真理値表では通常の選言(両立的選言)の他に両方の選言肢の両方が真である場合に全体が偽になるという排他的選言が紹介されることがある。 形式的証明体系であるシーケント計算や自然演繹で現れる選言の規則は両立的選言である。 …

数学的帰納法の歴史(2): "The origin of mathematical induction"(1917)を読む

前回数学的帰納法の歴史(1): "The origin of mathematical induction"(1917)を読む - Asinus's blog の続きから. 論文の著者Busseyはパスカルがマウロニクスの結果を参照しているということにはカントールに同意する. しかしマウロニクスが帰納法を用いて証…

数学的帰納法の歴史(1): "The origin of mathematical induction"(1917)を読む

W.H.Bussey, The origin of mathematical induction, The american mathematical monthly, vol.XXIV, No. 5, 1917. に沿ってパスカルとマウロニクスの帰納法に相当すると考えられることもある箇所を見ていく1. 私自身はこれらの用法と現代的な帰納法の用法の…

オッカムの仮言命題と真理値

オッカムは『大論理学』で連言と選言に関して次のように述べている1。 連言 Oportet autem scire quod semper a copulatiua ad utramque partem est consequentia bona, sicut sequitur 'Sortes non currit et Plato disputat, ergo Plato disputat'; sed e …

S4を含む様相論理は非可算無限個ある: Fine, "An ascending chain of S4 logics"(1974)を読む

様相論理を学ぶと体系が沢山現れることが気になると思う。 それじゃあ一体いくらあるんだ? という疑問に対してこう答えられる。 S4を含む様相論理だけで非可算無限個ある。 つまりアホほど存在するのである。 Kit Fine, "An ascending chain of S4 logics",…

直観主義論理の真理値について: Gödel: "Zur intuitionistischen Aussagenkalkül" (1932)を読む

入門書による独学でも大学の講義でも記号論理学の初歩として学ぶと思われるのは(古典論理の)真理値表の概念と計算方法である。そして少し進んだ講義ではそのあとに証明体系としてシーケント計算よりも自然演繹を学ぶところが多いのではないかと思う1。 真理…