Embedding intuitionistic-type theory in negationless-type theory
From MaRDI portal
(Redirected from Publication:1820157)
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.
Recommendations
- A formal system of negationless arithmetic that is conservative with respect to Heyting arithmetic
- scientific article; zbMATH DE number 3937178
- A negationless interpretation of intuitionistic theories
- scientific article; zbMATH DE number 3853066
- A negationless interpretation of intuitionistic theories. II
Cites work
- A formal system of negationless arithmetic that is conservative with respect to Heyting arithmetic
- scientific article; zbMATH DE number 3059607 (Why is no real title available?)
- 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
Cited in
(8)- A formal system of negationless arithmetic that is conservative with respect to Heyting arithmetic
- A negationless interpretation of intuitionistic theories. II
- A negationless interpretation of intuitionistic theories
- Shallow embedding of type theory is morally correct
- The FAN principle and weak König's lemma in Herbrandized second-order arithmetic
- scientific article; zbMATH DE number 3937178 (Why is no real title available?)
- scientific article; zbMATH DE number 25594 (Why is no real title available?)
- Typed Lambda Calculi and Applications
This page was built for publication: Embedding intuitionistic-type theory in negationless-type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1820157)
