Re: [isabelle] Is Isabelle/Pure really a meta-logic?
> If you treat "meta-logic" and "framework logic" as synonymous, does this
> problem go away?
I don't think they're synonymous though. My impression is that if an
object-logic is encoded within a meta-logic, then reasoning in the
object-logic involves some kind of meta-level reasoning. In both
cases, does the unification algorithm reason with higher-order
abstract syntax? Also, is there inference in both object- and
meta-levels in both cases?
> (Maybe you've heard "framework logic" used to mean something else somewhere,
Indeed. I've heard people refer to ELF as a framework logic only,
whereas Gödel as a meta-logic only.
This archive was generated by a fusion of
Pipermail (Mailman edition) and