Re: Are we simulated by some massive computer?
Hi Kory,
So we met two important theories or machines:
Classical Logic CL and Peano Arithmetic PA.
As collection of theorems, the first is a subset of
the second:
PA
|
|
|
CL
Now I have chosen PA to set the things. Any theory or
machine rich enough to prove elementary theorems about
numbers will do.
What will be important is that anybody (including possible
machines) should be able to verify mechanically if a given
proof is a proof, at least in principle (in case a given proof
is 2^64 steps long).
We will interview PA about its possible (consistent) extensions.
It is Godel who showed how to make such an interview,
by showing how to translate the meta-predicate of provability
into an arithmetical sentence.
Let me be a little more specific. Don't hesitate to tell me you know
all this, but it could help some others, and it could help
in front of futur misunderstandings.
PA has a language. Here it is:
L_PA = {v, , -, not, t, f, A, E, =, +, *,
SUC, 0, (, ), x,y,z,x1, y1, z1, x2, y2, ...}
We could code those symbol by the odd integer above 1. So
the Godel number of v is 3, and this I abbreviate by ng(v)=3.
So ng()=5, ng(-)=7, ng(not)=9, ng(t)=11, ..., ng(x)=33, ng(y)=35, etc.
So exactly in the sense that you can define the divisability predicate
Div(x,y) (which is true when x divide y) only with the available symbol
as in
Div(x,y) = Ez(x*z = y) (there exist a number z such that
x multiplied by z gives y)
you can define the meta-predicate IS-A-VARIABLE(x), which is
true when x is a number representing a variable, as Godel number.
Actually, with the code we have chosen:
IS-A-VARIABLE(x) = ODD(x) BIGGER-OR-EQUAL(x,3)
= Ey(x=2y+1) Ez(x = z+33)
Now we want to talk about formula also with PA. I recall
that there are precise formula formation rule like
if A is a formula then (not A) is a formula
if A and B are formula then (A B) is a formula,
etc.
To code a formula by a number, a traditional way relies
on the well known fundamental theorem of arithmetic
saying that all number have a unique decomposition
in product of prime numbers.
So the formula Ez(x*z = y) will be coded by the number
2^(ng(E))*3^(ng(z))*5^(ng(())*7^ng(x)*11^(ng(*))*13^(ng(z))* ...
(I let you continue)
(I have also avoid the quotation mark for not wasting ink,
but ng('(') is more readable than ng((), mmhh..
Now, a proof in, or by, PA [in if you think as PA
being a theory; by if you think as PA as a machine
(a theorem prover)] is just a sequence of formula
such that they are either axioms or has been obtained
from the axioms by a finite number of application of
the inference rule.
So, although it could be hard to *find* a proof (as
unpedagogical exercice try to prove the formula (A - A)
in the systeme send yesterday), it is easy to verify
a proof once the proof is given.
The point is that we can translate a proof into a number
by relying a second time on the fundamental theorem
of arithmetic. A proof is just a finite sequence of
formula F1 F2 F3 F4 F5 ... FN (actually it will be proof
of FN if F1, F2, ... are axioms or comes from axioms
and preeceeding formula by application of the inference
rule). Its (Godel) number will be
2^ng(F1)*3^ng(F2)*5^ng(F3)
Now, like we have define in PA language IS-A-VARIABLE(x)
we can translate meta-predicates like IS-AN-AXIOME(x),
HAS-BEEN-DERIVED-FROM-MODUS-PONENS(x,y,z), meaning
z is derivable from x and y by modus ponens.
Etc. Etc. So that we can defined in PA arithmetical language
IS-A-PROOF-OF(x,y) saying that y is a translation (a godel
number of) of a proof of formula (with Godel number) x.
This was the B(x,y) of yesterday.
And then the Godel formula BEW(x), that is PROVABLE(x),
is just EyB(x,y) i.e. it exist a number y such that y is a proof
of x, to make it short.
Now, a machine will be said to be consistent,if the machine
does not prove f.f is a symbol with the intended meaning of
an absurdity, or a contradiction. in arithmetic f could be defined
by the formula (1 = 0), well actually (SUC(0) = 0).
So the consistency of the machine, or of the theory, or
of PA (here) can be defined by the formula (not BEW(f)).
Godel second incompleteness theorem is that
if a machine is consistent then the machine cannot prove
she is consistent. Now I will explain in which sense we can
say that to be consistent is the same has having a consistent
extension, so you see that Godel second incompleteness
explain why, as I said to John, when we ask the machine
if she *do* have at least one consistent extension, she
remains silent.
Well that is a little bit discouraging isn' it? How could we
hope the machine to be able to give us the geometry
of its consistent extensions when she remain silent on
the very question of having consistent extensions at all?
But if you are patient enough with PA, she will justify
her silence by proving
Re: Are we simulated by some massive computer?
Dear Bruno, We are getting more coherent and on point in our understanding of each other. ;-) Interleaving. - Original Message - From: Bruno Marchal [EMAIL PROTECTED] To: Stephen Paul King [EMAIL PROTECTED] Cc: [EMAIL PROTECTED] Sent: Thursday, April 29, 2004 9:09 AM Subject: Re: Are we simulated by some massive computer? Hi Stephen, At 12:15 28/04/04 -0400, Stephen Paul King wrote: I struggle to find the right words to express the difficulty that I see. My problem is that your work ignores the computational complexity (NP-Completeness) of grading (defining measures) the relationships. This is due to the fact that from a first person point of view any delay will not been perceived. I do not pretend that complexity should always been ignored, but to introduce it at the start would be ad hoc. [SPK] But there is no such thing as a delay in Platonia, but that is not my point. I am trying to see how you deal with the problem of intractible computations - as implementable given infinite resources - and how it may be possible for measures to be defined using them. I had not considered this application but it is intriguing. You touch on this below. If complexity play a role it must be derived along with the measure on the comp histories. [SPK] Yes, but is this derivation on that can be taken to exist independent of the first person aspect of comp histories? This may be one of my key difficulties. On one hand, I do not have a problem with the idea of Platonic existence, re AR, of mathematical objects but I do have a problem with the seeming lack of a clear explanation of how the flow of temporality arises in the first person aspect. It seems to me that what ever our theory of Everything is, it must explain how it is not just possible to have a flow of temporality a priori; it must have a non-measure zero sampling in the class of all possible relationships between numbers - or whatever notion of Ur-object that one uses. I personaly eschew the notion of fundamental objects and use the Heraclitian notion of Process and fundamental, thus I see mathematical objects - numbers, etc. - as derivative of this notion of Process. I see Hintikka's idea of proofs as game theoretical constructs as strongly hinting at this idea... In Conscience Mecanisme I do make a case that Bennett notion of depth could play a role in order to derive the cosmological aspect of physics. Even prior a-la-Schmidhuber could play a role. But the methodology I advocate although it could justify the prior if needed, cannot rely on it at the start. [SPK] I agree. We have to have the methodology itself as an a priori existent. It is co-present in Platonia in your thinking, it seems to me. ;-) I do not see how the mere a priori existence of solutions (Integers) and the relationships between them (also Integers), as a priori existing numbers is sufficient. We will discuss that after I succeed in explaining how the whole things work. All Right? [SPK] Sure! ;-) BM: The comp reason why the soul or the first person is never captured by any complete third person description is akin to the reason truth and knowledge are not arithmetizable (as opposed to provable and consistent). Godel's theorem Co. makes universal machine a highly non trivial type of being. [SPK] Does not this statement, that truth and knowledge are not arithmetizable, imply that the postulation of AR is insufficient? [BM] No. And giving that Godel's incompleteness is true for much more general things than machine, we can say not only that arithmetical truth is not arithmetizable, but mathematical truth is not mathematicalizable, physical truth is not physicalizable, and more generally [whatever]-truth is not [whatver]izable. So strictly speaking AR could be sufficient (the Pythagorean version of my thesis). For reason of simplicity I do not use it. [SPK] Wait a minute! It is one thing to say that [whatever]-truth is not [whatver]izable and it is another to say that [whatever]-truth is finitely constructible or approximatable. The former deals with its existential aspects and the latter deals with its meaningfulness and expressiveness. We do not require absoluteness (truth, decidability or otherwise) in our interactions to be able to have meaningfulness. But this is not problematic to me; I am interested in how physicality MUST obtain, even if only in the first person sense. In fact, in my work I anly assume first person physicality - there is no such thing as third person or objective physicality. This is where our idea overlap strongly.;-) Let me state this in a different way. How does Digital Substitution ( yes, Doctor ) get coded into numbers without involving physical implementation? [BM] But that's the point of the whole work. Now, if you have follow a little bit the literature on the mind body problem you surely know that nobody has
