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/
