Bruno,
This is a stupid question but I'm hoping it contains the kernel of
an idea. Since logic is based on a few common definitions, do you really need
all these complicated steps and permutations to prove a theory? Why can't you
show us what you mean in a handful of clear, simple, logical statements?
marty a.
----- Original Message -----
From: Bruno Marchal
To: everything-list List
Sent: Monday, December 07, 2009 1:12 PM
Subject: Re: The seven step series (december 2009)
Hi,
We may be at a cross of the "seventh step" and "Why I am I?" thread.
Chose your favorite universal system.
Like LISP, FORTRAN, the combinators, the diophantine equations, etc.
Enumerate in lexicographical order the expressions corresponding to the
algorithms of the partial computable function of one variable.
(reread the math if necessary, or ask question).
This enumerates, with repetition, all the partial (and thus the total)
functions from N to N, usually described as the phi_i:
phi_0, phi_1, phi_2, phi_3, ....
phi_7 is the name of the 7th partial function in that enumeration.
So the "official" definition of a universal number I am using, is, having
fixed such an enumeration, a number u such that
phi_u(<x, y>) = phi_x(y). Where <x,y> represent some coding of the couple (x,
y). u is usually called the computer (hard version) or the interpreter (soft
version). (Later, or before, for some, soft and hard will be shown to be more
absolute than most people thought, and this as a consequence of comp; but in
the present context it could help to think them as relative notion).
In the definition of the universal number u, phi_u(<x, y>) = phi_x(y), u is
called the computer, x is called the program, and y is called the data.
phi_u itself is called the universal function, and u is just a program
computing that universal function.
From such a u, you can code easily a universal dovetailer. This is a program
which generate all the programs i, and compute, by dovetailing of the phi_i
executions, all those phi_i on all its different arguments, 0, 1, 2, ...
I may come back to the seven step per se later.
Having said what is a universal number, I may say what is a Löbian number.
Or if you prefer, having said what is a universal machine, I may say what is a
Löbian machine.
A Löbian machine is a universal machine which knows, in a very weak and
precise technical sense, that she is universal.
I can prove that any of you are universal machine. And if you understand the
proof, then I have a proof (for me!) that you are inhabited by a Löbian
machine. It means also, that it is just a matter of some work, made by you, to
convince yourself that a Löbian machine indeed inhabit your mind. Comp is the
assumption that there is a level where you can hope your are such a Löbian
machine.
Now I tell you this. A formula like "phi_u(<x, y>) = phi_x(y)" (the
definition of universal number) can be translated into an elementary formula of
first order arithmetic (like Robinson Arithmetic, or Peano Aritmetic).
It ease the things considerably to chose elementary arithmetic as initial
universal system. It happens that classical logic makes the very weak theory,
where 0, s(0), s(s(0)) ... represent the number 0 and its successors.
For all x: x + 0 = x
For all x and for all y: x + s(y) = s(x + y)
For all x: x * 0 = 0
For all x and for all y: x * s(y) = (x * y) + x
Those formula gives the usual recursive or inductive definition of addition
and multiplication.
Exercise: prove that 2 + 2 = 4. That is, prove that s(s(0)) + s(s(0)) =
s(s(s(s(0)))).
This theory is already universal, once we accept some coding of computations
into proof in that theory (using classical logic).
This is an amazing result, and actually is hard to prove. It is due mainly to
Gödel, Hilbert & Bernays, Löb). It is easier to prove that the combinators
equation Kxy = y, Sxyz = xz(yz) are Turing universal, than to show that
addition and multiplication are Turing universal (and thus simply universal
with Church thesis). If you know Matiyasevitch theorem, you can derive the
universality of addition and multiplication). Well, if you know that Conway's
game of life (2-dim cellular automata) is universal, you know universality is
cheap (yet non trivial).
But the theory,
<<For all x: x + 0 = x
For all x and for all y: x + s(y) = s(x + y)
For all x: x * 0 = 0
For all x and for all y: x * s(y) = (x * y) + x>>
although universal, is not Löbian.
You get a Löbian machine by adding some axioms, like
For all x and for all y: NOT(x = y) -> NOT(s(x) = s(y)) (different
numbers have different successors)
For all x: NOT(0 = s(x)) (0 is not a successor)
And above all the following infinity of axioms, known as the "induction
axioms". That is, for any first order logical formula A, you take the following
formula as axiom:
(A(0) & For all x: A(x) -> A(s(x))) -> For all x: A(x).
This is enough to get a Löbian machine, (Peano Arithmetic) which, as AUDA
will illustrate has already a stable and very complex theology, including its
physical quanta and qualia.
But before going to AUDA, I have to finish the seventh step properly, and
probably come back to the Movie graph problems we have encountered. Why a movie
of a computation is not a computation? What is the difference between a
computation and a description of a computation? etc. I guess we could finish
properly the seventh and the eight step.
Ask *any* question. It is not easy. But obviously comp relies on theoretical
computer science which is less known by the general public than the physical
sciences.
Bruno Marchal
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-l...@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.
--
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To post to this group, send email to everything-l...@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.
