A Godel-Artemov-Style Analysis of Constructible Falsity

摘要

David Nelson's logic of constructible falsity N is a well-known conservative extension to intuitionistic logic Int. Heinrich Wansing has suggested that extending the provability interpretation of Int to such extensions requires that one enriches the single category of formal proofs assumed intuitionistically with further categories representing formal refutations. This paper adapts the framework of Sergei Artemov's justification logic - which has provided incredible insight into Int - to capture a proof/refutation interpretation of N. To represent distinct types of justification, we identify the distinct agents of Tatiana Yavorskaya-Sidon's two-agent logic of proofs LP_(↑↑)~2 with categories of proof and refutation, permitting an embedding of N into LP_(↑↑)~2. In conclusion, we describe how a Godel-Artemov-style analysis can be given for Cecylia Rauszer's Heyting-Brouwer logic and show that Melvin Fitting's semantic realization proof can be extended to normal multimodal logics in general.