Re: [isabelle] Is Isabelle/Pure really a meta-logic?



Right. Thanks.

So is there actually meta-level inference in Isabelle? The unification
algorithm implemented is intended to work on object-logics, right?

John

On Wed, Aug 22, 2012 at 6:36 PM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> I regard the two terms as synonymous.
> Larry Paulson
>
>
> On 22 Aug 2012, at 18:34, John Munroe <munddr at gmail.com> wrote:
>
>>>
>>> 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.