coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]heyting arithmetic

From: "Michael O'Connor" <mkoconnor AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club]heyting arithmetic
Date: Wed, 8 Feb 2006 10:30:49 -0500
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:to:subject:mime-version:content-type; b=A6ytlkyf6J6s8JC69DAkYmotOjiUBbYJ80k/y0h1swaHyPFIU4uBodFVbIXDFtsFqXPlpg8JKSWFLS9UlpA1s/GEBfedthj7uu+3sK6ODdRaKjeaImQkeOiGlTTMDmWjrkd3cerbudRx9vvo98GZ1d1bZ8/VxxcGpa+94ESe0b0=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,

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,

Michael O'Connor

[Coq-Club]heyting arithmetic, Michael O'Connor
- Re: [Coq-Club]heyting arithmetic, Adam Chlipala
  - Re: [Coq-Club]heyting arithmetic, Benjamin Werner