On 24 Jan 2015, at 18:55, meekerdb wrote:
On 1/24/2015 12:20 AM, Bruno Marchal wrote:
Do you see the relationship between Gödel's second incompleteness
theorem and the modal formula
<>t -> ~[] <>t ?
I don't see it, because I don't understand what <>t means.
In a modal logic, you can read it as "possible t", or "diamond t". But
in our context it is the modal logic G (or G*) which axiomatize
completely (at the modal propositional level) the logic of Gödel's
provability Beweisbar.
So <>t = ~[] f = 'not provable false' = " I am consistent", so <>t
means "I am consistent".
t is a tautology, the negation of a contradiction.
That's correct, you can intepret it in arithmetic by "0=0", and f by
"0 = s(0)".
Yet you seem to use t to mean "has a model"?
I use the completeness theorem: a theory is consistent if and only if
the theory has a model. It is true for all first-order theory and
their effective mechanical extension (Recursively-Enumerable-
theories). To say "I am consistent" is equivalent with "I have a
model of myself", or "there is a reality satisfying my beliefs".
And I'm not clear on how one is supposed to know the true
propositions of a model.
We cannot generate them all, but we can belief many of them, by
proving, of by extending ourself with new axioms/beliefs.
Note that all what I say applies to any machine believing in PA
axioms, with possible other axioms, as long as they remain
arithmetically sound (never proves something false in the standard
model of arithmetic).
Let me remind you of Solovay theorem.
We define a realization by a function r from the propositional
variable (of the modal logic) into the sentences of arithmetic. Then
we extend R into a full translation T_r of the modal formula into
arithmetical formula:
T_r(A & B) = T_r(A) & T_r(B) (same for "v", "->", ...)
T_r(~A) = ~T_r(A)
T_r(f) = "0 = s(0)"
+ the only non trivial clause:
T_r([]A) = beweisbar('T_r(A)')
Solovay first theorem is:
G proves A iff for all realization r PA proves T_r(A)
Solovay second theorem is:
G* proves A iff for all realization r T_r(A) is true (in the standard
model of arithmetic (N, 0, +, *).
To extract physics, we need to restrict the arithmetical
interpretation to the sigma_1 formula. By a result of Visser, we have
the equivalent "Solovay" theorems, with G1 = G + (p-> []p) and G1* =
G* + (p -> []p). In fact p -> []p characterize the sigma_1 formula,
and so "p -> []p" is arithmetical-logical equation of the universal
dovetailer.
Note that G* (and G1*) can be interpreted in G (G1) making G*
decidable. Of course, PA, nor any Löbian machine can prove that G*
applies to itself (by the second theorem), that is why the ideally
correct machine remains mute on the its proper theology (G* minus G).
Yet, this representation theorem provides a theorem prover for G1*,
and its first and third person variants, the theory of matter are
given by Z1*, X1*, and S4Grz1* (= S4Grz1).
Bruno
Brent
(<=>
~[]f -> ~[] ~ [] f,
<==>
[]<>t -> ~<>t,
which shows that in G (and thus for the machine 3p self-
reference), consistency, <>t, is a simple solution to []x -> ~x.
--
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.
