On an interpretation of second order quantification in first order intuitionistic propositional logic
Journal of Symbolic Logic 57 (1):33-52 (1992)
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 $(\perp)$ using conjunction $(\wedge)$ , disjunction (∨) and implication (→). Write $\vdash\phi$ 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, \vdash \psi \rightarrow A_p\phi$ if and only if $\vdash \psi \rightarrow \phi$ . 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
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
On Flattening Elimination Rules.Grigory K. Olkhovikov & Peter Schroeder-Heister - 2014 - Review of Symbolic Logic 7 (1):60-72.
Uniform Interpolation and Propositional Quantifiers in Modal Logics.Marta Bílková - 2007 - Studia Logica 85 (1):1-31.
Undefinability of Propositional Quantifiers in the Modal System S.Silvio Ghilardi & Marek Zawadowski - 1995 - Studia Logica 55 (2):259 - 271.
Substitutions of Σ10-Sentences: Explorations Between Intuitionistic Propositional Logic and Intuitionistic Arithmetic.Albert Visser - 2002 - Annals of Pure and Applied Logic 114 (1-3):227-271.
Similar books and articles
On the Complexity of Propositional Quantification in Intuitionistic Logic.Philip Kremer - 1997 - Journal of Symbolic Logic 62 (2):529-544.
On the Period of Sequences (an(P)) in Intuitionistic Propositional Calculus.Wim Ruitenburg - 1984 - Journal of Symbolic Logic 49 (3):892 - 899.
Propositional Quantification in the Monadic Fragment of Intuitionistic Logic.Tomasz Połacik - 1998 - Journal of Symbolic Logic 63 (1):269-300.
The Decidability of Dependency in Intuitionistic Propositional Logi.Dick De Jongh & L. A. Chagrova - 1995 - Journal of Symbolic Logic 60 (2):498 - 504.
An Effective Fixed-Point Theorem in Intuitionistic Diagonalizable Algebras.Giovanni Sambin - 1976 - Studia Logica 35 (4):345 - 361.
On a Contraction-Less Intuitionistic Propositional Logic with Conjunction and Fusion.Romà J. Adillon & Ventura Verdú - 2000 - Studia Logica 65 (1):11-30.
A Syntactic Embedding of Predicate Logic Into Second-Order Propositional Logic.Morten H. Sørensen & Paweł Urzyczyn - 2010 - Notre Dame Journal of Formal Logic 51 (4):457-473.
Second Order Propositional Operators Over Cantor Space.Tomasz Połacik - 1994 - Studia Logica 53 (1):93 - 105.
Added to index2009-01-28
Total downloads25 ( #201,887 of 2,163,866 )
Recent downloads (6 months)2 ( #188,913 of 2,163,866 )
How can I increase my downloads?