On 07 Mar 2015, at 09:36, LizR wrote:
I thought <>P meant P was possible?
In the alethic interpretation of modal logic, <> means possible, and
[] means necessary.
In the temporal interpretation of modal logic, <> means sometime, and
[] means always.
In the locus interpretation of modal logic, <> means somewhere, and []
means everywhere.
In the deontic interpretation of modal logic, <> means permitted, and
[] means obligatory.
etc.
Note that all "<>" interpretation are form of possibility (alethic,
temporal, locative, ...).
In our interview of the Löbian machine, <> is translated in arithmetic
with Gödel beweisbar predicate:
In particular: <>t is consistency.
<>t = ~[] f = ~ beweisbar ("0 = 1"), with "0=1" being a number coding
the sentence "0 = s(0)".
Beweisbar(x) = Ey proof(y, x), that is: it exist a proof (y) of x.
Proof must be mechanically checkable, and so, like sentences, they can
be coded into numbers, and the predicate proof just decode the proof
named by y and looks if it proves the sentence coded by x.
<>t = ~[] f means intuitively, as said by PA: "PA does not prove the
false", or "PA is consistent".
Similarly and more generally <>p means (PA + p) is consistent, or "p
is consistent with PA", or PA does not prove "0= 1" when assuming
p, ... as formulated in the language of PA.
If so wouldn't P imply <>P? Or have I misremembered what <>P means?
Note that p -> <>p is the contrapositive of [] ~p -> ~p.
As a axiom, it is valid for all p, so, as an axiom, p -> <>p and []p -
> p are equivalent.
But []p -> p cannot be an axiom of the modal logic of provability (G),
that is when [] is the arithmetical beweisbar, given that []f -> f
cannot be proven by PA (PA would prove ~[]f, that <>t, that is, its
own consistency. PA is consistent, and cannot prove its own consistency.
So we don't have []p -> p, nor p -> <>p.
In fact, by Löb's theorem, we have that []p -> p is provable if and
only p itself is provable. And the machine can prove that: []([]p ->
p) -> []p (and the reverse which is trivial, if the machine proves p,
she can prove that anything implies p).
"Consistency of p" is a form of possibility.
In fact "p -> <>p" *is* true, for all p, but the machine cannot prove
all such formula, like she can't prove for all p that []p -> p.
This is made nice and precise by saying that "[]p -> p" and "p -> <>p"
belongs to G* minus G, the corona of the proper theology of the
machine. It contains all (3p) truth *about* the machine that the
machine cannot rationally justified, yet that she can intuit or
produce as true in a high number of different ways.
OK?
Now, that is why the "rational believability predicate" acts like a
believability and not a knowability, and that is why to get a knower,
we need to impose explicitly the link with the truth: that is, we have
to apply Theaetetus' idea, and get the new operator []p & p. That one,
unlike the G box (beweisbar), is NOT translatable in the language of
the machine. The first person has no name, no 3p description, and that
explains why it match so nicely with Plotinus universal soul or with
the greek inner god.
Bruno
On 7 March 2015 at 21:08, Bruno Marchal <[email protected]> wrote:
On 07 Mar 2015, at 02:51, meekerdb wrote:
On 3/6/2015 7:24 AM, Bruno Marchal wrote:
That might depend on the context. Usually, in our computationalist
context it means true in the standard model of arithmetic, which
is "this reality" if you want.
In the modal context, it means true in this world (which in our
arithmetical context is NOT necessarily among the accessible
world, because we don't have []p -> p). With the logic of
provability, we cannot access the world we are in. p does not
imply <>p
I wonder about such definitions of modal operators. WHY doesn't p
imply <>p? We could define <> so that it did. Is there some good
reason not to?
The modal logic are imposed by the fact that he box (and thus the
diamond) are the one describing the self-reference, by Solovay
theorem. The box is Gödel's beweisbar. It is an arithmetical
predicate. We really assume only Robinson (and Peano) arithmetic. We
don't have p -> <>p, because this would mean in particular t -> <>t,
and if that was a theorem of G, then <>t would be provable,
contradicting Gödel's incompleteness.
All modal logics are extracted from arithmetic. They are shortcuts
provided by Solovay's completeness theorem of G and G*, and the
Theaetetus' variants.
Bruno
Brent
--
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 everything-
[email protected].
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.
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/d/optout.
--
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/d/optout.
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/d/optout.
