Well, Dick, what can I say? I’m probably older than you, and the term ‘pragmatics’ was around in the early 1960s.
‘Semantics’ is not about the meaning of ‘words’; it is about the meaning of ‘utterances’ – typically statements in the language. It is the meaning conveyed
by the syntax given the terms that appear in the syntactic construct.
‘Pragmatics’ is about overloading the utterance per se with meaning conveyed by the speech act itself, and perhaps its context, and it touches on the notion
‘modality’ in logic and natural language.
The semantics of a formal language is primarily about the meaning of its syntactic constructs, stated in terms of parametric entities that are the non-terminal
symbols in the construct specification.
Formal language semantics can only deal with the meaning of terms (“words”) that have formal definitions in the language. Ultimately, any given ‘terminological
dictionary’ must be founded on a set of ‘primitive’ terms that do not have formal definitions. In the best of cases, e.g., mathematics, in lieu of a formal definition of a ‘primitive’ term, there is a set of axioms about the term, and any “thing” in the universe
of discourse that satisfies those axioms is necessarily a referent of the term. That is, if it walks like a duck and talks like a duck, it IS a duck. If you don’t have a formal definition or an axiomatic characterization, the term is formally UNDEFINED.
The meaning is something that only some speech community knows.
In formal languages, we tend to shy away from pragmatics. The speech act is almost always just presentation of a text corpus that stands for itself. That
said, the intended USE of the text corpus may have some pragmatic impact on its interpretation, but that is often confined to the intent of the primitive terms.
In logic languages, the semantics of the language is usually stated in terms of a set – the universe of discourse, the things that the language can refer to
– and two “distinguished values”: True and False. And the semantics of each syntactic construct is explained in terms of those elements. The “meaning” of a term is either a syntactic construct that is so described, or “unknown” -- the term is ‘primitive’.
For example, an OWL Class term refers to some subset of the universe of discourse set. If the term is said to be equivalent to an OWL Class _expression_, then you have a formal way of relating that set to other sets. If the term is primitive, you don’t have
a language rule that tells you anything much about what set that is, and in all probability the user will end up enumerating all the individual things that are interesting and are in it.
If you want to talk about the meanings of terms, and you are producing what you believe are formal definitions of the terms, you have to explain the syntax
of your formal definitions clearly, and you have to give the rule that explains how each syntactic construct relates to the universe of discourse, TRUE and FALSE (or something very much the like).
So, if:
existent: entity, characteristic, proposition
has a meaning in mKR, then there must be a syntax rule, e.g.,
definition = defined-term, “:”, defining-construct ;
defining-construct = union-construct | ... ;
union-construct = term1 { “,” termK } ;
and some ‘semantics’ rule that says:
The defined-term denotes a mapping from each element of the universe of discourse to exactly one of {TRUE, FALSE}.
For every element of the universe of discourse, the defined-term maps the element to TRUE if the defining-construct maps the element to TRUE, and otherwise
the defined-term maps the element to false.
Then you can define the union-construct as a mapping from the UoD to True/False in terms of term1 and each termK: For any element of the UoD, if ANY termK
in the list maps it to True, then the union-construct maps it to True; if no termK maps it to True, then the union-construct maps it to False.
There are other ways to do this. You can talk about sets instead of mappings, for example, as in the OWL semantics. But you need some kind of formal basis
for describing “semantics”. In fact, I think you did this, in your own way, to explain the meaning of that particular construct. But your readers are still pretty much in the dark about what the syntax rules are, and what the formal interpretation of an
arbitrary rule is.
This approach has been in use since the 1950s, even though I did not learn its application to formal logic until 1970. It is a version of “Tarski’s method”.
Peter Naur and friends used a very similar approach in defining the Algol programming language in 1960. You can see versions of it in the specifications for COBOL, Euclid, Pascal, Ada and C. That said, it took OMG a mere 12 years to figure out that they
needed to do something like this for UML.
There are lots of people trying to capture knowledge in various ways, coming from different backgrounds that don’t involve the formal concepts associated with
“semantics”. They use the term to mean “what the author meant by the word”, or “what my program does with that”, and that is NOT what ‘semantics’ means in ontological circles, including linguistics. And that is part of why your audience on this Forum is
confused by your writing.
I understand “proof of correctness” to be a characterization of an algorithm in terms of a parametrized start state and a corresponding end state that is seen
as the “correct result” of the start state. Then, using some formal characterization of the behavior of the algorithm, e.g. Z, you create a formal logical proof that the “correct” end state is exactly what is produced from the start state. That is you prove
that, for all admissible S1(v1, ..., vN), A maps S1 to S2 (v1, ..., vN). This is the Holy Grail of software assurance.
I have no idea what “proof of correctness” could possibly mean for an ontology. By definition, every assertion in an ontology is True. What you may be able
to prove is “consistency” -- that the intended reasoning rules applied to the ontology as a whole cannot produce (and P (not P)) for any proposition P.
-Ed
From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx [mailto:ontolog-forum-bounces@xxxxxxxxxxxxxxxx]
On Behalf Of Richard H. McCullough
Sent: Thursday, April 03, 2014 7:05 AM
To: [ontolog-forum]
Subject: Re: [ontolog-forum] mKR proof of correctness
Well -- I knew my age would betray me eventually.
I grew up in the era when the terms were
syntax
semantics
and semantics was concerned with the meaning of words.
Today, I think the popular terms are
syntax
semantics
pragmatics
and semantics is concerned with transformations of propositions
and pragmatics is concerned with the meaning of words.
So I am more focused on pragmatics, and haven't thought that much
about semantics.
But old habits are hard to break, and I keep saying semantics
when I shouldn't. I apologize for the confusion.
My errors in terminology do not alter the validity of the
Objectivist Axioms, or their usefulness. I will say more about
that later -- in response to another question which was raised
here in the Ontolog Forum.
Dick McCullough
Context Knowledge Systems
mKE and the mKR language
mKR/mKE tutorial
Date: Wed, 2 Apr 2014 23:26:21 -0700
From: steven@xxxxxxx
To: ontolog-forum@xxxxxxxxxxxxxxxx
Subject: Re: [ontolog-forum] mKR proof of correctness
Semantics generally say nothing about the world. They are the valid rules of syntax transformation (per Carnap).
McCullough's axioms make little sense to me. Indeed, they do not appear, in fact, to be axioms.
On Wed, Apr 2, 2014 at 8:21 PM, Pat Hayes <phayes@xxxxxxx> wrote:
On Apr 2, 2014, at 5:10 PM, Richard H. McCullough <rhmccullough@xxxxxxxxx> wrote:
> John
>
> I don't want there to be any doubt about what I'm saying,
> so I'm devoting one extra email to this topic.
>
> The mKR language is proved semantically correct
> because the mKR run-time system guarantees
> that the Objectivist Axioms are satisfied.
I actually laughed out loud when I read this. First, I have no idea what you mean by proving a language to be semantically correct, but claiming anything semantic **because some axioms are
present** misses the entire point of having semantics in the first place, which is to connect formal sentences with claims about the actual world. Then again there is your conflation of semantics with a 'run-time system', which I take it means a system that
performs inferences. But without an independent semantics, how does one know that these inferences are valid or complete? The general problem of proving that a program is correct is still open, of course, but any approach to even defining what this means requires
that the language of the program has some kind of separate semantics. If the run-time system *Is* the semantics then 'correctness' is trivial to prove - the program does what the program does - but also trivially meaningless. But the final howler here is the
idea that Ayn Rand's
thoughts might have anything, even the shred of a remotest connection, to do with correctness, in any sense of that word.
IF your notation had a semantic theory that would enable an objective check to be made on its validity, and IF you could then show that those axioms were satisfied AND that your run-time system preserved truth (or whatever your semantics calls it), then you
might reasonably claim that mKE had a property that one might call Randianicity: conformity to the thoughts of Ayn Rand. But to call this property "semantic correctness" is simply farcical.
Pat Hayes
>
> Dick McCullough
> Context Knowledge Systems
> mKE and the mKR language
> mKR/mKE tutorial
------------------------------------------------------------
IHMC (850)434 8903 home
40 South Alcaniz St. (850)202 4416 office
Pensacola (850)202 4440 fax
FL 32502 (850)291 0667 mobile (preferred)
phayes@xxxxxxx
http://www.ihmc.us/users/phayes
_________________________________________________________________
Message Archives:
http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr:
http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join:
http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
_________________________________________________________________ Message Archives:
http://ontolog.cim3.net/forum/ontolog-forum/ Config Subscr:
http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/ Unsubscribe:
mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx Shared Files:
http://ontolog.cim3.net/file/ Community Wiki:
http://ontolog.cim3.net/wiki/ To join:
http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J