On an interpretation of second order quantification in first order intuitionistic propositional logic
- 12 March 1992
- journal article
- Published by Cambridge University Press (CUP) in The Journal of Symbolic Logic
- Vol. 57 (1), 33-52
- https://doi.org/10.2307/2275175
Abstract
We 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 variablepand formula ϕ there exists a formulaApϕ (effectively computable from ϕ), containing only variables not equal topwhich occur in ϕ, and such that for all formulas ψ not involvingp, ⊢ψ →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 IpC2can be constructed whose algebra of truth-values is equal to any given Heyting algebra.Keywords
This publication has 5 references indexed in Scilit:
- Amalgamation and interpolation in the category of heyting algebrasJournal of Pure and Applied Algebra, 1983
- Semantical Investigations in Heyting’s Intuitionistic LogicPublished by Springer Science and Business Media LLC ,1981
- Proving termination with multiset orderingsCommunications of the ACM, 1979
- Doctrines in Categorical LogicPublished by Elsevier BV ,1977
- A new algorithm for derivability in the constructive propositional calculusAmerican Mathematical Society Translations: Series 2, 1970