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

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.