On 04 Mar 2014, at 03:00, LizR wrote:
Hm. I don't know if the first one was OK but anyway let's look at
the second one.
A Kripke multiverse (W, R) is said transitive if R is transitive.
That is
alpha R beta, and beta R gamma entails alpha R gamma, for all alpha
beta and gamma in W.
Show that
(W, R) respects []A -> [][]A if and only R is transitive,
I think "[]A -> [][]A" means (for a world alpha in (W,R)) that if A
is true in all worlds accessible from alpha, then it's true in all
worlds reachable from alpha that A is true in all worlds reachable
from alpha.
I am not sure.
"[]A -> [][]A" means, in a world alpha, in W, from (W,R), indeed, that
[]A -> [][]A is true in alpha. So if []A is true in alpha, you know
that [][]A is true in alpha, so that means that if A is true in all
accessible worlds, then []A is true in all the accessible worlds.
That's a bit - I don't know - recursive? I can feel a bit of
boggling starting in my mind. Let's try to keep things (very, very)
simple.
No problem.
Consider a world alpha in which p is true. I assume I can use p
since I'm used to typing []p by now!
And suppose we have beta and gamma as above.
So []p implies that p is true in beta because alpha R beta... OK so
far...
Hang on, does transitive imply reflexive? This is hard to think
about, having 3 things! For ALL a,b,c, in (W,R) we have
(aRb & bRc) -> aRc.
Specifically if a,b,c are the same (aRa & aRa) -> aRa, so we (kind
of redundantly) get reflexivity too. I think.
Well tried, but if (a Ra) is false, that is just f -> f.
Take a strict order relation like "strictly less than", on N, or R,
that relation is transitive, but not reflexive.
Take "less or equal", that relation is both reflexive and transitive.
"Strictly less than" is even worse than "not reflexive", it is
irreflexive. For all a ~(aRa), or if you prefer ~ Exist a such that a
R A.
By the way, I suspect that the 3-fold nature of the transitivity
rule somehow connects with the 3 []s in the thing I'm trying to
prove! But I have no idea why or how that works, if it does.
Maybe I should stop for a coffee break and let this percolate around
my brain for a bit.
Take the time.
And don't worry, at some point I will have to re-explained all this,
to what some people might take as a very dumb machine, which indeed
believes only few axioms of elementary arithmetic.
That will be the real things, some modal logics will impose themselves
there, including the one corresponding to alternating consistent
extensions.
The theory of everything, here, is classical first order logic + the
following formula:
0 ≠ s(x)
s(x) = s(y) -> x = y
x+0 = x
x+s(y) = s(x+y)
x*0=0
x*s(y)=(x*y)+x
An observer will be defined, in the theory above, by a sound extension
believer of the axioms above, + some amount of induction axioms, of
the type:
(F(0) & Ax(F(x) -> F(s(x))) -> AxF(x), with F(x) being a formula in
the arithmetical language (with "0, s, +, *).
We have to explain to a dumb machine, which understands only 0, s(0),
s(s(0)), ... and can only add and multiply, but yet can reason in
classical logic, the very functioning of such a dumb machine.
There is no miracle. To define the variables, we can use the letter x,
y, ..., it works well for many human people, but the dumb machine
understands only 0, s(0), s(s(0)), so we will have to decide to say
something like let the variable be defined by 0, s(s(0)),
s(s(s(s(0)))), that is, the even number, so we will defined in
arithmetic, the variable by the even numbers.
Variable(x) <-> even(x) <-> Ey(2*y = x)
And about "&", "->" "t", and even what about "(", and ")" ?
Well, again, there is no magic, you have to chose particular odd
numbers (to not confuse them from variable) to represent them.
That is both logic and polite.
And then, how about finite sequences of symbols like "0≠s(x)"?
There too must be defined in terms of number relations, and in this
case a simple way, if we allow ourselves the use of exponentiation, is
given by the uniqueness of prime decomposition. If g(0), g(≠), ...
represents the particular odd number symbol for "0", "≠", etc. then
you can represent "0≠s(x)" by
2^g(0)*3^g(≠)*5^g(s)*7^g(()*11^g(x)*13^g()).
Then the theory itself can be defined or represented, as a number,
being a finite sequences of the number corresponding to the axioms
above.
We will have to defined in arithmetic what we mean by a valid proof. A
proof is itself a finite (or infinite) sequences of application of
inference rules, making proof "easy" to check (and hard to find in
many domains). So we can define in arithmetic a predicate b(x, y)
true when y is a proof (in the dumb number language) of x.
Then provable(x) can be defined by EyB(x, y). It is a Turing complete
sigma_1 arithmetical predicate, a Löbian once it get few induction
axioms.
That "provable(x)", or "believable(x)", or "assertable(x)" by the
modest believer in the axiom above, is an arithmetical modality.
Solovay theorem shows that a modal logic G characterize completely and
soundly (and the logicians' sense) the logic of that provability.
G characterized actually what the machine (theory, believer) can prove
about this, and Solovay second theorem provides a logic G* which get
completely and soundly the truth about the machine. Amazingly enough.
The main axiom of G is the Löb formula []([]p->p) -> []p. We will talk
about it later.
That provability is the "[]" of the modal logic G. It is 3p self-
reference. 1p self-reference(s) will be obtained by weakening or
strengthening of the "[]" in G. The 8 hypostases, and infinitely many
others, are consequences of incompleteness, some of them should gives
the core physical observable (mainly the []p & <>t nuances), on the
sigma_1 sentences.
Modal logic can be used to describe quantum logic, (by results from
Goldblatt and others), and on the sigma_1 sentences (on the UD, if you
want), the "observable" (modal nuance) obeys the right modal laws
needed for an arithmetical quantization, which should normally defined
the core invariant laws obeyed by the measure "one" on the consistent
extensions.
Explaining everything to a very dumb machine is the task of emptying
the ocean with a tea spoon, I told you about. Take it easy. We are in
Platonia where we have all the time. Already, it takes incommensurably
eons to the dumb machine to just say its "name", that is the number
sequences of its primitive beliefs. It is
"s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(...)))), with a *very* big number of
0. Never asks it his name! Just muse on its possible dreams. I hope
you share its basic beliefs.
Bruno
--
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.
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.
