Tuesday, April 8, 20142:00 pmComputational Logic SeminarGraduate Center, rm. 3209.

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

Tudor Protopopescu

CUNY Graduate Center

Tudor Protopopescu

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.