Arun, Chris: (01)
In SpecWare (http://www.specware.org), there is one often used technique
that resembles the kind of metatheory you are talking about.
The principle is, roughly, to write a small specification that provides
an axiomatic theory of something; e.g., the concept of list, set, array,
etc...
and such specifications are used as "metatheories" by specifying axioms
regarding the existence of an isomorphism
between the "metatheory" specification (e.g., list, set, ...) to the
target "theory" which we claim to have the properties of the metatheory. (02)
I believe that other systems like HetCASL (see:
http://www.brics.dk/Projects/CoFI/) do similar tricks.
The key point; however, is that the "metatheory" and "theory" are
written in the same "logic" which, if it isn't implemented "natively"
can also be mapped via isomorphism to a semantically equivalent form in
another language for which we have a decision procedure
or theorem prover (e.g., SpecWare encodes its "MetaSlang" logic into
SNARK's language at which point it can use SNARK's theorem prover
to reason (indirectly) about logic sentences in MetaSlang). (03)
Is this the kind of approach that you are advocating Arun? (04)
-- Nicolas. (05)
Arun Majumdar wrote: (06)
> Dear Chris,
>
> Yes - that is precisely it! And then I was indicating my interest to
> enrich this with by building in a model for Category Theory (ie. to
> create a version with rules and operations) as a second step.
>
> Let me see if I can refine my language on this (noting that my
> curiosity and interest stem from the analogical cognitive reasoning
> capabilities that I naturally perceive humans to perform without even
> thinking about it!)
>
> I am trying to identify a logic using CL that would contain
> propositional connectives, or modifiers whose semantics refers to
> other models external to the model upon which they are defined. I
> think I can call this the metalogical operators that permit CL to be
> interpreted dynamically, so that CL might be used to provide a
> language to transform/change/update the current model (even CL
> itself). These metalogical (extralogical?) operatorssuggest that we
> try to capture the properties of model in an indirect manner by
> parameters of the model’s possible modifications.
>
> My hope is that we can consider for further use what elements along
> the lines suggested might provide a dynamical, evolvable,
> model-theoretic semantics, in which Kripkean possible-world semantics
> applies to levels of models (in a single state that perhaps we might
> over-zealously call 'context'?) instead of the level of states in a
> single model.
>
> Is there a preffered pointer to the Common Logic material regarding
> the proposals you mentioned (as I went to the site but was unsure and
> hope that you have indications where specifically I might look) ?
>
> Thank you Chris,
>
> Arun
>
> Chris Menzel wrote:
>
>> First, I kvetch yet again: Can we not have a COSMO-WG mailing list
>> rather than a humongous cc list?
>>
>> On Wed, Jan 18, 2006 at 12:29:21AM -0500, Arun Majumdar wrote:
>>
>>
>>> Dear Leo,
>>>
>>> You wrote the following (to which I strongly agree and have some
>>> comments following)
>>>
>>>
>>>
>>>> I would use some variant of Common Logic (and possibly IKL from the
>>>> IKRIS project, once that is fully specified), because it (they) as
>>>> first-order logic languages are more expressive formally than
>>>> >OWL+SWRL.
>>>>
>>>
>>> In my current commercial work elsewhere, the most troublesome aspect
>>> that I face in interoperability projects is the difficulty defining
>>> a theory that directly supports a first-order manipulation of
>>> theories and models, independently from the particular foundational
>>> ontology that it is plugged in: Common Logic is an excellent first
>>> step, however, all ACL's for knowledge exchange require the latter
>>> (theory) to succeed
>>> ...
>>>
>>
>>
>> Let me just see if I understand you, Arun: You want a formal
>> first-order theory that, in essence, axiomatizes the metatheory --
>> notably, the proof theory and the model theory -- of first-order logic.
>> So, more specifically, you want a theory that axiomatizes such
>> predicates as "constant", "predicate", "formula", "proof",
>> "interpretation", "true in an interpretation", etc, is that right? Of
>> course, through the magic of encoding, we already *have* such a theory
>> -- Zermelo-Fraenkel set theory -- but I take it you'd prefer something a
>> bit less abstract. The Common Logic group has already come up with a
>> couple of proposals for theories of quotation that enable one to
>> introduce metatheoretic predicates like the ones above. Add enough set
>> theory to define the semantic predicates, and the result would seem to
>> be the sort of thing you are looking for.
>>
>> Chris Menzel
>>
>>
>>
>>
>>
>
>
> _________________________________________________________________
> Message Archives: http://colab.cim3.net/forum/ontac-dev/
> To Post: mailto:ontac-dev@xxxxxxxxxxxxxx
> Subscribe/Unsubscribe/Config:
> http://colab.cim3.net/mailman/listinfo/ontac-dev/
> Shared Files: http://colab.cim3.net/file/work/SICoP/ontac/
> Community Wiki:
> http://colab.cim3.net/cgi-bin/wiki.pl?SICoP/OntologyTaxonomyCoordinatingWG
>
> (07)
_________________________________________________________________
Message Archives: http://colab.cim3.net/forum/ontac-dev/
To Post: mailto:ontac-dev@xxxxxxxxxxxxxx
Subscribe/Unsubscribe/Config: http://colab.cim3.net/mailman/listinfo/ontac-dev/
Shared Files: http://colab.cim3.net/file/work/SICoP/ontac/
Community Wiki:
http://colab.cim3.net/cgi-bin/wiki.pl?SICoP/OntologyTaxonomyCoordinatingWG (08)
|