Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem



On 7/20/2012 6:23 AM, Makarius wrote:
Axiomatizations are very difficult to get right. Experts usually avoid
them altogether, and use definitions exclusively. Definitions can be as
diverse as 'definition', 'inductive', 'function', 'locale', ...

I briefly thought about how to use definitions, just to try and use good discipline. Suppose I have 7 standard axioms that I have to use. Then I guess I could define an object, function, or property with a big conjunction using the 7 axioms.

If I see the right example, it'll become clear. Using axioms lets me start working on a real application right now as a diversion, instead of waiting until I've become thoroughly educated, which could be a long process. Trying to apply what I know at any point in time helps drive it into long term memory, and usually requires me to learn something in addition to the knowledge I'm trying to apply.

Lambda calculus is just notations for mathematical functions; '=' is
plain classical equality on arbitrary mathematical entities, including
functions.

HOL is more simple than FOL, because it does not impose any restrictions
about quantification and equality.

Types in HOL are just separate syntactic domains, which are always
non-empty by construction of the logic. This is like the implicit
(single) domain of discourse in FOL, but HOL allows many of them, also
constructors to operate on such domains: nat, nat => bool, nat set,
nat list, ..., 'a * 'b, ...

Thanks for the summary. Not understanding subtleties can kill me, but I also need to understand the big picture.

Quantifying over functions has me a little worried. I see the need to quantify over types of something like "sT => bool", rather than over just a primitive type variable. If I'm doing that in what would normally be a FOL system of logic, then I've entered the realm of higher order logic. I don't care about that. I only care that I get busted for doing it.

I head down the road semi-blind, and find out where it leads.

Regards,
GB






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