Interpreting descriptions in intensional type theory

DOI10.2178/jsl/1120224725zbMath1089.03051OpenAlexW2073858584MaRDI QIDQ5718672

Jesper Carlström

Publication date: 16 January 2006

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

Full work available at URL: https://semanticscholar.org/paper/4d9e749ea26d9204b7651e6b4a7024aca37d1e59

zbMATH Keywords

constructive mathematicsnatural deductiondefinite descriptionsindefinite descriptionsintensional type theory

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55)

Related Items (2)

A novel approach to equality ⋮ Free Definite Description Theory – Sequent Calculi and Cut Elimination

Cites Work

• The predicate calculus with \(\varepsilon\)-symbol
• A course in constructive algebra
• Heyting predicate calculus with epsilon symbol
• Intuitionistic Predicate Calculus with ^|^epsilon;-Symbol
• A General Theory of Completeness Proofs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Interpreting descriptions in intensional type theory