A new Glivenko 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.

GLIVENKO AND KURODA FOR SIMPLE TYPE THEORY

Glivenko’s theorem states that an arbitrary propositional formula is classically provable if and only if its double negation is intuitionistically provable. The result does not extend to full first-order predicate logic, but does extend to first-order predicate logic without the universal quantifier. A recent paper by Zdanowski shows that Glivenko’s theorem also holds for second-order propositional logic without the universal quantifier. We prove that Glivenko’s theorem extends to some versions of simple type theory without the universal quantifier. Moreover, we prove that Kuroda’s negative translation, which is known to embed classical first-order logic into intuitionistic first-order logic, extends to the same versions of simple type theory. We also prove that the Glivenko property fails for simple type theory once a weak form of functional extensionality is included.

On second order intuitionistic propositional logic without a universal quantifier

We 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 ⊥, ⋁, ⋀, →, ∃.

Glivenko theorems for substructural logics over FL

It 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.