On 25 Aug 2009, at 05:52, Brent Meeker wrote:
>
> Bruno, I would like to understand your arguments at a technical level,
> so I started reading your March 2007 paper.
Hmm.... The argument is really UDA. But after UDA, people may be
convinced that comp is just refuted or makes no sense at all, or that
it leads to intractable mathematics. AUDA (the main subject of the
Plotinus paper) is just an abstract translation of UDA in the language
of a Peano Arithmetic theorem prover (a Löbian machine), and it makes
the extraction of physics (among other things) more precise. But it
assumes some acceptation of the "knowledge theory" of Theaetetus,
which can easily be justified in comp from the "dream argument", and
it makes sense for the Loebian machines thanks to incompleteness.
It is really UDA which shows that comp => the reversal. AUDA is part
of the math which follows, and is not necessary for the understanding
that comp forces the reversal, but it gives the math for doing the
reversal in practice, and evaluating the technical difficulty, which
is of course gigantic.
But it is a pleasure for me to answer any question on AUDA. I would
just suggest to those who have not yet grasp the seven step of UDA, to
take it easy here. AUDA is really far more mathematically involved
than UDA. UDA needs just the notion of universal machine. AUDA needs
the notion of Löbian machine which can be grasped when you understand
how quick a universal machine can understand that she is universal.
You may take a look on the second part of the sane04 paper too.
> But I got kinda bogged
> down near the end of Section 2. Could you expand on the paragraph
> that begins with "Let us define an arithmetical realisation R by a
> function which assigns to each propositional letter p,q,r... an
> arithmetical sentence." I understand the general idea which is to
> create a mapping between propositions and arithmetical sentences
> R:p->i where i is some arithmetical statement. But where do the
> propositions come from?
We take them all. An arithmetical propositions are finite strings made
from the alphabet {E, A, &, V, ~, (, ), 0, s, +, *} + the variables x,
y, z, ... verifying a decidable grammar.
For example "prime numbers exists" = ExAy((y divides x) -> (y = s(0)
or y = x)) = ExAy(Ez(y = x*z)-> (y = s(0) or y = x))
You can put them in lexicographic order. Then you can put the sentence
letters of the modal propositional system in some order to: p1, p2,
p3, ...
So you can consider some realization R as being a computable (or not)
bijection between ALL propositional letters and ALL arithmetical
propositions (the true, the false, etc.).
> Are they the axioms appearing just above plus
> the theorems that follow from them?
No, it is just a way to interpret a letter (like p, q, or p1, p2,
p3, ....) by an arbitrary arithmetical proposition.
A letter like p can be assign to a proposition like "0 = s(0)".
(the false and non provable proposition "0 = 1").
> Are there no further conditions on R?
No further condition. R links languages only , (first order arithmetic
and modal logic), not theories. This happens later.
>
> You say that G proves A iff PA proves i(A). But doesn't that depend
> on what map R is chosen?
No. Exactly like a tautology does not depend on the proposition (for
example "(p & q) -> p" is true whatever the propositions p and q
represents). The provable provability tautologies, i.e. the theorems
of G, have to be independent of which arithmetical propositions the
sentence letters are representing. (The same for the true provability
tautologies, with G*)
Take Gödel's second incompleteness theorem general form: Dp -> ~BDp,
or ~B~p -> ~B(~B~p). It says that the non provability of '~p' (Gödel
number of "~p") entails the non provability of (the Gödel number of)
the non provability of the Gödel number of "~p". This is a theorem of
PA for *any* arithmetical proposition p.
Actually "comp" itself will be translated by a restriction of R on the
(false or true) arithmetical sigma_1 sentences. But this is done later
in the paper, and there too, I will take the true and false sigma_1
sentences in the range of R.
OK?
Ask any question. Help yourself with Sane04.
Bruno
http://iridia.ulb.ac.be/~marchal/
--~--~---------~--~----~------------~-------~--~----~
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To post to this group, send email to everything-list@googlegroups.com
To unsubscribe from this group, send email to
everything-list+unsubscr...@googlegroups.com
For more options, visit this group at
http://groups.google.com/group/everything-list?hl=en
-~----------~----~----~----~------~----~------~--~---
