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.
Similar content being viewed by others
References
D. van Dalen,The use of Kripke's schema as a reduction principle, Journal of Symbolic Logic 42 (1977), pp. 238–240.
G. Kreisel,A survey of proof theory II. Proc. 2nd Scandinavian Logic Symposium Oslo 1970, North-Holland Publ. Co. 1971, pp. 109–170.
H. Luckhardt,On constructive functions ranging over propositions, to appear in this journal, pp. 371–374.
-,Anti-basis results for the intuitionistic propositional quantifiers.
J. Myhill andA. Scedrov,Notices AMS 26 (Jan. 1979), A-21, 763-02-02.
A.S. Troelstra,Notes on intuitionistic second order arithmetic, Proceedings Cambridge Summer School in Mathematical Logic 1971, Lecture Notes in Mathematics 337 (1973), pp. 171–205.
-,Axioms for intuitionistic mathematics incompatible with classical logic, Proceedings 5th Int. Congr. Logic, Methodology and Philosophy of Science, London/Ontario 1975, Reidel Publ. Co. 1977, pp. 59–84.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Friedrich, W., Luckhardt, H. Intuitionistic uniformity principles for propositions and some applications. Stud Logica 39, 361–369 (1980). https://doi.org/10.1007/BF00713546
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00713546