Ontology Summit 2018

[kenb]

You are invited to attend the first research session of the Ontology
Summit 2018 "Ontologies in Context" which will be held on Wednesday,
September 13, 2017, starting at Noon Eastern Time. At this meeting we
will be discussing three papers as shown on the meeting page. I will be
presenting these papers.

The meeting page is http://bit.ly/2wVrWxz

The Video Conference URL is https://bluejeans.com/703588230

The Ontology Summit 2018 will consist of three phases:

Research and planning phase from now until mid-November.
Weekly invited speaker phase starting in January.
2-day Symposium at a date to be determined.

The schedule for the research and planning phase is:

2017-09-13 First Research Session
2017-09-20 Second Research Session
2017-09-27 Third Research Session
2017-10-04 Specifying Context with Situations
2017-10-11 Clarifying the Relationships among Ontologies, Context and
System Realization and Efficacy
2017-10-18 Specifying Context with Upper Ontologies
2017-10-25 Linguistic Contexts
2017-11-01 Contexts for Integration and Interoperability
2017-11-08 General Planning Session
2017-11-15 Final Planning Session

Ken Baclawski
Member - Ontolog Forum Board of Trustees

[Andrea Westerinen]

My apologies for missing the call yesterday, I was not feeling well.  Talk to you all next week!

Andrea Westerinen

T: 425.891.8407

arwest...@gmail.com or and...@ninepts.com

organizingknowledge.blogspot.com

[kenb]

You are invited to attend and participate in the next session of the
Ontology Summit 2018 which will feature John Sowa who will be speaking on:

"Reasoning with and about contexts: the 'ist' and 'that' operators"

The session will be held on Wednesday, Sept. 20, 2017 at Noon Eastern Time.
The meeting page is http://bit.ly/2xrtkrE

The Video Conference URL is https://bluejeans.com/703588230

The chat room is http://webconf.soaphub.org/conf/room/ontology_summit_2018

The video recording of the research session of the Ontology Summit 2018
held on 9/13/2017 is now available at http://bit.ly/2hcGb74 and the
meeting page is bit.ly/2wVrWxz

[John F Sowa]

I uploaded a draft of the slides that I'll present
at the ontology summit telecon. See
http://jfsowa.com/ikl/contexts/contexts.pdf

These slides are dated "19 September 2017".

Slide 19 says "This section is incomplete".

In about an hour or two, I'll update those slides. The date
on the first page will be "20 September 2017" and slide 19
will be replaced with several more slides about the 'ist' and
'that' operators in IKL and related logics.

See below for the official announcement of the telecon.

John

[Jack Hodges]

John,

Although it may seem obvious to many on this forum, I think it might be a good idea to define what you mean by Context before launching into its various usage 'contexts'. I find that when I talk about semantics with people that they all have a different idea of what it means to what languages are used to implement it. So I generally like to start a discussion by defining what I consider the most obvious terms. I think that the same problem can exist for context.

Jack

--
All contributions to this forum by its members are made under an open content license, open publication license, open source or free software license. Unless otherwise specified, all Ontolog Forum content shall be subject to the Creative Commons CC-BY-SA 4.0 License or its successors.
--- You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-forum+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--

Jack

[Jack Hodges]

John,

Admittedly I have been unable to attend any of the planning meetings yet this session, but our (professional) perspective is about machines and inter-machine understanding. Context is extremely important, but not the same as language. As one of your slides clearly states (although context is never defined clearly), every context reveals more context and that it never ends. With people and language that is surely correct. Is it the same for machines? At some point, if machines are capable/allowed to have the same kinds of goals, beliefs, themes, etc. as humans, then context will become endless for them as well. It makes for an interesting discussion in its own right. Will your talk raise this/these issues?

Jack

--

Jack

[Alex Shkotin]

​​

Hi Jack,

it's always good for me to look at the definition and I am surprised as simple is  it here 

"Definition of context

1:the parts of a discourse that surround a word or passage and can throw light on its meaning

2:the interrelated conditions in which something exists or occurs :environment, setting 

• -
  the historical context of the war

"

https://www.merriam-webster.com/dictionary/context

Alex

[Jack Hodges]

I am sure that we all have our own favorite definitions for context, but I was referring to John Sowa's presentation slides. It is his definition for the purposes of a presentation on context that I think is important. Personally I would avoid any definition specific to language unless language is the topic of the summit. Rather, I would personally prefer something simpler, such as "all states (environmental and otherwise) active at a specific moment in time and place and which can affect the choice of actions". I just made that up so it has almost no thought behind it.

Jack

[John F Sowa]

Uploaded to http://jfsowa.com/ikl/contexts/contexts.pdf

[Pat Hayes]

Regarding the IKL logic (and other ‘context logics’, as developed by John MCarthy and his students and colleagues), the foundational idea is to NOT give a definition of ‘context’. Contexts are whatever satisfy the logical sematnic conditions and perhaps axioms that are being used to describe them. (This kind of definitionally-neutral stance is normal for dealing with logical descriptions, by the way.) The very same logic can be used, it is claimed, to reason about ‘contexts' which are time-intervals, points of view, works of fiction, geographical locations, historical epochs, styles of fashion, publications, personal beliefs and many other kinds of thing. That was McCarthy’s position, at any rate. I am not so sanguine about there being a single logic of all these various topics, but that is an on-going debate. (See the last section of http://www.aaai.org/Papers/Symposia/Spring/2007/SS-07-05/SS07-05-011.pdf  for some remarks on this, backed up by some actual mathematics.) 

I would say that any attempt to define ‘context’ is bound to fail, because this is, like ‘rubbish’ or ‘background', a term which can only be defined negatively. There is no actual topic singled out by the word ‘context’. Context is whatever stuff that might be relevant to meaning or communication, but is not handled explicitly by the current theory under consideration. It is ‘all the rest’, whatever that might be. One cannot give a definition of such a term, and to insist on doing so is to miss the essential point. For more on this, see my short 1977 paper ‘contexts in context’ https://www.ihmc.us/users/phayes/Pub/ContextsInContext.pdf

Pat Hayes

To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.

[GMAIL]

@phayes that sounds very philosophical and noncommittal to me and hence not very useful in an engineering/practical context. You speak of a mathematical foundation but if context (however it is defined) has no structure or coherent form then how do you resolve it mathematically? From an engineering point of view all things 'contextual' must take the same canonical form. I do not personally care what that form is as long as it is consistent and can be operated in. Or did I wildly misunderstand your point?

Sent from my Siemens iPhone

[Adam Pease]

Hi All,
If I can take this opportunity to agree with what Pat is saying -

Context is not a single term and therefore cannot have any meaningful
single definition. Context is about many things. That is not to say
that there are not formalizations of things that are contextual.
For a very simple, yet precise axiom including a contextual element,
take a practical example from SUMO

http://sigma.ontologyportal.org:8080/sigma/Browse.jsp?kb=SUMO&lang=EnglishLanguage&flang=SUO-KIF&term=part

(=>
(and
(instance ?B VehicleBrake)
(instance ?V Vehicle)
(part ?B ?V))
(hasPurpose ?B
(exists (?S)
(and
(instance ?S
(StopFn Motion))
(patient ?S ?V)
(instrument ?S ?B)))))

A brake that's part of a particular vehicle has the purpose of stopping
that vehicle (rather than some other vehicle). The context of the
expression is a particular vehicle. There are many other examples of
more complex contextual relationships and they can also be formalized in
an expressive logic.
Contrast this with a taxonomy, such as one finds in WordNet, that
says "door" has a meronym relation with "doorknob". There's no context
of use there as would be specified in a grammatical sentence, or an
ontology based on at least first order logic. Not all doors have
doorknobs and not all doorknobs are part of any particular door, but
often a door has a particular doorknob, and we can say that one
particular door has one particular doorknob.
Informal expressions of relatedness and simple taxonomies or logics
lack a way to express the complexity of context in natural language. I
believe this often leads to the assumption that context should be a
single defined entity.

all the best,
Adam

On 09/20/2017 09:39 AM, GMAIL wrote:
> @phayes that sounds very philosophical and noncommittal to me and hence
> not very useful in an engineering/practical context. You speak of a
> mathematical foundation but if context (however it is defined) has no
> structure or coherent form then how do you resolve it mathematically?
> From an engineering point of view all things 'contextual' must take the
> same canonical form. I do not personally care what that form is as long
> as it is consistent and can be operated in. Or did I wildly
> misunderstand your point?
>
> Sent from my Siemens iPhone
>
> On Sep 20, 2017, at 9:19 AM, Pat Hayes <pha...@ihmc.us

>>> <mailto:jhodg...@gmail.com>> wrote:
>>>
>>> I am sure that we all have our own favorite definitions for context,
>>> but I was referring to John Sowa's presentation slides. It is his
>>> definition for the purposes of a presentation on context that I think
>>> is important. Personally I would avoid any definition specific to
>>> language unless language is the topic of the summit. Rather, I would
>>> personally prefer something simpler, such as "all states
>>> (environmental and otherwise) active at a specific moment in time and
>>> place and which can affect the choice of actions". I just made that
>>> up so it has almost no thought behind it.
>>>
>>> Jack
>>>
>>> On Wed, Sep 20, 2017 at 8:25 AM, Alex Shkotin <alex.s...@gmail.com
>>> <mailto:alex.s...@gmail.com>> wrote:
>>>
>>> ​​
>>> Hi Jack,
>>>
>>> it's always good for me to look at the definition and I am
>>> surprised as simple is it here
>>> "Definition of context
>>> 1:the parts of a discourse

>>> <https://www.merriam-webster.com/dictionary/discourse#h1> that

>>> surround a word or passage and can throw light on its meaning
>>> 2:theinterrelated

>>> <https://www.merriam-webster.com/dictionary/interrelated>conditions

>>> in which something exists or occurs:environment

>>> <https://www.merriam-webster.com/dictionary/environment>,setting
>>> <https://www.merriam-webster.com/dictionary/setting>
>>>
>>> *

>>> -
>>> the historical context of the war
>>>
>>> "
>>>
>>> https://www.merriam-webster.com/dictionary/context
>>> <https://www.merriam-webster.com/dictionary/context>
>>>
>>> Alex
>>>
>>> 2017-09-20 17:03 GMT+03:00 Jack Hodges <jhodg...@gmail.com

>>> <mailto:jhodg...@gmail.com>>:

>>> page is bit.ly/2wVrWxz <http://bit.ly/2wVrWxz>

>>>
>>> Ken Baclawski
>>> Member - Ontolog Forum Board of Trustees
>>>
>>>
>>> --
>>> All contributions to this forum by its members are
>>> made under an open content license, open publication
>>> license, open source or free software license. Unless
>>> otherwise specified, all Ontolog Forum content shall
>>> be subject to the Creative Commons CC-BY-SA 4.0
>>> License or its successors.
>>> --- You received this message because you are
>>> subscribed to the Google Groups "ontolog-forum" group.
>>> To unsubscribe from this group and stop receiving
>>> emails from it, send an email to

>>> ontolog-foru...@googlegroups.com
>>> <mailto:ontolog-forum%2Bunsu...@googlegroups.com>.

>>> For more options, visit
>>> https://groups.google.com/d/optout

>>> <https://groups.google.com/d/optout>.

>>>
>>>
>>>
>>>
>>> --
>>> Jack
>>>
>>>
>>>
>>>
>>> --
>>> Jack
>>>
>>> --
>>> All contributions to this forum by its members are made under
>>> an open content license, open publication license, open
>>> source or free software license. Unless otherwise specified,
>>> all Ontolog Forum content shall be subject to the Creative
>>> Commons CC-BY-SA 4.0 License or its successors.
>>> ---
>>> You received this message because you are subscribed to the
>>> Google Groups "ontolog-forum" group.
>>> To unsubscribe from this group and stop receiving emails from
>>> it, send an email to

>>> ontolog-foru...@googlegroups.com
>>> <mailto:ontolog-foru...@googlegroups.com>.

>>> For more options, visit https://groups.google.com/d/optout

>>> <https://groups.google.com/d/optout>.

>>>
>>>
>>>
>>> --
>>> All contributions to this forum by its members are made under an
>>> open content license, open publication license, open source or
>>> free software license. Unless otherwise specified, all Ontolog
>>> Forum content shall be subject to the Creative Commons CC-BY-SA
>>> 4.0 License or its successors.
>>> ---
>>> You received this message because you are subscribed to the
>>> Google Groups "ontolog-forum" group.
>>> To unsubscribe from this group and stop receiving emails from it,

>>> send an email to ontolog-foru...@googlegroups.com
>>> <mailto:ontolog-foru...@googlegroups.com>.

>>> For more options, visit https://groups.google.com/d/optout

>>> <https://groups.google.com/d/optout>.

>>>
>>>
>>>
>>>
>>> --
>>> Jack
>>>
>>> --
>>> All contributions to this forum by its members are made under an open
>>> content license, open publication license, open source or free
>>> software license. Unless otherwise specified, all Ontolog Forum
>>> content shall be subject to the Creative Commons CC-BY-SA 4.0 License
>>> or its successors.
>>> ---
>>> You received this message because you are subscribed to the Google
>>> Groups "ontolog-forum" group.
>>> To unsubscribe from this group and stop receiving emails from it,

>>> send an email to ontolog-foru...@googlegroups.com
>>> <mailto:ontolog-foru...@googlegroups.com>.

>>> For more options, visit https://groups.google.com/d/optout.
>>
>> --
>> All contributions to this forum by its members are made under an open
>> content license, open publication license, open source or free
>> software license. Unless otherwise specified, all Ontolog Forum
>> content shall be subject to the Creative Commons CC-BY-SA 4.0 License
>> or its successors.
>> ---
>> You received this message because you are subscribed to the Google
>> Groups "ontolog-forum" group.
>> To unsubscribe from this group and stop receiving emails from it, send

>> an email to ontolog-foru...@googlegroups.com
>> <mailto:ontolog-foru...@googlegroups.com>.

>> For more options, visit https://groups.google.com/d/optout.
>
> --
> All contributions to this forum by its members are made under an open
> content license, open publication license, open source or free software
> license. Unless otherwise specified, all Ontolog Forum content shall be
> subject to the Creative Commons CC-BY-SA 4.0 License or its successors.
> ---
> You received this message because you are subscribed to the Google
> Groups "ontolog-forum" group.
> To unsubscribe from this group and stop receiving emails from it, send

> an email to ontolog-foru...@googlegroups.com
> <mailto:ontolog-foru...@googlegroups.com>.

> For more options, visit https://groups.google.com/d/optout.

--

-------------------
Adam Pease
http://www.ontologyportal.org
http://www.adampease.org
@apease_ontology on Twitter

[Pat Hayes]

On Sep 20, 2017, at 11:39 AM, GMAIL <jhodg...@gmail.com> wrote:

@phayes that sounds very philosophical and noncommittal to me and hence not very useful in an engineering/practical context.

We seem to have different ideas about the relationship of clear thought to engineering. 

You speak of a mathematical foundation but if context (however it is defined) has no structure or coherent form then how do you resolve it mathematically?

Read the paper? It is quite short. 

From an engineering point of view all things 'contextual' must take the same canonical form.

I have no idea what you are talking about here (canonical?), but even from an engineering standpoint, to say that all contexts have the same form is just obviously wrong.

I do not personally care what that form is as long as it is consistent and can be operated in. Or did I wildly misunderstand your point?

Possibly, though I don’t think you did. There is no single notion of ‘context’. The things called ‘context’ vary widely from one usage to another. I once attended a three-day symposium on the very topic of contexts, and noted as accurately as I could what each speaker understood the word to mean. In three days of talks, no two people agreed on the meaning of the word. One speaker understood the context of an utterance to be something lasting a time measured in milliseconds; the next speaker understood it to be something lasting for centuries or millenia. Some speakers thought contexts were psychological things, others physical things, others still identified contexts with the linguistic common ground of a conversation. None of these ideas are remotely similar to the others. You will not find a single theory covering them all. 

Pat Hayes

[Alex Shkotin]

Pat,

We do not use "context" at all. Following model theory (mostly by Tarski), we build and investigate math finite models of parts of reality.

Maybe the model is most important context :-)

Some practical examples in John's today great report are just about different and hidden models and conversations about it.

Sometimes about such a tricky case as what kind of propositions some people (for ex. Mary) have in mind.

Discussion about different math models seems more interesting and practical, IMHO:-)

For ex. one group has Earth's crust model ECM1 and other - ECM2. Are these 2 models the same? contradict?...

Alex

[Cory Casanave]

John,
I would appreciate you clarifying something for me concerning the first sentence of your presentation: "Literally, a context is text that accompanies a text.".

Here you are characterizing the context as the text, not the situation(s) the text represents, implying that (as per slide 7) context is only a function of the model (or perhaps the theory) and not the "world" (or worlds) approximated by the model.

Is this your intent or is this just shorthand for the model-text representing a (real) context?

If the former, is there nothing that the context text is representing? Using the example (slide 13), if this were a real-world situation would not the intent of the text be to correspond to this real-or-possible-world situation?

On a similar note in slide 12, you say: " A situation without agents is possible, but meaningless.". If there is a planet orbiting a start, isn't that a situation? This situation would be the context for the path of the planet as well as other implications. The planet and the star are involved and related entities - are you considering them agents? If not, why would this situation be meaningless? Are you requiring an observer as part of the definition of the situation?

Thanks!
-Cory Casanave

-----Original Message-----
From: ontolo...@googlegroups.com [mailto:ontolo...@googlegroups.com] On Behalf Of John F Sowa
Sent: Wednesday, September 20, 2017 11:52 AM
To: ontolo...@googlegroups.com
Subject: Re: [ontolog-forum] Slides for today's telecon: Representing and Reasoning About Contexts

Uploaded to http://jfsowa.com/ikl/contexts/contexts.pdf

--
All contributions to this forum by its members are made under an open content license, open publication license, open source or free software license. Unless otherwise specified, all Ontolog Forum content shall be subject to the Creative Commons CC-BY-SA 4.0 License or its successors.
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.

[Pat Hayes]

Hi Alex

Who is “we” in your message?  

The context logics (as used for example by Cyc) do of course have a model theory, as does IKL. No, models are not contexts (though they may have things in them that play the role of a context.) 

BTW, the sense of ‘model’ in ‘Tarskian model theory’ and the sense in ‘crust model ECM1’ are rather different. The first is a technical usage, meaning an interpretation (‘possible world’) which satisfies some axioms; the second sense usually means the axioms themselves, ie an ontological description. John and I have had extensive email discussions on this distinction in past forums, several of them archived. You might find some of them amusing. 

Pat

To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.

[Alex Shkotin]

Hi Pat,

Please see below

 

2017-09-21 3:00 GMT+03:00 Pat Hayes <pha...@ihmc.us>:

Hi Alex

Who is “we” in your message?  

​I ​

 

​am:-)​

The context logics (as used for example by Cyc) do of course have a model theory, as does IKL. No, models are not contexts (though they may have things in them that play the role of a context.) 

​OK​

 

BTW, the sense of ‘model’ in ‘Tarskian model theory’ and the sense in ‘crust model ECM1’ are rather different. The first is a technical usage, meaning an interpretation (‘possible world’) which

​​

satisfies some axioms; the second sense usually means the axioms themselves, ie an

​​

​​

ontological description. John and I have had extensive email discussions on this distinction in past forums, several of them archived. You might find some of them amusing. 

​the profoundness between "

​

​

ontological description"​ and finite-model "

​

satisfies some axioms" is impassable:-)

Alex​

 

[John F Sowa]

Pat H, Jack H, GMAIL, Adam, Cory, and Alex,

I agree with Pat about the difficulty or even impossibility
of restricting what is or should be the content of a context.

Pat

> Regarding the IKL logic (and other ‘context logics’, as developed by
> John MCarthy and his students and colleagues), the foundational idea
> is to NOT give a definition of ‘context’. Contexts are whatever

> satisfy the logical semantic conditions and perhaps axioms that are

> being used to describe them. (This kind of definitionally-neutral
> stance is normal for dealing with logical descriptions, by the way.)

For McCarthy's operator ist(c,p), the context c is any set of
statements in FOL, and p is a single statement in FOL. But the
distinction between 'set' and 'single' is vague, since any set of
statements can be combined with the AND operator. In any case,
the *intent* is that the context c may be larger than p -- but
intentions are are outside the scope of most theories of logic.

Pat

> The very same logic can be used, it is claimed, to reason about
> ‘contexts' which are time-intervals, points of view, works of
> fiction, geographical locations, historical epochs, styles of
> fashion, publications, personal beliefs and many other kinds of
> thing. That was McCarthy’s position, at any rate. I am not so
> sanguine about there being a single logic of all these various

> topics, but that is an on-going debate. See the last section of

> http://www.aaai.org/Papers/Symposia/Spring/2007/SS-07-05/SS07-05-011.pdf
> for some remarks on this, backed up by some actual mathematics.

That paper, which has the title "Context Mereology", was written
shortly after the IKRIS project that specified IKL. It was
influenced by IKL, but it could be adapted to other logics.
I copied it to the directory where I'm including papers that
have been or are being discussed in the Summit lectures:
http://jfsowa.com/ikl/contexts/Hayes07.pdf

Jack

> I think it might be a good idea to define what you mean by Context

That was a good suggestion, and I added the following definition
on slide 2 before I presented the slides for yesterday's telecon:
> Literally, a context is text that accompanies a text. More
> generally, the context may be any background knowledge that
> helps explain a text.

Jack

> Personally I would avoid any definition specific to language unless
> language is the topic of the summit. Rather, I would personally
> prefer something simpler, such as "all states (environmental and
> otherwise) active at a specific moment in time and place and which
> can affect the choice of actions".

If you want to avoid any mention of NLs, replace the word 'text'
in my definition with "proposition or set of propositions". If
you want to avoid the word 'explain', replace it with McCarthy's
ist(c,p), which states "p is true in c" or "c entails p".

The definitions by McCarthy, Hayes, or me include, but are not
limited to "all states (environmental and otherwise) active at

a specific moment in time and place and which can affect the
choice of actions".

GMAIL
> @phayes that sounds very philosophical and noncommittal to me...

> From an engineering point of view all things 'contextual' must take

> the same canonical form... is as long as it is consistent and can
> be operated in.

Replace "very philosophical and noncommittal" with "sufficiently
general to cover all the versions that anyone has proposed".
And we're all using the same "canonical form": a context is
a set of propositions stated in some version of logic. McCarthy
assumed FOL. Pat and I assumed IKL, which includes FOL as a subset.

If you're talking about engineering, just look at all the branches,
ranging from bridges to airplanes to software. Can you find any
way to narrow the definition to anything more specific than
"a set of propositions". Maybe you could add "relevant to the
subject matter". But then you're stuck with the problem of
defining the word 'relevant' without sounding "philosophical".

Adam

> Context is about many things. That is not to say that there
> are not formalizations of things that are contextual.

That's a good, succinct summary.

Cory

> "Literally, a context is text that accompanies a text.".
> Here you are characterizing the context as the text, not the
> situation(s) the text represents, implying that (as per slide 7)
> context is only a function of the model (or perhaps the theory)
> and not the "world" (or worlds) approximated by the model.

By 'literal', I was talking about the original use of the word
for discussing documents. But my next sentence includes all
the options you mentioned: "More generally, the context may be
any background knowledge that helps explain a text."

Cory

> you say: "A situation without agents is possible, but meaningless."

> If there is a planet orbiting a star, isn't that a situation?
> ... The planet and the star are involved as related entities.

Yes. It's a possible situation. But everything in the universe
has some relationships to everything else. Every such relation is
a possible situation. Would you consider all of them meaningful?

Cory

> Are you requiring an observer as part of the definition of
> the situation?

I was assuming a point I have discussed many times:
"Without life, there is no meaning in the universe."

For example, a bacterium that swims toward sugar and away from
vinegar is doing something that no rock or planet could ever do:
observe and interpret some relations as sufficiently "meaningful"
that they motivate some response.

Alex

> Following model theory (mostly by Tarski), we build and investigate
> math finite models of parts of reality. Maybe the model is most
> important context :-)

You could relate a Tarski-style model M to McCarthy's ist(c,p):
Let the context c be a description of M as a conjunction of
atoms (each one consisting of just one relation, the names of
things it relates, and an optional not-sign in front). Then
for any proposition p, ist(c,p) if and only if M entails p.

But ist(c,p) is more general, since c could contain propositions
that are more complex than just atoms.

John

[Alex Shkotin]

John,

you just confirm my assertion I have written to Pat: " the profoundness between "

​

​

ontological description" and finite-model "

​

