Agda is a dependently-typed functional programming language, based on an extension of intuitionistic Martin-Löf type theory. We implement first order natural deduction in Agda. We use Agda's type checker to verify the correctness of natural deduction proofs, and also prove properties of natural deduction, using Agda's proof assistant functionality. This implementation corresponds to a formalisation of natural deduction in constructive type theory, and the proofs are verified by Agda to be correct (under the assumption that Agda itself is correct).
In a previous paper (of which this is a prosecution) we investigated the extraction of proof-theoretic properties of natural deduction derivations from their impredicative translation into System F. Our key idea was to introduce an extended equational theory for System F codifying at a syntactic level some properties found in parametric models. In a recent series of papers a different approach to extract proof-theoretic properties of natural deduction derivations was proposed by defining predicative variants of the usual translation, embedding intuitionistic propositional logic into the atomic…
This paper presents a way of formalising definite descriptions with a binary quantifier $ι$, where $ιx[F, G]$ is read as `The $F$ is $G$'. Introduction and elimination rules for $ι$ in a system of intuitionist negative free logic are formulated. Procedures for removing maximal formulas of the form $ιx[F, G]$ are given, and it is shown that deductions in the system can be brought into normal form.
The purpose of this paper is to give an easy to understand with step-by-step explanation to allow interested people to fully appreciate the power of natural deduction for first-order logic. Natural deduction as a proof system can be used to prove various statements in propositional logic, but we will see its extension to cover quantifiers which gives it more power over propositional logic in solving more complex, real-world problems. We started by going over logical connectives and quantifiers to agree on the symbols that will be used throughout the paper, as some authors use different symbols…
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…
我们介绍了\emph{resource control cube}，一个系统，由八个直观的lambda演算与资源的隐式或显式控制，无论是自然演绎或自然演算。本文介绍了Kesner和Renaud提出的与自然演绎对应的四种立方体演算，以及与λ演算对应的四种立方体演算。该演示文稿是参数化的一组资源（削弱或收缩），这使得一个统一的治疗的八个结石的立方体。简单类型的资源控制立方体一方面将Curry-Howard对应扩展为具有隐式或显式结构规则的直觉自然演绎和直觉推理逻辑，另一方面又与子结构逻辑相关。我们提出了一个通用的交叉型系统的资源控制立方体演算。我们的主要贡献是一个强大的归一化减少在这个立方体的特征。首先，我们证明了可类型性意味着强规范化的“自然演绎基地”的立方体，通过适应reductionmethod。然后，我们证明了可类型性意味着强规范化的“cubes基地”的立方体，通过使用一个组合良好的订单和一个合适的嵌入在“自然演绎基地”。最后，我们证明了强规范化意味着在立方体中使用头部主题扩展的可键入性。所有的证明都是通用的，并且可以通过实例化资源集来针对立方体的每个演算。
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.
The {\em tetravalent modal logic} ($\cal TML$) is one of the two logics defined by Font and Rius (\cite{FR2}) (the other is the {\em normal tetravalent modal logic} ${\cal TML}^N$) in connection with Monteiro's tetravalent modal algebras. These logics are expansions of the well--known {\em Belnap--Dunn's four--valued logic} that combine a many-valued character (tetravalence) with a modal character. In fact, $\cal TML$ is the logic that preserve degrees of truth with respect to tetravalent modal algebras. As Font and Rius observed, the connection between the logic $\cal TML$ and the algebras is…
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…
We consider an extension of first-order logic with a recursion operator that corresponds to allowing formulas to refer to themselves. We investigate the obtained language under two different systems of semantics, thereby obtaining two closely related but different logics. We provide a natural deduction system that is complete for validities for both of these logics, and we also investigate a range of related basic decision problems. For example, the validity problems of the two-variable fragments of the logics are shown coNexpTime-complete, which is in stark contrast with the high undecidabili…
