The logic of first order intuitionistic type theory with weak sigma-elimination

DOI10.2307/2274694zbMath0736.03023OpenAlexW2017441861MaRDI QIDQ3984424

M. D. G. Swaen

Publication date: 27 June 1992

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

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

zbMATH Keywords

Heyting arithmeticconservative extensionexistence elimination rulefirst order intuitionistic type theoryfirst-order intuitionistic arithmeticrealizing termsweak sigma-elimination

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30)

Cites Work

• Constructivism in mathematics. An introduction. Volume II

This page was built for publication: The logic of first order intuitionistic type theory with weak sigma-elimination