The Coq mailing list

[Benjamin Werner <Benjamin.werner AT inria.fr>]

Yes. Actually if t : P and P : HA_Prop, then HA_Prop should be Prop  
or Type. So indeed you have to formalize
the syntax of the propositions of arithmetic as a data-type, which  
you can call HA_Prop, and then define a predicate

HA : HA_Prop -> Prop (or Type)

which states that a proposition is provable in HA.

Note that you can "lift" HA into Coq by defining a translation :

tr : HA_Prop -> Prop (or Type)

and proving :

(HA p) -> (tr p)

(to be precise you have to deal with hypotheses and free variables also)

This was the topic of the individual Coq projets of last year's  
master's course over here.

Good luck,


Benjamin



Le 8 févr. 06 à 17:42, Adam Chlipala a écrit :

> 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.
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club