Modeling Intuitionistic Epistemic Logic via Provability and Verification (joint work with S. Artemov)

Computational Logic SeminarTuesday, April 8, 20142:00 pmGraduate Center, rm. 3209.

Tudor Protopopescu

Modeling Intuitionistic Epistemic Logic via Provability and Verification (joint work with S. Artemov)

CUNY Graduate Center

In 1933, Goedel offered a provability semantics for intuitionsitic logic IPC by means of a syntactical embedding of IPC into the modal logic S4 which Goedel considered a calculus for classical provability. Goedel’s embedding later became a key ingredient of the BHK-style semantics of classical proofs for intuitionsitic logic via the Logic of Proofs. We will establish the embedding/interpretation of Intuitionistic Epistemic Logic IEL into a natural extension (which we suggest calling S4V) of Goedel’s provability logic S4 by a verification modality. Basically, we will explain IEL via classical provability and verification coded in S4V the way Goedel explained intuitionistic logic via classical provability by interpreting it in S4.

Posted by on April 4th, 2014