Machine-Checked Meta-theory of Dual-Tableaux for Intuitionistic Logic

Abstract This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first-order intuitionistic logic with constant domains. It is shown that Fitting’s nested calculi naturally arise from their corresponding labelled calculi—for each of the aforementioned logics—via the elimination of structural rules in labelled derivations. The translational correspondence between the two types of systems is leveraged to show that the nested calculi inherit proof-theoretic properties from their associated labelled calculi, such as completeness, invertibility of rules and cut admissibility. Since labelled calculi are easily obtained via a logic’s semantics, the method presented in this paper can be seen as one whereby refined versions of labelled calculi (containing nested calculi as fragments) with favourable properties are derived directly from a logic’s semantics.

Download Full-text

On Correspondence between Selective CPS Transformation and Selective Double Negation Translation

Mathematics ◽

10.3390/math9040385 ◽

2021 ◽

Vol 9 (4) ◽

pp. 385

Author(s):

Hyeonseung Im

Keyword(s):

Programming Languages ◽

Intuitionistic Logic ◽

Reference Point ◽

Classical Logic ◽

Proof System ◽

Double Negation

A double negation translation (DNT) embeds classical logic into intuitionistic logic. Such translations correspond to continuation passing style (CPS) transformations in programming languages via the Curry-Howard isomorphism. A selective CPS transformation uses a type and effect system to selectively translate only nontrivial expressions possibly with computational effects into CPS functions. In this paper, we review the conventional call-by-value (CBV) CPS transformation and its corresponding DNT, and provide a logical account of a CBV selective CPS transformation by defining a selective DNT via the Curry-Howard isomorphism. By using an annotated proof system derived from the corresponding type and effect system, our selective DNT translates classical proofs into equivalent intuitionistic proofs, which are smaller than those obtained by the usual DNTs. We believe that our work can serve as a reference point for further study on the Curry-Howard isomorphism between CPS transformations and DNTs.

Download Full-text

Algebraic axiomatization of tense intuitionistic logic

Central European Journal of Mathematics ◽

10.2478/s11533-011-0063-6 ◽

2011 ◽

Vol 9 (5) ◽

pp. 1185-1191 ◽

Cited By ~ 20

Author(s):

Ivan Chajda

Keyword(s):

Intuitionistic Logic

Download Full-text

Decidability problems for the prenex fragment of intuitionistic logic

Proceedings 11th Annual IEEE Symposium on Logic in Computer Science ◽

10.1109/lics.1996.561467 ◽

2002 ◽

Cited By ~ 8

Author(s):

A. Degtyarev ◽

A. Voronkov

Keyword(s):

Intuitionistic Logic

Download Full-text

On the validity of hilbert's nullstellensatz, artin's theorem, and related results in grothendieck toposes

Journal of Symbolic Logic ◽

10.1017/s0022481200028000 ◽

1988 ◽

Vol 53 (4) ◽

pp. 1177-1187

Author(s):

W. A. MacCaull

Keyword(s):

Intuitionistic Logic ◽

Main Idea ◽

Rational Functions ◽

Completeness Theorem ◽

Point Of View ◽

Polynomial Rings ◽

Von Neumann ◽

Ordered Fields ◽

Von Neumann Regular ◽

Theoretic Point

Using formally intuitionistic logic coupled with infinitary logic and the completeness theorem for coherent logic, we establish the validity, in Grothendieck toposes, of a number of well-known, classically valid theorems about fields and ordered fields. Classically, these theorems have proofs by contradiction and most involve higher order notions. Here, the theorems are each given a first-order formulation, and this form of the theorem is then deduced using coherent or formally intuitionistic logic. This immediately implies their validity in arbitrary Grothendieck toposes. The main idea throughout is to use coherent theories and, whenever possible, find coherent formulations of formulas which then allow us to call upon the completeness theorem of coherent logic. In one place, the positive model-completeness of the relevant theory is used to find the necessary coherent formulas.The theorems here deal with polynomials or rational functions (in s indeterminates) over fields. A polynomial over a field can, of course, be represented by a finite string of field elements, and a rational function can be represented by a pair of strings of field elements. We chose the approach whereby results on polynomial rings are reduced to results about the base field, because the theory of polynomial rings in s indeterminates over fields, although coherent, is less desirable from a model-theoretic point of view. Ultimately we are interested in the models.This research was originally motivated by the works of Saracino and Weispfenning [SW], van den Dries [Dr], and Bunge [Bu], each of whom generalized some theorems from algebraic geometry or ordered fields to (commutative, von Neumann) regular rings (with unity).

Download Full-text