On Jun 19, 2014, at 8:07 AM, Tara Athan <taraathan@xxxxxxxxx> wrote: (01)
> 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". (02)
No, this is something else, though it may turn out to be related. I have never
published it because it is clearly incomplete and I have not been able to get
Chris Menzel interested enough in it to correspond with me about it. (I think
Chris has put away childish things like IKL, now he has become a grown-up
philosopher with tenure :-) (03)
First, 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. On
the face of it, IKL seems to be in opposition to Tarski's theorem about the
impossibility of representing the truth predicate in the logic consistently. So
I started looking at some very simple pathological axioms in IKL to see what
kind of models they have, to try to get a better intuition. (04)
For example (05)
((that (not (p)))) (06)
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*. That is, there is *no IKL interpretation* of this sentence over a
singleton universe. Which is kind of interesting: the IKL truth conditions do
have a slight force of a comprehension principle. I have not found any sentence
that requires more than two individuals in the universe, and I strongly suspect
that there isn't one, and that the need for two individuals arises from the
need for the space of propositions to be closed under negation, but I have no
idea how to set out to prove that. (07)
But here is the main idea. What I noticed while playing with variations on this
theme was that the IKL/Tarski principle (08)
(iff ((that S)) S) (09)
can be re-phrased as defining a function R on the free names N1...Nn in S: (010)
(forall (N1 ... Nn)(iff ((R N1 ... Nn)) S) (011)
where 'S' indicates a sentence, of course. (012)
The function R here is from the things named in S to the proposition which the
assertion of S says holds of them, i.e. the proposition (that S). But now we
have an ordinary CL term to denote this proposition, so we can replace every
occurrence of (that S) in a text T by the CL term (R N1 ... Nn) and the
resulting text - call it T' - is true exactly whan T is, provided that defining
axiom, above, is true. (013)
So consider the following algorithm IKL2CL, which takes two texts D and T as
input: (014)
If the text D T contains no (that ...) terms, then RETURN the pair <D, T> ;
Otherwise, choose a term (that S) occurring in the text D T ; let N1...Nn be
the names occurring free in S and let R be a new name not occurring in D or T ;
Make D be the text D[(that S)//(R N1...Nn)] (forall (N1 ...Nn)(iff ((R N1
...Nn)) S)) ;
Make T be the text T[(that S)//(R N1...Nn)] ;
Repeat from top. (015)
And suppose IKL2CL( { }, T) = <D', T'> , then T' is a CL text which is
IKL-equivalent to T when D' - also a CL text - is true. (016)
This algorithm always terminates because it reduces the number of distinct
(that ...) terms in the arguments by one in each iteration. It works with any
IKL sentence. It handles nested (that ...) terms, and quantifiers outside S
binding names inside the term (that S) (which is why we have to include all the
free names as arguments to the relation.) (017)
As an example, start with T being the simplest IKL liar sentence: (018)
(= p (that (not (p)))) (019)
you get (020)
(forall (x)(iff ((R x))(not (x)))) , (= p (R p)) (021)
which is perfectly legal CL. R here is the function on an object to the
proposition that this object is a false proposition. (022)
What happens in this algorithm is that the D sentences are in effect CL axioms
which re-state the 'Tarskian' IKL truth conditions on the (that ...) terms in
T, but as defining conditions on new names which are then used in the main
sentence. Of course, these truth condtions are the only problematic case in
IKL, which is in all other respects just CL with a single-universe semantics
(ie CLIF). So the issue of IKL's internal coherence becomes the issue of
guaranteeing that these D sentences will aways make sense, ie be consistent (in
CL.) If D turns out to be inconsistent, then the original T sentence has no IKL
interpretation, ie it will illustrate the internal incoherence in IKL that one
might suspect is there because of the apparent clash with Tarski's result on
representing the truth predicate. But I havn't been able to find a case where D
is unsatisfiable, and I suspect that in fact it is always satisfiable, which if
true is very nice for IKL but also suggests an intriguing line of research to
figure out why exactly IKL avoids the Tarski negative result. (IKL *seems* to
be able to define its own truth predicate, but it can't possibly. Where exactly
is the subtle crack that rescues it from paradox?) (023)
Unfortunately I have not yet been able to prove that D must always be
consistent. I imagine that it would be good to prove it inductively, assuming
that D is consistent at one stage of the algorithm and then showing that
consistency is preserved. And I am willing to bet a McDonald's breakfast that
this will fail precisely because CL definitions, even of new names not
occurring in the definiens, are not guaranteed to be conservative, which is the
key sticking point for the Russell paradox (which can of course be stated in CL
without help from IKL.) (024)
If you (or anyone else) can see how to take this idea and run with it to prove
that IKL is internally coherent (or demonstrate by example that it is not),
please make me a co-author of the resulting paper :-) (025)
Pat (026)
PS. Of course the reduction to CL might be of pragmatic interest even if it is
not guaranteed to always be correct. It is certainly correct in all practical
cases. (027)
PPS. the rest of your reply (beiow) is interesting for other reasons, but I
want to keep this thread focussed on this topic. (028)
> 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 not itself
>a time-interval. Point taken.
>>
>>> 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
>>
>>
>>
>>
>>
>>
>>
>>
>>
> (029)
------------------------------------------------------------
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 (030)
_________________________________________________________________
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 (031)
|