[Indigo]<KRL>document>str-spec-logic!1

Page Numbers: Yes First Page: 1
Heading:

May 16, 1979 4:37 PM[IVY]<krl>document>str-spec-logic

Formal description of quantifiers, truth, etc. in KRL1

NOTE: stuff here still appears in basicunits as well -- ther is some stuff there which still needs to get included here.

# UniversallyQuantifiedDescription↑1
1: HasFunctional (description, Universal, universalVariables)
description: A Description
universalVariables: SetOf(\[A Description; WhichIs NestedIn My description])

# RealWorld↑1
self/Instance: The worldModel *M* viewedAs a Processor
1:A TimeDependentSlot
Comment ("Those things I believe are true of the real world as it exists at time
*NOW*")

# LogicalWorld↑1
self/Instance: A DescriptionSpace
1:A TimeDependentSlot
Comment ("Those things I believe are true not only of the real world as it exists at
time *NOW*, but of all logically possible worlds as well")

# WorldExtension↑11: HasFunctional (self, ExtensionOf, base)
self: A DescriptionSpace with
entities = Superset(The entities from My base)
describings = Superset(The describings from My base)
base: A DescriptionSpace

# # # # # # # # # # # # # # #

Fikes examples -- Note: this is old

This is an attempt to do quantifiers and implications. I have copied Rich Fikes’ examples, putting his versions in italics, and mine (usually two different versions) in normal font. The notation is the following:

There is a meta-descriptor which can be associated with a UNIT as a whole (I have just put it into the first line) which is of one the forms (more might be added later):

(Whenever d1,d2,...,di then q1,q2,...,qn)

(Equiv d1,d2,...,di and q1,q2,...,qn)

where each di and qj is either a pointer to a slot or descriptor (I have used integers, but they could be labels or whatever in a better notation), or one of the special symbols MAP, or ALL.

The interpretation of Whenever is that whenever there is an entity for which there exists a mapping from this unit, in which all of the entities referred to by the d’s exist and the pointed-to descriptions apply, then all of the entities referred to by the q’s exist, and the pointed-to descriptions apply. MAP means "whenever there is a mapping specified with this unit as the prototype", and ALL means all of the slots and descriptions in the entire unit. Equiv implies two way implication. Not can be wrapped around any d or q, and there can be more than one of these descriptors in a unit.

Some Examples of Implications and Quantification

1. Representation of "Every man who lives in a US city has been
bitten by a rabid dog." An implication form of the statement is "For
all X, if X is a man and X lives in a US city, then there exists a
time T and a Y such that Y is a dog, Y has rabies at time T, and Y
bites X at time T".

[Impl UNIT Category
<SELF (an Implication with
consequent = (Items (a Biting with
biter = {(a Dog)(which HasRabies)}
bitee = (the USCityMan))>
<USCityMan (a person with sex = Male)(which LivesIn
(a City with
country = USA))>]

Version 1:

# Impl
self:A Person with sex = Male
Which LivesIn A City with country = USA
UNIT Category (Whenever 1 then ALL)

<SELF>

1<man {(a Person with sex = Male)
(which LivesIn (a City with country = USA))}>

<dog {(a Dog)(which HasRabies)}>]

Version 2:

[Impl UNIT Category (Whenever 1 then ALL)

1<man {(a Person with sex = Male)
(which LivesIn (a City with country = USA))}>

<dog {(a Dog)(which HasRabies)}>]

2. Two representations of "Every person has a first and a last
name". The implication form is "For all X, if X is a person then
there exists a Y and a Z such that Y is the first name of X and Z is
the last name of X."

[Person UNIT Category
<SELF (which HasFillersFor firstName lastName)>
<firstName (a String)>
<lastName (a String)>
-- ]

[Imp2 UNIT Category
<SELF (an Implication with
consequent = (Items ((an Exists with
unit = Person (the p)
slots = (ListOf firstName
lastName))))>
<p (a Person)>]

[Person UNIT Category (Whenever MAP then 1,2)
<SELF>
1<firstName (a String)>
2<lastName (a String)>
-- ]

3. Representation of "The first name of each of my children begins
with ’M’, and none of my children has a middle name." The implication
form is "If X is a child of mine, then the first name of X begins
with ’M’ and there does not exist a Y such that Y is the middle name
of X."

[Imp3 UNIT Category
<SELF (an Implication with
consequent = (Items (a FurtherDescription with
unit = Person (the child)
slot = firstName
description = (a String with
firstCharacter =
"M"))
(NOT (an Exists with
unit = Person (the child)
slot = middleName)))>
<child (a Person with father = RichFikes)>]

Version 1:

[Imp3 UNIT Category (Whenever 1 then 2,(NOT 3))
<SELF>

<child {1(a Person with father = RichFikes)
2(a Person with firstName = (a String with firstCharacter = "M"))>
3<middleName (the middleName from Person (the child)>]

Version 2:

[Imp3 UNIT Category (Whenever 1 then 2,(NOT 3))
<SELF {1(a Person with father = RichFikes)
2(a Person with firstName = (a String with firstCharacter = "M"))>
3<middleName (the middleName from Person ThisOne>]

4. Representation of "Every town has a person in it that has
been bitten by every dog in the town."
The implication form is "For every X, if X is a town, then there
exists a Y such that Y is in X and for every Z if
Z is a dog and Z is in X, then Z has bitten Y."

[Imp4 UNIT Category
<SELF (an Implication with
consequent = (Items (an InTown with
resident = Imp4TownPerson
town = (the Imp4Town))
SubImp4))>
<Imp4Town (a Town)>]

[Imp4TownPerson UNIT Manisfestation
<SELF (a person)>]

[SubImp4 UNIT Category
<SELF (an Implication with
consequent = (Items (a Biting with
biter = {(a dog)(which IsInTown
(the Imp4Town from Imp4))}
bitee = Imp4TownPerson)))>]

[Imp4 UNIT Category (Whenever 1 then 2)
<SELF>

<town 1(a Town)>
2<person {(a UniversalBitee with place = (the town))>]

[UniversalBitee UNIT Category (Equiv MAP and (Whenever 1 then 2))
<SELF (a Person)(which IsInTown (the town))}>
<town (a Town)>

1<dog (a Dog)(which IsInTown (the town))>
2<bite (a Biting with biter = (the dog) bitee (the person))>]

Another example:

A barber who shaves everyone who does not shave himself

[Russell’sBarber UNIT Category (EQUIV MAP and 1,(Whenever 2 then 3))
<SELF 1(a Barber)>
3<shave (a Shaving with shaver = ThisOne shavee = (the customer))>
2<customer {(a Person)
(NOT (the shaver from (a Shaving with shavee = (the customer))))}>

Descriptions of Units

Uniqueness of mapping, skolem links, etc.

with respect to environment, context?

Interactions with triggers, etc.

Individual, manifestation, etc.

[SkolemMap UNIT

<self>

]

Mapping statement (Skolem links, uniqueness, etc.).

[IsUnique PREDICATE SkolemMap (In determined)) determiners]

Truth and existence

The existence of an entity in a context is interpreted as the existing of the corresponding object in the sorld represented by the context. The existence of a relationship is equivalent to its truth. The non-presence of either is interpreted as non-knowledge, and there is an explicit NOT (notation to be determined) to state known non-existence or non-truth.

Assumption of uniqueness

If a description already contains a descriptor stating that some mapping exists, and a new descriptor is added stating the existence of a mapping from the same source to the same inheritor, it is assumed (unless explicitly denied by some yet-to-be-determined notation) that they are referring to the same mapping. In the simple case, this is equivalent to the combining of perspectives -- i.e. describing something as (a Give with giver = Tom) and then as (a Give with reciever = Arthur) is equivalent to describing it as (a Give with giver = Tom reciever = Arthur). The extra notation is needed in case we want, for example, to describe a single event both as (a hostileInteraction with aggressor = Tom) and (a hostileInteraction with aggressor = Arthur).