On 25 Aug 2012, at 07:30, Stephen P. King wrote:
On 8/24/2012 12:02 PM, Bruno Marchal wrote:
As emulator (computing machine) Robinson Arithmetic can simulate
exactly Peano Arithmetic, even as a prover. So for example Robinson
arithmetic can prove that Peano arithmetic proves the consistency
of Robinson Arithmetic.
But you cannot conclude from that that Robinson Arithmetic can
prove its own consistency. That would contradict Gödel II. When PA
uses the induction axiom, RA might just say "huh", and apply it for
the sake of the emulation without any inner conviction.
With Church thesis computing is an absolute notion, and all
universal machine computes the same functions, and can compute them
in the same manner as all other machines so that the notion of
emulation (of processes) is also absolute.
But, proving, believing, knowing, defining, etc. Are not absolute,
and are all relative to the system actually doing the proof, or the
knowing. Once such notion are, even just approximated semi-
axiomatically, they define complex lattices or partial orders of
unequivalent classes of machines, having very often transfinite
order type, like proving for example, for which there is a branch
of mathematical logic, known as Ordinal Analysis, which measures
the strength of theories by a constructive ordinal. PA's strength
is well now as being the ordinal epsilon zero, that is omega [4]
omega (= omega^omega^omega^...) as discovered by Gentzen).
Dear Bruno,
What happens when we take the notion of a system to those that
are not constructable by finite means? What happens to the proving,
believing, knowing defining, interviewing, etc.?
Amazingly, not a lot. That is why I say sometimes that comp can be
weakened a lot. G and G* are sound, not only for PA and ZF (which is
terribly more powerful than PA, with respect to provability, but, I
repeat, the same for computability). If you allow provability to be
even more powerful, and accept infinite inference rule, like the omega-
rule in analysis, or some axiomatic form of second order logic, or
even more non constructive, G and G* will still remains correct and
complete.
If you continue on that path, G and G* will remain correct, but no
more complete. That is the case if you define provability by satisfied
by some models of a rich theory. By Gödel completeness, satified in
all models of the theory, gives the usual provability. But
satisfaction by certain models leads to entities needing some
supllementary axioms to be added on G and G*. But the present comp
theory does not use completeness of G and G*, only the correctness,
and so .... you need to go really quite close to God, for avoding the
consequences of the arithmetical hypostases.
Now, to prove this is quite difficult. Solovay announced many of this
without proof, and the book by Boolos, the 1993 version gives the
detailed proof, but it is technically hard. I use comp, for reason of
simplicity, but it can be weakened a lot. I suspect that the real
needed axiom is just the assumption of self-duplicability, and not
digitalness.
Bruno
--
Onward!
Stephen
http://webpages.charter.net/stephenk1/Outlaw/Outlaw.html
--
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
.
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.
