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

On 11/06/2011 05:38 AM, Josef Urban wrote:
 I think it would not
hurt the formal systems to go where the mathematicians are.


Unfortunately "where the mathematicians are" is to use language in a way which is typical of natural languages, which contain exactly the sort of inconsistencies and ambiguities which lead people to use formal systems instead.

For example, mathematicians say things like "the derivative of f(x)", when they are referring to the derivative of f, and they say f(n) = O(g(n)) (but that O(g(n)) is a set of functions), when they mean f is _in the set_ O(g) - etc.


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