Neighbourhood and Lattice Models of Second-Order Intuitionistic Propositional Logic

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.

Download Full-text

On second order intuitionistic propositional logic without a universal quantifier

Journal of Symbolic Logic ◽

10.2178/jsl/1231082306 ◽

2009 ◽

Vol 74 (1) ◽

pp. 157-167 ◽

Cited By ~ 2

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

Download Full-text

Non-axiomatizable second order intuitionistic propositional logic

Annals of Pure and Applied Logic ◽

10.1016/s0168-0072(96)00034-6 ◽

1997 ◽

Vol 86 (1) ◽

pp. 33-46 ◽

Cited By ~ 3

Author(s):

D. Skvortsov

Keyword(s):

Propositional Logic ◽

Second Order ◽

Intuitionistic Propositional Logic

Download Full-text

Propositional quantification in the monadic fragment of intuitionistic logic

Journal of Symbolic Logic ◽

10.2307/2586601 ◽

1998 ◽

Vol 63 (1) ◽

pp. 269-300 ◽

Cited By ~ 3

Author(s):

Tomasz Połacik

Keyword(s):

Intuitionistic Logic ◽

Metric Space ◽

Propositional Logic ◽

Second Order ◽

Intuitionistic Propositional Logic ◽

Topological Interpretation ◽

Propositional Quantifiers ◽

Propositional Quantification

AbstractWe study the monadic fragment of second order intuitionistic propositional logic in the language containing the standard propositional connectives and propositional quantifiers. It is proved that under the topological interpretation over any dense-in-itself metric space, the considered fragment collapses to Heyting calculus. Moreover, we prove that the topological interpretation over any dense-in-itself metric space of fragment in question coincides with the so-called Pitts' interpretation. We also prove that all the nonstandard propositional operators of the form q ↦ ∃p (q ↔ F(p)), where F is an arbitrary monadic formula of the variable p, are definable in the language of Heyting calculus under the topological interpretation of intuitionistic logic over sufficiently regular spaces.

Download Full-text