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

DOI10.2307/2275440zbMATH Open0767.03030OpenAlexW2015291418MaRDI QIDQ4032872FDOQ4032872

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

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

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)

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)