Le 05-juil.-05, à 12:32, Russell Standish a écrit :
> On Tue, Jul 05, 2005 at 12:09:24PM +0200, Bruno Marchal wrote:
>>>
>>> How does it give the logic of "temporal knowledge"? I understand from
>>> your points below, that the necessitation rule is necessary for
>>> Kripke
>>> semantics, and its is clear to me that necessitation follows from
>>> Thaetetus 1 & 3, whereas it doesn't follow from consistency alone
>>> (one
>>> could consistently prove false things, I guess).
>>
>>
>> Right. But then I guess you mean Theaetetus 0 and 1. We loose
>> necessitation once we just add the consistency ~B~P requirement (in
>> Theaetetus 2 and 3). For example from the truth t we can deduce BP,
>> but
>> we cannot deduce Bt & ~B~t nor Bt & ~B~t & t.
>>
>> I recall:
>> BP (Theaetetus 0)
>> BP & P (Theaetetus 1)
>> BP & ~B~P (Theaetetus 2)
>> BP & ~B~P & P (Theaetetus 3) ?
>>
>
> If D'P = BP & ~B~P & P, then D'P => P (ie necessitation). So it seems
> it is the conjunction of truth of P that gives rise to necessitation,
> no?
No. Necessitation is the inference rule according to which if the
machine proves (soon or later) the proposition p then the machine will
prove soon or later D'p. D'p -> p is the reflexion axiom for D'
(indeed true for the logic obtained by applying Theaetetus 1 and 3 on
G).
Er ... Russell, if I have been wrong or especially unclear on that
point somewhere in SANE or another paper I would be very pleased in
case you tell me precisely where. I am quite able to confuse terms
myself!
>
>>
>>>
>>> I still haven't figured out how to get temporality from a modal
>>> logic. Sure I can _interpret_ a logic as having Kripke semantics, and
>>> I can interpret the Kripke semantics as a network of observer
>>> moments,
>>> with the accessibility relation connecting an observer moment to its
>>> successor. However, what I don't know is why I should make this
>>> interpretation.
>>
>>
>> Why not? It is a "natural" interpretation of S4 type of logic,
>> especially if you accept to interpret the accessibility relation as
>> relation between OMs. It is the case for any interpretation of any
>> theory. Perhaps I miss something here. Of course we could feel even
>> more entitled to take the temporal interpretation once we accept
>> Brouwer "temporal" analysis of intuitionist logic.
>> Beth and Grzegorczyk have defend similar interpretations. I will come
>> back on the question of interpreting Kripke structure once I will
>> translate a theory by Papaioannou in those terms next week (after a
>> brief explanation of what Kripke structures are for the
>> non-mathematician).
>
> Fair enough. It is very similar to the situation in my ontology of
> bitstrings, asking how bitstrings can observe themselves.
>
> The way I would probably phrase things is to appeal to something like
> my TIME axiom as implying a relationship between observer
> moments. These in turn naturally map into a Kripke structure defining
> a modal logic for knowlegde contained in each observer moment. Then we
> can do your Thaetetus move and so on. This is in the reverse order to
> the way it is presented in your thesis, but it makes more sense to
> me. Is there some error of logic in thsi process?
It is ok because the move are not logically related. Note that the
first person knowledge axioms S4 are not mine, but are those admitted
by almost everyone in the (analytical) philosophical field. But I don't
choose them. I am forced to define knowledge by Theaetetus one (it is
the simplest way to get the first axiom of S4 which is the reflexion
formula and which is obligatory to have a first person), and it is
suggested by the fact the (Bp & p) *is* equivalent to Bp (as G* told
us). It is non trivial because G told us the machine cannot justify
that equivalence (although true, this is a consequence of
incompleteness). This leads to the soundness of the resulting S4, and
that is nice, but not so amazing. But then we get antisymmetry for the
Kripke accessibility relation, and this is a truly amazing gift (non
trivial to prove). This confirmes the genuine character of the
Theaetetus definition in this context because it makes the machine
"first person" notion, not only a knower (in the analytical sense) but
a time experiencer sort of knower akin to Brouwer's theory of
consciousness.
I will say more later. The knower is just a step toward the observer,
who gamble on its successor observer-moments.
Best regards,
Bruno
http://iridia.ulb.ac.be/~marchal/
Received on Tue Jul 05 2005 - 11:48:55 PDT