On 14 Feb 2014, at 05:40, Russell Standish wrote:
On Thu, Feb 13, 2014 at 10:42:21AM +0100, Bruno Marchal wrote:
On 13 Feb 2014, at 05:38, Russell Standish wrote:
On Wed, Feb 12, 2014 at 12:24:18PM +0100, Bruno Marchal wrote:
On 12 Feb 2014, at 02:02, Russell Standish wrote:
On Tue, Feb 11, 2014 at 07:31:24PM +0100, Bruno Marchal wrote:
You are right, the qualia are in X1* \ X1, like we get quanta in
S4Grz1, Z1*, X1*.
The only thing you can say is that qualia ought to obey the
axioms of
X1*\X1, (and even that supposes that Z captures all observations,
which I think is debatable),
By UDA, "p" to refer to a "physical certainty" needs to
1) UD generated (= sigma_1 arithmetical and true).
2) provable (true in all consistent extensions)
3) and non "trivially" provable (= there must be at least one
consistent extension)
This give the []p & <>t, with p sigma_1.
So the logic of observable certainty should be given by the Z1*
logic.
This is certainly an interesting understanding that I hadn't met in
your writings before.
You worry me a bit, as I think this is explained in all papers and
the thesis. I know that I am concise.
Normally, if everything get clear, you should see that this is what
I am explaining everywhere.
Indeed this doesn't come out with your Lille thesis. There is almost
no
connection between Chapter 5 and the previous 4 chapters of the
thesis. This doesn't bother me - if you ever bothered to read my
thesis (not that I'm recommending you do so), you would find it
consists of two faily different topics, with only the most tenuous
connection between them. This was because it actually was two
different topics with two different supervisors. I was actually
lightly chided by one of the thesis reviewers for attempting to draw
out the connection between the topics :).
In "conscience and mécanisme" I make the link UDA and AUDA, more
explicit, but this was judged too much easy material, and, in the
Lille thesis I refer to "conscience & mécanisme".
(Of course I have realized since that this is not so much easy. It ask
some familiarity with mathematical logic).
I had a look at your SANE paper, which is the main paper where you
describe
your work that you published since your thesis.
There has been more. I gave the references. SANE remains the simplest
and the most accessible.
There has been the Plotinus paper too, from the Sienna conferences.
I should update my webpage ...
I can sort of see you
saying something a bit like the above on page 11 "Now DU [sic - should
be UD in English]
OK.
is emulated platonistically by the verifiable
propositions of arithmetic. They are equivalent to sentences of the
form ``if exists n such that P(n)'' with P(n) decidable."
Yes, but for the typo. It is of course "it exists n such that ...".
That is actually rather confusing. Obviously a UD executes all proofs
of all true Sigma 1 sentences,
All right.
but I think what you are trying to say that
all programs executed by the UD correspond to a proof of some true
Sigma 1 sentence.
The reverse. Yes.
Is that obvious?
It is obvious for a recursion theorists. It is "well known", among
theoretical computer scientists.
Sigma_1 completeness, that is the ability to prove all true sentences
with the shape "ExP(x, y)" and P decidable, leads to Turing
universality, and so, by the compiling theorem, you can translate, in
both direction from computation, in whatever universal systems, and
"some proof of the sigma_1 sentence".
We have the intensional Church thesis (consequence of the usual CT).
Not only all universal machines can compute the same class of
computable functions, but they can imitate also the other machines,
and compute functions in all possible digital manners.
I didn't get that when I read the SANE paper
originally, only got it in context of your statements above.
Thanks for making me realize this.
In associating provable with "true in all consistent extensions",
In case of "provable", this is Gödel COMPLEteness result (not
incompleteness!).
In case of an abstract box, in a modal logic having a Kripke
semantics, this is just the semantics of Kripke.
are
you meaning that so long as something (ie proposition) is computed
by
all programs instantiating your current state, no matter how far in
the future that calculation might require, then that something is
(sigma_1) provable.
I am not sure. "true in all consistent extensions" is a very general
notion.
It is your term. I take it to mean all programs compatible with your
current state, your current here-and-now.
OK.
What happens is that, in arithmetic, the sigma_1 sentences, when
true, are provable (already by RA).
So they verify the formula A -> []A. (called TRIV for trivial, as
that sentence makes many modal logic collapsing, but not so in the
provability logic, not even in the 1p S4Grz).
Yes - thanks for reminding me.
In fact a machine is Turing universal iff for all sigma_1 sentences
A we have A -> []A. So "A -> []A" is the Turing universality axiom,
when A is put for any sigma_1 sentence.
Where []A means provable by the machine in question, I take it.
OK. And if []A corresponds to the arithmetical beweisbar("A"), it
still means the same thing, for us, and presumably the machine, that
is "provable by the machine in question", but written in the language
of the machine (here: arithmetic language).
G1 is G + A->[]A. Visser proved an equivalent of Solovay theorem for
G1 and G1*. You can find it in Boolos 1993.
It is a way to restrict the logic of the different points of view on
the UD*. "To be a finite piece of computation" is itself given by a
sigma_1 formula, and the sigma-1 sentences model computations.
Then 1&2 gives your hypostase for knowledge, ie S4Grz1.
Only G1 at that stage. To get knowledge, you need to do 1 and 2, but
on []p & p,
But p statisfying 1&2 => p&[]p, so why is this G1 and not S4Grz1?
Perhaps you mean p satisfying p->[]p (-p v p&[]p), which can be added
to G (Visser's move).
The passage from G to S4Grz will correspond the defining knowledge
[°]p by []p & p, in G.
The sigma_1 restriction is when we limit the arithmetical
interpretation of the p, q, r ... on the sigma_1 sentences, and this,
by a theorem of Visser, correspond to adding p -> []p as axiom to G.
From this it does not follow that you will get S4Grz1 by adding p ->
[°]p. (Open problem for completeness, but that is sound).
Actually, that is the case for Z. Z1 is is Z + p -> []p. But that is
not entirely trivial to show, well, that is relative.
like to get observation/probability/expectation, you
need to do 1 and 2, but on (3) []p & <>t.
And to get sensible observation, you can mix knowledge ( " & p"),
and "consistency" <>t.
Yes - I still don't get that - either in the full or Sigma_1
restricted sense.
Where the penny dropped, if only slightly, was that the existence of a
universal dovetailer entails comp immortality, which entails the no
cul-de-sac conjecture, which can be written as []p&<>t restricted to
sigma_1.
Yes.
But is this the approach you are taking? I always felt that
the AUDA stood apart from the UDA.
AUDA stood apart, in the sense that everything is eventually
interpreted in term of arithmetical relations.
But the incompleteness entails the existence of intensions: some
number relations assert propositions on things, including themselves,
or their possible relations with other numbers or things.
But AUDA does not stood apart, as it is a translation of the UDA. Your
3-you is your 3p description, your "Gödel number", if you want, and
which is what the doctor might temporarily save on some disk. despite
this, it can have 3p high level feature, and self-reference does not
need big difference of level, to still follow the laws like G. This is
something well illustrated by Smullyan, in fact.
I will say more, as this is the goal of explaining a few modal logic
to Liz and others.
Eventually the whole is concealed in a sequence of representation
theorems.
Incompleteness makes all those views obeying to different logic.
It is, of
course the sigma_1 restriction of Theatetus's definition of
knowledge,
which both Brent & I share quibbles with, but accept for the "sake
of
the argument".
Since Plato, many philosophers quibble on Theaetetus' definition.
The fist quibbler being Socrate, who refuted it.
The magic things happening with comp, is that Socrate's refutation
does no more apply,
How so? Because comp => p->[]p ?
I would not say that comp => p -> []p. Comp, seen as a DU-
restriction, is translated into "p->[]p", as this limit the
provability logic on the computational accessible states.
I can come back on Socrate refutation, but you can guess he must be
wrong, as incompleteness provides an arithmetical sense to the
Theaetetus definition. A non trivial knower (S4Grz).
Actually seeing the equivalence between executed programs and proofs
of sigma_1 sentences probably alleviates my quibble, but I need to
think it over some more.
OK. It is not obvious.
and the only argument against it which remains,
is the argument put forward by people who believe that they can
distinguish, immediately in the 1p view, simulations or dreams from
reality. But this we have already abandoned when we accept an
artificial brain (like in step 6).
I can't even see the relevance. How is that quibble supposed to work?
[]p alone can be false or in the dark, or dreaming, it can awaken, in
principle, but []p & p is incorrigible, he is always true.
Some people confuse their 1p []p & p, and so communicates p as true,
instead as "assumptions/belief" ([]p).
They will say that they know that they are not dreaming, they believe
that they know their own correctness. They can't be Löbian.
But assuming 3) above is equivalent to assuming the no cul-de-sac
conjecture by fiat.
The beauty is that incompleteness makes sense of that move. In most
modal logic []p -> <>t.
I don't feel comfortable in assuming that axiomatically - I was
hoping
for a proof, or even just a better justification for that.
I am not sure what that would mean. Here the proofs is that the move
need to get a probability notion from a provability notion makes
genuine new sense thanks to incompleteness.
When we predict P(head) = 1/2, we also, but *implicitly*, assume <>t
by fiat. Incompleteness gives the opportunity to see that making it
explicit does change the logic, and that is why observation will
obeys to a different logic than knowledge, and that is exactly what
we need to get physics and knowledge, and belief, ... from the same
arithmetical reality accessible by a machine.
I think I see that. I pretty much do the same thing in getting
equation (D.5) of my book, which in words states that the probability
for getting a result of an observation (any result) is 1.
A cul-de-sac state would be one for which no result is obtained from
performing a measurement. I can see that would completely mess up
quantum mechanics (and for that matter probability theory, which
assumes the probability of the certain event is 1).
Yes. And the common modal axiomatization of probability and
credibility measure usually assumes []p -> <>p.
In the comp case, it introduces also a logic of conditionals and
counterfactuals, like quantum logic might be too, by some work of
Hardegree. The <>t conjunction gives the notion knows as relative
consistency ([]f V p), and it plays a bit the role of the default
hypotheses (I say yes to the doctor and I pray that he will not be
drunk, that no asteroids will crash the hospital, that etc.).
Bruno
http://iridia.ulb.ac.be/~marchal/
--
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
