On an Intuitionistic Modal Logic

In this paper we consider an intuitionistic variant of the modal logic S4 (which we call IS4). The novelty of this paper is that we place particular importance on the natural deduction formulation of IS4— our formulation has several important metatheoretic properties. In addition, we study models of IS4— not in the framework of Kirpke semantics, but in the more general framework of category theory. This allows not only a more abstract definition of a whole class of models but also a means of modelling proofs as well as provability.     

Intuitionistic Propositional Logic without 'Contraction' but with 'Reductio'

Routley-Meyer type relational complete semantics are constructed for intuitionistic contractionless logic with reductio. Different negation completions of positive intuitionistic logic without contraction are treated in a systematical, unified and semantically complete setting.     

Absolute Probability Functions for Intuitionistic Propositional Logic

Provided here is a characterisation of absolute probability functions for intuitionistic (propositional) logic L, i.e. a set of constraints on the unary functions P from the statements of L to the reals, which insures that (i) if a statement A of L is provable in L, then P(A) = 1 for every P, L's axiomatisation being thus sound in the probabilistic sense, and (ii) if P(A) = 1 for every P, then A is provable in L, L's axiomatisation being thus complete in the probabilistic sense. As there are theorems of classical (propositional) logic that are not intuitionistic ones, there are unary probability functions for intuitionistic logic that are not classical ones. Provided here because of this is a means of singling out the classical probability functions from among the intuitionistic ones.     

Quantum Logic in Intuitionistic Perspective

In their seminal paper Birkhoff and von Neumann revealed the following dilemma:[ ] whereas for logicians the orthocomplementation properties of negation were the ones least able to withstand a critical analysis, the study of mechanics points to the distributive identities as the weakest link in the algebra of logic.In this paper we eliminate this dilemma, providing a way for maintaining both. Via the introduction of the "missing" disjunctions in the lattice of properties of a physical system while inheriting the meet as a conjunction we obtain a complete Heyting algebra of propositions on physical properties. In particular there is a bijective correspondence between property lattices and propositional lattices equipped with a so called operational resolution, an operation that exposes the properties on the level of the propositions. If the property lattice goes equipped with an orthocomplementation, then this bijective correspondence can be refined to one with propositional lattices equipped with an operational complementation, as such establishing the claim made above. Formally one rediscovers via physical and logical considerations as such respectively a specification and a refinement of the purely mathematical result by Bruns and Lakser (1970) on injective hulls of meet-semilattices. From our representation we can derive a truly intuitionistic functional implication on property lattices, as such confronting claims made in previous writings on the matter. We also make a detailed analysis of disjunctivity vs. distributivity and finitary vs. infinitary conjunctivity, we briefly review the Bruns-Lakser construction and indicate some questions which are left open.     

A Negationless Interpretation of Intuitionistic Theories. II

