Skip to main content
Log in

Intuitionistic uniformity principles for propositions and some applications

  • Published:
Studia Logica Aims and scope Submit manuscript

Abstract

This note deals with the prepositional uniformity principlep-UP: ∧p ∈ ΚxN A (p, x) → ∨xNp ∈ Κ 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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. D. van Dalen,The use of Kripke's schema as a reduction principle, Journal of Symbolic Logic 42 (1977), pp. 238–240.

    Google Scholar 

  2. G. Kreisel,A survey of proof theory II. Proc. 2nd Scandinavian Logic Symposium Oslo 1970, North-Holland Publ. Co. 1971, pp. 109–170.

  3. H. Luckhardt,On constructive functions ranging over propositions, to appear in this journal, pp. 371–374.

  4. -,Anti-basis results for the intuitionistic propositional quantifiers.

  5. J. Myhill andA. Scedrov,Notices AMS 26 (Jan. 1979), A-21, 763-02-02.

    Google Scholar 

  6. 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.

    Google Scholar 

  7. -,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.

Download references

Author information

Authors and Affiliations

Authors

Rights and permissions

Reprints 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

Download citation

  • Received:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF00713546

Keywords

Navigation