Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default
I totally goofed. The title of the book is "Introduction to higher order categorical logic”.
There’s a lot of category theory to get through before they give you a presentation of intuitionistic HOL. But possibly some paper does it more directly. Isabelle does indeed support intuitionistic logics, though with less automation than for classical ones. See Isabelle/IFOL.
> On 21 Dec 2014, at 22:51, Josh Tilles <merelyapseudonym at gmail.com> wrote:
> and this does indeed require intuitionistic logic. If you really want to create a constructive theory of higher-order logic, you will need to start from scratch.
> *sigh* I knew that that it might come to that.
> A suitable axiom system can be found in the book Logic and Structure by Lambek and Scott.
This archive was generated by a fusion of
Pipermail (Mailman edition) and