On a second order propositional operator in intuitionistic logic

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

Abstract

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.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,593

External links

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

Through your library

Analytics

Added to PP
2009-01-28

Downloads
54 (#264,075)

6 months
6 (#202,901)

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