Scholarlink

<p>Gödel, working within axiomatic logic, succeeded in 1933 in establishing a translation from theorems of intuitionistic propositional logic to ones of classical logic enriched with a modal provability operator. The converse correspondence was established by semantical means in 1948, and by Gödel through a syntactic translation in unpublished work of 1941. It is shown through proof analysis of formal derivations in natural deduction for modal logic that steps of indirect proof in normal derivations of translations of intuitionistic formulas are vacuous. This conservativity of classical over intuitionistic modal logic for translated formulas is the reason why Gödel’s modal translation succeeds in singling out a “provability fragment” within classical modal logic that coincides with intuitionistic logic.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Gödel’s modal interpretation of intuitionistic logic and its proof theory

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年7月8日

查看全文
  • Jan von Plato

摘要

Gödel, working within axiomatic logic, succeeded in 1933 in establishing a translation from theorems of intuitionistic propositional logic to ones of classical logic enriched with a modal provability operator. The converse correspondence was established by semantical means in 1948, and by Gödel through a syntactic translation in unpublished work of 1941. It is shown through proof analysis of formal derivations in natural deduction for modal logic that steps of indirect proof in normal derivations of translations of intuitionistic formulas are vacuous. This conservativity of classical over intuitionistic modal logic for translated formulas is the reason why Gödel’s modal translation succeeds in singling out a “provability fragment” within classical modal logic that coincides with intuitionistic logic.