On the complexity of propositional quantification in intuitionistic logic.

*(English)*Zbl 0887.03002The propositionally quantified intuitionistic logic H\(\pi+\) is defined to be the set of all valid formulas, quantifiers being interpreted as ranging over all propositions. The main result of the paper says that H\(\pi+\) is rather non-constructive: it is recursively isomorphic to full second-order logic. The autor suggests to restrict the class of underlying model structures and to take into consideration only those of them that are trees; in this way one could obtain another plausible intuitionistic propositional logic with quantifiers. The paper is not self-contained. In fact, only 1-reducibility of second-order logic to H\(\pi+\) is actually proved, and the proof heavily relies on an earlier result (credited to Rabin and Scott) which allows to deal with a fragment of second-order logic admitting only certain binary relations. The converse (that second-order logic is 1-reducible to H\(\pi+\)) can be shown by methods used by the author in an earlier paper [J. Symb. Log. 58, 334-349 (1993; Zbl 0786.03016)].

Reviewer: Jānis Cīrulis (Riga)

##### MSC:

03B20 | Subsystems of classical logic (including intuitionistic logic) |

##### Keywords:

classical second order logic; intuitionistic logic; propositional quantification; recursively isomorphic
Full Text:
DOI

**OpenURL**

##### References:

[1] | Completeness in the theory of types pp 81– (1950) |

[2] | Semantical investigations in Heyting’s intuitionistic logic (1981) · Zbl 0453.03001 |

[3] | Archiv für Mathematische Logik und Grundlagenforsch pp 177– (1974) |

[4] | Theoria pp 336– (1970) |

[5] | Akademiya Nauk Soyuza SSR. Matematicheskie Zamietki pp 69– (1977) |

[6] | Annals of Pure and Applied Logic pp 155– (1984) |

[7] | S5 with quantifiable propositional variables pp 355– (1970) |

[8] | On an interpretation of second order quantification in first order intuitionistic propositional logic pp 33– (1992) |

[9] | Embedding first order predicate logic in fragments of intuitionistic logic pp 705– (1976) |

[10] | The Kleene symposium pp 181– (1980) |

[11] | Formal systems and recursive functions: Proceedings of the eighth logic colloquium pp 92– (1963) |

[12] | Quantifying over propositions in relevance logic: Non-axiomatisability of p and p pp 334– (1993) |

[13] | Reports on Mathematical Logic pp 9– (1981) |

[14] | Logic, methodology and the philosophy of science, proceeding of the 1964 international congress pp 58– (1965) |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.