Derived rules related to a constructive theory of metric spaces in intuitionistic higher order arithmetic without countable choice

DOI10.1016/0003-4843(80)90019-4zbMath0457.03054OpenAlexW1975401561MaRDI QIDQ3905274

Susumu Hayashi

Publication date: 1980

Published in: Annals of Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0003-4843(80)90019-4

zbMATH Keywords

algebraically closedcomplex numbersbar inductionconstructive analysisDedekind realscontinuous local choice

Mathematics Subject Classification ID

Metric spaces, metrizability (54E35) Other constructive mathematics (03F65) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50)

Related Items (3)

Choice and independence of premise rules in intuitionistic set theory ⋮ Derived rules for predicative set theory: an application of sheaves ⋮ Unique existence, approximate solutions, and countable choice.

This page was built for publication: Derived rules related to a constructive theory of metric spaces in intuitionistic higher order arithmetic without countable choice