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



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.