中央研究院 資訊科學研究所

活動訊息

友善列印

列印可使用瀏覽器提供的(Ctrl+P)功能

應用邏輯討論會系列 (XXXII) -- Justification Logics

:::

應用邏輯討論會系列 (XXXII) -- Justification Logics

  • 講者Melvin Fitting 教授 (Department of Mathematics and Computer Science (Emeritus), CUNY)
    邀請人:廖純中
  • 時間2017-02-24 (Fri.) 15:30 ~ 17:30
  • 地點資訊所新館106演講廳
摘要

Gödel inaugurated a project of finding an arithmetic semantics for intuitionistic logic, but did not complete it.  It was finished by Sergei Artemov, in the 1990’s.  As part of this work, Artemov introduced the first justification logic, LP, (standing for logic of proofs).  This is a propositional modal-like logic, with an infinite family of proof or justification terms.  Ir can be seen as an explicit version of the well-known modal logic S4.  There is a possible world semantics for LP (due to me).  Since then, many other justification logic/modal logic pairs have been investigated, and justification logic has become a subject of independent interest, going beyond the original connection with intuitionistic logic.  It is now known that there are infinitely many justification logics, but the exact extent of the family is not known.

Justification logics are connected with their corresponding modal logics via

Realization Theorems.   A Realization Theorem connecting LP and S4 has a

constructive proof, but there are other cases for which realization holds, but it is not known if a constructive proof exists.  In a sense, a realization of a modal theorem reflects the flow of information inherent in its formal proof.  I will present a sketch of the basic ideas.  I have an implementation of realization for S4 into LP available on my web page, but there will not be time to discuss it during the talk.