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


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