Embedding intuitionistic-type theory in negationless-type theory
type: Item
instance of: scholarly article
title: Embedding intuitionistic-type theory in negationless-type theory
zbMATH Open document ID: 0614.03057
DOI: 10.1007/BF01647635
published in: Mathematical Notes
publication date: 1986-01-01T00:00:00Z
review text: In ''A formal system of negationless arithmetic that is consistent with respect to Heyting arithmetic'' [Mat. Zametki 36, No.4, 583-592 (1984; Zbl 0576.03037)] the author shows that Heyting arithmetic is a conservative extension of \(HA^ N\)- a system of negationless arithmetic, under certain interpretation. Here he extends this result to the case of intuitionistic type theory HATT and a system of negationless type theory HATTN.
Mathematics Subject Classification ID: 03F55
Mathematics Subject Classification ID: 03F25
zbMATH DE Number: 3993583
zbMATH Keywords: Heyting arithmetic
zbMATH Keywords: intuitionistic type theory
zbMATH Keywords: negationless type theory
author: Victor N. Krivtsov
reviewed by: Roman Kossak
MaRDI profile type: Publication
cites work: A formal system of negationless arithmetic that is conservative with respect to Heyting arithmetic
cites work: Q5798786
cites work: Two Applications of Logic to Mathematics
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
description: scientific article; zbMATH DE number 3993583