Coq中定义归纳命题时，哪些约束可保障系统一致性？

Great question! You’re exactly right that defining inductive propositions in Coq feels like adding new reasoning rules or axioms to the system. To make sure Coq stays consistent (i.e., we can’t prove False), there are several key constraints you must follow when writing these definitions:

# Positive Occurrence (Strict Positivity) Requirement #

This is the most critical rule: the inductive proposition itself can only appear in positive positions within its own constructor types. A positive position is one where it’s not on the left side of an implication (->) or inside a negation (~).

For example, this is a bad definition that violates strict positivity:

Inductive Paradox : Prop := paradox : (Paradox -> False) -> Paradox.

This lets you derive False directly (you can construct a term that loops into a contradiction). On the other hand, a valid definition like evenness follows the rule:

Inductive Even : nat -> Prop :=
  | even_0 : Even 0
  | even_SS : forall n, Even n -> Even (S (S n)).

Here, Even only appears on the right side of implications (as the premise of even_SS), which is a positive position.

# Impredicativity Limits for Prop #

Coq treats Prop as an impredicative universe—meaning you can quantify over all propositions when defining a new one. But this comes with a catch: inductive propositions in Prop can’t have constructors that reference the inductive type in a way that creates a circular quantification over all propositions.

For example, you can’t define an inductive type like:

Inductive Bad : Prop := bad : (forall P : Prop, P -> Bad) -> Bad.

This would let you encode paradoxes by quantifying over all propositions, including Bad itself. Coq’s type checker rejects such definitions automatically.

# No Unguarded Recursion #

Inductive definitions can be recursive, but the recursive references must be guarded—meaning they’re nested inside the constructor’s parameters in a way that builds up the inductive structure, not loops infinitely.

A classic bad example is:

Inductive InfiniteLoop : Prop := loop : InfiniteLoop -> InfiniteLoop.

This has no base case and the recursive reference isn’t guarded by any structure-building step. Coq rejects this because it doesn’t correspond to a well-founded inductive structure (there’s no way to construct a finite term of this type without infinite recursion).

# Restrictions on Large Elimination #

By default, inductive propositions in Prop can only be eliminated into other propositions (i.e., you can use induction to prove another Prop, but not to construct a term in Set or Type). This is called "small elimination."

If you try to use large elimination (eliminating a Prop-valued inductive type into Set/Type), Coq will block you unless you explicitly enable it with commands like Set AllowLargeElimination. Doing this is risky, though—large elimination for impredicative Prop can lead to inconsistencies, as it lets you convert logical proofs into computational data in a way that breaks the system’s soundness.

These constraints aren’t arbitrary—they’re rooted in proof theory and ensure that every inductive proposition corresponds to a well-founded mathematical structure (a least fixed point in the universe of propositions). By following them, you guarantee that your additions to Coq’s logic don’t introduce contradictions.

内容的提问来源于stack exchange，提问作者ktak