The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Michael O'Connor wrote:

> I'm interested in verifying things which can be proven in Heyting 
> Arithmetic, i.e. intuitionistic Peano Arithmetic, so there is no 
> higher-order induction.  Would it be possible to do something like 
> define a type HA_Prop such that if P : HA_Prop and t : P then t is 
> guaranteed to be a proof just using first-order induction.  Thanks 
> very much,

You can always axiomatize a sufficiently restrictive proof system inside 
of Coq (probably with inductive types), and instead ask for t : 
MyProofsOf P, where MyProofsOf is an indexed inductive type of proofs 
that you define.  I'd be surprised if there's a way to restrict the use 
of higher-order induction without doing something like this suggestion.