Proof-irrelevant model of CC with predicative induction and judgmental equality

DOI10.2168/LMCS-7(4:5)2011MaRDI QIDQ3224695zbMATH OpenOpenAlexFDO

Authors Gyesik Lee, Benjamin Werner

Publication date 2 April 2012

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1111.0123

zbMATH Keywords

calculus of constructionsconsistencyjudgmental equalityproof-irrelevance

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Axiomatics of classical set theory and its fragments (03E30)

Abstract: We present a set-theoretic, proof-irrelevant model for Calculus of Constructions (CC) with predicative induction and judgmental equality in Zermelo-Fraenkel set theory with an axiom for countably many inaccessible cardinals. We use Aczel's trace encoding which is universally defined for any function type, regardless of being impredicative. Direct and concrete interpretations of simultaneous induction and mutually recursive functions are also provided by extending Dybjer's interpretations on the basis of Aczel's rule sets. Our model can be regarded as a higher-order generalization of the truth-table methods. We provide a relatively simple consistency proof of type theory, which can be used as the basis for a theorem prover.

Recommendations

• A proof-irrelevant model of Martin-Löf's logical framework
• Proof by consistency in conditional equational theories
• Predicate provability logic with non-modalized quantifiers
• The predicate modal logic of provability
• Finite Kripke models and predicate logics of provability
• Constructive predicate logic with strong negation and model theory
• Provability in predicate product logic
• Model existence theorem in superrelevant predicate logics
• Model-theoretic characterization of intuitionistic predicate formulas
• scientific article; zbMATH DE number 7204319

Cited in

(7)

• Independence of the induction principle and the axiom of choice in the pure calculus of constructions
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• scientific article; zbMATH DE number 2003160 (Why is no real title available?)
• A simple model construction for the calculus of constructions
• Cumulative inductive types in Coq
• An intuitionistic set-theoretical model of fully dependent CC
• Correct and complete type checking and certified erasure for \textsc{Coq}, in \textsc{Coq}

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Proof-irrelevant model of CC with predicative induction and judgmental equality

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3224695)