satisfies some axioms" is impassable:-)"

Alex

[Edward Barkmeyer]

John,

I hesitate to get involved in this, because I share Pat's view that there is no single theory of 'context' that addresses the general problem of interpreting statements, let alone purpose-built, or viewpoint-based, "ontologies".

But I have real problems with your comments on Cory's contribution:

CC> you say: "A situation without agents is possible, but meaningless."
CC> If there is a planet orbiting a star, isn't that a situation?
CC> ... The planet and the star are involved as related entities.

JS>Yes. It's a possible situation. But everything in the universe has some relationships to everything else. Every such relation is a possible situation. Would you consider all of them meaningful?

The meaningful situations are the relations that are significant to a decision I have to make, or to the effects of an action I take (or don't take). But a situation/relation can be importantly relevant to my decision or the effect of some action or inaction without involving a conscious "agent" who is involved in, or even aware of, the situation. I can even act in the knowledge that an instance of a situation type *could exist*, without having specific knowledge of its existence. (The "mental event" thing again.) That is, in fact, the fundamental nature of "risk avoidance".

[I am reminded of a colleague's observation about moving to Florida. In the light of possible hurricanes, he moved to a "mountain" in Clearwater, at an elevation of 30 metres. :-)]

CC> Are you requiring an observer as part of the definition of the situation?

JS>I was assuming a point I have discussed many times:
"Without life, there is no meaning in the universe." ...

Yes, part of the definition of "meaning" involves an interpreter, and we may assume that all interpreters are living things. But Cory asked about the definition of "situation". To say that any "relation" can exist without there being an interpreter strikes me as a contradiction in terms. The relation is, by its nature, a mental model of situations. OTOH, to say that not every existing situation in the universe is "observed" is quite reasonable. "Observation" is about coupling the actuality with the relation. The ancient Greeks observed lightning as instances of Zeus throwing thunderbolts; they had no way to form the relations by which we now describe the phenomenon. But the nature of lightning situations did not change.

JS>For example, a bacterium that swims toward sugar and away from vinegar is doing something that no rock or planet could ever do: observe and interpret some relations as sufficiently "meaningful" that they motivate some response.

If the action of the bacterium is a physio-chemical response to a chemical stimulus, how is that different from a rock dissolving to ions under acid rain? I don’t want to argue about the nature of "life". I'm just saying that your broad use of "meaning" here makes it another undefined term.

[And that is exactly why I did not want to get involved in this discussion.]

-Ed

Ed Barkmeyer
ebark...@thematix.com

-----Original Message-----
From: ontolo...@googlegroups.com [mailto:ontolo...@googlegroups.com] On Behalf Of John F Sowa
Sent: Thursday, September 21, 2017 12:38 PM
To: ontolo...@googlegroups.com
Subject: Re: [ontolog-forum] Slides for today's telecon: Representing and Reasoning About Contexts

--
All contributions to this forum by its members are made under an open content license, open publication license, open source or free software license. Unless otherwise specified, all Ontolog Forum content shall be subject to the Creative Commons CC-BY-SA 4.0 License or its successors.
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.

[Rich Cooper]

Ed, that is the best, clearest, most concise yet complete explanation of how "meaning" gets its meaning I've heard yet. 

Sincerely,

Rich Cooper,

Rich Cooper,

Chief Technology Officer,

MetaSemantics Corporation

MetaSemantics AT EnglishLogicKernel DOT com

( 9 4 9 ) 5 2 5-5 7 1 2

http://www.EnglishLogicKernel.com

[Ravi Sharma]

John and Ed

Observer comes into context whether we are talking about a situation or direct observer involvement.

Imagine innumerable combinations of chemical, physical, life and astrophysical phenomena - these might be there but for ontologies and reality (hoping logic provides these) determination, those are close to reality where observer is involved. Multiple simultaneous observers are more complex to handle, such as cognizance being same for those who agree (statistically), etc.

Another point and request for you to kindly clarify for me as I have this Q. Pat Hayes paper discusses IC internal models and EL external language. Also Logic is involved between these and disambiguation. Does that imply that the "meaning" that is correct has unique mapping or same IC among all who correctly understood the EL sentence (and implied thing!)? or that ICs are logically equivalent (example all rivers leading to ocean)?

Regards

Ravi

To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-forum+unsubscribe@googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

--

All contributions to this forum by its members are made under an open content license, open publication license, open source or free software license. Unless otherwise specified, all Ontolog Forum content shall be subject to the Creative Commons CC-BY-SA 4.0 License or its successors.

---

You received this message because you are subscribed to the Google Groups "ontolog-forum" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-forum+unsubscribe@googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

--
All contributions to this forum by its members are made under an open content license, open publication license, open source or free software license. Unless otherwise specified, all Ontolog Forum content shall be subject to the Creative Commons CC-BY-SA 4.0 License or its successors.
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-forum+unsubscribe@googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

--

Thanks.
Ravi
(Dr. Ravi Sharma)

 313 204 1740 Mobile 

[Mike]

Ed,

When you say:

EB> "To say that any "relation" can exist without there being an interpreter strikes me as a contradiction in terms."
EB> "The relation is, by its nature, a mental model of situations."
EB> "OTOH, to say that not every existing situation in the universe is "observed" is quite reasonable."
EB> ""Observation" is about coupling the actuality with the relation."

I lose sight of what you mean by "relation" as it might comprise part of a situation.
Are you restricting the sense of "relation" to strictly a mental figment?
Is it possible for a notion of "situation" to refer to, and represent, aspects of reality such as the contingent relations among bodies and phenomena of the physical world, independent of an observer / interpreter? In such a case, relations could inhere in materiality as Leibniz might suppose, or as Einstein would intend in E=MC2? If physical dependencies exist prior to and free from any cognition, it seems reasonable to be able to treat these as relations without interjecting a mental middleman. And, to the extent that situations may be comprised of such relations, situations would not necessarily be bound to an observer / interpreter.

When you go on to say (in response to JS):

EB> "If the action of the bacterium is a physio-chemical response to a chemical stimulus, how is that different from a rock dissolving to ions under acid rain?"

It sounds as if you are entertaining these two examples of direct physical interaction as being relations which, of course, would seem to exist without an "interpreter". So, I am somewhat confused again about what you would have "relation" mean.

I guess a simple answer here may be that there are two kinds of relation being discussed -- one at the material level and one at the mental level, but I would hate to see the notion of situation relegated exclusively to the world of mental construction, and unable to address the physical world head on.

Mike

Michael Denny

-----Original Message-----
From: ontolo...@googlegroups.com [mailto:ontolo...@googlegroups.com] On Behalf Of Edward Barkmeyer
Sent: Thursday, September 21, 2017 7:05 PM
To: ontolo...@googlegroups.com

[John F Sowa]

Ed, Mike, and Ravi,

I don't disagree with Ed's major points. But there is one point
on which I violently disagree:

Ed

> To say that any "relation" can exist without there being
> an interpreter strikes me as a contradiction in terms. The
> relation is, by its nature, a mental model of situations.

Mike

> I guess a simple answer here may be that there are two kinds
> of relation being discussed -- one at the material level and
> one at the mental level

For a logician or mathematician, the terms 'function' and 'relation'
are formally defined. They can be applied to anything of any kind
-- physical or mental. But the words 'situation' and 'meaningful'
depend on psycholinguistic issues.

In the 1980s, the logician Jon Barwise and the philosopher John Perry
teamed up to develop situation semantics as a foundation for defining
the "meaning" of natural language in terms "situations". They defined
them as finite regions that are observable by the people who are
talking in them and about them.

Ed

> The meaningful situations are the relations that are significant
> to a decision I have to make, or to the effects of an action I
> take (or don't take).

To make that definition consistent with B & P situations, add
the phrase "chunks of the world that contain" after the word
'and' and before the word 'the'.

Since natural languages are limited to humans, B & P did not
generalize their definition beyond Homo saps. But in the past
30+ years, cognitive scientists, especially anthropologists,
neuroscientists, psycholinguists, and comparative biologists
have been exploring how far down the tree of life the terms
'communication' and 'meaningful' can be applied.

It's reasonable to talk about meaningful situations for animals
-- at least the higher mammals. But if you allow them, where do
you stop? The neuroscientist Antonio Damasio talks about the
feelings of insects (see below). Do you want to consider an
encounter between a spider and a fly a meaningful situation?
For us, it may be interesting. For them, it's a life-and-death
struggle. Damasio would consider feelings meaningful for them.

Ed

> If the action of the bacterium is a physio-chemical response to
> a chemical stimulus, how is that different from a rock dissolving
> to ions under acid rain?

Huge difference: Physical causality is normally based on equal
actions and reactions. But a difference in sweetness on two sides
of a bacterium may cause it to swim upstream in a glucose gradient.

The energy of the action is minuscule compared to the reaction.
And unlike the "butterfly effect" in chaos theory, the reaction
by living things is tightly controlled. The only other systems
that exhibit tightly controlled amplification are the artifacts
explicitly designed by living things.

Ed

> I don’t want to argue about the nature of "life". I'm just saying
> that your broad use of "meaning" here makes it another undefined term.

From the biologist Lynn Margulis, who studied bacteria in detail:
> The growth, reproduction, and communication of these moving,
> alliance-forming bacteria become isomorphic with our thought,
> with our happiness, our sensitivities and stimulations.
See http://edge.org/documents/ThirdCulture/n-Ch.7.html

(By the way, LM was not a mathematician. She should have said
"homomorphic", not "isomorphic".)

If you want definitions that span the full range of living
things, google the term "biosemiotics".

Ravi

> I have this Q. Pat Hayes paper discusses IC internal models and
> EL external language. Also Logic is involved between these and
> disambiguation. Does that imply that the "meaning" that is correct
> has unique mapping or same IC among all who correctly understood
> the EL sentence (and implied thing!)? or that ICs are logically
> equivalent (example all rivers leading to ocean)?

In formal logic with a Tarski-style model theory, very few
propositions have a unique model. More often, there are
infinitely many models that could make some proposition true.

When you get to natural languages, all bets are off. People
always have to ask follow-up questions to clarify the meaning.

In 1991, Keith Devlin wrote a book on situation semantics that
synthesized the research of the 1980s. But in his 2005 article,
he discussed the complex, thorny issues related to contexts and
situations. On page 8, he stated the "six P's about contexts":
pervasive, primary, perpetuate, proliferate, potentially pernicious.

See http://jfsowa.com/ikl/contexts/Devlin05.pdf

John
___________________________________________________________________

Antonio R. Damasio & Gil B. Carvalho (2013) The nature of feelings:
evolutionary and neurobiological origins, Nature Reviews,
Neuroscience 14, 143-152.
> Feelings are mental experiences of body states. They signify
> physiological need, tissue injury, optimal function, threats
> to the organism, or specific social interactions... Feelings
> constitute a crucial component of the mechanisms of life
> regulation, from simple to complex. Their neural substrates can
> be found at all levels of the nervous system, from individual
> neurons to subcortical nuclei and cortical regions.

Damasio, Interview (2014),
> I’m ready to give the very teeny brain of an insect – provided it
> has the possibility of representing its body states – the possibility
> of having feelings... Of course, what flies don’t have is all the
> intellect around those feelings that could make use of them: to found
> a religious order, or develop an art form, or write a poem.
http://www.technologyreview.com/qa/528151/the-importance-of-feelings/

[Ravi Sharma]

John

Thanks.

JS> " More often, there are

infinitely many models that could make some proposition true."

Q:

Then when observer is "in" or "about" the context e.g. situation, then only is it real or formal and hence verifiable, repeatble by other observers? 

Otherwise things are happening in nature and in minds without our context awareness and also may or may not have real (that affect the observer) consequences? 

Action usually is in awareness or inContext?

Regards

--
All contributions to this forum by its members are made under an open content license, open publication license, open source or free software license. Unless otherwise specified, all Ontolog Forum content shall be subject to the Creative Commons CC-BY-SA 4.0 License or its successors.
--- You received this message because you are subscribed to the Google Groups "ontolog-forum" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-forum+unsubscribe@googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

[Pat Hayes]

On Sep 22, 2017, at 2:28 AM, Ravi Sharma <drravi...@gmail.com> wrote:

John and Ed

….

Another point and request for you to kindly clarify for me as I have this Q. Pat Hayes paper discusses IC internal models and EL external language. Also Logic is involved between these and disambiguation. Does that imply that the "meaning" that is correct has unique mapping or same IC among all who correctly understood the EL sentence

While probably not actually true in reality, this would be a good working hypothesis for theorists in this area, just as linguists typically assume that syntactic structures are unique and unambiguous. 

Pat

To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.

[Pat Hayes]

On Sep 21, 2017, at 3:38 AM, Alex Shkotin <alex.s...@gmail.com> wrote:

…

PJH:

BTW, the sense of ‘model’ in ‘Tarskian model theory’ and the sense in ‘crust model ECM1’ are rather different. The first is a technical usage, meaning an interpretation (‘possible world’) which

​​

satisfies some axioms; the second sense usually means the axioms themselves, ie an

​​

​​

ontological description. John and I have had extensive email discussions on this distinction in past forums, several of them archived. You might find some of them amusing. 

​the profoundness between "

​

​

ontological description"​ and finite-model "

​

satisfies some axioms" is impassable:-)

Honestly, I have no idea what you are intending to say here. First, satisfaction does not assume finiteness, and indeed many ontologies (eg those which use numerals) do not have finite models. So let us ignore that distraction. But what ‘impassable profoundness’ do you see separating a formal ontology (consisting of axioms, ie sentences in a formal notation) and its interpretations? They are of course distinct kinds of entity (is that what you mean?), but they are closely related: indeed, that relationship is exactly Tarski’s theory of truth, now grown up into model-theoretic semantics. So it is hardly ‘impassable'. But even if you meant the first, relatively innocuous, point, that word “impassable” is still inappropriate, since Herbrand showed that one can construct interpretations out of the very stuff of the theories themelves, so that in a (technical, but) very real sense the theories can actually be their own interprations (of a special, but rather useful, kind.) 

Pat

[Edward Barkmeyer]

John,

I think we agree on the B&P ideas. I assumed that 'situation' refers to "states of affairs" or "actualities" -- B&P "chucks of the world", whereas "relation" is a logical characterization of "situations", or aspects of them. And in that regard I misspoke in saying:

> > The meaningful situations are the relations that are significant to a
> decision I have to make, or to the effects of an action I take (or don't take).

As you pointed out, that should have said: The meaningful situations are chunks of the world that (are taken to) instantiate the relations that are significant ...

I don't want to debate the application of cognition terms to arbitrary natural systems that amplify the response to a stimulus. I don't think anyone would deny that there are some truly cognitive functions/systems in insects, but they are a fairly high form of life. You can assign cognitive terms to the responses of bacteria to chemical stimuli if it pleases you. I truly don't care; I was just asking what your criterion was.

-Ed

-----Original Message-----
From: ontolo...@googlegroups.com [mailto:ontolo...@googlegroups.com] On Behalf Of John F Sowa
Sent: Friday, September 22, 2017 11:58 AM
To: ontolo...@googlegroups.com
Subject: Re: [ontolog-forum] Slides for today's telecon: Representing and Reasoning About Contexts

[Pat Hayes]

On Sep 21, 2017, at 11:38 AM, John F Sowa <so...@bestweb.net> wrote:

Pat H, Jack H, GMAIL, Adam, Cory, and Alex,

I agree with Pat about the difficulty or even impossibility
of restricting what is or should be the content of a context.

Pat

Regarding the IKL logic (and other ‘context logics’, as developed by
John MCarthy and his students and colleagues), the foundational idea
is to NOT give a definition of ‘context’.  Contexts are whatever
satisfy the logical semantic conditions and perhaps axioms that are
being used to describe them. (This kind of definitionally-neutral
stance is normal for dealing with logical descriptions, by the way.)

For McCarthy's operator ist(c,p), the context c is any set of
statements in FOL, and p is a single statement in FOL.

Actually in McC’s (and Cyc’s) logics, c is a term (understood to be denoting a ‘context’; the Cyc term is ‘microtheory’) rather than a sentence. As McCarthy and Buvac said (http://www-formal.stanford.edu/jmc/mccarthy-buvac-98/context.pdf), their logic treated contexts as ‘first-class’ entities – things that can be quantified over and named – and as ‘rich’ objects, ie (typically) too complex to be described fully by any finite set of sentences.  And of course the mapping into IKL follows this but also has the second argument be a term, since IKL treats propositions themselves as also first-class. Thus in IKL, ist is simply a two-place relation between things in the universe. 

Pat

 But the
distinction between 'set' and 'single' is vague, since any set of
statements can be combined with the AND operator.  In any case,

the *intent* is that the context c may be larger than -- but

--
All contributions to this forum by its members are made under an open content license, open publication license, open source or free software license. Unless otherwise specified, all Ontolog Forum content shall be subject to the Creative Commons CC-BY-SA 4.0 License or its successors.
--- You received this message because you are subscribed to the Google Groups "ontolog-forum" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.

[Alex Shkotin]

Dear Pat,

For me, interpretation is a defined function from token, term and formula of some language to their values on math object. In classical Model Theory, math object is an algebraic system.

In my case, an algebraic system is finite and uses strings and rational numbers as values.

My joke about "profoundness" is that somebody may say that I need not have an algebraic system, but "

​

​

ontological description" converting my beautiful algebraic system in a finite set of OWL 2 "axioms".

And when I have a special sublanguage to handle finite algebraic system with rational numbers and strings somebody may say that all these things are possible by handling OWL 2 text.

For me a more subtle thing is "eg those which use numerals": I hope you agree that finite algebraic system may use as one of its carrier/sort Natural Numbers, and keep some of them in it; i.e. it's possible to have multi-carrier (or multi-sorted) finite algebraic system which uses numerals. 

Alex

[John F Sowa]

Pat,

I certainly agree with your point:
>> [JFS] For McCarthy's operator ist(c,p), the context c is any set

>> of statements in FOL, and p is a single statement in FOL.
>
> Actually in McC’s (and Cyc’s) logics, c is a term (understood
> to be denoting a ‘context’; the Cyc term is ‘microtheory’) rather
> than a sentence.

But I just realized that we can define 'that' as a function from
sentences to equivalence classes. This implies that we don't
need IKL: We can treat the 'that' operator as syntactic sugar
for a that-function from quoted sentences to equivalence classes.

> Thus in IKL, ist is simply a two-place relation between things
> in the universe.

Yes. And as we agreed during the IKRIS project, Common Logic,
by itself, already contains 0-adic relations as first-class
citizens. If we call them propositions, then the ist(c,p)
relation could be stated and used in CL.

However, there is a problem of defining equality of propositions
when used in a proof. For example, the proposition defined by
"2+2=4" and the proposition that states Fermat's last theorem,
are both true in every model of Peano's axioms.

Therefore, you can say
"2+2=4 if and only if Fermat's last theorem is true."

But the proof of the left-hand side is trivial, and the proof
of the right-hand side took several centuries to prove. If
proofs are being considered, we can't use "iff" as the criterion
for equality of propositions.

On the other hand, there are some syntactic changes that have
little or no effect on the difficulty of a proof. For example,
the following sentences "obviously" say "the same thing":

p and q <=> q and p

p or q <=> q or p

p and (q and r) <=> (p and q) and r

But that depends on how you define "obvious" and "the same thing".
We want to include these options, but exclude the option that
"2+2=4" means "the same thing" as Fermat's last theorem. For our
discussions in 2005, see http://jfsowa.com/logic/proposit.pdf

Note the following two criteria on page 2 of proposition.pdf:

> Every equivalence class p in the partition of L determined by
> [an MPT function] f contains exactly one canonical sentence c.
>
> the sentence s is said to state the proposition p if and only if
> s is contained in the equivalence class p.

This implies that we can define IKL as syntactic sugar for CL with
the option of using a that-function from any CL sentence s to the
canonical sentence of the equivalence class that contains s.

Then the truth of any proposition in any model M is defined as
the truth of its canonical sentence in M.

The equality of any two propositions is defined as the equality
of their canonical propositions.

Any IKL text that contains one or more occurrences of propositions
may be translated to an equivalent CL text that replaces the
syntactic sugar according to the above criteria.

John

[Pat Hayes]

On Sep 23, 2017, at 3:39 AM, Alex Shkotin <alex.s...@gmail.com> wrote:

Dear Pat,

For me, interpretation is a defined function from token, term and formula of some language to their values on math object.

..on object. There’s no such thing as a ‘math object’. Math itself is a system of ways to describe reality, but that does not imply that the reality so described is made up of ‘math objects’. 

In classical Model Theory, math object is an algebraic system.

In my case, an algebraic system is finite

How can you know that your system is finite? Finiteness isn’t first-order axiomatizable.

and uses strings and rational numbers as values.

Last time I looked, there were infinitely many rational numbers :-) (see below)

My joke about "profoundness" is that somebody may say that I need not have an algebraic system, but "

​

​

ontological description" converting my beautiful algebraic system in a finite set of OWL 2 "axioms".

And when I have a special sublanguage to handle finite algebraic system with rational numbers and strings somebody may say that all these things are possible by handling OWL 2 text.

For me a more subtle thing is "eg those which use numerals": I hope you agree that finite algebraic system may use as one of its carrier/sort Natural Numbers, and keep some of them in it; i.e. it's possible to have multi-carrier (or multi-sorted) finite algebraic system which uses numerals. 

Well, actually this is a rather delicate matter. I do see what you mean, but I also am reluctant to allow you (or anyone) to claim that their theory only has ‘standard’ interpretations. Non-standard interpretations exist, whether you want to think about them or not, and they play an important role in metatheory. Let me illustrate with a toy example. Suppose you only use the numerals ‘3’ and ‘5.5’ in your axioms, and you wish to claim that these denote the rationals three and 11/5 respectively, and as these are the only rationals you need, you have a finite model. This makes sense if one takes a resolutely Platonic view of rational numbers, under which the number three is an actual object: an abstract object to be sure, but as real and well-individuated as, say, the leaning tower of Pisa. But this is a rather extreme philosophical position, IMO. It makes more sense to me to think of numbers as tokens in a system of arithmetic. Three is the thing that is the successor of two, the sum of 7 and -4, the cube root of 27, and so on, and each of these in turn is defined by its position in the algebraic system of generalized arithmetic. On this view, there really are no numbers sui generis; there are only ‘positions’ in a mathematical system of operations. (A parallel contrast describes the history of mathematics differently: was zero discovered (Plato) or invented (Relational)? ) And on this second view, your clain to have just 3 and 5.5 in your model, and nothing else, sounds crazy. What algebraic framework gives these two tokens the right to be so labelled? Does your model have their sum in it? Their product? The first raised ot the power of the second? If not, you have no valid claim to call them rational numbers (on this second view); but if so, then your model must be infinite, because just one (non-zero) rational is enough to generate the entire number line, when the operations defined by arithmetic are allowed free reign to apply to it (as, on this view, they must be in order to validate the ontological claim.) 

I would be interested in your reaction, by the way.

Pat

Alex

2017-09-23 1:48 GMT+03:00 Pat Hayes <pha...@ihmc.us>:

On Sep 21, 2017, at 3:38 AM, Alex Shkotin <alex.s...@gmail.com> wrote:

…

PJH:

BTW, the sense of ‘model’ in ‘Tarskian model theory’ and the sense in ‘crust model ECM1’ are rather different. The first is a technical usage, meaning an interpretation (‘possible world’) which

​​

satisfies some axioms; the second sense usually means the axioms themselves, ie an

​​

​​

ontological description. John and I have had extensive email discussions on this distinction in past forums, several of them archived. You might find some of them amusing. 

​the profoundness between "

​

​

ontological description"​ and finite-model "

​

satisfies some axioms" is impassable:-)

Honestly, I have no idea what you are intending to say here. First, satisfaction does not assume finiteness, and indeed many ontologies (eg those which use numerals) do not have finite models. So let us ignore that distraction. But what ‘impassable profoundness’ do you see separating a formal ontology (consisting of axioms, ie sentences in a formal notation) and its interpretations? They are of course distinct kinds of entity (is that what you mean?), but they are closely related: indeed, that relationship is exactly Tarski’s theory of truth, now grown up into model-theoretic semantics. So it is hardly ‘impassable'. But even if you meant the first, relatively innocuous, point, that word “impassable” is still inappropriate, since Herbrand showed that one can construct interpretations out of the very stuff of the theories themelves, so that in a (technical, but) very real sense the theories can actually be their own interprations (of a special, but rather useful, kind.) 

Pat

--
All contributions to this forum by its members are made under an open content license, open publication license, open source or free software license. Unless otherwise specified, all Ontolog Forum content shall be subject to the Creative Commons CC-BY-SA 4.0 License or its successors.
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-forum+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
All contributions to this forum by its members are made under an open content license, open publication license, open source or free software license. Unless otherwise specified, all Ontolog Forum content shall be subject to the Creative Commons CC-BY-SA 4.0 License or its successors.
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.

[Alex Shkotin]

Pat, please, give me 12+ hours :-)

Alex

[John F Sowa]

On 9/23/2017 1:43 PM, John F Sowa wrote:
> Every equivalence class p in the partition of L determined by
> [an MPT function] f contains exactly one canonical sentence c.
> the sentence s is said to state the proposition p if and only if
> s is contained in the equivalence class p.

After reading that passage, I noticed that I should have included
a bit more from page 2 of proposit.pdf in order to make it clear
to readers who don't bother to click on the URL:

1. The article proposit.pdf defines an MPT as a "meaning-preserving
translation" from sentences to equivalence classes.

2. Each proposition is defined as an equivalence class of
sentences that contains exactly one "canonical sentence" c.

3. All the sentences in each equivalence class are "obviously"
synonymous according to "fairly simple" rules. There are
5 levels of "simplicity" -- you choose which level you prefer.

4. Given your choice of level (I suggest 4 or 5), you can use
the corresponding MPT to define a translation from any CL
sentence to its canonical sentence for that level.

5. For determining whether two propositions are identical,
just check whether their canonical sentences are identical.

6. For any CL model M, the truth value of any proposition p is
identical to the truth value in M of its canonical sentence.

These conditions are sufficient to define a purely syntactic
translation from any IKL text to an equivalent CL text that
does not contain the 'that' operator.

For more detail, see http://jfsowa.com/logic/proposit.pdf
It's only 5 pages long.

John

[Pat Hayes]

On Sep 23, 2017, at 1:35 PM, Alex Shkotin <alex.s...@gmail.com> wrote:

Pat, please, give me 12+ hours :-)

Of course. No rush, I doubt if we will come to a firm conclusion before, say, next Tuesday :-)

Pat

To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.

[Pat Hayes]

> On Sep 23, 2017, at 2:13 PM, John F Sowa <so...@bestweb.net> wrote:
>
> On 9/23/2017 1:43 PM, John F Sowa wrote:
>> Every equivalence class p in the partition of L determined by
>> [an MPT function] f contains exactly one canonical sentence c.
>> the sentence s is said to state the proposition p if and only if
>> s is contained in the equivalence class p.
>
> After reading that passage, I noticed that I should have included
> a bit more from page 2 of proposit.pdf in order to make it clear
> to readers who don't bother to click on the URL:
>
> 1. The article proposit.pdf defines an MPT as a "meaning-preserving
> translation" from sentences to equivalence classes.
>
> 2. Each proposition is defined as an equivalence class of
> sentences that contains exactly one "canonical sentence" c.
>
> 3. All the sentences in each equivalence class are "obviously"
> synonymous according to "fairly simple" rules. There are
> 5 levels of "simplicity" -- you choose which level you prefer.
>
> 4. Given your choice of level (I suggest 4 or 5), you can use
> the corresponding MPT to define a translation from any CL
> sentence to its canonical sentence for that level.
>
> 5. For determining whether two propositions are identical,
> just check whether their canonical sentences are identical.
>
> 6. For any CL model M, the truth value of any proposition p is
> identical to the truth value in M of its canonical sentence.

Well, as I understand it, of any sentence in the eq. class, right? Since they are all logically equivalent. Yes, this is the T-condition, written in IKL as

S iff ((that S))

(well, for closed sentences S: free names involve a universal quantification) and guaranteed to be true by the current IKL model theory, but which of course is the sticking point for ensuring the internal coherence of full IKL, because of Tarski’s theorem.

See my previous message for some sketchy notes about this topic.

Pat

[Pat Hayes]

On Sep 23, 2017, at 12:43 PM, John F Sowa <so...@bestweb.net> wrote:

Pat,

I certainly agree with your point:

[JFS] For McCarthy's operator ist(c,p), the context c is any set
of statements in FOL, and p is a single statement in FOL.

Actually in McC’s (and Cyc’s) logics, c is a term (understood
to be denoting a ‘context’; the Cyc term is ‘microtheory’) rather
than a sentence.

But I just realized that we can define 'that' as a function from sentences to equivalence classes.  This implies that we don't
need IKL:  We can treat the 'that' operator as syntactic sugar
for a that-function from quoted sentences to equivalence classes.

I don’t see how that would work. Remember that in IKL, one can quantify into a ‘that’ expression (denoting a proposition), so the inner sentence (the S in (that S) ) is not quoted. 

Thus in IKL, ist is simply a two-place relation between things
in the universe.

Yes.  And as we agreed during the IKRIS project, Common Logic,
by itself, already contains 0-adic relations as first-class
citizens.  If we call them propositions, then the ist(c,p)
relation could be stated and used in CL.

What is missing in CL is the ‘that’ operator of IKL, which forms transparent names of propositions. And the fact that it is transparent means that the relation corresponding to (that S) is actually n-ary, where n is the number of names occurring free in S. 

However, there is a problem of defining equality of propositions
when used in a proof.  For example, the proposition defined by
"2+2=4" and the proposition that states Fermat's last theorem,
are both true in every model of Peano's axioms.

Therefore, you can say
"2+2=4 if and only if Fermat's last theorem is true."

But the proof of the left-hand side is trivial, and the proof
of the right-hand side took several centuries to prove.  If
proofs are being considered, we can't use "iff" as the criterion
for equality of propositions.

I don’t see why not. The proposition (that <Fermat’s theorem>) is a perfectly well-formed proposition name. Perhaps we don't know if its true or not, but we can still refer to it. And we then also don’t know if 

2+2=4 iff <Fermat’s theorem> is true or not. So what? 

On the other hand, there are some syntactic changes that have
little or no effect on the difficulty of a proof.  For example,
the following sentences "obviously" say "the same thing":

  p and q           <=>     q and p

  p or q            <=>     q or p

  p and (q and r)   <=>     (p and q) and r

But that depends on how you define "obvious" and "the same thing".
We want to include these options, but exclude the option that
"2+2=4" means "the same thing" as Fermat's last theorem.  For our
discussions in 2005, see http://jfsowa.com/logic/proposit.pdf

Yes, we agreed to use that as the basis for propositional equality in IKL theories. 

Note the following two criteria on page 2 of proposition.pdf:

Every equivalence class p in the partition of L determined by
[an MPT function] f contains exactly one canonical sentence c. the sentence s is said to state the proposition p if and only if
s is contained in the equivalence class p.

This implies that we can define IKL as syntactic sugar for CL with
the option of using a that-function from any CL sentence s to the
canonical sentence of the equivalence class that contains s.

I agree we can treat IKL as syntactic sugar for CL, but its not trivial, and I still have not worked out the full details. The only mapping I know of involves ‘unwrapping’ each that-expression using a kind of Skolemization, adding a new name for the relation; and since that’s can be nested, this has to be done recursively. And it is *not* an exact transcription; there is a conditional attached to the translate which represents the additional (and still unresolved) model-theoretic assumptions underlying the (still unproven) internal coherence of IKL model theory. 

I sketched this in an email to Chris several years ago, but he did not react, and I had already decided that CL and IKL had taken enough of my time and energy, so I never took it further. This whole issue needs some rather deep logical work to resolve, but someone else is going to have to do it. 

Here’s the unwrapping idea, in the form of (old) notes to myself, with later thoughts in {{ }} brackets:

Given any IKL sentence S containing a proposition name (that P), where P contains the free names x1…xn, define two syntactic transformations on S:

r[S] = S[A /(that P)] where A is a new simple name not occurring in S

c[S] = (forall (x1 … xn)(iff (A x1…xn) P))

Let R(S) be the result of applying r to S, N times until it contains no proposition names, and C(S) to be the CL text (ie the conjunction of the sentences)

c[S]  c[r[S]]  c[r[r[S]]] … c[r|N-1[s]] 

{{added later. This is too simple, because P itself might contain a proposition name. The full definition of the necessary recursion needs to take this into account.}}

For example, when S is the 'Kripke paradox' sentence

(forall (x)(iff (K x)
(= x (that (forall (y)(if (K y)(not (y)) ))) ) ))

then 

R(S) = (forall (x)(iff (K x)(= x A)))

and 

C(S) = (forall (K)(iff (A K) (forall (y)(if (K y)(not (y)))) )

Both R(S) and C(S) are in CL, so this seems to be a reduction of IKL to CL! But is it? We need to show that given any CL interpretation I of (R(S) union C(S)), (note, not just for every model) we can construct a modified CL interpretation I' with I'[C(S)] = true. Then that any such interpretation I' defines an IKL interpretation of S. The second part is where things get difficult. 

{{Aha, not so fast. What I think is true is that given any I which is a model of C(S), there is a corresponding IKL interpretation of S. But C(S) might be inconsistent. Or at least I can't see how to prove it can't be.}}

{{What Im now thinking is that we should use this reduction to define the truth-conditions for IKL, so that IKL is Russell-ishly reducible to CL, and we simply acknowledge that there are going to be cases which reduce to nonsense (are inconsistent), but that there are two ways for this to happen, one involving the failure of the T-condition. Kind of messy, though.

The real killer is the universal denial, (forall (x)(not (x))). This is consistent in both CL and IKL, but 

((that (forall(x)(not (x))) ))  and (forall (x)((that (not (x)) ))) are both inconsistent in IKL. I can't see any way to rescue the original T condition from that. }}

Hmmm. Later thought. In fact, all it shows is that you can't have a singleton IKL model. Maybe we need, in IKL, to insist that the universe contains at least TWO individuals (to play the roles of the true and false propositions, when needed) ??

Pat

Then the truth of any proposition in any model M is defined as
the truth of its canonical sentence in M.

The equality of any two propositions is defined as the equality
of their canonical propositions.

Any IKL text that contains one or more occurrences of propositions
may be translated to an equivalent CL text that replaces the
syntactic sugar according to the above criteria.

John

[Alex Shkotin]

2017-09-23 20:58 GMT+03:00 Pat Hayes <pha...@ihmc.us>:

On Sep 23, 2017, at 3:39 AM, Alex Shkotin <alex.s...@gmail.com> wrote:

Dear Pat,

For me, interpretation is a defined function from token, term and formula of some language to their values on math object.

..on object. There’s no such thing as a ‘math object’. Math itself is a system of ways to describe reality, but that does not imply that the reality so described is made up of ‘math objects’. 

Tell me how to point out to algebraic system and I am with you. math entity? What is it algebraic system for you?

In classical Model Theory, math object is an algebraic system.

In my case, an algebraic system is finite

How can you know that your system is finite? Finiteness isn’t first-order axiomatizable.

 

I have a special sublanguage​

 

​to handle such a systems from scratch to some size. And I hope operations always create finite system.

and uses strings and rational numbers as values.

Last time I looked, there were

​​

infinitely many rational numbers :-) (see below)

My joke about "profoundness" is that somebody may say that I need not have an algebraic system, but "

​

​

ontological description" converting my beautiful algebraic system in a finite set of OWL 2 "axioms".

And when I have a special sublanguage to handle finite algebraic system with rational numbers and strings somebody may say that all these things are possible by handling OWL 2 text.

For me a more subtle thing is "eg those which use numerals": I hope you agree that finite algebraic system may use as one of its carrier/sort Natural Numbers, and keep some of them in it; i.e. it's possible to have multi-carrier (or multi-sorted) finite algebraic system which uses numerals. 

​​

Well, actually this is a rather delicate matter. I do see what you mean, but I also am

​​

reluctant to allow you (or anyone) to claim that their theory only has ‘standard’ interpretations. Non-standard interpretations exist, whether you want to think about them or not, and they play an important role in metatheory. Let me illustrate with a toy example. Suppose you only use the numerals ‘3’ and ‘5.5’ in your axioms, and you wish to claim that these denote the rationals three and

​​

11/5

​<2 is better>​

respectively, and as these are the only rationals you need, you have a finite model. This makes sense if one takes a resolutely Platonic view of rational numbers, under which the number three is an actual object: an abstract object to be sure, but as real and well-individuated as, say,

​​

the leaning tower of Pisa. But this is a rather extreme philosophical position, IMO. It makes more sense to me to think of numbers as tokens in a system of arithmetic. Three is the thing that is the successor of two, the sum of 7 and -4, the cube root of 27, and so on, and each of these in turn is defined by its position in the algebraic system of generalized arithmetic. On this view, there really are no numbers

​​

sui generis; there are only ‘positions’ in a mathematical system of operations.

​​

(A parallel contrast describes the history of mathematics differently: was zero discovered (Plato) or invented (Relational)?) And on this second view, your

​​

clain to have just 3 and 5.5 in your model, and nothing else, sounds crazy. What algebraic framework gives these two tokens the right to be so labelled? Does your model have their sum in it? Their product? The first raised ot the power of the second? If not, you have no valid claim to call them rational numbers (on this second view); but if so, then your model must be infinite, because just one (non-zero) rational is enough to generate the entire number line, when the operations defined by arithmetic are allowed free reign to apply to it (as, on this view, they must be in order to validate the ontological claim.) 

I would be interested in your reaction, by the way.

​

​​

​At the end of this paragraphe you touch in me the ​idea of "the inevitability of algorithmic

​

 nowadays​

​

"

​

: Do we have algorithms to compare and operate with rational number tokens? Yes. And we usualy count on hardware realization of them.

​W

e may have axiom

​ ​

that sum of volume percentage content of sample

​chemical ​

components must be 100

​.​ A

nd these kind of axiom should be checked on a particular finite-algebraic system to name it the Model

​of this axiom ​

or not. 

The beauty of finite systems is that they allow direct calculation even

​ for​

quantors! And more

​,​

for them we may use in language v

​e​

ry usefull quantor # for

​number of

:

(#x:sample VPC_SiO2(x)>90)

i.e. the number of samples wich volume percentage content of SiO2 is more that 90.

​Alex​

[John F Sowa]

Pat,

Summary of the translation semantics for IKL:

1. Every text in IKL can be translated to an equivalent text in CL.
For every CL model M, the truth value of any IKL sentence is
defined to the truth value in M of its translation to CL.

2. Every that-clause is a name of a proposition. That proposition
(a) corresponds to an equivalence class of sentences, and (b)
is represented by the unique canonical sentence of its class.

3. The canonical sentence of a proposition is used to determine
(a) the identity of two propositions in a comparison by '=', and
(b) the truth value of the proposition in terms of a CL model.

To illustrate the method, consider an ambiguous sentence in English:

"Bill thinks that Sue will marry a sailor."

Two possible translations to IKL:

1. "There is a sailor x and Bill thinks that Sue will marry x."
(exists ((x Sailor)) (thinks Bill
(that (Sue will_marry x)) ))

2. "Bill thinks that there is a sailor x and Sue will marry x."
(thinks Bill
(that (exists ((x Sailor)) (will_marry Sue x))) )

> Remember that in IKL, one can quantify into a ‘that’ expression
> (denoting a proposition), so the inner sentence (the S in (that S))
> is not quoted.

I agree. The character string that follows 'that' is sent to the
translator that generates the canonical sentence of the equivalence
class. But the result of translation (the canonical sentence itself)
is not quoted during an evaluation.

For example #1 above the original sentence has no Boolean operators
or quantifiers. Therefore, that sentence is already the canonical
sentence of its equivalence class.

But the following that-clause happens to have two identical
conjuncts: (that (and (will_marry Sue x) (will_marry Sue x))).
For the canonical sentence, one duplicate is deleted, and the
result just (will_marry Sue x).

Therefore, the following sentence will evaluate to True:
(= (that (will_marry Sue x))
(that (and (will_marry Sue x) (will_marry Sue x))) )

For example #2, the that-clause contains one existential quantifier
and no Boolean operators. For the canonical sentence, translate
all bound names to some pattern that is not used elsewhere, such
as an underscore followed by an integer. The resulting canonical
sentence would be (exists ((_1 Sailor)) (will_marry Sue _1))).

> the ‘that’ operator of IKL ... forms transparent names of

> propositions. And the fact that it is transparent means that
> the relation corresponding to (that S) is actually n-ary,
> where n is the number of names occurring free in S.

This translation method produces a 0-adic relation. But it may
have some names, such as 'Sailor', 'will_marry', and 'Sue' that
are not bound to quantifiers inside the that-clause. Those names
are preserved in the canonical sentence.

>> [JFS] If proofs are being considered, we can't use "iff" as
>> the test for equality of propositions.

>
> I don’t see why not. The proposition (that <Fermat’s theorem>)
> is a perfectly well-formed proposition name. Perhaps we don't
> know if its true or not, but we can still refer to it.

There is no contradiction in saying that every theorem provable
from Peano's axioms is "the same proposition". But it causes
the concept "same proposition" to be useless for all practical
purposes: No mathematician would ever say that all theorems
provable from Peano's axioms "have the same meaning".

From the note by Pat to ontolog forum on 21 June 2014:
> For example
>
> ((that (not (p))))
>
> requires two individuals in the universe of discourse to be
> satisfied. In fact, it requires two individuals in the universe
> to even have an IKL interpretation *at all*

By the translation method, the result of translating the IKL
sentence ((that (not (p))) is the CL sentence (not (p)).
CL model theory is much simpler than IKL model theory.

> observe that the IKL model theory is not entirely guaranteed
> to be safe, in the sense that the truth conditions themselves
> might not be consistent.

With the translation method, the truth value of every IKL sentence
is defined to be the truth value of the CL sentence to which it is
translated. Therefore, IKL would be just as safe as CL.

> As an example, start with T being the simplest IKL liar sentence:
> (= p (that (not (p))))

If you evaluate that in CL, p is the name of some proposition
with a canonical sentence c. And (that (not (p)) is the name
of a proposition whose canonical sentence is (not c). Since
c cannot be the same sentence as (not c), the CL sentence
is false -- and therefore the IKL sentence is false.

> all instances of the IKL T-sentence (iff S ((that S)))
> are true in all IKL interpretations, which seems to violate
> Tarski’s theorem.

By the translation method, (iff S ((that S))) in IKL is translated
to (iff S S) in CL. That sentence is true in CL.

John

[Pat Hayes]

> On Sep 24, 2017, at 9:52 AM, John F Sowa <so...@bestweb.net> wrote:
>
> Pat,
>
> Summary of the translation semantics for IKL:
>
> 1. Every text in IKL can be translated to an equivalent text in CL.

Well, I remain unconvinced about this. The translation I outlined gives what one might call a conditional translation: it produces CL sentences C and T such that *if* C is true *then* T is a correct translation of the original IKL into CL. But that condition is all-important to the coherence of the translation, as it encodes the extra truth-conditions in the IKL semantics. I don’t believe that anything much simpler will be adequate; but as I still don’t follow the details of your proposal, I await further clarification :-)

> For every CL model M, the truth value of any IKL sentence is
> defined to the truth value in M of its translation to CL.

Ah. OK, that proposal certainly guarantees the correctness of the translation, by fiat, but now the question arises of the relationship of this version of IKL to the original IKL semantics.

>
> 2. Every that-clause is a name of a proposition. That proposition
> (a) corresponds to an equivalence class of sentences,

OK, let me probe on this. What exactly do you mean by ‘corresponds’ here?

> and (b)
> is represented by the unique canonical sentence of its class.

and by ‘is represented by’ here?

>
> 3. The canonical sentence of a proposition is used to determine
> (a) the identity of two propositions in a comparison by '=', and
> (b) the truth value of the proposition in terms of a CL model.
>
> To illustrate the method, consider an ambiguous sentence in English:
>
> "Bill thinks that Sue will marry a sailor."
>
> Two possible translations to IKL:
>
> 1. "There is a sailor x and Bill thinks that Sue will marry x."
> (exists ((x Sailor)) (thinks Bill
> (that (Sue will_marry x)) ))
>
> 2. "Bill thinks that there is a sailor x and Sue will marry x."
> (thinks Bill
> (that (exists ((x Sailor)) (will_marry Sue x))) )

I don't understand your point. The English is irrelevant. These are two different IKL expressions with different truth conditions. Neither of them is valid CL. Um…so…?

>> Remember that in IKL, one can quantify into a ‘that’ expression
>> (denoting a proposition), so the inner sentence (the S in (that S))
>> is not quoted.
>
> I agree. The character string that follows 'that' is sent to the
> translator that generates the canonical sentence of the equivalence
> class. But the result of translation (the canonical sentence itself)
> is not quoted during an evaluation.

Whoa. I really have no idea what you are talking about here. What ‘translator’? what is ‘evaluation’?

>
> For example #1 above the original sentence has no Boolean operators
> or quantifiers. Therefore, that sentence is already the canonical
> sentence of its equivalence class.
>
> But the following that-clause happens to have two identical
> conjuncts: (that (and (will_marry Sue x) (will_marry Sue x))).

? How did that happen?

> For the canonical sentence, one duplicate is deleted, and the
> result just (will_marry Sue x).
>
> Therefore, the following sentence will evaluate to True:
> (= (that (will_marry Sue x))
> (that (and (will_marry Sue x) (will_marry Sue x))) )

Yes, we agreed in the original IKL spec that this would be valid. I don’t think this point needs to be labored.

>
> For example #2, the that-clause contains one existential quantifier
> and no Boolean operators. For the canonical sentence, translate
> all bound names to some pattern that is not used elsewhere, such
> as an underscore followed by an integer. The resulting canonical
> sentence would be (exists ((_1 Sailor)) (will_marry Sue _1))).

If you insist. I really do not see what the point of this is, but whatever. (You will still not be able to check identity by simple string matching, if that was part of your plan. The gensym idea for skolemizing in RDF has identical problems.)

>> the ‘that’ operator of IKL ... forms transparent names of
>> propositions. And the fact that it is transparent means that
>> the relation corresponding to (that S) is actually n-ary,
>> where n is the number of names occurring free in S.
>
> This translation method produces a 0-adic relation. But it may
> have some names, such as 'Sailor', 'will_marry', and 'Sue' that
> are not bound to quantifiers inside the that-clause. Those names
> are preserved in the canonical sentence.

How can a term with a 0-adic relation contain other names?

The issue here is that those free names might be bound by ‘outer’ quantifiers when this is part of a larger expression. So if you eliminate them from the synax or change them, your translation cannot be applied recursively. Which is not completely fatal, but does get you into intensive care.

>>> [JFS] If proofs are being considered, we can't use "iff" as
>>> the test for equality of propositions.
>> I don’t see why not. The proposition (that <Fermat’s theorem>)
>> is a perfectly well-formed proposition name. Perhaps we don't
>> know if its true or not, but we can still refer to it.
>
> There is no contradiction in saying that every theorem provable
> from Peano's axioms is "the same proposition". But it causes
> the concept "same proposition" to be useless for all practical
> purposes: No mathematician would ever say that all theorems
> provable from Peano's axioms "have the same meaning”.

Yes, OK, let me withdraw that comment. I am quite happy to use the criteria for identity of concepts that you have developed.

>
> From the note by Pat to ontolog forum on 21 June 2014:
>> For example
>> ((that (not (p))))
>> requires two individuals in the universe of discourse to be
>> satisfied. In fact, it requires two individuals in the universe
>> to even have an IKL interpretation *at all*
>
> By the translation method, the result of translating the IKL
> sentence ((that (not (p))) is the CL sentence (not (p)).

But that does not capture the same meaning as the IKL sentence. See the examples in my earlier email.

> CL model theory is much simpler than IKL model theory.

Yes, I know. (I did write both of them, John :-)

>> observe that the IKL model theory is not entirely guaranteed
>> to be safe, in the sense that the truth conditions themselves
>> might not be consistent.
>
> With the translation method, the truth value of every IKL sentence
> is defined to be the truth value of the CL sentence to which it is
> translated. Therefore, IKL would be just as safe as CL.

Sure, but it wouldn't be IKL. I agree this idea - to redefine IKL semantics in terms of a translation into CL, so IKL is just syntactic sugar for a simpler logic - might be worth pursuing. (In fact I also suggested this idea in earlier emails, with reference to my translation.) But we do need to face up to the fact that this will be a different logic than the current IKL, and may have significantly different logical properties.

Pat

[John F Sowa]

On 9/24/2017 2:01 PM, Pat Hayes wrote:
> as I still don’t follow the details of your proposal, I await
> further clarification

The details are the ones we discussed during the IKRIS project
in 2005. Following is the 5-page article on propositions,
which I had extracted from a longer article about modal logic:
http://jfsowa.com/logic/proposit.pdf

I'll summarize relevant points in this article as they arise.

>> [JFS] Every text in IKL can be translated to an equivalent text
>> in CL. For every CL model M, the truth value of any IKL sentence
>> is defined to be the truth value in M of its translation to CL.

>
> OK, that proposal certainly guarantees the correctness of the
> translation, by fiat, but now the question arises of the
> relationship of this version of IKL to the original IKL semantics.

Two primary requirements: (1) preserve upward compatibility with
CL, and (2) avoid contradictions. Since nobody ever implemented
the previous version of IKL and there are still concerns about
contradictions, I would consider compatibility with the previous
version to be less important.

>> Every that-clause is a name of a proposition. That proposition

>> (a) corresponds to an equivalence class of sentences, and

>> (b) is represented by the unique canonical sentence of its class.
>

> What exactly do you mean by ‘corresponds’?
> and by ‘is represented by’?

From page 1 of proposit.pdf: "a proposition shall be defined as
an equivalence class of sentences that preserve truth, vocabulary,
and structure under some meaning-preserving translation (MPT)."

From pp. 1 and 2: An MPT is a function f from sentences to
sentences with four properties: (1) invertible (has an inverse);
(2) truth preserving (if f(s1)=s2, then (s1 iff s2)); (3) vocabulary
preserving (same ontology); and (4) structure preserving (a minimal
amount of Boolean transformations).

But the word 'minimal' raises some issues. On pp. 3 to 5 of
proposit.pdf, I specify five functions with different levels of
"minimality". You can take your pick, but I recommend f4 or f5
as efficiently computable and similar to what people would
usually consider "meaning preserving".

To answer the question "What do you mean by corresponds?":

On p. 1, I defined a proposition as an equivalence class.
For specifying IKL, I would say "There is a one-to-one
correspondence between propositions and equivalence classes,
as determined by the MPT f4."

To answer "And by 'is represented by'?:

From p. 2: A meaning-preserving translation defines an equivalence
class of sentences, all of which are mapped to the same "canonical
sentence", which is one of the shortest and simplest sentences in
that class. (It differs from other short and simple sentences
only by an ordering of its terms in alphabetical order.)

The proposition that corresponds to that equivalence class is
said to be *represented by* its canonical sentence. That
sentence has three primary uses:

1. For any comparison of propositions by the '=' operator,
the check for identity is performed by comparing their
canonical sentences.

2. For any Boolean operator on propositions, the canonical
sentence of the resulting proposition is determined by
applying the same operator to their canonical sentences
and deriving the canonical sentence of the result.

3. Finally, for any CL model M, the truth value of a proposition
is defined to be identical to the truth value of its canonical
sentence in terms of M.

>> But the following that-clause happens to have two identical
>> conjuncts: (that (and (will_marry Sue x) (will_marry Sue x))).
>
> ? How did that happen?

That's just an example I pulled out of thin air to show how a
non-canonical sentence could be compared to the canonical one.

> (You will still not be able to check identity by simple string
> matching, if that was part of your plan. The gensym idea for
> skolemizing in RDF has identical problems.)

I'm not doing simple string matching. I'm relying on the
uniqueness of the simplifying operations by the MPT functions.
Do you claim that those operations do not guarantee uniqueness?
What RDF operations are "identical" to the MPT operations?

Note that (1) the mapping of a that-clause to the canonical sentence
of a proposition uses only logical operators that are defined in CL,
and (2) the above uses of canonical sentences do not require any
operations that are not available in CL. Therefore, CL extended
with the notation and operations on that-clauses is a *conservative*
extension of CL -- it does not require any functionality that is
not previously available in CL.

>> This translation method produces a 0-adic relation. But it may
>> have some names, such as 'Sailor', 'will_marry', and 'Sue' that
>> are not bound to quantifiers inside the that-clause. Those names
>> are preserved in the canonical sentence.
>
> How can a term with a 0-adic relation contain other names?

Just look at one of the examples from my previous note:

(that (exists ((x Sailor)) (will_marry Sue x)) )

There are four names: 'x' is bound by a quantifier inside the
that-clause. The other four names are or may be linked to
names that occur in the environment of the that-clause.

But the sentence inside the that-clause is not a lambda expression.
It does not have any formal parameters. The free names inside
of it may (or may not) be linked to names that occur in the
environment. But the linkage is not specified by a lambda
expression or the equivalent.

>> By the translation method, the result of translating the IKL
>> sentence ((that (not (p))) is the CL sentence (not (p)).
>
> But that does not capture the same meaning as the IKL sentence.
> See the examples in my earlier email.

That is true. But as you said, the original definition of IKL
raised some issues that have never been resolved.

> I agree this idea - to redefine IKL semantics in terms of a
> translation into CL, so IKL is just syntactic sugar for a simpler
> logic - might be worth pursuing. (In fact I also suggested this
> idea in earlier emails, with reference to my translation.) But we
> do need to face up to the fact that this will be a different logic
> than the current IKL, and may have significantly different logical
> properties.

Yes. I remember the many rounds of discussion we had during
the IKRIS project. I also remember that you had discussed some
alternatives that did not go beyond CL. But I certainly don't
remember all the details. And I won't claim that the version I
proposed here will solve every problem.

But I would raise the following issues:

1. What problems or applications require the logical properties
of the original IKL that are not supported by your earlier
CL version or the version I just summarized?

2. Is there anyone who ever requested or required the features
of IKL that go beyond one or the other translation to CL?

3. If we adopted a kind of "IKL light" that does not go beyond
CL semantics, would it block some later extension to a more
powerful IKL?

4. What about Tarski's paradoxes? With IKL light, it seems that
they just have the truth value False, rather than Unstable.

John

[Pat Hayes]

On Sep 24, 2017, at 4:43 PM, John F Sowa <so...@bestweb.net> wrote:

On 9/24/2017 2:01 PM, Pat Hayes wrote:

as I still don’t follow the details of your proposal, I await
further clarification

The details are the ones we discussed during the IKRIS project
in 2005.  Following is the 5-page article on propositions,
which I had extracted from a longer article about modal logic:
http://jfsowa.com/logic/proposit.pdf

This is all about the identity conditions for propositions. I am happy to agree with you about that topic, just as we decided to do during the IKRIS discussions. So let us agree to take this as given. But nothing in there explains exactly how your proposed translation of IKL into CL is supposed to work. Since IKL is, basically, CL with the ‘that’ operator added, you have to explain how to translate IKL sentences containing ‘that’ into CL sentences while preserving meaning, or at any rate preserving it as far as possible. I havn't yet seen a clear explanation of this translation. 

I'll summarize relevant points in this article as they arise.

[JFS] Every text in IKL can be translated to an equivalent text
in CL.  For every CL model M, the truth value of any IKL sentence
is defined to be the truth value in M of its translation to CL.

OK, that proposal certainly guarantees the correctness of the
translation, by fiat, but now the question arises of the
relationship of this version of IKL to the original IKL semantics.

Two primary requirements:  (1) preserve upward compatibility with
CL, and (2) avoid contradictions.  Since nobody ever implemented
the previous version of IKL and there are still concerns about
contradictions, I would consider compatibility with the previous
version to be less important.

Every that-clause is a name of a proposition.  That proposition
(a) corresponds to an equivalence class of sentences, and
(b) is represented by the unique canonical sentence of its class.

What exactly do you mean by ‘corresponds’?
and by ‘is represented by’?

From page 1 of proposit.pdf: "a proposition shall be defined as
an equivalence class of sentences

This doesn't work for IKL, if we want to claim that (that S) expressions denote propositions. Whatever they denote, its certainly not an equivalence class of syntactic objects. But in any case, we already have a definition of a proposition in IKL: it is a zero-adic relation. 

that preserve truth, vocabulary,
and structure under some meaning-preserving translation (MPT)."

From pp. 1 and 2:  An MPT is a function f from sentences to
sentences with four properties: (1) invertible (has an inverse);
(2) truth preserving (if f(s1)=s2, then (s1 iff s2)); (3) vocabulary
preserving (same ontology); and (4) structure preserving (a minimal
amount of Boolean transformations).

But the word 'minimal' raises some issues.  On pp. 3 to 5 of
proposit.pdf, I specify five functions with different levels of "minimality".  You can take your pick, but I recommend f4 or f5
as efficiently computable and similar to what people would
usually consider "meaning preserving".

To answer the question "What do you mean by corresponds?":

On p. 1, I defined a proposition as an equivalence class.
For specifying IKL, I would say "There is a one-to-one
correspondence between propositions and equivalence classes,

as determined by the MPT f4.”

OK. So any proposition (at least any one denoted by a (that S) expression) corresponds to a class of sentences all of which are logically equivalent to S. Right? I am fine with that, but not with *identifying* the proposition with a sentence or class of sentences. But this might not be important for the current discussion. 

To answer "And by 'is represented by'?:

From p. 2:  A meaning-preserving translation defines an equivalence
class of sentences, all of which are mapped to the same "canonical
sentence", which is one of the shortest and simplest sentences in
that class.  (It differs from other short and simple sentences
only by an ordering of its terms in alphabetical order.)

The proposition that corresponds to that equivalence class is
said to be *represented by* its canonical sentence.  That
sentence has three primary uses:

1. For any comparison of propositions by the '=' operator,
   the check for identity is performed by comparing their
   canonical sentences.

Comparing how, exactly? Not by a simple string match...

2. For any Boolean operator on propositions, the canonical
   sentence of the resulting proposition is determined by
   applying the same operator to their canonical sentences
   and deriving the canonical sentence of the result.

3. Finally, for any CL model M, the truth value of a proposition
   is defined to be identical to the truth value of its canonical
   sentence in terms of M.

If I follow this correctly, these are exactly the same truth conditions that IKL already has. (Since the canonical sentence of S is always logically equivalent to S, they always have the same truth conditions. Right?) So OK, we can agree on that. Now, what exactly is your translation from IKL to CL? 

But the following that-clause happens to have two identical
conjuncts:  (that (and (will_marry Sue x) (will_marry Sue x))).

? How did that happen?

That's just an example I pulled out of thin air to show how a
non-canonical sentence could be compared to the canonical one.

(You will still not be able to check identity by simple string
matching, if that was part of your plan. The gensym idea for
skolemizing in RDF has identical problems.)

I'm not doing simple string matching.  I'm relying on the
uniqueness of the simplifying operations by the MPT functions.
Do you claim that those operations do not guarantee uniqueness?

Yes. You can’t guarantee that bound variable names will be identical.

What RDF operations are "identical" to the MPT operations?

RDF had a similar problem in wanting its skolemization (using URIs) to be unique. 

But this is an aside from the main topic here, so lets take it to another thread if you want to pursue it. 

Note that (1) the mapping of a that-clause to the canonical sentence
of a proposition uses only logical operators that are defined in CL,
and (2) the above uses of canonical sentences do not require any
operations that are not available in CL.  Therefore, CL extended
with the notation and operations on that-clauses is a *conservative*
extension of CL -- it does not require any functionality that is
not previously available in CL.

I don’t follow you here. You havn’t said anything about what happens to that-clauses. Can you show us a few actual examples of what the CL translation would be of some realistic sentences? For example, take the re/dicto distinction:

(Believes Jim (that (exists ((x Man))(Married x Mary))))

(exists ((x Man))(Believes Jim (that (Married x Mary))))

or the definition of the truth-predicate

(forall (p) (iff (True p)(p) ))

or one of the ‘paradoxes'

(forall (x)(iff (K x)(= x (that (forall (y)(if (K y)(not (y) ) ))) ))

This translation method produces a 0-adic relation.  But it may
have some names, such as 'Sailor', 'will_marry', and 'Sue' that
are not bound to quantifiers inside the that-clause.  Those names
are preserved in the canonical sentence.

How can a term with a 0-adic relation contain other names?

Just look at one of the examples from my previous note:
(that (exists ((x Sailor)) (will_marry Sue x)) )

There are four names:  'x' is bound by a quantifier inside the
that-clause.  The other four names are or may be linked to
names that occur in the environment of the that-clause.

But the sentence inside the that-clause is not a lambda expression.
It does not have any formal parameters.  The free names inside
of it may (or may not) be linked to names that occur in the
environment.  But the linkage is not specified by a lambda
expression or the equivalent.

Why are you talking about lambda? Look, that expression contains three free names (actually Im not sure if ‘Sailor’ counts, need to check that detail, so maybe 2) which can be bound by external quantifiers if this is part of a larger expression:

(exists (Sue)(Believes Jim (that (exists ((x Sailor)) (will_marry Sue x))) ))

My point is that if you translate your example to an expression - any expression - which does not contain those names, then this binding will not happen:

(exists (Sue)(Believes Jim (<expression without ‘Sue' in it>)))

so *any* such mapping cannot properly capture the same meaning. 

By the translation method, the result of translating the IKL
sentence ((that (not (p))) is the CL sentence (not (p)).

But that does not capture the same meaning as the IKL sentence.
See the examples in my earlier email.

That is true.  But as you said, the original definition of IKL
raised some issues that have never been resolved.

I agree this idea - to redefine IKL semantics in terms of a
translation into CL, so IKL is just syntactic sugar for a simpler
logic - might be worth pursuing. (In fact I also suggested this
idea in earlier emails, with reference to my translation.) But we
do need to face up to the fact that this will be a different logic
than the current IKL, and may have significantly different logical
properties.

Yes.  I remember the many rounds of discussion we had during
the IKRIS project.  I also remember that you had discussed some
alternatives that did not go beyond CL.  But I certainly don't
remember all the details.  And I won't claim that the version I
proposed here will solve every problem.

But I would raise the following issues:

1. What problems or applications require the logical properties
   of the original IKL that are not supported by your earlier
   CL version or the version I just summarized?

I have no idea. I guess this isn't the way I tend to think. IKL is a very clean, conceptually simple logic which seems to have an unrivalled expressive power. That makes it interesting.

2. Is there anyone who ever requested or required the features
   of IKL that go beyond one or the other translation to CL?

As we don’t know what those are, its hard to say.

3. If we adopted a kind of "IKL light" that does not go beyond
   CL semantics, would it block some later extension to a more
   powerful IKL?

Block?? Of course not. How could it?

4. What about Tarski's paradoxes?  With IKL light, it seems that
   they just have the truth value False, rather than Unstable.

Well, given Chris’ recent re-think, the original IKL might not have this problem after all. I did make a quite determined effort to find an actual problem, and never could, so maybe IKL is sounder than we feared. 

Pat

x

[doug foxvog]

On Mon, September 25, 2017 16:43, Pat Hayes wrote:
>> On Sep 24, 2017, at 4:43 PM, John F Sowa <so...@bestweb.net> wrote:
>> On 9/24/2017 2:01 PM, Pat Hayes wrote:
>>> as I still don't follow the details of your proposal, I await
>>> further clarification

>> The details are the ones we discussed during the IKRIS project
>> in 2005. Following is the 5-page article on propositions,
>> which I had extracted from a longer article about modal logic:
>> http://jfsowa.com/logic/proposit.pdf

>> <http://jfsowa.com/logic/proposit.pdf>

>>>> [JFS] Every text in IKL can be translated to an equivalent text
>>>> in CL. For every CL model M, the truth value of any IKL sentence
>>>> is defined to be the truth value in M of its translation to CL.
>>> OK, that proposal certainly guarantees the correctness of the
>>> translation, by fiat, but now the question arises of the
>>> relationship of this version of IKL to the original IKL semantics.

>> Two primary requirements: (1) preserve upward compatibility with
>> CL, and (2) avoid contradictions. Since nobody ever implemented
>> the previous version of IKL and there are still concerns about
>> contradictions, I would consider compatibility with the previous
>> version to be less important.

...

> OK. So any proposition (at least any one denoted by a (that S) expression)
> corresponds to a class of sentences all of which are logically equivalent
> to S. Right? I am fine with that, but not with *identifying* the
> proposition with a sentence or class of sentences. But this might not be
> important for the current discussion.

>> To answer "And by 'is represented by'?:

>> From p. 2: A meaning-preserving translation defines an equivalence
>> class of sentences, all of which are mapped to the same "canonical
>> sentence", which is one of the shortest and simplest sentences in
>> that class. (It differs from other short and simple sentences
>> only by an ordering of its terms in alphabetical order.)

>> The proposition that corresponds to that equivalence class is
>> said to be *represented by* its canonical sentence. That
>> sentence has three primary uses:

>> 1. For any comparison of propositions by the '=' operator,
>> the check for identity is performed by comparing their
>> canonical sentences.

> Comparing how, exactly? Not by a simple string match...

If the variables are canonicalized, e.g., converted into sequential names,
VAR1, VAR2, ..., VAR<N>, why not?

>> 2. For any Boolean operator on propositions, the canonical
>> sentence of the resulting proposition is determined by
>> applying the same operator to their canonical sentences
>> and deriving the canonical sentence of the result.

>> 3. Finally, for any CL model M, the truth value of a proposition
>> is defined to be identical to the truth value of its canonical
>> sentence in terms of M.

> If I follow this correctly, these are exactly the same truth conditions
> that IKL already has. (Since the canonical sentence of S is always
> logically equivalent to S, they always have the same truth conditions.
> Right?) So OK, we can agree on that. Now, what exactly is your translation
> from IKL to CL?

>>>> But the following that-clause happens to have two identical
>>>> conjuncts: (that (and (will_marry Sue x) (will_marry Sue x))).
>>> ? How did that happen?

>> That's just an example I pulled out of thin air to show how a
>> non-canonical sentence could be compared to the canonical one.

>>> (You will still not be able to check identity by simple string
>>> matching, if that was part of your plan. The gensym idea for
>>> skolemizing in RDF has identical problems.)

>> I'm not doing simple string matching. I'm relying on the
>> uniqueness of the simplifying operations by the MPT functions.
>> Do you claim that those operations do not guarantee uniqueness?

> Yes. You cant guarantee that bound variable names will be identical.

That's just another conversion step: variable name substitution. The
first variable to appear in the string becomes VAR1 in the cannonical
form, the next becomes, VAR2, etc.

??? This means that Jim believes that some specific person will marry a
sailor, since "Sue" is unbound and "Jim" is bound outside the sentence.
Previous examples had both "Sue" and "Jim" bound outside the sentence.
So, this has a different meaning.

> My point is that if you translate your example to an expression - any
> expression - which does not contain those names, then this binding will
> not happen:

Correct. If you change "Sue" from being bound to being unbound, you
change the meaning, and therefore have an incorrect translation.

> (exists (Sue)(Believes Jim (<expression without ‘Sue' in it>)))

> so *any* such mapping cannot properly capture the same meaning.

If you change bound terms to unbound terms, or vice-versa, you have a
different meaning. I don't see that John proposed that.

...

> Pat

>> John

[Ken Baclawski]

We had a lively session of the Ontology Summit 2018 which featured John Sowa on
September 20.  You are invited to attend and participate in the next session of
the Ontology Summit 2018 which will continue the discussion of the topics
developed by John Sowa.

The session will be held on Wednesday, September 27, 2017 at Noon Eastern Time.
The meeting page is http://bit.ly/2y4IbJz
The Video Conference URL is https://bluejeans.com/703588230
The chat room is http://webconf.soaphub.org/conf/room/ontology_summit_2018

The video recording of the research session of the Ontology Summit 2018 held on
9/20/2017 is now available at http://bit.ly/2wQzL8z and the meeting page is
http://bit.ly/2xrtkrE
The meeting had a followup discussion at http://bit.ly/2wSVPdX

Ken Baclawski
Member - Ontolog Forum Board of Trustees

[John F Sowa]

Pat and Doug,

Pat

> This is all about the identity conditions for propositions.

I agree.

Pat

> we want to claim that (that S) expressions denote propositions.
> Whatever they denote, its certainly not an equivalence class
> of syntactic objects.

I agree. The article proposit.pdf was an excerpt from a longer
article about modal logic. For that purpose, I defined a proposition
as an equivalence class of sentences. For CL, however, I accept
the definition of a proposition as a 0-adic relation.

But I use the notion of equivalence class as one step along the way
toward mapping the sentence S in (that S) to a simpler "canonical
sentence" c that has "the same meaning" according to a "meaning
preserving translation" (MPT). For IKL lite, I'll use the MPT f4
as specified in http://jfsowa.com/logic/proposit.pdf .

>> [Pat] You cant guarantee that bound variable names will be identical.
>
> [Doug] That's just another conversion step: variable name substitution.

> The first variable to appear in the string becomes VAR1 in the

> canonical form, the next becomes, VAR2, etc.

I agree with Doug. But you have to translate the Boolean expressions
of S and sort the result before you can number the bound variables.

The translation f4 has the following properties:

1. Truth preserving: That implies (iff S1 S2).

2. Vocabulary preserving: The set of free names in S1 and S2
(not bound by a quantifier) must be identical. The bound
names in S1 and S2 shall be replaced by some standard
sequence of names, such as _1, _2, _3, ...

3. Structure preserving: S1 and S2 shall be translated to the
canonical sentences their equivalence class: f4(S1) and f4(S2).
If f4(S1) and f4(S2) happen to be the same sentence c, then the
propositions p and q are defined to be the same. Otherwise, not.

Pat

> since "Sue" is unbound and "Jim" is bound outside the sentence.
> Previous examples had both "Sue" and "Jim" bound outside the
> sentence. So, this has a different meaning.

Doug

> If you change bound terms to unbound terms, or vice-versa, you
> have a different meaning. I don't see that John proposed that.

I agree with Doug. Free names in S are left unchanged. Bound
names shall be replaced by the sequence _1, _2, ...

In proposit.pdf, the translation by f4 replaces all Boolean operators
by 'and' and 'not' according to the usual definitions. It also
replaces every universal quantifier in the form (forall (x) S) with
the existential (not (exists (x) (not S)).

Since Common Logic allows multiple bound names in the same quantifier,
we need to translate all options to a standard form. For example,
the following two sentences

(exists ((S Sailor) (P Plumber)) S)
(exists (x) (exists (y) (and (Plumber x) (and (Sailor y) S))

would map to the same canonical sentence:

(exists (_1 _2) (and (Plumber _1) (Sailor _2) S).

Order of translating any S to its canonical sentence:

1. First translate all Boolean operators to 'and' and 'not'.

2. Move all quantifiers to prenex form (in front) and translate
all universal quantifiers to existential. The beginning of
the sentence will be a string of existential quantifiers
intermixed with some occurrences of 'not'. It will be
followed by a mixture of 'and' and 'not' expressions.
Apply any Boolean simplifications.

3. Within a conjunction of two or more expressions, larger
expressions are sorted after simpler ones. Expressions of
the same complexity are sorted in alphabetical order according
to the free names -- but ignore the spelling of the bound names.

4. Then rename (and number) all bound names in the order in
which they occur in the Boolean part. For example, "_1"
would replace the first bound name that occurs in the Boolean
part, but it might not be the first name in the quantifiers.

But I admit that proposit.pdf did not say anything about
any occurrence of 'that' nested inside the S of (that S).

Before translating sentences according to f4, start by translating
every 'that' expression which does not contain a nested 'that':
If S in (that S) is an ordinary CL sentence, replace it with
(that f4(S)). By the definition of f4, this replacement has
the "same meaning" as (that S). And by the definition of the
'that' operator, (that f4(S)) is a name. Treat (that f4(S))
like a name in any further translations by f4.

John

[Pat Hayes]

John, we seem to be talking past each other. You keep giving me details of a way to normalize sentences of CL. This is a (these are) mapping(s) from sentences to logically equivalent sentences. OK, fine. But I am not deeply interested in these mappings, as they seem to have no relevance to (what I understood you be announcing) a way to reduce IKL to CL, or perhaps to re-understand IKL sentences as syntactic sugar for more complicated CL sentences. To do this latter, you need to explain how to map an IKL sentence containing a that-term into one not containing it, but with the same meaning. I do not yet see in any of your emails where you do that.

Just to keep things simple, take this IKL sentence:

(exists (x)(and (R (that (exists (y)(M x y A))) x) (exists (y)(M x y A)) ))

which has the overall form (exists (x)(and (R (that S) x) S)). I believe that the inner sentence S is already in your canonical form, except perhaps for a change of bound variable name, so the meaning-preserving canonicalization is irrelevant.

This has the following entailments in IKL (among many others, of course):

(exists (x p)(R p x) (p) )
(exists (x z)(and (R (that (exists (y)(M x y z))) x) (exists (y)(M x y z)) ))

What would be the translations of these three sentences into CL, on your proposal, and would the translation of the first CL-entail those of the other two?

Pat

[John F Sowa]

On 9/26/2017 1:46 PM, Pat Hayes wrote:
> we seem to be talking past each other. You keep giving me
> details of a way to normalize sentences of CL. This is a
> (these are) mapping(s) from sentences to logically equivalent
> sentences. OK, fine.

That is all I was trying to do.

Pat

> you need to explain how to map an IKL sentence containing a that-term
> into one not containing it, but with the same meaning. I do not yet
> see in any of your emails where you do that.

I didn't want to do that. I like the IKL syntax, and I wanted
to define a way to evaluate it while using only CL model theory.

I apologize for saying that my version of "IKL lite" was
"syntactic sugar" for CL. That was a mistake, because I realize
that metalanguage does introduce a semantic feature that cannot
be represented in just the object language by itself.

I knew that from reading Tarski, but I carelessly used the phrase
"syntactic sugar" in my earlier note. That phrase sounded good
at the moment, but it was false and misleading.

But the original IKL semantics from 2005 goes beyond CL semantics.
When I reread my proposit.pdf article, I realized that it would be
sufficient to support the syntax of the that-term with a semantics

that did not go beyond CL.

Advantage of "IKL Lite" over the original (2005) semantics of IKL:

1. Any CL implementation could implement IKL Lite with just one
syntactic feature added to the translator.

2. In CL, paradoxes such as the liar have the stable truth-value F,
not an unstable wavering between T and F.

John

[John F Sowa]

I made some minor revisions to the slides I presented last week,
and I added a new section 4.

For today's session, I'll briefly skim through the slides from
last week, and anybody can ask any questions that may be relevant.
After that, I'll go through the slides in Section 4.

I posted the latest version of the slides at
http://jfsowa.com/context/contexts.pdf

I'm still making some revisions. So the current version has
the date "Draft: 26 September 2017". At some point before the
session begins, the date on the slides will be "27 September 2017".

John

[joseph simpson]

John:

The link to the slides appears to be broken.

Take care,

Joe

--
All contributions to this forum by its members are made under an open content license, open publication license, open source or free software license. Unless otherwise specified, all Ontolog Forum content shall be subject to the Creative Commons CC-BY-SA 4.0 License or its successors.
--- You received this message because you are subscribed to the Google Groups "ontolog-forum" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-forum+unsubscribe@googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

--

Joe Simpson

“Reasonable people adapt themselves to the world. 

Unreasonable people attempt to adapt the world to themselves. 

All progress, therefore, depends on unreasonable people.”

George Bernard Shaw

[Ken Baclawski]

The correct link is http://jfsowa.com/ikl/contexts/contexts.pdf

-- Ken

[Pat Hayes]

> On Sep 26, 2017, at 2:37 PM, John F Sowa <so...@bestweb.net> wrote:
>
> On 9/26/2017 1:46 PM, Pat Hayes wrote:
>> we seem to be talking past each other. You keep giving me
>> details of a way to normalize sentences of CL. This is a
>> (these are) mapping(s) from sentences to logically equivalent
>> sentences. OK, fine.
>
> That is all I was trying to do.
>
> Pat
>> you need to explain how to map an IKL sentence containing a that-term
>> into one not containing it, but with the same meaning. I do not yet
>> see in any of your emails where you do that.
>
> I didn't want to do that. I like the IKL syntax, and I wanted
> to define a way to evaluate it while using only CL model theory.
>
> I apologize for saying that my version of "IKL lite" was
> "syntactic sugar" for CL. That was a mistake, because I realize
> that metalanguage does introduce a semantic feature that cannot
> be represented in just the object language by itself.
>
> I knew that from reading Tarski, but I carelessly used the phrase
> "syntactic sugar" in my earlier note. That phrase sounded good
> at the moment, but it was false and misleading.
>
> But the original IKL semantics from 2005 goes beyond CL semantics.
> When I reread my proposit.pdf article, I realized that it would be
> sufficient to support the syntax of the that-term with a semantics
> that did not go beyond CL.

OK, lets agree that this new logic has the syntax of IKL, but a weaker semantics based on that of CL, so it is a new logic, call it IKLL. But I am still in the dark about what that semantics looks like. What *is* the semantics of IKLL? In particular, what does it say a term of the form (that S) denotes? How, if at all, does S relate to ((that S)), bearing in mind that the outer parentheses are simply application of a zero-adic relation ?

We could start with the examples in my earlier email: does this new semantics support those entailments, ie existential generalization over a proposition name and also over a free name inside a proposition name?

>
> Advantage of "IKL Lite" over the original (2005) semantics of IKL:
>
> 1. Any CL implementation could implement IKL Lite with just one
> syntactic feature added to the translator.
>
> 2. In CL, paradoxes such as the liar have the stable truth-value F,
> not an unstable wavering between T and F.

Well, they seem to have the F value in IKL, with the current semantics. The issue is whether that semantics is internally coherent.

Pat

>
> John
>

[John F Sowa]

After I posted those slides, I took a short nap.

I just woke up. I'm very sorry.

John

[Ken Baclawski]

We are still meeting.  Try joining us.

-- Ken

[Jakub Moskal]

We are still on the call, can you join us now?

Jakub

[Alex Shkotin]

John,

about the call: last meeting I remember you told that from one phone you can't join BlueJeans and from another it's OK.

Is this correct?

Alex

[David Whitten]

John,

The link to Pat Hayes original discussion in your pdf needs a capital H. When it has a lowercase h, it gets a 404 error.

[John F Sowa]

On 9/27/2017 11:58 AM, Pat Hayes wrote:
> lets agree that this new logic has the syntax of IKL, but a weaker
> semantics based on that of CL, so it is a new logic, call it IKLL.
> But I am still in the dark about what that semantics looks like.

Before I say anything else, I'll repeat the apology in my last note:
I apologize for saying that IKLL (AKA IKL Lite) is syntactic sugar
for CL. The 'that' operator introduces metalanguage, which cannot
be eliminated in any translation to CL.

Therefore, the model theory for IKLL must recognize any expression
of the form (that S), and it must translate S to its canonical form
before it can do any comparison, such as (= (that S1) (that S2)).

The model theory for IKLL must also do that translation whenever it
evaluates the truth value of any occurrence of the 'that' operator.

Short summary of IKLL semantics:

1. A term (that S) is the name of a CL proposition (0-adic relation).

2. For any sentence S, (iff S ((that S))) is true.

3. If (= P (that S)) is true, then the name P denotes "the same"
0-adic relation (AKA proposition).

4. For any two sentences (= (that S1) (that S2)) is true if and
only if they have the same canonical sentence: f4(S1) = f4(S2).

> We could start with the examples in my earlier email

From note of Sept. 26 by PJH:

> take this IKL sentence:
>
> (exists (x)(and (R (that (exists (y)(M x y A))) x)
> (exists (y)(M x y A)) ))
>
> which has the overall form (exists (x)(and (R (that S) x) S)).
> I believe that the inner sentence S is already in your canonical
> form, except perhaps for a change of bound variable name, so the
> meaning-preserving canonicalization is irrelevant.

I agree. And as I said in my apology, no sentence in IKLL
that contains a 'that' operator can be translated to plain CL.

> This has the following entailments in IKL (among many others, of course):
>
> (exists (x p)(R p x) (p) )
>
> (exists (x z)(and (R (that (exists (y)(M x y z))) x)
> (exists (y)(M x y z)) ))
>
> What would be the translations of these three sentences into CL,
> on your proposal, and would the translation of the first CL-entail
> those of the other two?

The IKLL sentence above does indeed entail both of these sentences.

John

[John F Sowa]

On 9/27/2017 2:11 PM, Alex Shkotin wrote:
> last meeting I remember you told that from one phone you can't join
> BlueJeans and from another it's OK.

No. That wasn't the problem. The issue has something to do with
the cookies that Blue Jeans keeps. I was able to use Blue Jeans
the first time. But the second time, its cookies created a problem,
and today's attempt was a disaster.

After erasing the cookies and doing some fiddling, I was able
to restart as a new user. But I think that I now know how to
get Blue Jeans to work, and I'll try it next week (when I won't
be the speaker).

John

[Pat Hayes]

On Sep 27, 2017, at 2:22 PM, John F Sowa <so...@bestweb.net> wrote:

….

Short summary of IKLL semantics:

1. A term (that S) is the name of a CL proposition (0-adic relation).

2. For any sentence S, (iff S ((that S))) is true.

3. If (= P (that S)) is true, then the name P denotes "the same"
   0-adic relation (AKA proposition).

4. For any two sentences (= (that S1) (that S2)) is true if and
   only if they have the same canonical sentence: f4(S1) = f4(S2).

But this is *exactly* the IKL model theory, John. (Well, not quite exactly, since IKL has a few other minor differences from CL, but lets ignore those for now.)  The model theory in https://www.ihmc.us/users/phayes/ikl/spec/spec.html imposes precisely the first three constraints, and the fourth was agreed by the IKRIS group as appropriate for deciding equality between propositions. (See https://www.ihmc.us/users/phayes/IKL/GUIDE/GUIDE.html#propIdent .)

So IKLL *is* IKL.

Pat

We could start with the examples in my earlier email

From note of Sept. 26 by PJH:

take this IKL sentence:
(exists (x)(and (R (that (exists (y)(M x y A))) x)
               (exists (y)(M x y A)) ))
which has the overall form (exists (x)(and (R (that S) x) S)).
I believe that the inner sentence S is already in your canonical
form, except perhaps for a change of bound variable name, so the
meaning-preserving canonicalization is irrelevant.

I agree.  And as I said in my apology, no sentence in IKLL
that contains a 'that' operator can be translated to plain CL.

This has the following entailments in IKL (among many others, of course):
(exists (x p)(R p x) (p) )
(exists (x z)(and (R (that (exists (y)(M x y z))) x)
                    (exists (y)(M x y z)) ))

What would be the translations of these three sentences into CL,
on your proposal, and would the translation of the first CL-entail
those of the other two?

The IKLL sentence above does indeed entail both of these sentences.

John

[Douglas Miles]

It will help me understand a great deal if I had names for the  ___s?

(domain that 1 ___)  ;; arg1Isa/argQuotedIsa

(range that ___)  ;; resultIsa/resultQuotedIsa

(domain ist 1 ___)

(domain ist 2 ___)

Also it is fine to have multiple things such as:

(range that UnaryPredicate)

(range that SomethingElse)

In fact, the more, the better.

-Douglas

[David Whitten]

I think that code that implements IKL should treat  the form "(that ?)"  as a syntactic function that returns a proposition which should be treated as a first class object.  

In the document

https://www.ihmc.us/users/phayes/ikl/spec/spec.html

There is a statement:

"   Relations with no arguments are identified with propositions and character sequences corresponding to names, when used as functions with no arguments, are required to evaluate to the denotation of the name.   "

I think the syntax "that" must be a way of marking relations with no arguments so the range of a "that" must be a denotation.

When John Sowa talks about the unique canonical sentence of its equivalence class, does that mean that every sentence in the equivalence class has the same denotation? 

The aforementioned document also has the statement:

Character sequences which capture names in a vocabulary have a special semantic condition imposed on them in any interpretation of that vocabulary. 

Which I think means that the rest of a "that" clause must be a character sequence. Combined with the "(that" and the ")" the full character sequence must constitute a sentence. 

Does this gibe with everyone else's understanding? . 

--

All contributions to this forum by its members are made under an open content license, open publication license, open source or free software license. Unless otherwise specified, all Ontolog Forum content shall be subject to the Creative Commons CC-BY-SA 4.0 License or its successors.
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-forum+unsubscribe@googlegroups.com.

[John F Sowa]

On 9/29/2017 12:29 AM, Pat Hayes wrote:
>> [JFS] Short summary of IKLL semantics:

>>
>> 1. A term (that S) is the name of a CL proposition (0-adic relation).
>>
>> 2. For any sentence S, (iff S ((that S))) is true.
>>
>> 3. If (= P (that S)) is true, then the name P denotes "the same"
>>    0-adic relation (AKA proposition).
>>
>> 4. For any two sentences (= (that S1) (that S2)) is true if and
>>    only if they have the same canonical sentence: f4(S1) = f4(S2).
>
> But this is *exactly* the IKL model theory, John.

Yes. We agreed to these four principles during the IKRIS project.
And I have always been happy with them. I don't want to change them.

> (Well, not quite exactly, since IKL has a few other minor
> differences from CL, but lets ignore those for now.)

It's those "minor" differences that raise serious questions about
"safety" or freedom from paradoxes. They are the reasons why we
did not propose IKL as an option for the revised CL.

What I'm proposing is to use CL model theory unchanged -- except
for one semantic rule that specifies how the truth value of
the syntactic form (that S) is evaluated:

1. Map S to its canonical sentence C = f4(S).

2. In any model M, the truth value in M of the proposition
named (that S) is identical to the truth value of C in M.

I claim that CL model theory with this rule supports IKL Lite,
it is just as safe as CL in avoiding paradoxes, and it can be
implemented in any CL processor by adding software to support
the above rule.

John

[John F Sowa]

On 9/29/2017 12:54 AM, Douglas Miles wrote:
> It will help me understand a great deal if I had names for the __s?

>
> (domain that 1 ___)  ;; arg1Isa/argQuotedIsa

> ...

What you're asking for is a feature that has been implemented
in many languages. One of the earliest is IBM's notorious
JCL (Job Control Language) for OS/360, MVS... But many new
versions keep popping up all the time.

Problems with such notations:

1. The syntax has a huge proliferation of terminology, options,
features, defaults, exceptions...

2. Programmers who master all those options love it. They can
do wonders with the notation.

3. But beginners hate it. They are hopelessly confused, and they
need to study manuals, take courses, and get long experience
to use it effectively.

4. Programmers who had mastered it, discover that if they go
away for 6 months, they have to relearn it before they can
begin using it again.

But I won't say "no" to your proposal. What I will say is "Go do it."
Write the syntax for the notation you want, and specify how it is
mapped to a base logic, which may be ordinary FOL, or CL, or IKL,
or whatever.

Then try to get support for it (funding, adopters, users...).

As somebody who has done such things in the past, I have
zero desire to get involved.

John

[Douglas Miles]

On Fri, Sep 29, 2017 at 8:40 AM, John F Sowa <so...@bestweb.net> wrote:

On 9/29/2017 12:54 AM, Douglas Miles wrote:

It will help me understand a great deal if I had names for the __s?

(domain that 1 ___)  ;; arg1Isa/argQuotedIsa
...

What you're asking for is a feature that has been implemented
in many languages.  One of the earliest is IBM's notorious
JCL (Job Control Language) for OS/360, MVS...  But many new
versions keep popping up all the time.

Problems with such notations:

 1. The syntax has a huge proliferation of terminology, options,
    features, defaults, exceptions...

I understand.  The worse part is I was asking for "names" in which has proliferated many contentious debates.  

For me, I have no problem looking past the issues of exceptions and defaults (I wouldn't have tried to turn this to a knowledge engineering debate if under some system it would have caused problems)

 

 2. Programmers who master all those options love it.  They can
    do wonders with the notation.

 3. But beginners hate it.  They are hopelessly confused, and they
    need to study manuals, take courses, and get long experience
    to use it effectively.

  4. Programmers who had mastered it, discover that if they go
     away for 6 months, they have to relearn it before they can
     begin using it again.

I can't imagine many ​people once they learn IKL,CGIF,CLIF,KIF,CYCL,MELD  will let themselves escape thinking about it for such a duration :)  

 

But I won't say "no" to your proposal.  What I will say is "Go do it."

​Sure it only takes a few minutes,

Write the syntax for the notation you want, and specify how it is
mapped to a base logic, which may be ordinary FOL, or CL, or IKL,
or whatever.

​​

​​(domain ist​ 1 PropositionalContext)

​(domain ist​ 2 AskableSentence)  ;; note ​​Askable means open whereas Assertable implies closed

​(domain that AskableSentence) 

​(range that AskableSentence) 

​(range that Individual) ;; vs class

​(range that UnaryPredicate)

​(comment that "A function that allows one or more sentences to become a first class individual  and still retrain its propositional interpretation") ​​

 

Then try to get support for it (funding, adopters, users...).

​I am one of your adopter​s.

 

As somebody who has done such things in the past, I have
zero desire to get involved.

​I do not think you really mean which to not wishing to declare how parts of IKL are used in context to SUMO  or BFO, if so or not, please explain.

- Douglas

[Douglas Miles]

​All,

 see below,  this is my real question:

​

 

But I won't say "no" to your proposal.  What I will say is "Go do it."

​​

​​(domain ist​ 1 PropositionalContext)

​(domain ist​ 2 AskableSentence)  ;; note ​​Askable means open whereas Assertable implies closed

​(domain that AskableSentence) 

​(range that Sentence

​Reified​

) 

​(range that Individual) ;; vs class

​(range that UnaryPredicate)

​(comment that "A function that allows one or more sentences to become a first class individual  and still retrain its propositional interpretation") ​​

​Why I am asking this.. is if one of my users queries or uses the following as an anteceedant:

(ist (KnowsFn DMiles) ?What)

I was intending to return each proposition surrounded by  (that ...)

In fact most operations about sentences I planned on surround with 'that' 

which tempts them to use...

(ist (KnowsFn DMiles) (that ?Idea) )

I am trying to decide and understand what properties  ?Idea should have

-Douglas

​

 

[Pat Hayes]

Hi Douglas

Um…IKL isn’t OWL; there are no assigned range or domain restrictions. IKL is an extension of CLIF, and part of the design philosophy of CLIF was to be as ‘permissive’ as possible, perhaps to an extreme degree (we refer to it informally as ‘wild west syntax’). So any name can be used as a constant, a relation or a function, with any number of arguments, and can be applied to anything, including by the way itself, or to nothing at all, ie no arguments. So expressions like this are legal in CLIF, and therefore in IKL:

(R (R R))   ie the property R is true of the result of applying the function R to the individual R.

(R (R))   the property R is true of the result of applying the function R to nothing. 

Because of this, it does not really make sense, in IKL, to ask if something *is* a property or a relation or a function: the answer is always "yes, or no if you prefer." It does however make sense to ask, of any particular occurrence of a name inside an expression, how that name is being used there: is it denoting a function, or relation, or… etc.., because that can be determined from its position in the syntax. So in the first example above, the expression is at the top level of a text, so it must be a sentence, so it must be an atomic sentence (no connectives or quantifiers in first position), so that first R must be denoting a relation, with (check it) one argument. That argument must be a term, so the second R must be denoting a function of one argument, so that third R must be interpreted as an individual name. 

But in any case, the (that S) construction is a new piece of syntax, not even meaningful in a conventional logic. (DON'T think of it as a function ’that’ applied to an argument! It's a completely different entity, it just looks similar because IKL syntax is LISPish and uses parentheses for everything.) It is defined in IKL to be a *name* of a special kind, which denotes some thing which, when used as a zero-adic relation, ie when used in a an atomic sentence of the form (<name>) – which is IKL’s understanding of what a proposition is – will have the same truth-value as S. That is, IKL requires S and ( (that S) ) – both sentences – always have the same truthvalue. 

If you feel like your head is exploding, all I can tell you is that you are not alone, but that it is possible to get used to IKL after a while (and when you do, it is wonderfully expressive and natural). For more attempts to give an intuitive explanation of the (that S) idea and IKL in general, try looking at one of these, if you have the time:

https://www.slideshare.net/PatHayes/ikl-survey

https://www.slideshare.net/PatHayes/ikl-presentation-for-ontolog

https://www.ihmc.us/users/phayes/ikl/guide/guide.html#propositionNames

Pat

[Pat Hayes]

> On Sep 29, 2017, at 10:11 AM, John F Sowa <so...@bestweb.net> wrote:
>
> On 9/29/2017 12:29 AM, Pat Hayes wrote:
>>> [JFS] Short summary of IKLL semantics:
>>>
>>> 1. A term (that S) is the name of a CL proposition (0-adic relation).
>>>
>>> 2. For any sentence S, (iff S ((that S))) is true.
>>>
>>> 3. If (= P (that S)) is true, then the name P denotes "the same"
>>> 0-adic relation (AKA proposition).
>>>
>>> 4. For any two sentences (= (that S1) (that S2)) is true if and
>>> only if they have the same canonical sentence: f4(S1) = f4(S2).
>> But this is *exactly* the IKL model theory, John.
>
> Yes. We agreed to these four principles during the IKRIS project.
> And I have always been happy with them. I don't want to change them.

Then you are talking about IKL, and have been all along. In which case I really do not know what this thread is supposed to be about.

>> (Well, not quite exactly, since IKL has a few other minor
>> differences from CL, but lets ignore those for now.)
>
> It's those "minor" differences that raise serious questions about
> "safety" or freedom from paradoxes.

No. They are things like different ways of handling importation, restricted quantification, etc: syntactic details of no relevance to the central semantic issue of proposition names and Tarski’s theorem. (There is also the captured-name convention in IKL but not CL, which allows for quantification over names, and which may conceivably have some long-term consequences, though nobody, including you, has raised any and I do not know of any, so I continued to ignore it.)

> They are the reasons why we
> did not propose IKL as an option for the revised CL.

No, they are not. All the concern about IKL’s internal coherence arise from that semantic condition on truth which aligns S with ((that S)) for all sentences. The other differences between IKL and CL have, correctly, been ignored; indeed, I have come to think that I am the only person who remembers them.

> What I'm proposing is to use CL model theory unchanged -- except
> for one semantic rule that specifies how the truth value of
> the syntactic form (that S)

(that S) is a referring name: it does not have a truth value.

> is evaluated:
>
> 1. Map S to its canonical sentence C = f4(S).

If you prefer, but this is irrelevant to the model theory.

>
> 2. In any model M, the truth value in M of the proposition
> named (that S) is identical to the truth value of C in M.

Propositions do not have truth values. IKL model theory already requires the zero-adic relational extension of (that S) to be true exactly when S is, which gives the central tautologies

(iff S ((that S)) )

for any sentence S. (Actually it gives their universal closures, which is even stronger.)

>
> I claim that CL model theory with this rule supports IKL Lite,

CL with this condition is, effectively, IKL. Your IKL Lite *is* IKL (ignoring the peripheral differences concerning syntax and quotifying over names.) .

> it is just as safe as CL in avoiding paradoxes,

No, it isn’t, with this condition in the semantics. All the discussion about paradoxes, etc., has effectively been about this logic, CL plus the (iff S ((that S))) rule.

> and it can be
> implemented in any CL processor by adding software to support
> the above rule.

This sentence has to be one of the greatest hand-waves of all time. All you are saying here is that one can get an IKL reasoner by ‘adding software to support’ the IKL features. That is no doubt true, but what kind of support do you think that ‘rule’ requires? With apologies to Inigio Montoya, I do not think that this rule means what you think it means. Just that one semantic condition, added to the CL semantics, makes a whole lot of unusual entailments valid in IKL. How do you suggest adding software to handle these examples, just for a start:

(and (R (that (P A)) A) (P A))

entails

(exists (x)(and (R (that (P x)) x) (P x) ))

and also

(exists (p)(and (R p A) (p) ))

Pat

[Douglas Miles]

On Fri, Sep 29, 2017 at 3:22 PM, Pat Hayes <pha...@ihmc.us> wrote:

Hi Douglas

Um…IKL isn’t OWL; there are no assigned range or domain restrictions. IKL is an extension of CLIF, and part of the design philosophy of CLIF was to be as ‘permissive’ as possible,

​That is good, I like that​

 

perhaps to an extreme degree (we refer to it informally as ‘wild west syntax’). So any name can be used as a constant, a relation or a function, with any number of arguments, and can be applied to anything, including by the way itself, or to nothing at all, ie no arguments. So expressions like this are legal in CLIF, and therefore in IKL:

​(R (R R))   ie the property R is true of the result of applying the function R to the individual R.​

(R (R))   the property R is true of the result of applying the function R to nothing. 

Because of this, it does not really make sense, in IKL, to ask if something *is* a property or a relation or a function: the answer is always "yes, or no if you prefer." It does however make sense to ask, of any particular occurrence of a name inside an expression, how that name is being used there: is it denoting a function, or relation, or… etc.., because that can be determined from its position in the syntax. So in the first example above, the expression is at the top level of a text, so it must be a sentence, so it must be an atomic sentence (no connectives or quantifiers in first position), so that first R must be denoting a relation, with (check it) one argument. That argument must be a term, so the second R must be denoting a function of one argument, so that third R must be interpreted as an individual name.  

But in any case, the (that S) construction is a new piece of syntax, not even meaningful in a conventional logic. (DON'T think of it as a function ’that’ applied to an argument! It's a completely different entity, it just looks similar because IKL syntax is LISPish and uses parentheses for everything.) It is defined in IKL to be a *name* of a special kind, which denotes some thing which, when used as a zero-adic relation, ie when used in a an atomic sentence of the form (<name>) – which is IKL’s understanding of what a proposition is – will have the same truth-value as S. That is, IKL requires S and ( (that S) ) – both sentences – always have the same truthvalue. 

​Is see so 'that' would even be a disambiguator if I wanted to say:

The property R is true of the Proposition: "property R with an argument of the individual R.​" 

​​(R (that (R R)))    ;; No function in this case

​

If you feel like your head is exploding, all I can tell you is that you are not alone, but that it is possible to get used to IKL after a while (and when you do, it is wonderfully expressive and natural). For more attempts to give an intuitive explanation of the (that S) idea and IKL in general, try looking at one of these, if you have the time:

​

Not to try to make it over complex:

​​(R ((that (R R)))) 

;; The property R is true of the "logical truth" of the Proposition: "property R with an argument of the individual R.​"  ?

​

https://www.slideshare.net/PatHayes/ikl-survey

https://www.slideshare.net/PatHayes/ikl-presentation-for-ontolog

​​Side 14 is an interesting treat.

so the bare 'p' in all those cases is   (= p  (that (p)))   ?

 

https://www.ihmc.us/users/phayes/ikl/guide/guide.html#propositionNames

​IKL is very powerful and so far nothing that I dislike.

I missed in my readings how to access access a sentence arg using an index...

I'd like to define the 'argN'

(argN TERM N FORMULA) 




To means that TERM occurs in the Nth argument-position within FORMULA. 

For example:

    (argN Dog 1 (that (subclass  Dog Mammal)))  ;; would be true.

Here is a candidate guess I have:

;; arg1

(forall (rel term sentence rest)

   (iff (argN term 1 (that (r term @rest)))

   (rel term @rest)))

;; arg2

(forall (rel term sentence rest)

   (iff (argN term 2 (that (r ? term @rest)))

   (rel ? term @rest)))

Is this correct?

Thank you in advance

 Douglas

[Douglas Miles]

​Oops had an extra variable in my last email  I will edit in place:

 

I missed in my readings how to access access a sentence arg using an index...

I'd like to define the 'argN'

(argN TERM N FORMULA) 




To means that TERM occurs in the Nth argument-position within FORMULA. 

For example:

    (argN Dog 1 (that (subclass  Dog Mammal)))  ;; would be true.

Here is a candidate guess I have:

Removed unused 'sentence' variable:​

 

;; arg1

​ ​

(forall (rel term rest)

   (iff (argN term 1 (that (r

​el​

term @rest)))

   (rel term @rest)))

;; arg2

(forall (rel term rest)

   (iff (argN term 2 (that (r

rel​

? term @rest)))

   (rel ? term @rest)))

 

Is this correct?

Thank you in advance

 Douglas

​Also, would this version2 to getting arg1 work out?

(forall (

​

sentence 

​ ​

​

rel term rest

​ ​

)

   (iff 

​     (and 

         (= (that 

sentence 

) (

that 

(r

​el​

term @rest)

​) 

          sentence)​

​

    (argN term 1 sentence ))

​

​Again, thank you,

   Douglas​

[John F Sowa]

Pat,

> Then you are talking about IKL, and have been all along.

If you agree to that, then we are "almost" in agreement.

I admit that I had not dug into the details of those "minor" issues
(see below), but I did worry about some of them.

> Propositions do not have truth values.

What??? Some logics use the word 'sentence' instead of 'proposition'.
But every logic that uses the word 'proposition' (starting with
"propositional logic") does indeed assume that propositions evaluate
to T or F in the model theory.

> IKL model theory already requires the zero-adic relational extension
> of (that S) to be true exactly when S is, which gives the central
> tautologies (iff S ((that S)) )

Yes, of course. I assumed that we had agreed to use the word
'proposition' as a synonym for "zero-adic relation". And that
tautology you stated is one I had also stated several notes ago.

>> [JFS} It's those "minor" differences that raise serious questions

>> about "safety" or freedom from paradoxes.
>
> No. They are things like different ways of handling importation,
> restricted quantification, etc: syntactic details of no relevance
> to the central semantic issue of proposition names and Tarski’s
> theorem.

For quantifiers in CL, we had agreed that the following notation

(forall ((x T)) S)
(exists ((x T)) S)

is syntactic sugar for

(forall (x) (if (T x) S))
(exists (x) (and (T x) S))

I would assume that sentences with restricted quantifiers are
resolved by expanding them to sentences without them.

> (There is also the captured-name convention in IKL but not CL,
> which allows for quantification over names, and which may
> conceivably have some long-term consequences, though nobody,
> including you, has raised any and I do not know of any,
> so I continued to ignore it.)

Although I did not discuss the issue in detail, I was assuming
something along the lines of the examples below.

> How do you suggest adding software to handle these examples,
> just for a start:
>
> (and (R (that (P A)) A) (P A))
>
> entails
>
> (exists (x)(and (R (that (P x)) x) (P x) ))
>
> and also
>
> (exists (p)(and (R p A) (p) ))

Given a CL theorem prover, create an IKL theorem prover by
adding the software to support the derivation of a canonical
sentence for any that-term.

The IKL theorem prover would use the same methods of unification
and inference as the CL theorem prover, but with one extension:
whenever it encounters 'that' in function position, it invokes
the IKL software to generate or unify canonical sentences -- and
that unification process would invoke the CL software recursively.

For sentence #1 above, which contains (that (P A)), the IKL theorem
prover would derive the canonical sentence (P A).

For sentence #2, it would unify (P A) with (P x) to force (= x A}.

For sentence #3, it would unify (R p A) with (R (that P A) A)
to force p to be the name of a proposition with canonical
sentence (P A).

Both entailments would be proved -- QED (Quite Easily Done).

John

[Pat Hayes]

> On Sep 29, 2017, at 10:01 PM, John F Sowa <so...@bestweb.net> wrote:
>
> Pat,
>
>> Then you are talking about IKL, and have been all along.
>
> If you agree to that, then we are "almost" in agreement.

Well, we are not in agreement about the claim of “reducing” IKL to CL. I have already pointed out how such a reduction can be done, and it isn’t what you are talking about here.

>
> I admit that I had not dug into the details of those "minor" issues
> (see below), but I did worry about some of them.
>
>> Propositions do not have truth values.
>
> What???

I repeat, propositions do not have truth values. Sentences have truth values; propositions are zero-adic relations.

> Some logics use the word 'sentence' instead of 'proposition'.
> But every logic that uses the word 'proposition' (starting with
> "propositional logic") does indeed assume that propositions evaluate
> to T or F in the model theory.

IKL does not assume this. an IKL name '(that S)' denotes an individual in the universe of discourse, not a truth value.

>> IKL model theory already requires the zero-adic relational extension
>> of (that S) to be true exactly when S is, which gives the central
>> tautologies (iff S ((that S)) )
>
> Yes, of course. I assumed that we had agreed to use the word
> 'proposition' as a synonym for "zero-adic relation". And that
> tautology you stated is one I had also stated several notes ago.

Then you must also have agreed that propositions do not have truth values.

(Why are we even having this conversation??)

>>> [JFS} It's those "minor" differences that raise serious questions
>>> about "safety" or freedom from paradoxes.
>>
>> No. They are things like different ways of handling importation,
>> restricted quantification, etc: syntactic details of no relevance
>> to the central semantic issue of proposition names and Tarski’s
>> theorem.
>
> For quantifiers in CL, we had agreed that the following notation
>
> (forall ((x T)) S)
> (exists ((x T)) S)
>
> is syntactic sugar for
>
> (forall (x) (if (T x) S))
> (exists (x) (and (T x) S))
>
> I would assume that sentences with restricted quantifiers are
> resolved by expanding them to sentences without them.

But the exact syntactic details of this differ – in perhaps minor ways, but they do differ – between CL and IKL. For example, IKL allows for numerical quantifiers, while CL does not. (Both logics have exact EBNF syntactic specifications given in full detail in their respective formal description documents. Like anyone else, you can check the details yourself.)

Maybe. You are proposing a mechanism to support IKL reasoning as an extension to a resolution-style CL theorem-prover. I am sure this could handle some IKL entailments, but I am not convinced it can handle all of them, and I havn’t seen even the ghost of a completeness proof. And you need to show how to reduce IKL sentences to clausal form. But, yes, this might be a good way to get work started in this direction. After all, IKL is essentially CL with a new category of name added to the syntax, and unification is all about names.

BTW, if you check the translation of IKL into CL that I outline in an earlier email, I think you will find that the auxiliary conjuncts it generates, which encode the IKL truth conditions, would represent exactly the recursive calls that your method would need to make in order to establish unification of terms which include that-terms. This might be a good way to show completeness, in fact.

[John F Sowa]

Pat,

I'll start with your final two paragraphs:

> You are proposing a mechanism to support IKL reasoning as an
> extension to a resolution-style CL theorem-prover. I am sure
> this could handle some IKL entailments, but I am not convinced
> it can handle all of them, and I havn’t seen even the ghost of
> a completeness proof.

That is a clear statement of the problem. As your examples
illustrate, the critical issues occur in unifying expressions
that contain a that-term -- or a name had been or is being
unified with some part of the sentence S in a that-term.

For concreteness, I happened to mention a resolution theorem
prover since it's commonly used. But it's irrelevant whether you
use resolution or Gentzen-style natural deduction or any other
proof procedure. Your examples illustrate the issues that occur
during when unifying expressions that contain that-terms.

1. For every theorem-proving method, unification of terms is required.

2. The that-term of IKL creates issues that must be addressed
during unification. Other rules of inference re not affected.

3. Unification of that-terms can occur in three cases:

a) Two that-clauses, (that S1) and (that S2), are being unified.
Iff f4(S1) and f4(S2) can be unified to a sentence C, the
unification succeeds with the result (that C).

b) A sentence S1 is being unified to (that S2). Iff f4(S1)
and f4(S2) can be unified to a sentence C, the unification
succeeds with the result C.

c) A name p, which has not previously been unified with any
value, is being unified to (that S). The unification
succeeds with p having the value (that S).

d) A name p has previously been unified with (that S), and p
is now being unified with some expression X. The unification
with X succeeds only according to one of the cases
a, b, or c above.

> BTW, if you check the translation of IKL into CL that I outline
> in an earlier email, I think you will find that the auxiliary
> conjuncts it generates, which encode the IKL truth conditions,
> would represent exactly the recursive calls that your method would
> need to make in order to establish unification of terms which
> include that-terms. This might be a good way to show completeness,
> in fact.

That's a good suggestion. I have some other pressing issues that
I need to finish in the next two weeks. But I'll do that later this
month. I doubt that Till Mossakowski has been reading these email
messages, but I'd also ask Till to check the results if and when
I gather and format all these notes in a systematic form.

Re propositions: For over 2000 years, logicians have been saying
that a proposition is either true or false. To use different
terminology would create more confusion than enlightenment.

> I repeat, propositions do not have truth values. Sentences have
> truth values; propositions are zero-adic relations.

Since the word 'proposition' is not a syntactic category in
CL, we have been saying "A proposition is a 0-adic relation."
But note the implication of using the word 'is':

The extension of an N-adic relation R is the set of N-tuples for
which (R x1, ..., xN) is true.

For a 0-adic relation P, all we have is an empty tuple () for
which (P) is true -- or nothing if (P) is false.

To simplify terminology, I recommend that we say "A proposition
is *represented by* a 0-adic relation." Then we can define the
sentence "A proposition p is true" iff p is represented by a
0-adic relation P such that the sentence (P) is true.

> For example, IKL allows for numerical quantifiers, while
> CL does not.

That's a separate issue that doesn't create any serious problems.
I'm happy to include them.

John

[Pat Hayes]

On Oct 2, 2017, at 3:33 PM, John F Sowa <so...@bestweb.net> wrote:

Pat,

I'll start with your final two paragraphs:

You are proposing a mechanism to support IKL reasoning as an
extension to a resolution-style CL theorem-prover. I am sure
this could handle some IKL entailments, but I am not convinced
it can handle all of them, and I havn’t seen even the ghost of
a completeness proof.

That is a clear statement of the problem.  As your examples
illustrate, the critical issues occur in unifying expressions
that contain a that-term -- or a name had been or is being
unified with some part of the sentence S in a that-term.

Well, that issue (how to unify expressions containing the new IKL syntax) certainly arises, but I am not persuaded that this is the *only* issue that arises, which you seem to be assuming without any argument. 

For concreteness, I happened to mention a resolution theorem
prover since it's commonly used.  But it's irrelevant whether you
use resolution or Gentzen-style natural deduction or any other
proof procedure.

A Gentzen or ND inference sytem would not use unification, so I don’t think the issues would be exactly similar in those cases.

 Your examples illustrate the issues that occur
during when unifying expressions that contain that-terms.

Some of the issues :-) I am sure there will be more. 

It might be a good idea, if this line of thought is going to be pursued, to go back to the root definition of mg common instance, and apply it to instantiation of (that ..)-terms. They are much more complicated than anything in a normal first-order syntax. In many respects they are more similar to lambda expressions in a higher-order logic in that they may contain inner bound variables.

1. For every theorem-proving method, unification of terms is required.

2. The that-term of IKL creates issues that must be addressed
   during unification.  Other rules of inference re not affected.

How do you know this? 

3. Unification of that-terms can occur in three cases:

   a) Two that-clauses, (that S1) and (that S2), are being unified.
      Iff f4(S1) and f4(S2) can be unified

What does it mean to unify *sentences*? The usual algorithm only unifies terms with no bound names. 

OK, let me concede on this. Yes, you can say that a proposition *has* a truth value (in a given interpretation, of course). But be careful: a sentence also “has" a truth value, but the sentence *denotes* the truth value, while the proposition name denotes an individual (which is associated with a truth value in a special way, but is conceptually and semantically distinct from that truth value.) It is important to keep the distinction between expressions which denote propositions, and those which denote truth values, very clear. From the “IKL guide”: 

'It is important to distinguish between a proposition name and the sentence it contains. Although they 'say the same thing' in an intuitive sense, one cannot write a proposition name in place of a sentence, or vice versa, since they play distinct syntactic and semantic roles in the IKL logic. Writing a sentence asserts it to be true, but a proposition name simply refers to the proposition, and does not assert anything about it. ’

Since the word 'proposition' is not a syntactic category in
CL, we have been saying "A proposition is a 0-adic relation."
But note the implication of using the word 'is':

The extension of an N-adic relation R is the set of N-tuples for
which (R x1, ..., xN) is true.

For a 0-adic relation P, all we have is an empty tuple () for
which (P) is true -- or nothing if (P) is false.

To simplify terminology, I recommend that we say

I recommend that we stick to the terminology which we have carefully (and somewhat painfully) worked out to keep these distinctions sharp and intuitive. In IKL, a ‘proposition name’ IS a special syntactic construct of the form (that S) where S is a sentence, and it DENOTES a proposition, which IS a zero-adic relation (and therefore yields a truth-function when applied to no arguments, yes :-). There is no extra relation of ‘representing’ between the denotation of a proposition name and something else (what??) called a proposition; and if we talk that way, we will only create needless confusion, because it sounds like there are three things where there are only two. 

"A proposition
is *represented by* a 0-adic relation."  Then we can define the
sentence "A proposition p is true" iff p is represented by a
0-adic relation P such that the sentence (P) is true.

For example, IKL allows for numerical quantifiers, while
CL does not.

That's a separate issue that doesn't create any serious problems.
I'm happy to include them.

They certainly make theorem-proving more complicated. And if you want to claim all of IKL, you also need to show how to deal with indirect naming (https://www.ihmc.us/users/phayes/IKL/GUIDE/GUIDE.html#IndirectNames) although my intuition is that this might not be particularly hard to do, as character strings are very rigid when it comes to unification. 

[Ken Baclawski]

The regular Ontology Summit 2018 planning sessions will continue tomorrow,  Wednesday, October 4.  This session will feature David Whitten who will be discussing
"Contexts for Medical Decision Making".  You are cordially invited to attend and participate.

The session will be held on Wednesday, October 4, 2017 at Noon Eastern Time.
The meeting page is http://bit.ly/2fONsxx

The Video Conference URL is https://bluejeans.com/703588230
The chat room is http://webconf.soaphub.org/conf/room/ontology_summit_2018

[Pat Hayes]

On Sep 29, 2017, at 8:15 PM, Douglas Miles <logi...@gmail.com> wrote:

On Fri, Sep 29, 2017 at 3:22 PM, Pat Hayes <pha...@ihmc.us> wrote:

Hi Douglas

Um…IKL isn’t OWL; there are no assigned range or domain restrictions. IKL is an extension of CLIF, and part of the design philosophy of CLIF was to be as ‘permissive’ as possible,

​That is good, I like that​

 

perhaps to an extreme degree (we refer to it informally as ‘wild west syntax’). So any name can be used as a constant, a relation or a function, with any number of arguments, and can be applied to anything, including by the way itself, or to nothing at all, ie no arguments. So expressions like this are legal in CLIF, and therefore in IKL:

​(R (R R))   ie the property R is true of the result of applying the function R to the individual R.​

(R (R))   the property R is true of the result of applying the function R to nothing. 

Because of this, it does not really make sense, in IKL, to ask if something *is* a property or a relation or a function: the answer is always "yes, or no if you prefer." It does however make sense to ask, of any particular occurrence of a name inside an expression, how that name is being used there: is it denoting a function, or relation, or… etc.., because that can be determined from its position in the syntax. So in the first example above, the expression is at the top level of a text, so it must be a sentence, so it must be an atomic sentence (no connectives or quantifiers in first position), so that first R must be denoting a relation, with (check it) one argument. That argument must be a term, so the second R must be denoting a function of one argument, so that third R must be interpreted as an individual name.  

But in any case, the (that S) construction is a new piece of syntax, not even meaningful in a conventional logic. (DON'T think of it as a function ’that’ applied to an argument! It's a completely different entity, it just looks similar because IKL syntax is LISPish and uses parentheses for everything.) It is defined in IKL to be a *name* of a special kind, which denotes some thing which, when used as a zero-adic relation, ie when used in a an atomic sentence of the form (<name>) – which is IKL’s understanding of what a proposition is – will have the same truth-value as S. That is, IKL requires S and ( (that S) ) – both sentences – always have the same truthvalue. 

​Is see so 'that' would even be a disambiguator if I wanted to say:

The property R is true of the Proposition: "property R with an argument of the individual R.​" 

​​(R (that (R R)))    ;; No function in this case

Correct. But….

​

If you feel like your head is exploding, all I can tell you is that you are not alone, but that it is possible to get used to IKL after a while (and when you do, it is wonderfully expressive and natural). For more attempts to give an intuitive explanation of the (that S) idea and IKL in general, try looking at one of these, if you have the time:

​

Not to try to make it over complex:

​​(R ((that (R R)))) 

;; The property R is true of the "logical truth" of the Proposition: "property R with an argument of the individual R.​“  ?

Nope. Sorry :-) This is illegal because a sentence ( such as ((that (R R))) ) denotes a truthvalue, and truthvalues themselves are not objects in the logical universe. But you can do things like this, which defines a function on propositions corresponding to the conjunction truth function on truthvalues:

(forall (p q)(iff ((that (AND p q))) (and ((that p))((that q)) )))

and similarly for NOT, OR, etc., so you can ‘mirror’ the connectives in functions-applied-to-propositions language. Then you can say things like 

((AND Human Irish) Pat_Hayes)

In fact, this is exactly how we mapped description-logic style syntax into IKL in IKRIS, with things like 

((RESTRICT ParentOf Human) Pat) 

being the IKL translation of the OWL-ish assertion that Pat is in the restriction class of ParentOf to the class Human, which in IKL is a function from two properties of adicity 2 and 1 to a third property with adicity 1. Full details in the IKL guide. 

https://www.slideshare.net/PatHayes/ikl-survey

https://www.slideshare.net/PatHayes/ikl-presentation-for-ontolog

​​Side 14 is an interesting treat.

so the bare 'p' in all those cases is   (= p  (that (p)))   ?

Yes, that equation is true. I hadn’t even thought of that one :-)

 

https://www.ihmc.us/users/phayes/ikl/guide/guide.html#propositionNames

​IKL is very powerful and so far nothing that I dislike.

I missed in my readings how to access access a sentence arg using an index...

I'd like to define the 'argN'

(argN TERM N FORMULA) 




To means that TERM occurs in the Nth argument-position within FORMULA. 

Hmm. I don’t think this is possible (in IKL). The propositions aren’t syntactic objects, so functions on them aren’t going to work: and sentences themselves are not objects in the IKL semantics, so you can’t really talk about things like argument positions. And its important to not think of ‘that’ as a *function* from the sentence syntax to the proposition. The S inside a (that S) proposition name isn’t being quoted: it is treated by the IKL semantics just like any other sentence. (This, BTW, is why its OK to quantify into that-terms, which  wouldnt really make sense if the inner S were being quoted.) 

For example:

    (argN Dog 1 (that (subclass  Dog Mammal)))  ;; would be true.

Here is a candidate guess I have:

;; arg1

(forall (rel term sentence rest)

   (iff (argN term 1 (that (r term @rest)))

   (rel term @rest)))

;; arg2

(forall (rel term sentence rest)

   (iff (argN term 2 (that (r ? term @rest)))

   (rel ? term @rest)))

Is this correct?

I see what you are wanting to do (although sequences are indicated by the prefix … in IKL rather than @ as in KIF :-) but it won’t work because it doesn't instantiate correctly. The second half of your iff’s here are just assertions of the (rel … ) expression, so they just say that it is true, but you are using them as a kind of display of the syntactic form. Why would the first term being what it is depend on the *truth* of the expression it occurs in? But also, you can change the form of that term using equality. For example, suppose IKL knows enough about arithmetic to know that  (= (plus 9 8) 17); then it would follow from (Rl 17 3) that (argN (plus 9 8) 1 (that (R 17 3))). Do you see the problem? IKL is, at bottom, a conventional FO logic which talks about things, and refers to them using terms. It doesn’t talk about the syntactic form of the terms themselves. 

Pat

[Pat Hayes]

Whoa, just realized that I made a mistake in this response, see below at ****:

On Oct 3, 2017, at 6:43 PM, Pat Hayes <pha...@ihmc.us> wrote:

On Sep 29, 2017, at 8:15 PM, Douglas Miles <logi...@gmail.com> wrote:

On Fri, Sep 29, 2017 at 3:22 PM, Pat Hayes <pha...@ihmc.us> wrote:

Hi Douglas

Um…IKL isn’t OWL; there are no assigned range or domain restrictions. IKL is an extension of CLIF, and part of the design philosophy of CLIF was to be as ‘permissive’ as possible,

​That is good, I like that​

 

perhaps to an extreme degree (we refer to it informally as ‘wild west syntax’). So any name can be used as a constant, a relation or a function, with any number of arguments, and can be applied to anything, including by the way itself, or to nothing at all, ie no arguments. So expressions like this are legal in CLIF, and therefore in IKL:

​(R (R R))   ie the property R is true of the result of applying the function R to the individual R.​

(R (R))   the property R is true of the result of applying the function R to nothing. 

Because of this, it does not really make sense, in IKL, to ask if something *is* a property or a relation or a function: the answer is always "yes, or no if you prefer." It does however make sense to ask, of any particular occurrence of a name inside an expression, how that name is being used there: is it denoting a function, or relation, or… etc.., because that can be determined from its position in the syntax. So in the first example above, the expression is at the top level of a text, so it must be a sentence, so it must be an atomic sentence (no connectives or quantifiers in first position), so that first R must be denoting a relation, with (check it) one argument. That argument must be a term, so the second R must be denoting a function of one argument, so that third R must be interpreted as an individual name.  

But in any case, the (that S) construction is a new piece of syntax, not even meaningful in a conventional logic. (DON'T think of it as a function ’that’ applied to an argument! It's a completely different entity, it just looks similar because IKL syntax is LISPish and uses parentheses for everything.) It is defined in IKL to be a *name* of a special kind, which denotes some thing which, when used as a zero-adic relation, ie when used in a an atomic sentence of the form (<name>) – which is IKL’s understanding of what a proposition is – will have the same truth-value as S. That is, IKL requires S and ( (that S) ) – both sentences – always have the same truthvalue. 

​Is see so 'that' would even be a disambiguator if I wanted to say:

The property R is true of the Proposition: "property R with an argument of the individual R.​" 

​​(R (that (R R)))    ;; No function in this case

Correct. But….

​

If you feel like your head is exploding, all I can tell you is that you are not alone, but that it is possible to get used to IKL after a while (and when you do, it is wonderfully expressive and natural). For more attempts to give an intuitive explanation of the (that S) idea and IKL in general, try looking at one of these, if you have the time:

​

Not to try to make it over complex:

​​(R ((that (R R)))) 

;; The property R is true of the "logical truth" of the Proposition: "property R with an argument of the individual R.​“  ?

Nope. Sorry :-) This is illegal because a sentence ( such as ((that (R R))) ) denotes a truthvalue, and truthvalues themselves are not objects in the logical universe. But you can do things like this, which defines a function on propositions corresponding to the conjunction truth function on truthvalues:

(forall (p q)(iff ((that (AND p q))) (and ((that p))((that q)) )))

and similarly for NOT, OR, etc., so you can ‘mirror’ the connectives in functions-applied-to-propositions language.

****  Sorry, the rest of this is misleading. It is all true, and you can do that stuff, but that (below) is rather different from this (above). Sorry about the confusion. What this (above) is about is mirroring the connectives by functions on propositions. What that (below) is about is mirroring description logics by functions on relations. Not the same thing. You can do that (below) in CL, you don't need the IKL (that…) name machinery.

So, bottom line, both ideas are kosher and work, but they are different ideas. 

****

[Douglas Miles]

On Tue, Oct 3, 2017 at 4:43 PM, Pat Hayes <pha...@ihmc.us> wrote:

On Sep 29, 2017, at 8:15 PM, Douglas Miles <logi...@gmail.com> wrote:

​

​IKL is very powerful and so far nothing that I dislike.

I missed in my readings how to access access a sentence arg using an index...

I'd like to define the 'argN'

(argN TERM N FORMULA) 




To means that TERM occurs in the Nth argument-position within FORMULA. 

Hmm. I don’t think this is possible (in IKL). 

​... <snip> ..​

The second half of your iff’s here are just assertions of the (rel … ) expression, so they just say that it is true, but you are using them as a kind of display of the syntactic form. Why would the first term being what it is depend on the *truth* of the expression it occurs in? 

​Yeah that was a mistake,  the truth value of  (rel ? term @rest) should not have come into ​play!

My train of thought would have made more sense if I had tried to write instead

; EXHIBIT 1

(forall (t s)

 (iff ​

    (argN term 1 (that s))

    (= (that s) (that (? term  ...?))) ​)

(forall (t s)

 (iff ​

    (argN term  2 (that s))

    (= (that s) (that (? ? term   ...?))) ​)

It may still not work ...  but bare with me...

The S inside a (that S) proposition name isn’t being quoted: it is treated by the IKL semantics just like any other sentence. (This, BTW, is why its OK to quantify into that-terms, which  wouldnt really make sense if the inner S were being quoted.) 

So my in my KLIFIKL above, I am quantifying (ok 'grabbing') into the 'term' enclosed in (that ...) 

Thus later I might write:

; EXHIBIT 2

(forall (someone s)

  (if 

   (and (ist (MindOf DMiles) (that s))

           (argN someone 2 (that s) )

  (knowsOf DMiles someone))

Here, 's

omeone

​' was 

the 'logical thing'

​..​

 and not the syntactic mention of object (syntactic object

​ 

would not be very useful in (knowsOf ...) anyways)

​

​So in what ways is EXHIBIT 2 dissimilar to EXHIBIT 3?

; EXHIBIT 3

(forall (someone s)

  (if 

    (ist (MindOf DMiles) (that (loves DMiles someone)))

​  ​

  (knowsOf DMiles someone))

​)​

​

 

But also, you can change the form of that term using equality. For example, suppose IKL knows enough about arithmetic to know that  (= (plus 9 8) 17); then it would follow from

​

 (Rl 17 3) 

​

that

​

(argN (plus 9 8) 1 (that (R 17 3)))

​

.

​Oops,  yes I was intending on​

​; EXHIBIT 4​

​(forall (whatnot)

  ​(iff​

      ​(argN (plus 9 8) 1 (that (R whatnot  3)))​

​      (= whatnot 17))​

​(forall (whatnot )

  ​(iff​

      ​(argN (plus 9 whatnot) 1 (that (R 17 3)))​

​      (= whatnot 8))​

To be considered true due to the fact that EXHIBIT 1 is asserted

 

Do you see the problem?

Maybe, though maybe I can sort of see it if it was explained why this is not true:

(= (that (age DMiles 52))(that (age DMiles (plus 50 2)))

 

IKL is, at bottom, a conventional FO logic which talks about things, and refers to them using terms. It doesn’t talk about the syntactic form of the terms themselves. 

Being the case I should expect that: 

(ask (= (that (age DMiles ?number))(that (age DMiles (plus 50 2))))

?number = 52

And *not* bound to "(plus 50 2)" As this was the syntax I typed but "meant" 52?

- Douglas

[Douglas Miles]

​​Oh I do see how it looks like i am using (that .. )   as an "escape quote"​ing function in

​

(forall (

​

term

​

s)

 (iff ​

    (argN term 1 (that s))

    (= (that s) (that (? term  ...?))) ​)

Yet, had I not been introduced to the syntax operator called 'that' I might have written:

​(forall (term s)

 (iff ​

    (argN term 1 s)

    (= s (? term  ...?))) ​

Or even

​(forall (t s)

    (argN term 1 (? term  ...?)))

[John F Sowa]

On 10/2/2017 8:52 PM, Pat Hayes wrote:
> A Gentzen or ND inference system would not use unification, so

> I don’t think the issues would be exactly similar in those cases.

Gentzen invented two proof procedures: clause form and natural
deduction. Both methods involve finding some functional term t
to substitute for some variable x. For the rules of ND, see the
attached gentzen.gif. Note the two pairs of quantifier rules.

Alan Robinson started with Gentzen's clause form and developed
algorithms based on (a) a method called resolution for
simplifying the Boolean operations and (b) a method called
unification for finding a suitable term t to substitute for
some variable x.

Note: Gentzen's rules just say "substitute some t for x", but
they don't specify any method for finding a suitable t. What
Robinson invented was an algorithm for finding some t that
unifies two sentences. Any version of FOL could use it.

Basic point: All the issues concerning that-terms arise during
the substitutions. The Boolean rules (in any proof procedure)
have no effect on anything inside a sentence (such as 'that').

> What does it mean to unify *sentences*? The usual algorithm only
> unifies terms with no bound names.

I'm sorry. In one of the examples I was working on, I was trying
to unify a term (that S) with a sentence (x). But what I should
have done is to unify (that S) with x to get ((that S)), which
is then evaluated to S.

I'll delete that mistake. The result will actually be simpler.

John

[Douglas Miles]

On Mon, Oct 2, 2017 at 5:52 PM, Pat Hayes <pha...@ihmc.us> wrote:

​To John>​

What does it mean to unify *sentences*? The usual algorithm only unifies terms with no bound names. 

Well my big question is if this

    

(forall (?number)

    (if

      ​(= (that (age DMiles ?number))(that (age DMiles 52)))​

​     (age SMartins ?number))​

Should make  this

(age SMartins 52)

​True.

-Douglas​

[John F Sowa]

On 10/4/2017 10:30 AM, Douglas Miles wrote:
> Well my big question is if this
> (forall (?number)
>     (if
>       ​(= (that (age DMiles ?number))(that (age DMiles 52)))​
> ​     (age SMartins ?number))​
>
> Should make  this
>
> (age SMartins 52)
>
> ​True.

That is correct. My mistake was to try to unify a sentence
with a that-term. This example unifies two that-terms,
each of which contains a nested sentence:

(that (age DMiles ?number))
(that (age DMiles 52))

This unification works with 52 substituted for "?number".

But in CLIF and IKL, variables do not have an initial "?".
They do in KIF and CGIF, but not in CLIF.

John

[Douglas Miles]

On Wed, Oct 4, 2017 at 8:42 AM, John F Sowa <so...@bestweb.net> wrote:

On 10/4/2017 10:30 AM, Douglas Miles wrote:

Well my big question is if this
(forall (?number)
     (if
       ​(= (that (age DMiles ?number))(that (age DMiles 52)))​
​     (age SMartins ?number))​

Should make  this

(age SMartins 52)

​True.

That is correct.

​Excellent!​

 

  My mistake was to try to unify a sentence
with a that-term.   This example unifies two that-terms,
each of which contains a nested sentence:

   (that (age DMiles ?number))
   (that (age DMiles 52))

This unification works with 52 substituted for "?number".

But in CLIF and IKL, variables do not have an initial "?".
They do in KIF and CGIF, but not in CLIF.

Do I understand correctly that "?" may be treated as normal letter in IKL/CLIF ?

(forall (?var)​

​  (if

     (?qu​estion joe ?var)

     (wantsAnswerTo joe ?var)))

So that there is only one variable here "?var "  ?  

- Douglas

[David Whitten]

My slides are attached

--
All contributions to this forum by its members are made under an open content license, open publication license, open source or free software license. Unless otherwise specified, all Ontolog Forum content shall be subject to the Creative Commons CC-BY-SA 4.0 License or its successors.
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-forum+unsubscribe@googlegroups.com.

[Ken Baclawski]

When you get a chance, could you convert your slides to pdf?  There is no hurry about this.

Thanks,

-- Ken

[Pat Hayes]

That is a very interesting example! 

Actually I don’t know if it is true or not offhand, because the basic IKL model theory doesn’t give exact conditions for the equality (identity) of propositions. So it would all depend on John’s transformations on sentences, and I’m not sure if they take account of instantiation. 

John: will any of your equivalences map the atomic sentences ‘(age DMiles ?number)’ and ‘(age DMiles 52)’ into one another? Doesn’t seem to me that they do. (??) But if not, how could those two propositions, in the above antecedent, ever get to be equal? IKL quantifiers aren’t substitutional, remember :-)

I have CCd Chris M on this, as it raises a really interesting issue for IKL (which as far as I recall, we never seriously considered before.)

Pat

-Douglas​

[Douglas Miles]

On Oct 4, 2017, at 3:32 PM, Pat Hayes <pha...@ihmc.us> wrote:

On Oct 4, 2017, at 9:30 AM, Douglas Miles <logi...@gmail.com> wrote:

On Mon, Oct 2, 2017 at 5:52 PM, Pat Hayes <pha...@ihmc.us> wrote:

​To John>​

What does it mean to unify *sentences*? The usual algorithm only unifies terms with no bound names. 

Well my big question is if this

    

(forall (?number)

    (if

      ​(= (that (age DMiles ?number))(that (age DMiles 52)))​

​     (age SMartins ?number))​

Should make  this

(age SMartins 52)

​True.

That is a very interesting example! 

Actually I don’t know if it is true or not offhand, because the basic IKL model theory doesn’t give exact conditions for the equality (identity) of propositions. So it would all depend on John’s transformations on sentences, and I’m not sure if they take account of instantiation.

John: will any of your equivalences map the atomic sentences ‘(age DMiles ?number)’ and ‘(age DMiles 52)’ into one another?

​​Well if I understand what you are saying, it is that it is more along the lines 

  that this would be true: 

   (= (that (age DMiles ?number))

          (that (forall (?number) (age DMiles ?number))))  

and this to:

   (= (that (age DMiles ?foo))

          (that  (age DMiles ?bar)))

 

Doesn’t seem to me that they do. (??) But if not, how could those two propositions, in the above antecedent, ever get to be equal? IKL quantifiers aren’t substitutional, remember :-)

 

​Will be nice to hear John's ideas.​

 

I have CCd Chris M on this, as it raises a really interesting issue for IKL (which as far as I recall, we never seriously considered before.)

​On Wed, Oct 4, 2017 at 1:56 PM, Christopher Menzel <cme...@tamu.edu> wrote:
There’s no way IKL can handle that inference at the moment. You need fine-grainedness axioms for propositions, e.g., in this case:
(if (= (that (R a)) (that (S b))) (and (= R S) (= a b)))

​Well if it is expected by users to be able to axiomatize that way, then no problem.  

 

And ensuring those axioms are valid requires some sort of algebraic semantics for propositions. See, e.g., the work of George Bealer, Quality and Concept, in this regard.

​Thank you for the reference​.

Actually funny you should mention since I had planned on having users write rules to explain what sentences the system generates (talked about in next response). That in itself is the same process (in reverse).

Either way they will probably want (if confused) to expand the proof nodes of whichever predicate playing unify sentence and see each step.

​

Pat

I hoping that IKL supports this so when I show proofs of why the "system deduced" whatever I do, what they see is valid IKL.

What I am doing is allowing assertions from the user that sort of 'idiomatically' constructs later sentences (via forward chaining) that get added to their Planner Domain Definition Language (PDDL) Microtheory.   When the user is scratching their heads debugging, I want them to be looking at the proofs returned (for each forward assertion) that got considered to be valid IKL (or by proxy, CLIF).

- Douglas

​Ps.

If technically that is asking for too much girth from plain ol '=', (to be everyone's favorite conceptual meaning of equals)  I suppose I can claim the system is using a "code implemented [external] predicate" called   sentence-unify?​

[John F Sowa]

Pat, Chris, and Douglas,

The equality of propositions is a topic that we discussed during
the IKRIS project in 2005. At that time, I took an excerpt from
an earlier article that defined a proposition as an equivalence
class of sentences. And I posted it as a short article at
http://jfsowa.com/logic/proposit.pdf

And at that time, Pat and Chris seemed to like the idea (at least
to the stage of not disagreeing). I thought that the issue had been
settled. But Pat recently raised the issue that a proposition is
not an equivalence class, but a 0-adic relation.

But I consider that a trivial matter of terminology. We can
*define* a proposition as a 0-adic relation that may be specified
by a that-term. And we can *define* equality of two that-terms
iff their sentences map to the canonical sentence of the same
equivalence class.

Assuming those definitions and using the f4 function specified
in proposit.pdf, I would say that the following two that-terms
are equal:

(that (age DMiles number))
(that (age DMiles 52))

The proof takes three steps:

1. Map each sentence to its canonical sentence by f4:

f4 of (age DMiles number) is (age DMiles number).
f4 of (age DMiles 52) is (age DMiles 52)

2. Applying the unification algorithm to both sentence produces
(age DMiles 52).

3. Therefore, (= (that (age DMiles 52)) (that (age DMiles 52)))
is true.

These steps depend on two assumptions: (1) We use the methods
of proposit.pdf for determining the canonical sentence of the
equivalence class; and (2) we treat the 'that' operator as
a special kind of function that allows unification of its
argument (some sentence S) during a proof.

I admit that CL does not support this kind of unification,
but IKL with this way of treating that-terms seems to work.

Since the f4 mapping preserves truth (as determined by 'iff'),
it can be computed in (n long n) time, it preserves vocabulary
(same names), and it preserves structure (mapping to the same
Boolean form with just the operators 'and' and 'not'), it seems
to be very close to the intuitive notion of "same meaning".

Can anybody suggest a method that is better by any other measure?

John

[Pat Hayes]

On Oct 4, 2017, at 7:03 PM, Douglas Miles <logi...@gmail.com> wrote:

 

On Oct 4, 2017, at 3:32 PM, Pat Hayes <pha...@ihmc.us> wrote:

On Oct 4, 2017, at 9:30 AM, Douglas Miles <logi...@gmail.com> wrote:

On Mon, Oct 2, 2017 at 5:52 PM, Pat Hayes <pha...@ihmc.us> wrote:

​To John>​

What does it mean to unify *sentences*? The usual algorithm only unifies terms with no bound names. 

Well my big question is if this

    

(forall (?number)

    (if

      ​(= (that (age DMiles ?number))(that (age DMiles 52)))​

​     (age SMartins ?number))​

Should make  this

(age SMartins 52)

​True.

That is a very interesting example! 

Actually I don’t know if it is true or not offhand, because the basic IKL model theory doesn’t give exact conditions for the equality (identity) of propositions. So it would all depend on John’s transformations on sentences, and I’m not sure if they take account of instantiation.

John: will any of your equivalences map the atomic sentences ‘(age DMiles ?number)’ and ‘(age DMiles 52)’ into one another?

​​Well if I understand what you are saying, it is that it is more along the lines 

  that this would be true: 

   (= (that (age DMiles ?number))

          (that (forall (?number) (age DMiles ?number))))  

That is surely not true. The second proposition says that you are *every* age. 

No, the issue is that in order to make the argument you gave in your example, one has to reason along the lines: if the name ?n denotes 52, then the proposition name '(that (R ?n))' denotes the *same exact proposition* as (that (R 52)). And that ‘same exact proposition’ is where IKL stumbles, I think. But maybe John can find a way to rescue it :-)

and this to:

   (= (that (age DMiles ?foo))

          (that  (age DMiles ?bar)))

 

Doesn’t seem to me that they do. (??) But if not, how could those two propositions, in the above antecedent, ever get to be equal? IKL quantifiers aren’t substitutional, remember :-)

 

​Will be nice to hear John's ideas.​

 

I have CCd Chris M on this, as it raises a really interesting issue for IKL (which as far as I recall, we never seriously considered before.)

​On Wed, Oct 4, 2017 at 1:56 PM, Christopher Menzel <cme...@tamu.edu> wrote:
There’s no way IKL can handle that inference at the moment. You need fine-grainedness axioms for propositions, e.g., in this case:
(if (= (that (R a)) (that (S b))) (and (= R S) (= a b)))

​Well if it is expected by users to be able to axiomatize that way, then no problem. 

I think there is still a problem. In order to write the axioms you need, you will likely need to be able to quantify over forms of expressions, and that isn’t something that IKL can do. In fact, I don’t know of any logic that can do this (quantify over its own expressions).

And ensuring those axioms are valid requires some sort of algebraic semantics for propositions. See, e.g., the work of George Bealer, Quality and Concept, in this regard.

​Thank you for the reference​.

Actually funny you should mention since I had planned on having users write rules to explain what sentences the system generates (talked about in next response). That in itself is the same process (in reverse).

Either way they will probably want (if confused) to expand the proof nodes of whichever predicate playing unify sentence and see each step.

​

Pat

I hoping that IKL supports this so when I show proofs of why the "system deduced" whatever I do, what they see is valid IKL.

What I am doing is allowing assertions from the user that sort of 'idiomatically' constructs later sentences (via forward chaining) that get added to their Planner Domain Definition Language (PDDL) Microtheory.   When the user is scratching their heads debugging, I want them to be looking at the proofs returned (for each forward assertion) that got considered to be valid IKL (or by proxy, CLIF).

Sounds like you want a way to display proofs, ie derivations. There are lots of ideas about that, and some of them have been implemented. See for example ftp://ftp.ksl.stanford.edu/pub/KSL_Reports/KSL-05-01.pdf. IKL isn’t particularly designed to talk about proofs. 

- Douglas

​Ps.

If technically that is asking for too much girth from plain ol '=', (to be everyone's favorite conceptual meaning of equals)  I suppose I can claim the system is using a "code implemented [external] predicate" called   sentence-unify?​

That might be safer, yes. Poor old ‘=‘ does get rather overloaded these days. If you later discover that you have just re-invented equality, you can always say so at that point: but my guess is that you will have hold of something else, in fact. 

Pat

[Pat Hayes]

> On Oct 4, 2017, at 9:51 PM, John F Sowa <so...@bestweb.net> wrote:
>
> Pat, Chris, and Douglas,
>
> The equality of propositions is a topic that we discussed during
> the IKRIS project in 2005. At that time, I took an excerpt from
> an earlier article that defined a proposition as an equivalence
> class of sentences. And I posted it as a short article at
> http://jfsowa.com/logic/proposit.pdf
>
> And at that time, Pat and Chris seemed to like the idea (at least
> to the stage of not disagreeing). I thought that the issue had been
> settled. But Pat recently raised the issue that a proposition is
> not an equivalence class, but a 0-adic relation.
>
> But I consider that a trivial matter of terminology. We can
> *define* a proposition as a 0-adic relation that may be specified
> by a that-term. And we can *define* equality of two that-terms
> iff their sentences map to the canonical sentence of the same
> equivalence class.

Yes, that is exactly my understanding of what we had agreed at IKRIS, and what is now written into the IKL specification documents. But on a strict interpretation of these rules, (that (R ?x)) and (that (R a)) would be distinct propositions.

>
> Assuming those definitions and using the f4 function specified
> in proposit.pdf, I would say that the following two that-terms
> are equal:
>
> (that (age DMiles number))
> (that (age DMiles 52))

Really? But these seem clearly to NOT be the same proposition, on their face.

>
> The proof takes three steps:
>
> 1. Map each sentence to its canonical sentence by f4:
>
> f4 of (age DMiles number) is (age DMiles number).
> f4 of (age DMiles 52) is (age DMiles 52)

Right. Being atomic sentences, the propositional tweaking can be ignored.

>
> 2. Applying the unification algorithm to both sentence

Whoa: where does f4 allow unification? And on what grounds do you allow the name ‘number’ to be unified with the numeral ’52’? But in any case, if you allow unifiability to decide equality, then many apparently different propositions will be called equal. For example (let me assume that some names are variables here to keep the example short): (R ?x b) and (R a ?y) are unifiable, but their mgu (R a b) is different from either of them. Seems to me that we have here three distinct propositions. Certainly, sentences containing these will be different in meaning, eg these are all very different sentences:

(forall (?x)(Q (that (R ?x b)) ?x))
(forall (?x)(Q (that (R a ?y)) ?x))
(forall (?x)(Q (that (R a b)) ?x))

> produces
> (age DMiles 52).
>
> 3. Therefore, (= (that (age DMiles 52)) (that (age DMiles 52)))
> is true.

This isn’t justified by what we agreed at IKRIS nor by normal intuitions. Having a common instance seems *much* weaker than identity.

>
> These steps depend on two assumptions: (1) We use the methods
> of proposit.pdf for determining the canonical sentence of the
> equivalence class; and (2) we treat the 'that' operator as
> a special kind of function that allows unification of its
> argument (some sentence S) during a proof.

We can certainly *use* unification on that-terms because names inside them behave normally, but that does not imply the equality you are assuming here.

>
> I admit that CL does not support this kind of unification,
> but IKL with this way of treating that-terms seems to work.
>
> Since the f4 mapping preserves truth (as determined by 'iff'),
> it can be computed in (n long n) time, it preserves vocabulary
> (same names), and it preserves structure (mapping to the same
> Boolean form with just the operators 'and' and 'not'), it seems
> to be very close to the intuitive notion of "same meaning”.

Sure, but that is all about normalizing the propositional form, eg mapping P&P to P, etc.. It says nothing about quantiifers or unification.

> Can anybody suggest a method that is better by any other measure?

I would like to get something that is simply correct, before we make judgements about which one is best :-)

To end on a posiitve note, would it make sense to introduce a notion of one proposition being an ‘instance' of another? At the very least, we might then be able to give a rational account of what it means to use unifiers on proposition names.

Pat

>
> John

[Douglas Miles]

Hi Pat,

On Thu, Oct 5, 2017 at 7:37 AM, Pat Hayes <pha...@ihmc.us> wrote:

On Oct 4, 2017, at 7:03 PM, Douglas Miles <logi...@gmail.com> wrote:

 

On Oct 4, 2017, at 3:32 PM, Pat Hayes <pha...@ihmc.us> wrote:

On Oct 4, 2017, at 9:30 AM, Douglas Miles <logi...@gmail.com> wrote:

On Mon, Oct 2, 2017 at 5:52 PM, Pat Hayes <pha...@ihmc.us> wrote:

​To John>​

What does it mean to unify *sentences*? The usual algorithm only unifies terms with no bound names. 

Well my big question is if this

    

(forall (?number)

    (if

      ​(= (that (age DMiles ?number))(that (age DMiles 52)))​

​     (age SMartins ?number))​

Should make  this

(age SMartins 52)

​True.

That is a very interesting example! 

Actually I don’t know if it is true or not offhand, because the basic IKL model theory doesn’t give exact conditions for the equality (identity) of propositions. So it would all depend on John’s transformations on sentences, and I’m not sure if they take account of instantiation.

John: will any of your equivalences map the atomic sentences ‘(age DMiles ?number)’ and ‘(age DMiles 52)’ into one another?

​​Well if I understand what you are saying, it is that it is more along the lines 

  that this would be true: 

   (= (that (age DMiles ?number))

          (that (forall (?number) (age DMiles ?number)))) 

That is surely not true. The second proposition says that you are *every* age. 

​​Oh I was going off the belief the first proposition having an ​unquantified variable (so default quantification) would make '?number' become universal.     So I miss assumed the difference was syntax only.    Then again,  a  "?" did make it a variable :)

​

 

No, the issue is that in order to make the argument you gave in your example, one has to reason along the lines: if the name ?n denotes 52, then the proposition name '(that (R ?n))' denotes the *same exact proposition* as (that (R 52)). And that ‘same exact proposition’ is where IKL stumbles, I think. But maybe John can find a way to rescue it :-)

​Yeah his email about propsit.pdf seemed to ​.

 

and this to:

   (= (that (age DMiles ?foo))

          (that  (age DMiles ?bar)))

 

Doesn’t seem to me that they do. (??) But if not, how could those two propositions, in the above antecedent, ever get to be equal? IKL quantifiers aren’t substitutional, remember :-)

 

​Will be nice to hear John's ideas.​

 

I have CCd Chris M on this, as it raises a really interesting issue for IKL (which as far as I recall, we never seriously considered before.)

​On Wed, Oct 4, 2017 at 1:56 PM, Christopher Menzel <cme...@tamu.edu> wrote:
There’s no way IKL can handle that inference at the moment. You need fine-grainedness axioms for propositions, e.g., in this case:
(if (= (that (R a)) (that (S b))) (and (= R S) (= a b)))

​Well if it is expected by users to be able to axiomatize that way, then no problem. 

I think there is still a problem. In order to write the axioms you need, you will likely need to be able to quantify over forms of expressions, and that isn’t something that IKL can do. In fact, I don’t know of any logic that can do this (quantify over its own expressions).

Some people would claim ​CycL does it thru quoting (I dislike using that term because it is way overloaded, this is not lisp quoting, or something I've heard called logical quoting, but different called "Cycorp quoting.")  I would not be surprised that you know as much, or more, about Cycorp's brand of quoting than I do.  But I think you are right because while Cyc is using CycLExpressions,  probably is not being a "logic" at that point.   I only bring it up as we may quantify (and make inferences about) over CycLExpressions.  But they no longer Propositions during that time.  Oh, also, we may quantify over CycAssertions  (which are no longer Expressions).  

 

And ensuring those axioms are valid requires some sort of algebraic semantics for propositions. See, e.g., the work of George Bealer, Quality and Concept, in this regard.

​Thank you for the reference​.

Actually funny you should mention since I had planned on having users write rules to explain what sentences the system generates (talked about in next response). That in itself is the same process (in reverse).

Either way they will probably want (if confused) to expand the proof nodes of whichever predicate playing unify sentence and see each step.

​

Pat

I hoping that IKL supports this so when I show proofs of why the "system deduced" whatever I do, what they see is valid IKL.

What I am doing is allowing assertions from the user that sort of 'idiomatically' constructs later sentences (via forward chaining) that get added to their Planner Domain Definition Language (PDDL) Microtheory.   When the user is scratching their heads debugging, I want them to be looking at the proofs returned (for each forward assertion) that got considered to be valid IKL (or by proxy, CLIF).

Sounds like you want a way to display proofs, ie derivations. There are lots of ideas about that, and some of them have been implemented. See for example ftp://ftp.ksl.stanford.edu/pub/KSL_Reports/KSL-05-01.pdf.

​

​Thank you.​

 

IKL isn’t particularly designed to talk about proofs. 

Well showing people the original language (be it IKL) would be embedded in the proofs

​

​-Douglas​

[Douglas Miles]

John, Chris and Pat,

​Pat, ​

​I believe John has expected that higher up " The proof takes three steps " it was given that 'number' had been  quantified somewhere as thus became a variable.   I assume, also, you two might have a history of teasing each other about CLIF dropping the "?" in front of variables.   Myself, I will probably get opposite flak since  I will undoubtedly continue to use "?" (and hopefully will not annoy John too much)  in front of variables and not mistakenly forget to quantify (like I did in my previous email where I expected you assume '?number' to be a variable).

 

But in any case, if you allow unifiability to decide equality, then many apparently different propositions will be called equal. For example (let me assume that some names are variables here to keep the example short): (R ?x b) and (R a ?y) are unifiable, but their mgu

​​

(R a b) is different from either of them. Seems to me that we have here three distinct propositions. Certainly, sentences containing these will be different in meaning, eg these are all very different sentences:

(forall (?x)(Q (that (R ?x b)) ?x))
(forall (?x)(Q (that (R a ?y)) ?x))
(forall (?x)(Q (that (R a b)) ?x))

> produces
>    (age DMiles 52).
>
> 3. Therefore, (= (that (age DMiles 52)) (that (age DMiles 52)))
>    is true.

This isn’t justified by what we agreed at IKRIS nor by normal intuitions. Having a common instance seems *much* weaker than identity.

>
> These steps depend on two assumptions:  (1) We use the methods
> of proposit.pdf for determining the canonical sentence of the
> equivalence class;

​

​​After I had read ​http://jfsowa.com/logic/proposit.pdf , the MTP part about  "Truth preserving"   I was thinking about with ist/2 ..  

it not be possible to create a temporary to comfirm  tmp-ctx 

Like:

1. ;; some sentence unifier ?
2. (forall (sent1 sent2)
3.  (exists (tmp-ctx)
4.   (if
5.    (and
6.     (subContextOf tmp-ctx LogicalEquivAxiomsMt)
7.     (iff
8.      (ist tmp-ctx sent1)
9.      (ist tmp-ctx sent2)))
10.   (sents-unify sent1 sent2))))

​Or​

1.  
2. ;; some sentence unifier ?
3. (forall (sent1 sent2)
4.  (exists (tmp-ctx)
5.   (if
6.    (and
7.     (subContextOf tmp-ctx LogicalEquivAxiomsMt)
8.     (ist tmp-ctx (iff sent1 sent2)))
9.   (sents-unify sent1 sent2))))

​

(the LogicalEquivAxiomsMt​​ maybe isn't necessary, but was thinking about Chris' thoughts and if implementing them I can isolate certain general truth axioms i need to that Microtheory)

​​

 

and (2) we treat the 'that' operator as
> a special kind of function that allows unification of its
> argument (some sentence S) during a proof.

We can certainly *use* unification on that-terms because names inside them behave normally, but that does not imply the equality you are assuming here. 

>
> I admit that CL does not support this kind of unification,
> but IKL with this way of treating that-terms seems to work.
>
> Since the f4 mapping preserves truth (as determined by 'iff'),
> it can be computed in (n long n) time, it preserves vocabulary
> (same names), and it preserves structure (mapping to the same
> Boolean form with just the operators 'and' and 'not'), it seems
> to be very close to the intuitive notion of "same meaning”.

Sure, but that is all about normalizing the propositional form, eg mapping P&P to P, etc.. It says nothing about quantiifers or unification.

> Can anybody suggest a method that is better by any other measure?

I would like to get something that is simply correct, before we make judgements about which one is best :-)

To end on a posiitve note, would it make sense to introduce a notion of one proposition being an ‘instance' of another? At the very least, we might then be able to give a rational account of what it means to use unifiers on proposition names.

That would cover unification ​if

​if

 

  "(forall (?x)(Q (that (R a b)) ?x))​"

was an instance of  ​

  "​(forall (?x)(Q (that (R a ?y)) ?x))" 

​- Douglas

 

Pat

>
> John
>
> --
> All contributions to this forum by its members are made under an open content license, open publication license, open source or free software license. Unless otherwise specified, all Ontolog Forum content shall be subject to the Creative Commons CC-BY-SA 4.0 License or its successors.
> --- You received this message because you are subscribed to the Google Groups "ontolog-forum" group.

> To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-forum+unsubscribe@googlegroups.com.

> For more options, visit https://groups.google.com/d/optout.
>

--
All contributions to this forum by its members are made under an open content license, open publication license, open source or free software license. Unless otherwise specified, all Ontolog Forum content shall be subject to the Creative Commons CC-BY-SA 4.0 License or its successors.
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-forum+unsubscribe@googlegroups.com.

[John F Sowa]

Pat and Douglas,

Re '?': That was the marker for variables in KIF. For CGIF,
I adopted it for names governed by a quantifier, and I kept it
when CLIF dropped it to avoid conflicts with other CG features.
I can go either way.

Pat
>> 2. Applying the unification algorithm to both sentences

>
> Whoa: where does f4 allow unification? And on what grounds do
> you allow the name ‘number’ to be unified with the numeral ’52’?

f4 never does a unification. It does the first step of converting
the S in each that-term to a canonical form. After that conversion,
a theorem prover for FOL with equality will try to unify both of
the canonical sentences to determine they might be the same.

For example, consider

(= (func DMiles number) (func Dmiles 52))

In this case, 'func' is the name of a ordinary function; 'DMiles'
and 'number' are ordinary names, and '52' is a special kind of
name that has a previously defined denotation.

During a proof, a theorem prover will attempt to unify the
term '(func DMiles number)' with '(func DMiles 52)'.

If the unification fails, this sentence is false.

If the unification succeeds, 'number' will be assigned the
value '52'. But it's possible that a later step of the
proof may cause a failure if there's an attempt to unify
'number' with something else.

Pat (using '?')

> these are all very different sentences:
>
> (forall (?x)(Q (that (R ?x b)) ?x))
> (forall (?x)(Q (that (R a ?y)) ?x))
> (forall (?x)(Q (that (R a b)) ?x))

That is true. But that point is irrelevant to anything above.
A theorem prover doesn't arbitrarily try to unify terms unless
there is some step in some proof that requires it.

>> 3. Therefore, (= (that (age DMiles 52)) (that (age DMiles 52)))
>> is true.
>
> This isn’t justified by what we agreed at IKRIS nor by normal
> intuitions. Having a common instance seems *much* weaker than identity.

I performed that operation in trying to answer a question by Douglas.

>> (forall (?number)
>> (if
>> ​(= (that (age DMiles ?number))(that (age DMiles 52)))​
>> ​ (age SMartins ?number))​
>>

>> Should make (age SMartins 52) ​True.

Douglas is asserting that the implication is true for every value
of ?number. Any value of ?number that would make the antecedent
false would guarantee that the implication is true. Therefore,
we need to check which value would make the antecedent true.

Therefore, I unified the two that-terms in the antecedent.
Unification works iff (= ?number 52). Any other value of
?number would make the antecedent false and the implication
would be true.

Since Douglas said that the implication is true for every value,
it must be true for (= ?number 52). Since that makes the antecedent
true, the consequent (age SMartins 52) must also be true.

John

[Pat Hayes]

> On Oct 5, 2017, at 10:10 PM, John F Sowa <so...@bestweb.net> wrote:
>
> Pat and Douglas,
>
> Re '?': That was the marker for variables in KIF. For CGIF,
> I adopted it for names governed by a quantifier, and I kept it
> when CLIF dropped it to avoid conflicts with other CG features.
> I can go either way.

OK, fair enough. But when (if) we ever start trying to speak with precision about IKL,we should follow the conventions strictly defined in the IKL specs, which do not give the ‘?’ marker any special status.

>>> 2. Applying the unification algorithm to both sentences
>>
>> Whoa: where does f4 allow unification? And on what grounds do
>> you allow the name ‘number’ to be unified with the numeral ’52’?
>
> f4 never does a unification. It does the first step of converting
> the S in each that-term to a canonical form.

It is not a ‘first step’. The criteria for identifying propositions (which you introduced and championed in the IKRIS work) says that (= (that S1)(that S2)) is true *exactly* when f4(S1) is identical to f4(S2). It does not provide for any ‘next step’.

> After that conversion,
> a theorem prover for FOL with equality will try to unify both of
> the canonical sentences to determine they might be the same.

On what grounds? As far as I can see, this step is not justified either by the IKL semantics or by your account of sentence normalization to determine propositional identity. Theorem provers should be built to do what is semantically correct, not be used as a criterion for that correctness.

>
> For example, consider
>
> (= (func DMiles number) (func Dmiles 52))
>
> In this case, 'func' is the name of a ordinary function; 'DMiles'
> and 'number' are ordinary names, and '52' is a special kind of
> name that has a previously defined denotation.
>
> During a proof, a theorem prover will attempt to unify the
> term '(func DMiles number)' with '(func DMiles 52)'.
>
> If the unification fails, this sentence is false.
>
> If the unification succeeds, 'number' will be assigned the
> value '52'. But it's possible that a later step of the
> proof may cause a failure if there's an attempt to unify
> 'number' with something else.
>
> Pat (using '?')
>> these are all very different sentences:
>> (forall (?x)(Q (that (R ?x b)) ?x))
>> (forall (?x)(Q (that (R a ?y)) ?x))
>> (forall (?x)(Q (that (R a b)) ?x))
>
> That is true. But that point is irrelevant to anything above.
> A theorem prover doesn't arbitrarily try to unify terms unless
> there is some step in some proof that requires it.

And we do not yet have a proof theory for IKL which is proven to be correct and complete wrt the IKL model theory.

>
>>> 3. Therefore, (= (that (age DMiles 52)) (that (age DMiles 52)))
>>> is true.
>> This isn’t justified by what we agreed at IKRIS nor by normal
>> intuitions. Having a common instance seems *much* weaker than identity.
>
> I performed that operation in trying to answer a question by Douglas.
>>> (forall (?number)
>>> (if
>>> ​(= (that (age DMiles ?number))(that (age DMiles 52)))​
>>> ​ (age SMartins ?number))​
>>>
>>> Should make (age SMartins 52) ​True.
>
> Douglas is asserting that the implication is true for every value
> of ?number. Any value of ?number that would make the antecedent
> false would guarantee that the implication is true. Therefore,
> we need to check which value would make the antecedent true.
>
> Therefore, I unified the two that-terms in the antecedent.

If these were normal terms, of course. But they aren’t: they are a special IKL proposition name. So by simply unifying them, you are begging the question. We do not (yet) have a theory of identity for propsitions which accounts for what happens when inner names are instantiated or bound to other values. Your own theory based on sentence transformations (your f4) does NOT do this. So this step is not yet justified by any theory: it is just a wild guess about what that as-yet-hypothetical theory will justify. Until that guess is solidified into some real semantic account, any talk about what theorem-provers will or won’t do is premature.

Pat

[Pat Hayes]

> On Oct 4, 2017, at 8:29 AM, John F Sowa <so...@bestweb.net> wrote:
>
> On 10/2/2017 8:52 PM, Pat Hayes wrote:
>> A Gentzen or ND inference system would not use unification, so
>> I don’t think the issues would be exactly similar in those cases.
>
> Gentzen invented two proof procedures: clause form and natural
> deduction. Both methods involve finding some functional term t
> to substitute for some variable x.

The ND and sequent proof systems simply allow proofs to use any legal instance. “Finding” is not an issue until one sets out to automate the search, at which point it is not practical to search through all possible terms.

> For the rules of ND, see the
> attached gentzen.gif. Note the two pairs of quantifier rules.

> Alan Robinson started with Gentzen's clause form and developed
> algorithms based on (a) a method called resolution for
> simplifying the Boolean operations and (b) a method called
> unification for finding a suitable term t to substitute for
> some variable x.
>
> Note: Gentzen's rules just say "substitute some t for x", but
> they don't specify any method for finding a suitable t.

Of course they don’t. They don’t specify how to find suitable sentences to apply the propositional rules to, either. Why would you expect that they would do either of these things? That is not what proof systems do. They define a space of possible proofs, but they do not tell you how to search it.

> What
> Robinson invented was an algorithm for finding some t that
> unifies two sentences.

Actually the (unique) most general unifier, which is why it works.

> Any version of FOL could use it.
>
> Basic point: All the issues concerning that-terms arise during
> the substitutions. The Boolean rules (in any proof procedure)
> have no effect on anything inside a sentence (such as 'that’).

But they may have effects on the sentences which are embedded inside the (that S) proposition names. None of those arise in conventional FOL, but they may have consequences in IKL.

Look, you may be correct about the effects being limited to instantiation, but you have not given any actual argument for this, and it needs to be shown to be true before we can rely on it. I have grave doubts about it, myself, but I am willing to be persuaded.

Pat

[John F Sowa]

On 10/6/2017 5:00 PM, Christopher Menzel wrote:
>> [Pat] In fact, I don’t know of any logic that can do this (quantify
>> over its own expressions).
>
> [CM] Perhaps not a *logic* per se but you know as well as anyone,
> Pat, that any system containing a bit of arithmetic can (in effect)
> quantify over its own expressions via the magic of Gödel coding.
> But there’s also no reason why you couldn’t develop a theory whose
> subject matter was explicitly (sans coding) its own syntax.

This may be a way to get a completeness proof: treat 'that' as
a function from sentences to propositions. It will require some
analysis and carefully written definitions. But if it can be done,
IKL simply becomes CL with a peculiar function named 'that'.

Pat

> we should follow the conventions strictly defined in the IKL specs,
> which do not give the ‘?’ marker any special status.

I agree.

>> [JFS] Therefore, I unified the two that-terms in the antecedent.
>
> [Pat] If these were normal terms, of course. But they aren’t: they

> are a special IKL proposition name. So by simply unifying them, you
> are begging the question. We do not (yet) have a theory of identity

> for propositions which accounts for what happens when inner names

> are instantiated or bound to other values.

Yes. It can only be justified if Chris's suggestion can be
developed and applied.

John

[Pat Hayes]

> On Oct 6, 2017, at 4:00 PM, Christopher Menzel <chris....@gmail.com> wrote:

>
> On Oct 5, 2017, at 9:37 AM, Pat Hayes <pha...@ihmc.us> wrote:
>>>> Well my big question is if this
>>>>
>>>> (forall (?number)
>>>> (if
>>>> ​(= (that (age DMiles ?number))(that (age DMiles 52)))​
>>>> ​ (age SMartins ?number))​
>>>>
>>>> Should make this
>>>>
>>>> (age SMartins 52)
>>>>
>>>> ​True.
>>>

>>> ​On Wed, Oct 4, 2017 at 1:56 PM, Christopher Menzel <cme...@tamu.edu> wrote:
>>> There’s no way IKL can handle that inference at the moment. You need fine-grainedness axioms for propositions, e.g., in this case:
>>> (if (= (that (R a)) (that (S b))) (and (= R S) (= a b)))
>>>
>>> ​Well if it is expected by users to be able to axiomatize that way, then no problem.
>>
>> I think there is still a problem. In order to write the axioms you need, you will likely need to be able to quantify over forms of expressions, and that isn’t something that IKL can do.
>

> No you won't. You simply need logical axioms that reflect the fine-grained structure of the propositions that the that-expressions denote.

OK, I stand corrected. (Of course :-). I should have said, to be able to quantify over things with the full algebraic structure of expressions, standing in a semantically sanctioned relationship to the actual expressions. (I wonder, is there an analogy to the Herbrand result, that one can construct such an algebra from the expressions themselves?)

> Thus, e.g., "(that (P a))" will denote the atomic proposition resulting from the predication of P of a (where predication is a semantic operation). “(that (not (and (P a) (Q b))))” will denote the negation of the conjunction of the predication of P of a and Q of b, where negation and conjunction are semantic operations. And so on.

It occurs to me that we can say all this in IKL directly:

(forall (P ...)(= (PRED P ...)(that (P ...)) ))
(forall (p q)(= (AND p q) (that (and (p) (q))) ))
(forall (p)(= (NOT p)(that (not (p)) ))

etc.., so some of the algebra seems to be ‘built in’. For example

(that (not (and (P a)(Q b))))
= (that (not ((that (and ((that (P a))) ((that (Q b))) ))) ))
= (NOT (that (and ((that (P a))) ((that (Q b))) )))
= (NOT (AND (that (P a)) (that (Q b)) ))
= (NOT (AND (PRED P a)(PRED Q b)))

> Quantified cases are more complex to state but straightforward.


Where can I see an account of the details of this straightforward stuff? (Pointer, reference?) This is where our rubber meets the road. I can’t see how to do quantifiers in IKL using the style above.

> The extensions of all properties, relations, and propositions on this approach constitute a cylindrical algebra. You don’t need to refer to the syntax of the language at all. This is what Bealer does in Quality and Concept.

>
>> In fact, I don’t know of any logic that can do this (quantify over its own expressions).
>

> Perhaps not a *logic* per se but you know as well as anyone, Pat, that any system containing a bit of arithmetic can (in effect) quantify over its own expressions via the magic of Gödel coding. But there’s also no reason why you couldn’t develop a theory whose subject matter was explicitly (sans coding) its own syntax.

It sounds like the algebras you mention might do exactly this, no? I guess I need to find out more about them, sigh. Got a pointer to a text/source?

Pat


>
> -chris
>
>
>

[John F Sowa]

On 10/8/2017 12:13 PM, Pat Hayes wrote:
> It occurs to me that we can say all this in IKL directly:
>
> (forall (P ...)(= (PRED P ...)(that (P ...)) ))
> (forall (p q)(= (AND p q) (that (and (p) (q))) ))
> (forall (p)(= (NOT p)(that (not (p)) ))

No. The operator 'that' creates a barrier between contexts.
Any truth-preserving operations must preserve that barrier.
For example, suppose we have the sentence

(believes Bill (that (and p (not p))))

That implies Bill believes a contradiction. The outer context
may be completely consistent. We don't want Bill's confusion
to infect the outer context.

This leads to McCarthy's axioms for the 'ist' operator:
he allowed information from an outer context to be imported
into an inner context, but exports were much more restricted.

I think that those axioms would support the unifications
in the examples we were discussing.

John

[Pat Hayes]

> On Oct 8, 2017, at 4:49 PM, John F Sowa <so...@bestweb.net> wrote:
>
> On 10/8/2017 12:13 PM, Pat Hayes wrote:
>> It occurs to me that we can say all this in IKL directly:
>> (forall (P ...)(= (PRED P ...)(that (P ...)) ))
>> (forall (p q)(= (AND p q) (that (and (p) (q))) ))
>> (forall (p)(= (NOT p)(that (not (p)) ))
>
> No. The operator 'that' creates a barrier between contexts.

Um…no, it doesn’t say anything about contexts. It is a name for a proposition.

> Any truth-preserving operations must preserve that barrier.
> For example, suppose we have the sentence
>
> (believes Bill (that (and p (not p))))
>
> That implies Bill believes a contradiction. The outer context
> may be completely consistent. We don't want Bill's confusion
> to infect the outer context.

Agreed, and that is why we would probably NOT want the axiom

** (forall (p x)(if (believes x p)(p) )) **

but without this, there is no such infection.

But all this is about the ‘believes’ relation and its properties, and does not have the slightest bearing on the definitions above from my previous email, or the topic that it tries to address.

>
> This leads to McCarthy's axioms for the 'ist' operator:
> he allowed information from an outer context to be imported
> into an inner context, but exports were much more restricted.

In the context logic in Buvac’s thesis (with McCarthy as his supervisor), there is free movement of assertions both in and out of contexts. The Cyc logic was much more circumspect in this regard, however, and I think we both agree that this is wise. However, context logics are rather a tangent from this thread.

Pat

[John F Sowa]

On 10/8/2017 10:27 PM, Pat Hayes wrote:
> But all this is about the ‘believes’ relation and its properties

I used 'believes' as the verb because it's the simplest example.

But the definition of 'ist' implies that statements in the outer
context are true in the nested context.

In fact, that point could be included as a rule of inference
for that-terms: Any S stated or implied by sentences in the
outer context may be copied into the that-term. That would
allow certain kinds of unifications during a proof.

Whether info in a that-term may be exported to the containing
context would depend on axioms associated with predicates
applied to the that-term.

For example, "Bill knows that S" implies S.
But "Bill believes/thinks/hopes/fears that S" does not imply S.

John

[Pat Hayes]

> On Oct 8, 2017, at 10:07 PM, John F Sowa <so...@bestweb.net> wrote:
>
> On 10/8/2017 10:27 PM, Pat Hayes wrote:
>> But all this is about the ‘believes’ relation and its properties
>
> I used 'believes' as the verb because it's the simplest example.
>
> But the definition of 'ist' implies that statements in the outer
> context are true in the nested context.

? Which definition of ‘ist’ ? We didn’t have any such definition in the IKRIS work, because no single definition could cover all the various cases. Selene Makarios wanted there to be a single all-purpose definition, but we never found one that worked.

But why are you bringing this up in this thread? We havn't been talking about contexts or versions of ‘ist’ until your recent email.

> In fact, that point could be included as a rule of inference
> for that-terms: Any S stated or implied by sentences in the
> outer context may be copied into the that-term.

I am not following this at all. IKL does not mention contexts anywhere, and has no notion of ‘inner’ or ‘outer’.

One can *axiomatise* context assertions in IKL, but then the contexts are just ordinary IKL individuals, and all their properties follow from the axioms of your theory. So you can make truths go in or out, or not, as you please. But again, this doesn't seem relevant to the topic here.

Pat