Dear Chris, (01)
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. (02)
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!) (03)
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. (04)
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. (05)
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) ? (06)
Thank you Chris, (07)
Arun (08)
Chris Menzel wrote: (09)
>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
>
>
>
>
> (010)
_________________________________________________________________
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 (011)
|