Le 26-juin-05, ˆ 08:47, Russell Standish a Žcrit :
> On Fri, Jun 24, 2005 at 03:25:29PM +0200, Bruno Marchal wrote:
>>
>> Perhaps. It depends of your definition of "OM", and of your
>> "everything" theory.
>>
>> Let me tell you the "Lobian's answer": if I have a successor OM then
>> I
>> have a successor OM which has no successor OM.
>>
>> OK, I am cheating here, but not so much. As I just said to Stathis I
>> must find a way to convince people about the urgency of using the
>> modal
>> logical tools.
>>
>
> This reminds me of something I wanted to ask you Bruno. In your work
> you axiomatise knowledge and end up with various logical systems that
> describe variously 1st person knowledge, 1st person communicable
> knowledge, 3rd person knowledge etc. In some of these, the Deontic
> axiom comes up, which if translated into Kripke semantics reads "all
> worlds have a successor word" (or "no worlds are terminal").
OK. For the benefit of others I recall that I am interested in what
machines can prove and can expect about themselves.
The goal is to interview the machine about the "measure on the
collection of its maximal consistent extensions". The "maximal
consistent extensions" are playing the role of the computational
histories, but in a language available to the machine (by Godel
technic).
I limit myself to sound machine with enough provability power. By a
technic akin to godel or meta-programing, we can translate "the machine
proves <some proposition P> " *in* the language of the machine. I
note that translation Bp. So BP means "the machine proves P" in the
language of the machine. It can be shown that if the machine proves
some proposition P, then such a machine has enough "introspective
power" to also prove that she prove P. We have
If the machine proves P, then the machine proves BP,
which, for a modal logician, is the closer under the necessitation
rule. Then, the machine has again enough "introspection" to "know"
this, in the sense, for any formula P in its language, she can proves
the true formula:
BP -> BBP
She can prove also that she is close for the modus ponens: if she
proves A and if she proves A->B, then she proves that B. "She know
that" means that for any A she proves (and its is true) that
B(P->Q) -> (BP -> BQ)
And it can be proved that she is Loebian, which means she proves BP->P
only if she actually proves P. In particular she cannot prove Bf -> f.
(where "f" = "01"). Actually she knows she is Loebian: for any P, she
proves
B(BP -> P) -> BP
OK? By a theorem of Solovay, those formula and rules axiomatizes
soundly and completely the (propositional) part of the machine's
provability logic. Those formula and rules constitutes the logic G).
If the formula BP->P is true for any P, this really means the machine
is sound. But the machine cannot prove its soundness. She cannot prove
BP->P for any P. She cannot prove, for example its own consistency ~Bf
(~P is equivalent to P-> f).
So although (BP & P) is generally equivalent to BP about the machine,
she cannot generally prove it, and from its perspective BP is not
(necessarily) equivalent to (BP & P).
So provability, from the machine perspective, behaves like a "belief"
modality, where Bp does not (necessarily) entails P.
I recall that for knowledge CP, philosopher asks for both CP -> P, and
the closure for the necessitation rule.
But then this means we can define "knowledge of P", CP, by BP & P.
And then we can interview the machine (through an infinite
conversation, ok, but finitely summarized thanks to Solovay's G) about
the logic of knowledge "CP". This gives a logic of "temporal knowledge"
of a "knower" verifying the philosophers' most agreed upon definition.
I take it as the simplest first person notion "definable" in the
language of the machine.
[Careful here: CP will appear to be only very indirectly definable by
the machine: no machine can give a third person description of its "CP"
logic!
The logic of CP is the system known as S4Grz. The subjective
temporality aspect come from the fact that on finite transitive frames
respecting the Grz formula the Kripke accessibility relation is
antisymmetric and reflexive, like in Bergson/Brouwer conception of
time. See perhaps:
van Stigt, W.ÊP. (1990). Brouwer's Intuitionism, volumeÊ2 of Studies
in the history and philosophy of Mathematics. North Holland,
Amsterdam.
Boolos, G. (1980b). Provability in Arithmetic and a Schema of
Grzegorczyk. Fundamenta Mathematicae, 96:41-45
Goldblatt, R.ÊI. (1978). Arithmetical Necessity, Provability and
Intuitionistic Logic. Theoria, 44:38-46. (also in Goldblatt, R.ÊI.
(1993). Mathematics of Modality. CSLI Lectures Notes, Stanford
California).
See also
http://homepages.inf.ed.ac.uk/v1phanc1/dummet.html
Note that BP -> P is equivalent to ~P -> ~B~ ~P, and if that is
true/provable for any P, then it is equivalent to P -> ~B~p, so BP ->
P, as axioms, entails BP -> ~B~P (the deontic formula). But, by
incompleteness the reverse is false.
Now you were just pointing on tis little less simple definition of
first person based on the deontic transformation. This one has been
studied in my thesis, so I have only my papers in my url for
references). Here a new logic is defined by DP = BP & ~B~P. It is not
used to define a first person knower, but more a first person plural
gambler. The logic of DP loses the necessitation rule and loses the
Kripke semantics, but get interesting quasi-topological spaces instead.
A "immediate time" notion (re)appear though the combination of the two
ideas: define D'P by BP & ~B~P & P.
Do you you grasp the nuance between
BP (Theaetetus 0)
BP & P (Theaetetus 1)
BP & ~B~P (Theaetetus 2)
BP & ~B~P & P (Theaetetus 3) ?
Only Theaetetus 1 gives rise to a "temporal subjectivity".
(Now if you interview the machine on *comp* itself, by limiting the
atomic P to DU accessible truth, the Theaetetus 1, 2 and 3 all leads to
different "quantum logics". In my thesis of Brussels and Lille I have
been wrong, I thought wrongly that the pure (given by Theaetetus 1)
first person collapse with comp).
> Yet it
> appears that you would like to identify what I call psychological time
> as a succession of worlds that follow according to these Kripke
> semantics. Particularly in comments like the above. Since we have
> started with an interpretation of knowledge, formalised it to a
> logical system - how do we make sense of this backwards
> interpretation, ie treating the Kripke semantics as describing the 1st
> person appearance of time? You make no reference (or perhaps only
> hints) in your Lille thesis - I never got around to downloading your
> Brussels thesis - is there something in that? or is it a more recent
> development.
Things are indeed explained, with much details in the Brussel's thesis.
There is also new developments (Blok and Ysapia) but I have skipped
them now: there is perhaps an infinity of first person notions between
the "quantum like" to the classical one, and that could perhaps give a
beginning of a description of a purely arithmetical decoherence
phenomenon: a very fine grained description of the transformation from
possibility into actuality from a sequence of intermediate first person
point of views. For a many-worlder this is a description of
differentiations of worlds/states/histories/OMs...). The
differentiation should lead to an internal coherent information flux
.... I don't know. What is new also is that I have realised that the
Shoenfinkel Curry Combinators (alias the Church lambda calculus) can
provide big help to simplify the mathematical conjectures I have been
led to, and that's progress, I guess.
Bruno
http://iridia.ulb.ac.be/~marchal/
Received on Sun Jun 26 2005 - 11:38:42 PDT