A characterization of ML in many-sorted arithmetic with conditional application

DOI10.2307/2275440MaRDI QIDQ4032872zbMATH OpenOpenAlexFDO

Authors M. D. G. Swaen

Publication date 1 April 1993

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2307/2275440

zbMATH Keywords

intuitionistic type theoryformulas-as-types correspondenceMartin-Löf's type theorymany-sorted arithmeticaxiom of conditional choice

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50) Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• scientific article; zbMATH DE number 3853066
• Realizability and intuitionistic logic
• Characterizing the interpretation of set theory in Martin-Löf type theory
• scientific article; zbMATH DE number 1302058
• The strength of some Martin-Löf type theories

Cites work

• Constructivism in mathematics. An introduction. Volume II

Cited in

(1)

• Realizability and intuitionistic logic

This page was built for publication: A characterization of ML in many-sorted arithmetic with conditional application

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4032872)