Email Gateway (Aug 22 2022 at 19:25): Email Gateway (Aug 22 2022 at 19:25):From: daniel de la concepción sáez <danconsa@hotmail.com>
Hello,
I’m trying to create a command for defining types from FOL, inspired from typedef.ML in HOL, but my axioms do not unify with the theorems because the new type have no sorts and “term” is needed.
Can anybody help me with this?
Thank you,
Daniel de la Concepción
Email Gateway (Aug 22 2022 at 19:54):From: Makarius <makarius@sketis.net>
(This thread is still open.)
First note that a "typedef" in HOL is a certain axiom scheme that can be
interpreted as a definition in the context particular semantics for HOL
that allows to do that. That sounds a bit self-referential, but reflects
the true situation.
If you want to mimic that in FOL, you cannot assume such an
interpretation a-priori, but FOL specifications are usually axiomatic
anyway. Thus it is better to call such a command something like
'subtype_axiomatization'.
For the implementation in Isabelle/ML, the usual strategy is to look
very closely how it is done elsewhere and transfer that carefully to
your own application. That is a very abstract hint, in practice it needs
to be applied to concrete sources and concrete examples (which are
missing here).
Guessing blindly at your situation, I would say that it is a problem of
the "base sort" of the object-logic. See also Typedecl.typedecl and the
following description in header of that module:
"Type declarations (with object-logic arities) and type abbreviations."
The relevant operations are Object_Logic.get_base_sort and
Object_Logic.add_base_sort -- the latter is used in src/HOL/HOL.thy at
the start.
That omission in FOL is not an accident: the logic works slightly
differently from HOL, not all types are automatically considered plain
things.
Thus we are back to the observation that transferring the peculiar HOL
typedef to FOL requires to rethink the logic carefully.
Makarius
Last updated: May 06 2024 at 08:19 UTC