Re: [isabelle] Trying to fit HOL to traditional math verbiage
On Sat, Nov 5, 2011 at 11:46 AM, James Frank <james.isa at gmx.com> 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.
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and