Note on the Strong Normalizability of the Logic with Self-Referential Predicates
スポンサーリンク
概要
- 論文の詳細を見る
1. INTRODUCTION2. LANGUAGE FOR SELF-REFERENTIAL PREDICATES3. UNTYPED SELF-REFERENTIAL LANGUAGE AND RUSSELL'S PARADOX4. STRONG NORMALIZABILITY5. REFERENCESWe consider a logical system in which the second order terms can be also used as first order terms. As a consequence, predicates can be taken as arguments of another predicate. In other words, a predicate can refer to predicates. The proposed framework seems very different from the tradition of formal logic which has been developped since Aristotle, where the distinction between the predicates and the individuals are essential. While in the traditional (Aristotelean) logical language a typical and basic sentence is of the form, e.g., Love(Socrates, Phaidon) "Socrates loves Phaidon", in our proposed language we could also express e.g., Love(Socrates, Love), Socrates "loves (the idea of) love", (which can be also express as Love(Socrates, λx, y. Love(x, y) by the usual η-conversion), or a sentence Love(God, λx ∀y Love(x, y)), "God loves (the idea of) loving everyone", or a predicate on x such as Love(x, λy Love(x, y)), "x loves x's own love". The purpose of this note is to give some proof-theoretic properties of the proposed logic; in particular, the strong normalizability is shown by slightly modifying Girard's strong normalizability proof for the traditional higher order logic. The use of this proposed logical language for the analysis of "self-references" and "intensionality" as Well as a connection with natural language semantics is discussed in Okada", and the connection with mobile communication processes and with linear logic are discussed in Okada.
- 慶應義塾大学の論文
- 1993-07-00
著者
関連論文
- 現代応用オントロジーの哲学的・論理学的源泉(オントロジーの進化と普及(前編))
- 線形論理に基づく計算モデルの理論概説
- 線形論理に基づいたセキュリティ・プロトコルの論理的検証法(自動推論 : 演繹, 帰納, モデル検査/生成, 仮説推論アブダクション, 論理プログラム, プランニング, 時相論理, etc.)
- ウィトゲンシュタイン, 言語の限界, 飯田隆著, 講談社, 1997年.
- BAN論理からProtocol Composition Logicへ : セキュリティプロトコルの論理的検証法(数理的技法による情報セキュリティ)
- A Hierarchy of the Fragments of the System of Inductive Definition : Preliminary Report
- Semantic Characterizations for Reachability and Trace Equivalence in a Linear Logic-Based Process Calculus : Preliminary Report
- A Relationship among Gentzen's Proof-Reduction, Kirby-Paris' Hydra Game, and Buchholz's Hydra Game(Preliminary Report)(Mathematical Incompleteness in Arithmetic)
- 論理記号導入規則による論理的意味論について
- 矛盾は矛盾か (特集 ラッセルのパラドックス・100年)
- 歪んだ真珠(バロック) : 音楽における規則性VS反規則性,またはロゴスVSパトス
- オントロジー応用のための方法論の考察と展望(哲学とAIにおける対象世界モデリング)(〔第4回〕)
- 現代のフォーマルオントロジーの動向とオントロジー工学(「哲学とAIにおける対象世界モデリング」〔第3回〕)
- フッサールのフォーマルオントロジーとその影響(哲学とAIにおける対象世界モデリング〔第2回〕)
- オントロジーの哲学的・論理学的背景
- 「哲学とAIにおける対象世界モデリング」の企画にあたって
- 日本語の文末表現における意味解釈と音響特性
- フッサールの形式論理学分析における「多様体」概念の役割
- Characterization Theorems for Multiplicative Fragment of Intuitionistic Non-Commutative Linear Logic : Preliminary Report
- 3.線形論理に基づく並行計算モデル : 並行計算の論理的理解の試み (並行計算の理論の最近の動向)
- 倫理学入門のためのPersonal Guide
- デカルトにおける「論証」の概念と彼の形而上学的論証の論理的基準(100集記念号)
- A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic(Preliminary Report)(Non-Classical Logics and Their Kripke Semantics)
- 諸状況における終助詞「か」の意味解釈と音響特性
- 論理学入門のためのPersonal Guide
- 「普遍学」の夢と現実 : 論理推論体系の可能性を求めて(文学部創設百周年記念論文集I)
- フッサ-ル初期の「哲学的-数学的諸研究の終結テ-マ」とゲッチンゲン学派の論理哲学
- 論理的意味論と整合性証明
- Some Remarks on a Difference between Gentzen's Finitist and Heyting's Intuitionist Approaches toward Intuitionistic Logic and Arithmetic
- Completeness Proofs for Linear Logic Based on the Proof Search Method(Preliminary Report)(Type Theory and its Applications to Computer Systems)
- Note on the Strong Normalizability of the Logic with Self-Referential Predicates
- "The Concluding Theme of Philosophical-Mathematical Students" in the Early Husserl, and the Logical Philosophy of Goettingen School