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

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