Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem
On Thu, 19 Jul 2012, Gottfried Barrow wrote:
Here is my conclusion/lesson, which is merely stating the obvious: If I
don't axiomatize things right, I get inconsistencies.
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', ...
Unfortunately, I don't understand types, lambda calculus, and the "="
function well enough to know why.
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, ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and