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
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