On a second order propositional operator in intuitionistic logic

Studia Logica 40 (2):113 - 139 (1981)
  Copy   BIBTEX


This paper studies, by way of an example, the intuitionistic propositional connective * defined in the language of second order propositional logic by. In full topological models * is not generally definable, but over Cantor-space and the reals it can be classically shown that; on the other hand, this is false constructively, i.e. a contradiction with Church's thesis is obtained. This is comparable with some well-known results on the completeness of intuitionistic first-order predicate logic.Over [0, 1], the operator * is (constructively and classically) undefinable. We show how to recast this argument in terms of intuitive intuitionistic validity in some parameter. The undefinability argument essentially uses the connectedness of [0, 1]; most of the work of recasting consists in the choice of a suitable intuitionistically meaningful parameter, so as to imitate the effect of connectedness.



    Upload a copy of this work     Papers currently archived: 91,322

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

57 (#273,573)

6 months
6 (#506,019)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Anne Troelstra
Last affiliation: University of Amsterdam

Citations of this work

Pitts' Quantifiers Are Not Topological Quantification.Tomasz Połacik - 1998 - Notre Dame Journal of Formal Logic 39 (4):531-544.
Propositional Quantification in the Topological Semantics for S.Philip Kremer - 1997 - Notre Dame Journal of Formal Logic 38 (2):295-313.

Add more citations