首页/论文/2006.02417

arXiv 2006.024172020-06math.LOcs.LO

Curry-Howard-Lambek Correspondence for Intuitionistic Belief

Cosimo Perini Brogi

备注：: Submitted to Studia Logica on January 31st, 2020

英文摘要：

This paper introduces a natural deduction calculus for intuitionistic logic of belief $\mathsf{IEL}^{-}$ which is easily turned into a modal $λ$-calculus giving a computational semantics for deductions in $\mathsf{IEL}^{-}$. By using that interpretation, it is also proved that $\mathsf{IEL}^{-}$ has good proof-theoretic properties. The correspondence between deductions and typed terms is then extended to a categorical semantics for identity of proofs in $\mathsf{IEL}^{-}$ showing the general structure of such a modality for belief in an intuitionistic framework.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

Disjunctive Axioms and Concurrent $λ$-Calculi: a Curry-Howard Approach

We add to intuitionistic logic infinitely many classical disjunctive tautologies and use the Curry--Howard correspondence to obtain typed concurrent $λ$-calculi; each of them features a specific communication mechanism, including broadcasting and cyclic message-exchange, and enhanced expressive power with respect to the $λ$-calculus. Moreover they all implement forms of code mobility. Our results provide a first concurrent computational interpretation for many propositional intermediate logics, classical logic included.

2018-02-13cs.LOmath.LO

Curry and Howard Meet Borel

We show that an intuitionistic version of counting propositional logic corresponds, in the sense of Curry and Howard, to an expressive type system for the probabilistic event lambda-calculus, a vehicle calculus in which both call-by-name and call-by-value evaluation of discrete randomized functional programs can be simulated. Remarkably, proofs (respectively, types) do not only guarantee that validity (respectively, termination) holds, but also reveal the underlying probability. We finally show that by endowing the type system with an intersection operator, one obtains a system precisely captu…

2022-03-21cs.LOmath.LO

On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic

Intuitionistic first-order logic extended with a restricted form of Markov's principle is constructive and admits a Curry-Howard correspondence, as shown by Herbelin. We provide a simpler proof of that result and then we study intuitionistic first-order logic extended with unrestricted Markov's principle. Starting from classical natural deduction, we restrict the excluded middle and we obtain a natural deduction system and a parallel Curry-Howard isomorphism for the logic. We show that proof terms for existentially quantified formulas reduce to a list of individual terms representing all possi…

2017-10-17cs.LOmath.LO

Formalizing the Curry-Howard Correspondence

The Curry-Howard Correspondence has a long history, and still is a topic of active research. Though there are extensive investigations into the subject, there doesn't seem to be a definitive formulation of this result in the level of generality that it deserves. In the current work, we introduce the formalism of p-institutions that could unify previous aproaches. We restate the tradicional correspondence between typed $λ$-calculi and propositional logics inside this formalism, and indicate possible directions in which it could foster new and more structured generalizations. Furthermore, we ind…

2019-12-23cs.LOmath.LO

Intuitionistic First-Order Logic: Categorical Semantics via the Curry-Howard Isomorphism

This reports introduces a novel sound and complete semantics for first order intuitionistic logic, in the framework of category theory and by the computational interpretation of the logic based on the so-called Curry-Howard isomorphism. Aside, a sound and complete semantics for the corresponding lambda-calculus is derived, too. This semantics extends, in a way, the more traditional meanings given by Heyting categories, the topos-theoretic interpretation, and Kripke models. The feature which justifies the introduction of this novel semantics is the fact that it is 'point-free', i.e., there is n…

2013-06-29cs.LOmath.LO

λ演算的证明逻辑

Justification Logic of the Lambda Calculus

Faculty of Technical Sciences, University of Novi Sad（诺维萨德大学技术科学学院）；Mathematical Institute of the Serbian Academy of Sciences and Arts（塞尔维亚科学院数学研究所）；School of Computer Science, University of Birmingham（伯明翰大学计算机学院）

研究λ演算的证明逻辑，通过引入一种逻辑，其模态证明项为类型化λ项，能同时推理计算与证明。给出公理系统、自然演绎系统及Curry-Howard解释，还构建相继式演算并证明切割消去，得到归一化结果。

