Most type systems are agnostic regarding the evaluation strategy for the underlying languages, with the value restriction for ML which is absent in Haskell as a notable exception. As type systems become more precise, however, detailed properties of the operational semantics may become visible because properties captured by the types may be sound under one strategy but not the other. For example, intersection types distinguish between call-by-name and call-by-value functions, because the subtyping law ∩≤A→ is unsound for the latter in (...) the presence of effects.In this paper we develop a proof-theoretic framework for analyzing the interaction of types with evaluation order, based on the notion of polarity. Polarity was discovered through linear logic, but we propose a fresh origin in Dummett’s program of justifying the logical laws through alternative verificationist or pragmatist “meaning-theories”, which include a bias towards either introduction or elimination rules. We revisit Dummett’s analysis using the tools of Martin-Löf’s judgmental method, and then show how to extend it to a unified polarized logic, with Girard’s “shift” connectives acting as intermediaries. This logic safely combines intuitionistic and dual intuitionistic reasoning principles, while simultaneously admitting a focusing interpretation for the classical sequent calculus.Then, by applying the Curry–Howard isomorphism to polarized logic, we obtain a single programming language in which evaluation order is reflected at the level of types. Different logical notions correspond directly to natural programming constructs, such as pattern-matching, explicit substitutions, values and call-by-value continuations. We give examples demonstrating the expressiveness of the language and type system, and prove a basic but modular type safety result. We conclude with a brief discussion of extensions to the language with additional effects and types, and sketch the sort of explanation this can provide for operationally sensitive typing phenomena. (shrink)

We present a natural deduction system for dual-intuitionistic logic. Its distinctive feature is that it is a single-premise multiple-conclusions system. Its relationships with the natural deduction systems for intuitionistic and classical logic are discussed.

We consider a logic which is semantically dual (in some precise sense of the term) to intuitionistic. This logic can be labeled as “falsification logic”: it embodies the Popperian methodology of scientific discovery. Whereas intuitionistic logic deals with constructive truth and non-constructive falsity, and Nelson's logic takes both truth and falsity as constructive notions, in the falsification logic truth is essentially non-constructive as opposed to falsity that is conceived constructively. We also briefly clarify the relationships of our falsification logic to (...) some other logical systems. (shrink)

This study introduces refutation-aware Gentzen-style sequent calculi and Kripke-style semantics for propositional until-free linear-time temporal logic. The sequent calculi and semantics are constructed on the basis of the refutation-aware setting for Nelson’s paraconsistent logic. The cut-elimination and completeness theorems for the proposed sequent calculi and semantics are proven.

In this study, falsification-aware semantics and sequent calculi for first-order classical logic are introduced and investigated. These semantics and sequent calculi are constructed based on a falsification-aware setting for first-order Nelson constructive three-valued logic. In fact, these semantics and sequent calculi are regarded as those for a classical variant of N3. The completeness and cut-elimination theorems for the proposed semantics and sequent calculi are proved using Schütte’s method. Similar results for the propositional case are also obtained.

Falsification-aware (hyper)sequent calculi and Kripke semantics for normal modal logics including S4 and S5 are introduced and investigated in this study. These calculi and semantics are constructed based on the idea of a falsification-aware framework for Nelson’s constructive three-valued logic. The cut-elimination and completeness theorems for the proposed calculi and semantics are proved.

Dual-intuitionistic logics are logics proposed by Czermak , Goodman and Urbas . It is shown in this paper that there is a correspondence between Goodman's dual-intuitionistic logic and Nelson's constructive logic N−.

The sequent system LDJ is formulated using the same connectives as Gentzen's intuitionistic sequent system LJ, but is dual in the following sense: (i) whereas LJ is singular in the consequent, LDJ is singular in the antecedent; (ii) whereas LJ has the same sentential counter-theorems as classical LK but not the same theorems, LDJ has the same sentential theorems as LK but not the same counter-theorems. In particular, LDJ does not reject all contradictions and is accordingly paraconsistent. To obtain a (...) more precise mapping, both LJ and LDJ are extended by adding a "pseudo-difference" operator which is the dual of intuitionistic implication. Cut-elimination and decidability are proved for the extended systems and , and a simply consistent but -inconsistent Set Theory with Unrestricted Comprehension Schema based on LDJ is sketched. (shrink)

In this paper, we study the relationship among classical logic, intuitionistic logic, and quantum logic . These logics are related in an interesting way and are not far apart from each other, as is widely believed. The results in this paper show how they are related with each other through a dual intuitionistic logic . Our study is completely syntactical.

Mortensen studies dual intuitionistic logic by dualizing topos internal logic, but he did not study a sequent calculus. In this paper I present a sequent calculus for complement-topos logic, which throws some light on the problem of giving a dualization for LJ.

In this paper we introduce a logic that we name semi Heyting–Brouwer logic, \, in such a way that the variety of double semi-Heyting algebras is its algebraic counterpart. We prove that, up to equivalences by translations, the Heyting–Brouwer logic \ is an axiomatic extension of \ and that the propositional calculi of intuitionistic logic \ and semi-intuitionistic logic \ turn out to be fragments of \.

It is well-established that topos theory is inherently connected with intuitionistic logic. In recent times several works appeared concerning so-called complement-toposes, which are allegedly connected to the dual to intuitionistic logic. In this paper I present this new notion, some of the motivations for it, and some of its consequences. Then, I argue that, assuming equivalence of certain two definitions of a topos, the concept of a complement-classifier is, at least in general and within the conceptual framework of category theory, (...) not appropriately defined. For this purpose, I first analyze the standard notion of a subobject classifier, show its connection with the representability of the functor Sub via the Yoneda lemma, recall some other properties of the internal structure of a topos and, based on these, I critically comment on the notion of a complement-classifier. (shrink)