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" = "0≠1"). 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/
