Well, Dick, what can I say? I’m probably older than you, and the term ‘pragmatics’ was around in the early 1960s.
>> I had already graduated from college then -- before transistors & computers & computer science were the mainstream
‘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.
>> don't sentences and words both have meanings?
‘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.
>> now you've lost me. can you say that in simpler terms?
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.
>> i.e., it's all about symbols, and not connected to the real world? I prefer natural language.
>> do you call a computer language a formal language? it has a real world connection to an executable program.
>> the mKR language has an executable program
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.
>> I agree, up to the last sentence which I don't understand. Are you saying only people know what axiomatic concepts are,
>> and they know the meaning by direct perception (ostensive definition)
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.
>> there's so much jargon in these last two sentences, I don't know what you mean
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.
>> that sounds more like pragmatics, or is that forbidden in a logic language?
If you want to talk about the meanings of terms, and you are producing what you bel
ieve 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).
>> the syntax of mKR formal definition is: concept is genus with differentia;
So, if:
existent: entity, characteristic, proposition
>> you stumped me with this one, Ed.
>> I did not define a syntax for definition by enumeration.
>> I have enumerations, exclusive ors, etc.
>> but they are all designed to allow you to incrementally add species.
>> existent isc entity, characteristic, proposition; means a concept with 3 or more species
>> my actual complete meaning for this [no syntax defined]:
>> it is a definition by enumeration
>> species are mutually exclusive
>> species are exhaustive
>> this comment applies to all hierarchy descriptions
>> the species may be exclusive or not
>> the species may be exhaustive or not
>> if you choose to use only "isa", "isc", the species may actually be a unit or not
>> genus may be unique or not (if not, I call it ambiguous)
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.
>> I use Backus-Naur form to define syntax
>> I also plan to use standard iyacc/ulex tools (Unicon's variant of original yacc/lex tools)
>> but for my original implementation, I hand coded all my parsers using Unicon pattern matching
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.
>> I agree ![Emoji]()
-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: [ontolo
g-
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 rais
ed
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![]()
(850)434 8903 home
40 South Alcaniz St. (850)202 4416![]()
(850)202 4416 office
Pensacola (850)202 4440![]()
(850)202 4440 fax
FL 32502 (850)291 0667![]()
(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
_________________________________________________________________
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