2026-07-28cs.LOmath.LO

更多相关论文收起更多论文

Lambek-Grishin Calculus: Focusing, Display and Full Polarization

\emph{Focused sequent calculi} are a refinement of sequent calculi, where additional side-conditions on the applicability of inference rules force the implementation of a proof search strategy. Focused cut-free proofs exhibit a special normal form that is used for defining identity of sequent calculi proofs. We introduce a novel focused display calculus fD.LG and a fully polarized algebraic semantics FP.LG for Lambek-Grishin logic by generalizing the theory of \emph{multi-type calculi} and their algebraic semantics with \emph{heterogenous consequence relations}. The calculus fD.LG has \emph{st…

2020-11-05cs.LOmath.LO

Gentzen-Mints-Zucker duality

The Curry-Howard correspondence is often described as relating proofs (in intutionistic natural deduction) to programs (terms in simply-typed lambda calculus). However this narrative is hardly a perfect fit, due to the computational content of cut-elimination and the logical origins of lambda calculus. We revisit Howard's work and interpret it as an isomorphism between a category of proofs in intuitionistic sequent calculus and a category of terms in simply-typed lambda calculus. In our telling of the story the fundamental duality is not between proofs and programs but between local (sequent c…

2020-08-23cs.LOmath.LO

Realizability algebras II : new models of ZF + DC

Using the proof-program (Curry-Howard) correspondence, we give a new method to obtain models of ZF and relative consistency results in set theory. We show the relative consistency of ZF + DC + there exists a sequence of subsets of R the cardinals of which are strictly decreasing + other similar properties of R. These results seem not to have been previously obtained by forcing.

2012-03-29cs.LOmath.LO

On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains

The logic of constant domains is intuitionistic logic extended with the so-called forall-shift axiom, a classically valid statement which implies the excluded middle over decidable formulas. Surprisingly, this logic is constructive and so far this has been proved by cut-elimination for ad-hoc sequent calculi. Here we use the methods of natural deduction and Curry-Howard correspondence to provide a simple computational interpretation of the logic.

2018-10-18cs.LOmath.LO

Computational interpretation of classical logic with explicit structural rules

We present a calculus providing a Curry-Howard correspondence to classical logic represented in the sequent calculus with explicit structural rules, namely weakening and contraction. These structural rules introduce explicit erasure and duplication of terms, respectively. We present a type system for which we prove the type-preservation under reduction. A mutual relation with classical calculus featuring implicit structural rules has been studied in detail. From this analysis we derive strong normalisation property.

2012-03-21cs.DCcs.LOmath.LO

Lambda Mu Calculus and Duality: Call-by-Name and Call-by-Value

Under the extension of Curry-Howard's correspondence to classical logic, Gentzen's NK and LK systems can be seen as syntax-directed systems of simple types respectively for Parigot's Lambda Mu Calculus and Curien-Herbelin's Lambda Bar Mu Mu Tidle Calculus. We aim at showing their computational equivalence. We define translations between these calculi. We prove simulation theorems for an undirected evaluation as well as for call-by-name and call-by-value evaluations.

2007-06-12math.LO

Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search

A new, comprehensive approach to inhabitation problems in simply-typed lambda-calculus is shown, dealing with both decision and counting problems. This approach works by exploiting a representation of the search space generated by a given inhabitation problem, which is in terms of a lambda-calculus for proof search that the authors developed recently. The representation may be seen as extending the Curry-Howard representation of proofs by lambda-terms, staying within the methods of lambda-calculus and type systems. Our methodology reveals inductive descriptions of the decision problems, driven…

2017-03-11cs.LOmath.LO

完全选择公理的一个程序

A program for the full axiom of choice

本文在经典可实现性框架下，提出了完全选择公理（AC）的第一个显式程序，填补了此前仅有依赖选择公理（DC）程序的空白。

2021-08-31cs.LOmath.LO

Cut elimination and normalization for generalized single and multi-conclusion sequent and natural deduction calculi

Any set of truth-functional connectives has sequent calculus rules that can be generated systematically from the truth tables of the connectives. Such a sequent calculus gives rise to a multi-conclusion natural deduction system and to a version of Parigot's free deduction. The elimination rules are "general," but can be systematically simplified. Cut-elimination and normalization hold. Restriction to a single formula in the succedent yields intuitionistic versions of these systems. The rules also yield generalized lambda calculi providing proof terms for natural deduction proofs as in the Curr…

2021-05-31math.LO

Arithmetical proofs of strong normalization results for symmetric lambda calculi

We give arithmetical proofs of the strong normalization of two symmetric $λ$-calculi corresponding to classical logic. The first one is the $\barλμ\tildeμ$-calculus introduced by Curien & Herbelin. It is derived via the Curry-Howard correspondence from Gentzen's classical sequent calculus LK in order to have a symmetry on one side between "program" and "context" and on other side between "call-by-name" and "call-by-value". The second one is the symmetric $λμ$-calculus. It is the $λμ$-calculus introduced by Parigot in which the reduction rule $μ'$, which is the symmetric of $μ$, is added. These…

2009-05-06math.LO

双边主义设定中证明的意义与同一性：一个用于证明与反驳的双类类型化λ演算

Meaning and identity of proofs in a bilateralist setting: A two-sorted typed lambda-calculus for proofs and refutations

本文为Wansing双直觉主义逻辑2Int构建双类类型化λ演算λ-2Int，建立带项标注的证明系统并证明对偶化定理，从而从双边主义视角探讨证明的意义、指称与同一性问题。

2024-02-23cs.LOmath.LO

Categorical and Algebraic Aspects of the Intuitionistic Modal Logic $\operatorname{IEL}^{-}$ and its predicate extensions

The system of intuitionistic modal logic ${\bf IEL}^{-}$ was proposed by S. Artemov and T. Protopopescu as the intuitionistic version of belief logic \cite{Artemov}. We construct the modal lambda calculus which is Curry-Howard isomorphic to ${\bf IEL}^{-}$ as the type-theoretical representation of applicative computation widely known in functional programming. We also provide a categorical interpretation of this modal lambda calculus considering coalgebras associated with a monoidal functor on a cartesian closed category. Finally, we study Heyting algebras and locales with corresponding operat…

2020-12-07math.CTmath.LO

关于$λμρθ$-演算的归约序列长度的估计

An estimation for the lengths of reduction sequences of the $λμρθ$-calculus

本文基于Xi的结果，给出扩展了$ρ$-和$θ$-规则的$λμ$-演算归约序列长度的上界，证明新规则不增加计算复杂度。

2018-06-21math.LO

A Logic of Interactive Proofs (Formal Theory of Knowledge Transfer)

We propose a logic of interactive proofs as a framework for an intuitionistic foundation for interactive computation, which we construct via an interactive analog of the Goedel-McKinsey-Tarski-Artemov definition of Intuitionistic Logic as embedded into a classical modal logic of proofs, and of the Curry-Howard isomorphism between intuitionistic proofs and typed programs. Our interactive proofs effectuate a persistent epistemic impact in their intended communities of peer reviewers that consists in the induction of the (propositional) knowledge of their proof goal by means of the (individual) k…

2017-08-08cs.CRcs.DCcs.LO

A Coinductive Approach to Proof Search through Typed Lambda-Calculi

In reductive proof search, proofs are naturally generalized by solutions, comprising all possibly infinite structures generated by locally correct, bottom-up application of inference rules. We propose an extension of the Curry-Howard paradigm of representation, from proofs to solutions: to represent solutions by possibly infinite terms of a dedicated lambda-calculus. This new, comprehensive approach to proof search is exemplified with the sequent calculus LJT for intuitionistic implication logic. A finitary representation is proposed, comprising lambda-terms extended with a formal greatest fix…

2021-07-29cs.LOmath.LO

对 Gödel 完备性定理的 Henkin 证明之构造性内容的分析

An analysis of the constructive content of Henkin's proof of Gödel's completeness theorem

本文在直觉主义二阶算术中形式化修改版 Henkin 完备性证明，并借助 Curry-Howard 对应将其刻画为把 Tarski 有效性证明转换为可推导性证明的程序。

2024-01-24math.LO