scholarly journals A new Glivenko Theorem

10.29007/7l98 ◽  
2018 ◽  
Author(s):  
Majid Alizadeh ◽  
Mohammad Ardeshir ◽  
Wim Ruitenburg
Keyword(s):  
Propositional Logic ◽  
Boolean Algebras ◽  
Heyting Algebras ◽  
Double Negation ◽  
Glivenko’S Theorem

We generalize the double negation construction of Boolean algebras in Heytingalgebras, to a double negation construction of the same in Visser algebras (alsoknown as basic algebras).This result allows us to generalize Glivenko's Theorem from intuitionisticpropositional logic and Heyting algebras to Visser's basic propositional logicand Visser algebras.

scholarly journals Glivenko theorems for substructural logics over FL

2006 ◽  
Vol 71 (4) ◽  
pp. 1353-1384 ◽  
Author(s):  
Nikolaos Galatos ◽  
Hiroakira Ono
Keyword(s):  
Propositional Logic ◽  
Substructural Logics ◽  
Residuated Lattices ◽  
Substructural Logic ◽  
Classical Propositional Logic ◽  
Double Negation ◽  
Glivenko’S Theorem

AbstractIt is well known that classical propositional logic can be interpreted in intuitionistic prepositional logic. In particular Glivenko's theorem states that a formula is provable in the former iff its double negation is provable in the latter. We extend Glivenko's theorem and show that for every involutive substructural logic there exists a minimum substructural logic that contains the first via a double negation interpretation. Our presentation is algebraic and is formulated in the context of residuated lattices. In the last part of the paper, we also discuss some extended forms of the Koltnogorov translation and we compare it to the Glivenko translation.

scholarly journals Bitopological duality for distributive lattices and Heyting algebras

2010 ◽  
Vol 20 (3) ◽  
pp. 359-393 ◽  
Author(s):  
GURAM BEZHANISHVILI ◽  
NICK BEZHANISHVILI ◽  
DAVID GABELAIA ◽  
ALEXANDER KURZ
Keyword(s):  
Boolean Algebras ◽  
Distributive Lattices ◽  
Heyting Algebras ◽  
Priestley Spaces ◽  
Spectral Spaces ◽  
Algebraic Concepts ◽  
Stone Spaces

We introduce pairwise Stone spaces as a bitopological generalisation of Stone spaces – the duals of Boolean algebras – and show that they are exactly the bitopological duals of bounded distributive lattices. The category PStone of pairwise Stone spaces is isomorphic to the category Spec of spectral spaces and to the category Pries of Priestley spaces. In fact, the isomorphism of Spec and Pries is most naturally seen through PStone by first establishing that Pries is isomorphic to PStone, and then showing that PStone is isomorphic to Spec. We provide the bitopological and spectral descriptions of many algebraic concepts important in the study of distributive lattices. We also give new bitopological and spectral dualities for Heyting algebras, thereby providing two new alternatives to Esakia's duality.

scholarly journals On an interpretation of second order quantification in first order intuitionistic propositional logic

1992 ◽  
Vol 57 (1) ◽  
pp. 33-52 ◽  
Author(s):  
Andrew M. Pitts
Keyword(s):  
Propositional Logic ◽  
Heyting Algebra ◽  
Propositional Calculus ◽  
Interpolation Theorem ◽  
Second Order ◽  
Heyting Algebras ◽  
Intuitionistic Propositional Logic ◽  
First Order ◽  
Intuitionistic Propositional Calculus ◽  
Algebraic Counterpart

AbstractWe prove the following surprising property of Heyting's intuitionistic propositional calculus, IpC. Consider the collection of formulas, ϕ, built up from propositional variables (p, q, r, …) and falsity (⊥) using conjunction (∧), disjunction (∨) and implication (→). Write ⊢ϕ to indicate that such a formula is intuitionistically valid. We show that for each variable p and formula ϕ there exists a formula Apϕ (effectively computable from ϕ), containing only variables not equal to p which occur in ϕ, and such that for all formulas ψ not involving p, ⊢ψ → Apϕ if and only if ⊢ψ → ϕ. Consequently quantification over propositional variables can be modelled in IpC, and there is an interpretation of the second order propositional calculus, IpC2, in IpC which restricts to the identity on first order propositions.An immediate corollary is the strengthening of the usual interpolation theorem for IpC to the statement that there are least and greatest interpolant formulas for any given pair of formulas. The result also has a number of interesting consequences for the algebraic counterpart of IpC, the theory of Heyting algebras. In particular we show that a model of IpC2 can be constructed whose algebra of truth-values is equal to any given Heyting algebra.

On decidable varieties of Heyting algebras

1992 ◽  
Vol 57 (3) ◽  
pp. 988-991 ◽  
Author(s):  
Devdatt P. Dubhashi
Keyword(s):  
Order Theory ◽  
Boolean Algebras ◽  
Semantic Interpretation ◽  
Structure Theory ◽  
Heyting Algebras ◽  
Quantitative Classification ◽  
First Order ◽  
First Order Theory ◽  
Famous Result

