各位
先日ご案内しました Segei Artemov 教授， Elena Nogina 教授の講演会の場所が間違えていたので訂正します．
日本大学文理学部1号館1階122教室
とあったのは誤りで，正しくは
日本大学文理学部1号館2階122教室
です．よろしくお願いします．
菊池誠
--
各位
先日ご案内いたしました Segei Artemov 教授 (City University of New York)，Elena Nogina 教授 (City University of New York) の講演会とセミナーのアブストラクトをお送りします．（一部，講演題目が変更されています．）講演会，セミナーにご出席希望の方は事前にそれぞれの問い合わせ先までご連絡下さい．
【１】論理学講演会
日時：2013年3月24日（日）14:30-18:00 場所：日本大学文理学部1号館1階122教室 プログラム:
14:30-16:00 Sergei Artemov (CUNY) Formalizing Brouwer-Heyting-Kolmogorov semantics 16:30-18:00 Elena Nogina (CUNY) Joining Two Goedel's Models of Provability
アブストラクト：
Speaker: Sergei Artemov, The City University of New York Title: Formalizing Brouwer-Heyting-Kolmogorov semantics Abstract:
According to Brouwer, intuitionistic truth is provability; this led to the informal Brouwer-Heyting-Kolmogorov (BHK) semantics of proofs for intuitionistic logic (1934). There are two well-known problems with BHK exposed by Kreisel in 1962. First, in the original BHK, any proof vacuously “proves” the negation of any unprovable sentence; this dubious feature ruins constructive connection between a sentence and its proof. Second, original BHK’s treating of universal quantifiers admits unacceptable bogus “proofs” for any true Π1-sentence, e.g., for Fermat’s Last Theorem or the consistency statement. Kreisel offered plausible corrections to BHK which we suggest calling BHK*. The problem of an exact provability interpretation of BHK* turned out to be elusive. For example, BHK- inspired semantics based on computational programs (Realizability, Curry-Howard isomorphism, Intuitionistic Type Theory) though have constituted a major development in logic and computer science, do not satisfy BHK*.
In the 1930s, Gödel suggested to define intuitionistic logic via classical provability represented by modal logic S4 and interpret the latter via explicit proofs rather then provability. Later developments of the Logic of Proofs LP in the 1990s opened the door to realizing Gödel’s approach. In this talk, we survey provability semantics obtained by Gödel’s embedding of intuitionistic logic into S4, followed by a realization in the Logic of Proofs. We show that it satisfies BHK* requirements and provides a desired provability foundation for intuitionistic logic.
Speaker: Dr. Elena Nogina, The City University of New York Title: Joining Two Gödel's approaches to provability Abstract:
In 1933, Gödel suggested S4 as a modal logic of provability but pointed out that S4 was not compatible with a straightforward interpretation of modality as formal provability. This left "a provability semantics without a calculus" and "a provability calculus without a semantics." In 1976, Solovay found that modal logic GL was the logic of formal provability; in 1995, Artemov found a precise provability semantics for S4 via Logic of Proofs LP.
In this talk, we introduce logic GLA representing both aforementioned Gödel's approaches to provability, as well as new provability principles which appear as a result of interactions between these models. GLA is supplied with a Kripke-style semantics and the corresponding completeness theorem. Soundness and completeness of GLA with respect to the arithmetical provability semantics is established.
問い合わせ先： 日本大学文理学部哲学科 飯田隆 iida.takashi19@nihon-u.ac.jp
【２】Seminar in Logic and Philosophy of Mathematics
日時：2013年3月26日（火）〜27日（水） 場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室） プログラム：
3月26日 10:30-12:00 Sergei Artemov (CUNY) Logic of Proofs and Justification (1/2) 13:00-14:30 Elena Nogina (CUNY) On Provability and Explicit Proofs 15:00-16:30 Taishi Kurahashi (Kobe) Syntax and semantics of predicate modal logic of provability
3月27日 10:30-12:00 Sergei Artemov (CUNY) Logic of Proofs and Justification (2/2) 13:00-14:30 Ryota Akiyoshi (Kyoto) Proper Explanation of Brouwer's Fundamental Assumption 15:00-16:30 Hidenori Kurokawa Kreisel's second clause and the theory of constructions
Speaker: Sergei Artemov, The City University of New York Title: Logic of Proofs and Justification Abstract:
We describe a general logical framework, Justification Logic, for reasoning about epistemic justification. Justification Logic is based on classical propositional logic augmented by justification assertions t:F that read `t is a justification for F.' In this talk, we show how Justification Logic originated from the mathematical proof-theoretical semantics as the Logic of Proofs and then extended to the mainstream epistemology. In the foundations of constructive reasoning, the Logic of Proofs has completed Gödel's effort of the 1930s to find a classical provability interpretation of intuitionistic logic. In epistemology, Justification Logic offered the missing justification component to formal analysis of Knowledge as Justified True Belief approach commonly attributed to Plato. As a case study, we offer a resolution of the Goldman–Kripke ‘Red Barn’ paradox and analyze Russell’s ‘prime minister example’ in Justification Logic. We state a general Correspondence Theorem showing that behind each epistemic modal logic, there is a robust system of justifications. This renders a new, evidence-based foundation for epistemic logic.
Speaker: Dr. Elena Nogina, The City University of New York. Title: On Provability and Explicit Proofs Abstract:
Gödel's Incompleteness Theorem drew a sharp distinction between explicit proofs and formal provability. In particular, reflection principle "if A is formally provable then A holds" is true but not internally provable, whereas explicit reflection principle "if p is a proof of A, then A holds" is both true and provable. According to Solovay, all valid principles of formal provability are described by Gödel-Löb modal logic GL. Artemov's Logic of Proofs LP describes all valid principles of explicit proofs with a basic set of operations.
Some meaningful provability principles require both provability and explicit proofs. E.g., the negative introspection fails in GL as well as in LP, but admits an adequate formulation in mixed language of GL and LP.
We introduce logic GLA, that describes, along with GL and LP, all valid principles in the language of proofs and provability. GLA has been supplied with Kripke-style semantics and shown to be complete with respect to the intended arithmetical provability interpretation.
問い合わせ先： 神戸大学大学院システム情報学研究科 菊池誠 mkikuchi@kobe-u.ac.jp