Re: [isabelle] Trying to fit HOL to traditional math verbiage


On Sat, Nov 5, 2011 at 11:46 AM, James Frank <james.isa at> wrote:

>> Anything that you can define in higher-order logic is not merely
>> explicable in traditional mathematical terms, but it is easily so. But there
>> are plenty of things you can write in mathematics that are impossible to
>> formalise in higher-order logic.
> The good news is that different foundations converge at a higher point where
> they a lot of math in common.
> Again, there's no real problem. Very few people have an in-depth
> understanding of the foundations of math, so there's a lot of skipping that
> low level stuff anyway, or totally ignoring it.
> --James

JFYI, perhaps you should bring up some of these questions on the
Foundations of Mathematics (FOM) mailing list to get some of the
insight from the "other side" and see what they have to say about HOL
and FOM.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.