An intensional type theory: motivation and cut-elimination

DOI10.2307/2694928zbMath0980.03007OpenAlexW2063169574MaRDI QIDQ2732287

Paul C. Gilmore

Publication date: 12 March 2002

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

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

zbMATH Keywords

consistencycut-eliminationintentionalityRussell's setTakahashi-Prawitz completeness proofuse/mention distinction

Mathematics Subject Classification ID

Philosophical and critical aspects of logic and foundations (03A05) Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Second- and higher-order model theory (03C85)

Related Items (1)

An untyped higher order logic with Y combinator

Uses Software

• TPS
• HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Conceptual realism versus Quine on classes and higher-order logic
• A proof of cut-elimination theorem in simple type-theory
• Natural deduction based set theories: a new resolution of the old paradoxes
• A partial functions version of Church's simple theory of types

This page was built for publication: An intensional type theory: motivation and cut-elimination