Pat- I agree with you on almost all
points, exceptions noted below.
Regarding removing "that" by reducing to CL, no, I don't think I
have seen your notes on ... er, that, except for what appears in
the IKL guide
( http://www.ihmc.us/users/phayes/IKL/GUIDE/GUIDE.html) in the
section "Eliminating ist". If that is what you are referring to,
then I think it may be expressible using the metalanguage I
developed in http://ruleml.org/papers/Athan_SyntaxReuse.pdf. And
since that is based on XSLT, it might not be too far from
implementation, at least for some XML-based rendering of IKL. But
it would take some investigation to confirm that conjecture.
More below...
Tara
On 6/19/14 1:37 AM, Pat Hayes wrote:
On Jun 17, 2014, at 6:51 AM, Tara Athan <taraathan@xxxxxxxxx> wrote:
On 6/17/14 1:03 AM, Pat Hayes wrote:
Using the IKL “that” operator and a “during” relationship and the concept “July” (a ‘calendar month’):
Whoa. No, this is NOT the right way to do it. In fact, this is meaningless. According to the IKL semantics, (that (employs C P)) denotes a fixed proposition which is true or false. There is no room for any time-dependent variability in its truth value, or for making it depend on some other parameter.
It may not be the *best* way to do it, but I don't agree that it's wrong
or meaningless.
Yes, you are right, and I withdraw my strong statement. It is indeed one way to do it. (It is exactly how we coded so-called "context" logic in IKL, in fact, using 'ist' rather than 'during' and contexts rather than times.)
What I will claim is that it is wrong to claim that one *needs* the 'that' operator in order to handle time-variation properly, however. The conventional ways need only conventional reasoning and have a better logical foundation, as well as being widely used already.
Using the proposition (that (employs C P)) as an
argument in a relation is not obstructed by its denotation of a fixed
proposition which is true or false (in any given interpretation).
Starting off without quantifiers:
(cl:comment 'C employs P'
(employs C P) )
(cl:comment 'It holds during time interval T that C employs P'
(during (that (employs C P)) T )
Nothing wrong with that - the truth values of these sentences are
independent of each other.
Now bring on the quantifiers to relate the two
(forall C P
(if
(cl:comment 'C employs P'
(employs C P) )
(exists T
(cl:comment 'It holds during some time interval T that C employs P'
(during (that (employs C P)) T )
) ) )
Some users may find this clearer than the polymorphic representation.
Why not let them use it?
Well I am hardly in a position to prevent anyone doing anything :-) . But I will resist the idea that this kind of construction is *necessary* in order to handle time-relative assertions.
It is still possible to have the polymorphic representation behind the
scenes for reasoning purposes.
(forall C P T
(iff
(cl:comment 'It holds during time interval T that C employs P''
(during (that (employs C P)) T )
(cl:comment 'C employs P during time interval T'
(employs C P T)
) )
Also, using the "that" operator for temporal context
"temporal context" ? Blech. call them what they are, time-intervals. That "context" word does nothing but add confusion and muddle.
OK. A temporal context might be derived from a time-interval
(ist TemporalContextYear1995
(that (exists ((x isHuman)) (and (Democrat x)(PresidentOfUSA
x))))
)
could also be written
(ist TemporalContext(Year1995)
(that (exists ((x isHuman)) (and (Democrat x)(PresidentOfUSA
x))))
)
where Year1995 is a time-interval but TemporalContext(Year1995)
is a gateway to
using it for other contexts/modalities.
I find the symmetry appealing:
(cl:comment 'It holds before time interval T that C employs P'
(before (that (employs C P)) T)
(cl:comment 'It holds after time interval T that C employs P'
(after (that (employs C P)) T )
(cl:comment 'It is possible that C employs P'
(possible (that (employs C P)) )
(cl:comment 'It is forbidden that C employs P'
(forbidden (that (employs C P)) )
(cl:comment 'Jane believes that C employs P'
(believes Jane (that (employs C P)) )
(cl:comment 'Omar knows that C employs P'
(knows Omar (that (employs C P)) )
(cl:comment 'Maria asserts that C employs P'
(asserts Maria (that (employs C P)) )
These look cute
Ooooh, that hurts.
but all they do is put the entire burden of representing their meanings on the relation names (possible, forbidden, knows, etc.), and implicitly make a claim that the relevant concepts (possibility, prohibition, knowledge,..) are indeed properly representable as relations between propositions and something else. In some cases, I think this is at best doubtful: possibility for example is usually thought of as a modality rather than a relation.
Hmm, there is no such thing as a modality in IKL. Are you saying
that an additional layer of syntax is needed, beyond IKL, to handle
alethic modalities? Why should alethic be different than doxastic,
which is modelled using a "Belief" relation and "that" in the IKL
guide?
And in any case, none of this has any actual content until one gives axioms for these intended meanings.
Of course. And the same is true when "that" is avoided by using a
time-interval directly in the relation.
One needs to mirror all the conventional inferences in explicit axioms. For example, from P being true at T and Q being true at T, it should follow that (and P Q) is true at T. In the conventional ways of writing time-dependent statements, this follows trivially from notmal logical reasoning, but here it needs to be stated by quantifying over propositions and by having a function on propositions which mirrors conjunction:
(forall (P Q)(iff ((AND P Q)) (and (P)(Q)) ))
(forall (P Q)(iff (during (AND P Q) T)(and (during P T)(during Q T)) ))
Although its not "necessary" to create the relation AND, I agree it
is convenient, rather than the explicit, but hard to read
(forall (P Q)(iff (during (that (and (P)(Q))) T)(and (during P T)(during Q T)) ))
But I wonder if introducing AND, etc. doesn't in the end make this more complicated, because it is not correct to write
(forall (P Q)(= (AND P Q) (that (and (P)(Q))) ))
so you end up creating a bigger set of propositions to deal with,
and similarly for all the other connectives.
compounded by all these interactions.
I leave handling "inner" quantifiers as an exercise for the reader :-)
Well, it only needs to be done, and published, once - everyone else
can import it, and use it for any proposition they like, independent
of what relations it contains, or whether it is a complex
proposition built up with logical connectives and quantifiers. There
could even be an axiom schema with quantification over the "modal"
relation ("during", etc.), conditional on its membership in a
relation "A-clear", "N-clear", etc.
Seems to me like the infrastructure for these kinds of expressions
is worth building, one way or another. Wish I could get somebody to
pay me to do it ...
Tara
Pat
PS. BTW, did I ever send you my ideas on how to reduce IKL to CL by
eliminating "that" constructions recursively? I would be interested
in your reactions.
...
Tara
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
------------------------------------------------------------
IHMC (850)434 8903 home
40 South Alcaniz St. (850)202 4416 office
Pensacola (850)202 4440 fax
FL 32502 (850)291 0667 mobile (preferred)
phayes@xxxxxxx http://www.ihmc.us/users/phayes
|
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (01)
|