This work is a sequel to our [16]. It is shown how Theorem 4 of [16], dealing with the translatability of HA(Heyting's arithmetic) into negationless arithmetic NA, can be extended to the case of intuitionistic arithmetic in higher types.     

A Negationless Interpretation of Intuitionistic Theories. I

The present work contains an axiomatic treatment of some parts of the restricted version of intuitionistic mathematics advocated by G. F. C. Griss, also known as negationless intuitionistic mathematics. Formal systems NPC, NA, and FIM ^N for negationless predicate logic, arithmetic, and analysis are proposed. Our Theorem 4 in Section 2 asserts the translatability of Heyting's arithmetic HAinto NA. The result can in fact be extended to a large class of intuitionistic theories based on HAand their negationless counterparts. For instance, in Section 3 this is shown for Kleene's system of intuitionistic analysis FIMand our FIM ^N . This revised version was published online in June 2006 with corrections to the Cover Date.     

New Intuitionistic Logical Constants and Novikov Completeness

Extending the language of the intuitionistic propositional logic Int with additional logical constants, we construct a wide family of extensions of Int with the following properties: (a) every member of this family is a maximal conservative extension of Int; (b) additional constants are independent in each of them. This revised version was published online in June 2006 with corrections to the Cover Date.     

Irreflexive Modality in the Intuitionistic Propositional Logic and Novikov Completeness

A. Kuznetsov considered a logic which extended intuitionistic propositional logic by adding a notion of 'irreflexive modality'. We describe an extension of Kuznetsov's logic having the following properties: (a) it is the unique maximal conservative (over intuitionistic propositional logic) extension of Kuznetsov's logic; (b) it determines a new unary logical connective w.r.t. Novikov's approach, i.e., there is no explicit expression within the system for the additional connective; (c) it is axiomatizable by means of one simple additional axiom scheme.     

The Greatest Extension of S4 into which Intuitionistic Logic is Embeddable

This paper gives a characterization of those quasi-normal extensions of the modal system S4 into which intuitionistic propositional logic Int is embeddable by the Gödel translation. It is shown that, as in the normal case, the set of quasi-normal modal companions of Int contains the greatest logic, M*, for which, however, the analog of the Blok-Esakia theorem does not hold. M* is proved to be decidable and Halldén-complete; it has the disjunction property but does not have the finite model property.     

On Different Intuitionistic Calculi and Embeddings from Int to S4

In this paper, we compare several cut-free sequent systems for propositional intuitionistic logic Intwith respect to polynomial simulations. Such calculi can be divided into two classes, namely single-succedent calculi (like Gentzen's LJ) and multi-succedent calculi. We show that the latter allow for more compact proofs than the former. Moreover, for some classes of formulae, the same is true if proofs in single-succedent calculi are directed acyclic graphs (dags) instead of trees. Additionally, we investigate the effect of weakening rules on the structure and length of dag proofs.The second topic of this paper is the effect of different embeddings from Int to S4. We select two different embeddings from the literature and show that translated (propositional) intuitionistic formulae have sometimes exponentially shorter minimal proofs in a cut-free Gentzen system for S4than the original formula in a cut-free single-succedent Gentzen system for Int. Moreover, the length and the structure of proofs of translated formulae crucially depend on the chosen embedding.     

Dual Intuitionistic Logic and a Variety of Negations: The Logic of Scientific Research

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.     

Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic

We describe a sequent calculus, based on work of Herbelin, of which the cut-free derivations are in 1-1 correspondence with the normal natural deduction proofs of intuitionistic logic. We present a simple proof of Herbelin's strong cut-elimination theorem for the calculus, using the recursive path ordering theorem of Dershowitz.     

AN INTUITIONISTIC CHARACTERIZATION OF CLASSICAL LOGIC

By introducing the intensional mappings and their properties, we establish a new semantical approach of characterizing intermediate logics. First prove that this new approach provides a general method of characterizing and comparing logics without changing the semantical interpretation of implication connective. Then show that it is adequate to characterize all Kripke_complete intermediate logics by showing that each of these logics is sound and complete with respect to its (unique) ‘weakest characterization property’ of intensional mappings. In particular, we show that classical logic has the weakest characterization property , which is the strongest among all possible weakest characterization properties of intermediate logics. Finally, it follows from this result that a translation is an embedding of classical logic into intuitionistic logic, iff. its semantical counterpart has the property .      

The Pleasures of Anticipation: Enriching Intuitionistic Logic

We explore a relation we call anticipation between formulas, where A anticipates B (according to some logic) just in case B is a consequence (according to that logic, presumed to support some distinguished implicational connective ) of the formula AB. We are especially interested in the case in which the logic is intuitionistic (propositional) logic and are much concerned with an extension of that logic with a new connective, written as a, governed by rules which guarantee that for any formula B, aB is the (logically) strongest formula anticipating B. The investigation of this new logic, which we call ILa, will confront us on several occasions with some of the finer points in the theory of rules and with issues in the philosophy of logic arising from the proposed explication of the existence of a connective (with prescribed logical behaviour) in terms of the conservative extension of a favoured logic by the addition of such a connective. Other points of interest include the provision of a Kripke semantics with respect to which ILa is demonstrably sound, deployed to establish certain unprovability results as well as to forge connections with C. Rauszer's logic of dual intuitionistic negation and dual intuitionistic implication, and the isolation of two relations (between formulas), head-implication and head-linkage, which, though trivial in the setting of classical logic, are of considerable significance in the intuitionistic context.     

Intuitionistic Autoepistemic Logic

In this paper we address the problem of combining a logic with nonmonotonic modal logic. In particular we study the intuitionistic case. We start from a formal analysis of the notion of intuitionistic consistency via the sequent calculus. The epistemic operator M is interpreted as the consistency operator of intuitionistic logic by introducing intuitionistic stable sets. On the basis of a bimodal structure we also provide a semantics for intuitionistic stable sets.     

Statistics of Intuitionistic versus Classical Logics

For the given logical calculus we investigate the proportion of the number of true formulas of a certain length n to the number of all formulas of such length. We are especially interested in asymptotic behavior of this fraction when n tends to infinity. If the limit exists it is represented by a real number between 0 and 1 which we may call the density of truth for the investigated logic. In this paper we apply this approach to the intuitionistic logic of one variable with implication and negation. The result is obtained by reducing the problem to the same one of Dummett's intermediate linear logic of one variable (see [2]). Actually, this paper shows the exact density of intuitionistic logic and demonstrates that it covers a substantial part (more than 93%) of classical prepositional calculus. Despite using strictly mathematical means to solve all discussed problems, this paper in fact, may have a philosophical impact on understanding how much the phenomenon of truth is sporadic or frequent in random mathematics sentences.