On a second order propositional operator in intuitionistic logic |
| |
Authors: | A S Troelstra |
| |
Institution: | (1) Mathematisch Instituut, Universiteit van Amsterdam, Postbus 20239, 1000 HE Amsterdam, Netherlands |
| |
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.Parameters of the required kind can be obtained as so-called projections of lawless sequences. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|