Propositional quantification in intuitionistic logic

The author deals with a system of second order propositional intuitionistic logic, \(\text{IPC}^2\), consisting of the standard axiomatization of Heyting calculus and the axiom schemes and rules \[ F(q) \rightarrow \exists p F(p), \quad \forall p F(p) \rightarrow F(q), \quad {F(p) \rightarrow G \over \exists p F(p) \rightarrow G}, \quad {G \rightarrow F(p) \over G \rightarrow \forall p F(p)} \] (with \(p\) not free in \(G\)). \(\text{IPC}^2\) is not complete with respect to any natural semantics, for the intuitively true formula \(\neg \forall p (p \lor \neg p)\) is not derivable in the system. However, \textit{A. Pitts} [J. Symb. Logic 57, 33-52 (1992; Zbl 0763.03009)], has shown that quantified propositional formulas can be translated into Heyting calculus. In fact, for every quantifier-free formula \(F\) and a propositional variable \(p\), one can effectively find formulas \(\text{A}p F\) and \(\text{E}p F\) containing only those variables which occur in \(F\) and are distinct from \(p\). The operators A and E model universal and existential quantifier, respectively, and the above axioms and rules become valid under this modelling. In the paper under review, a few topological interpretations of \(\text{IPC}^2\) in metric spaces are tested to see whether the equivalences \(\text{A} p F \leftrightarrow \forall p F\) and \(\text{E} p F \leftrightarrow \exists p F\) are valid in these semantics. The answer is affirmative for the monadic fragment of \(\text{IPC}^2\) and interpretations in dense-in-itself metric spaces, and negative for fragments with more variables. For the entire collection see [Zbl 0870.00023].

Recommendations

Cited in

(23)

This page was built for publication: Propositional quantification in intuitionistic logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4364519)