Hi Telmo,
On 20 Feb 2014, at 13:40, Telmo Menezes wrote:
On Thu, Feb 20, 2014 at 9:31 AM, Bruno Marchal <marc...@ulb.ac.be>
wrote:
On 19 Feb 2014, at 19:13, Telmo Menezes wrote:
"If no human can check a proof of a theorem, does it really count
as mathematics? That's the intriguing question raised by the latest
computer-assisted proof. It is as large as the entire content of
Wikipedia, making it unlikely that will ever be checked by a human
being."
http://www.newscientist.com/article/dn25068-wikipediasize-maths-proof-too-big-for-humans-to-check.html#.UwTytEJdV69
This reminded me of something that Bruno mentions frequently: the
idea of deriving physics from the natural numbers, addition and
multiplication. Should we expect wikipedia-size proofs (or worse)?
Hi Bruno,
Er well, people seems not quite aware of this, but the physics has
already been derived, and it would take 50 pages, when done starting
from zero, but it is shortened a lot by using Solovay's completeness
theorems (on G and G*).
Of course, the physics obtained might seem a bit abstract, and it
remains many open problems. But the equation are there, and it
remains only mathematical problems to solve.
It would be astonishing that the first interview of the machine
gives the correct physics, but up to now, it fits, and this at a
place where many logicians predicted it would be miraculous that it
would not be contradicted immediately.
I have to admit, I think I follow the main ideas you've been
explaining on the mailing list, but here you just sound
mysterious... Have you published any of this?
Yes. In the original long 'belgian" version, UDA is just UDP, that is
the paradox of the universal dovetailer, and it is "just" a motivation
for the mathematical definition ([]p & <>p), for the mathematicians.
The original thesis is mainly "AUDA", the "translation of UDA" in
arithmetic. Here the formulation provides "the solution", a bit like a
differential equation "gives" its solution(s).
Quentin made a genuine point, already done by J.P. Delahaye, that
physics is redefined, and that it might have been trivial, only
geography, but the whole point is that there is a core non trivial
physics, which is natural, as it is the laws on the statistical
combinations of *all* computations, below the substitution level.
Physics is redefined by "universal machine observable", and this can
be translated (in platonia, i.e. in arithmetic) by p sigma_1 (p ->
[]p, and []p & <>t). That gives already the "quantum" tautologies, and
the comparison match up to now.
That's why they push me to publish and do a PhD thesis.
Of course, comp can be false, and this might only be a bad lucky
coincidence. This we can always say for any theory.
I am actually explaining to Liz and others, how the physics is
extracted (UDA explains already how physics needs to be redefine,
and AUDA just do the math of that redefinition). I have to explain a
bit of modal logic before, just to be able to give the enunciation
of Solovay theorems.
Ok, I've been silently following your modal logical class as time
permits. Thanks for that, by the way!
You are welcome,
I will try soon to send a long post explaining the main gist of the
whole AUDA. It is really consequences of Gödel's second incompleteness
theorem (and Löb's theorem, and the Solovay theorems), for machines
which are simple enough so that we can "know" them to be correct, and
rich enough (having enough induction power) to "know" their own turing
universality, and be Löbian.
Bruno
Telmo.
Best,
Bruno
Cheers,
Telmo.
--
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 everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-
l...@googlegroups.com.
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
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 everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
--
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 everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
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 everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
