Intuitionistic uniformity principles for propositions and some applications |
| |
Authors: | W Friedrich H Luckhardt |
| |
Institution: | (1) J.W. Goethe-Universität Fachbereich Mathematik, Frankfurt am Main |
| |
Abstract: | This note deals with the prepositional uniformity principlep-UP: p x N A (p, x) x N p A (p, x) ( species of all propositions) in intuitionistic mathematics.p-UP is implied by WC and KS. But there are interestingp-UP-cases which require weak KS resp. WC only. UP for number species follows fromp-UP by extended bar-induction (ranging over propositions) and suitable weak continuity. As corollaries we have the disjunction property and the existential definability w.r.t. concrete objects. Other consequences are: there is no non-trivial countable partition of;id is the only injective function from to; there are no many-place injective prepositional functions; card () is incomparable with the cardinality of all metric spaces containing at least three elements. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|