Embedding intuitionistic-type theory in negationless-type theory

DOI10.1007/BF01647635zbMath0614.03057MaRDI QIDQ1820157

Victor N. Krivtsov

Publication date: 1986

Published in: Mathematical Notes (Search for Journal in Brave)

zbMATH Keywords

Heyting arithmeticintuitionistic type theorynegationless type theory

Mathematics Subject Classification ID

Intuitionistic mathematics (03F55) Relative consistency and interpretations (03F25)

Cites Work

• Unnamed Item
• A formal system of negationless arithmetic that is conservative with respect to Heyting arithmetic
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Two Applications of Logic to Mathematics