CODEWITHSUNDEEP
logiccoq
ktak
ktak

Reputation: 23

Consistency of Inductive propositions

In coq, defining an inductive proposition seems analogous to adding new inference rules/axioms to a logic. What constraints in defining an inductive proposition guarantees that coq remains consistent?

Upvotes: 2

Views: 66

Answers (1)

ejgallego
ejgallego

Reputation: 6852

This is a very good, and not easy to answer question. The "Calculus of Inductive Constructions" has been analyzed in literally hundredths of papers.

The most accepted argument for justification of consistency is the equivalence of W-types with inductive data types. In this sense, every inductive type you add to the theory is just an instance of a W-type, which is an object that is supposed to be well-founded and thus not a danger to the consistency of the theory.

However, the details of Coq's implementation are a bit more complicated, mainly due to the reliance on the "guard condition" for programming convenience. The also provide support for impredicate inductives and these tend to be quite complicated objects. I suggest you read a bit about this and ask more concrete questions. The main reference is "C. Paulin-Mohring. Inductive Definitions in the System Coq" .

See also this wiki page

Upvotes: 2

Related Questions