In this paper we present a new proof of a decidability result for the firstorder theories of certain subvarieties of Heyting algebras. By a famous result of Grzegorczyk, the full first-order theory of Heyting algebras is undecidable. In contrast, the first-order theory of Boolean algebras and of many interesting subvarieties of Boolean algebras is decidable by a result of Tarski [8]. In fact, Kozen [6] gives a comprehensive quantitative classification of the complexities of the first-order theories of various subclasses of Boolean algebras (including the full variety).This stark contrast may be reconciled from the standpoint of universal algebra as arising out of the byplay between structure and decidability: A good structure theory entails positive decidability results. Boolean algebras have a well-developed structure theory [5], while the corresponding theory for Heyting algebras is quite meagre. Viewed in this way, we may hope to obtain decidability results if we focus attention on subclasses of Heyting algebras with good structural properties.K. Idziak and P. M. Idziak [4] have considered an interesting subvariety of Heyting algebras, , which is the variety generated by all linearly-ordered Heyting algebras. This variety is shown to be the largest subvariety of Heyting algebras with a decidable theory of its finite members. However their proof is rather indirect, proceeding via semantic interpretation into the monadic second order theory of trees. The latter is a powerful theory—it interprets many other theories—but is computationally highly infeasible. In fact, by a celebrated theorem of Rabin, its complexity is not bounded by any elementary recursive function. Consequently, the proof of [4], besides being indirect, also gives no information on the quantitative computational complexity of the theory of .Here we pursue the theme of structure and decidability. We isolate the indecomposable algebras in and use this to prove a theorem on the structure of if -algebras. This theorem relates the -algebras structurally to Boolean algebras. This enables us to bootstrap the known decidability results for Boolean algebras to the variety if .

On second order intuitionistic propositional logic without a universal quantifier

2009 ◽  
Vol 74 (1) ◽  
pp. 157-167 ◽  
Author(s):  
Konrad Zdanowski
Keyword(s):  
Propositional Logic ◽  
Second Order ◽  
Universal Quantifier ◽  
Intuitionistic Propositional Logic ◽  
Glivenko’S Theorem ◽  
Free Variables ◽  
Universal Quantification

AbstractWe examine second order intuitionistic propositional logic, IPC2. Let ℱ∃ a be the set of formulas with no universal quantification. We prove Glivenko's theorem for formulas in ℱ∃ that is, for φ ∈ ℱ∃, φ is a classical tautology if and only if ┐┐φ is a tautology of IPC2. We show that for each sentence φ ∈ ℱ∃ (without free variables), φ is a classical tautology if and only if φ is an intuitionistic tautology. As a corollary we obtain a semantic argument that the quantifier ∀ is not definable in IPC2 from ⊥, ⋁, ⋀, →, ∃.

Decidability problem for finite Heyting algebras

1988 ◽  
Vol 53 (3) ◽  
pp. 729-735 ◽  
Author(s):  
Katarzyna Idziak ◽  
Pawel M. Idziak
Keyword(s):  
Boolean Algebras ◽  
Heyting Algebras ◽  
First Order ◽  
Decidable Theory ◽  
Decidability Problem ◽  
Ordered Algebras

AbstractThe aim of this paper is to characterize varieties of Heyting algebras with decidable theory of their finite members. Actually we prove that such varieties are exactly the varieties generated by linearly ordered algebras. It contrasts to the result of Burris [2] saying that in the case of whole varieties, only trivial variety and the variety of Boolean algebras have decidable first order theories.

An algebraic approach to intuitionistic connectives

2001 ◽  
Vol 66 (4) ◽  
pp. 1620-1636 ◽  
Author(s):  
Xavier Caicedo ◽  
Roberto Cignoli
Keyword(s):  
Algebraic Approach ◽  
Propositional Calculus ◽  
Heyting Algebras ◽  
Classical Formula ◽  
Double Negation ◽  
Intermediate Logic ◽  
Intermediate Logics ◽  
Intuitionistic Propositional Calculus ◽  
Third Law

Abstract.It is shown that axiomatic extensions of intuitionistic propositional calculus defining univocally new connectives, including those proposed by Gabbay, are strongly complete with respect to valuations in Heyting algebras with additional operations. In all cases, the double negation of such a connective is equivalent to a formula of intuitionistic calculus. Thus, under the excluded third law it collapses to a classical formula, showing that this condition in Gabbay's definition is redundant. Moreover, such connectives can not be interpreted in all Heyting algebras, unless they are already equivalent to a formula of intuitionistic calculus. These facts relativize to connectives over intermediate logics. In particular, the intermediate logic with values in the chain of length n may be “completed” conservatively by adding a single unary connective, so that the expanded system does not allow further axiomatic extensions by new connectives.

THE LOGIC OF LEIBNIZ’S GENERALES INQUISITIONES DE ANALYSI NOTIONUM ET VERITATUM

2016 ◽  
Vol 9 (4) ◽  
pp. 686-751 ◽  
Author(s):  
MARKO MALINK ◽  
ANUBAV VASUDEVAN
Keyword(s):  
Propositional Logic ◽  
Boolean Algebras ◽  
Algebraic Reasoning ◽  
Symbolic Calculus ◽  
Classical Propositional Logic ◽  
Simple Class

AbstractThe Generales Inquisitiones de Analysi Notionum et Veritatum is Leibniz’s most substantive work in the area of logic. Leibniz’s central aim in this treatise is to develop a symbolic calculus of terms that is capable of underwriting all valid modes of syllogistic and propositional reasoning. The present paper provides a systematic reconstruction of the calculus developed by Leibniz in the Generales Inquisitiones. We investigate the most significant logical features of this calculus and prove that it is both sound and complete with respect to a simple class of enriched Boolean algebras which we call auto-Boolean algebras. Moreover, we show that Leibniz’s calculus can reproduce all the laws of classical propositional logic, thus allowing Leibniz to achieve his goal of reducing propositional reasoning to algebraic reasoning about terms.

Sign in / Sign up

Export Citation Format

Share Document