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

Indeed. I've heard people refer to ELF as a framework logic only,
whereas Gödel as a meta-logic only.

John

>>
>>
>> Thanks
>>
>> John
>>
>





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