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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and