On 03 Jul 2017, at 16:00, John Clark wrote:
On Mon, Jul 3, 2017 at 6:18 AM, Bruno Marchal <[email protected]>
wrote:
>>> there is no proof that such larger prime number don't exist
in the theory RA:
>>Then theory RA sucks.
>It is a very useful theory
Useful maybe, but "very" useful?
In the field of mathematical logic, the theories are not used at all.
The theories are the object of study.
There is no largest prime number, if RA can't prove there is no
largest prime number then it is weaker than another axiomatic system
that can.
> You could say that E. Coli sucks because it cannot write
english.
Exactly. E. Coli is less useful at writing English
literature than William Shakespeare was because The
Bard of Avon had more literary power than bacteria does. As a
poet E. Coli sucks.
Yes. Sure.
Then, in biology, E. Coli is a star, along with the Drosophila
melanogaster (the vinegar fly), and many others.
In Metamathematics (an older name of mathematical logic) RA, PA, ZF
are famous, as well as many others.
> RA can (and do) emulate PA, and all other Löbian machine
including us.
I wish you's stop talking about that, even Google doesn't know what
a "Löbian machine" is.
You don't believe in God but you talk like if Google was omniscient.
Turing explained exactly how to build one of his machines but I've
never heard the construction details on
just how to manufacture one of your "Löbian machines".
I wrote the programs, it is easy. Read the books, or my papers.
Interpreted as a theorem prover, Peano Arithmetic, is *the* exemple of
a Löbian Machine.
The most useful current definition is that a machine is Löbian if the
two following conditions hold:
1) it is Turing universal, which is equivalent with being able to
prove all sigma_1 true arithmetical sentences.
Put in another way, p -> []p is true (for p sigma_1 sentence).
Here the box abbreviates the provability ability of the machine
translated in the language of the machine (like Gödel's arithmetical
beweisbar predicate).
+
2) the machine is able to prove p -> []p for each p sigma_1.
That makes the machines obeying the Hilbert-Bernays-Löb provability
conditions, and it makes the machine's (called M) provability obeying
to Löb's theorem: if M proves []p -> p, then M proves p. Formally, it
can be shown that the condition "1)" above entails that the Löbian
machine will "know" that she is Löbian, that it she can prove the
formal version of Löb's theorem: []([]p -> p) -> []p.
If you remember that (~p) is equivalent with (p -> f) f the constant
falsity, you can see that Löb's formula generalizes Gödel's second
incompleteness theorem. Just substitute "f" for p in Löb's formula, []
([]f -> f) -> []f, that is [](~[]f) -> []f, and take the
contrapositive: ~[]f -> ~[](~[]f).
Informally, a machine is Löbian once it is universal (can compute all
computable function) and knows that it is universal (and thus knows
all the sh.t going with that condition too).
RA verifies "1)", but only PA verifies both 1 and 2, and so is Löbian,
or Gödel-Löbian if you prefer.
RA is handy to keep in mind the difference between being universal,
and being universal and knowing being universal.
> It is good to keep in mind that emulating is not the same as
proving or believing. RA can prove that PA can prove RA's
consistency, but that does NOT make RA able to prove its own
consistency
Nothing powerful enough to do arithmetic can prove it's own
consistency;
Powerful to do enough of arithmetic, and being consistent. OK.
and if it is consistent then there are true statements that it can't
prove.
For example, the truth of its own consistency.
Note that ~[]f, (consistency) is the same as <>t. (by definition <>t
= ~[]~t = ~[]f).
It is incompleteness which makes the logic of []p and of []p & <>t
(and []p & p) different.
The Lôbian machine are those able to prove their own conditional
incompleteness. They are able to understand the difference between
proof and truth. In fact, they get a bit mystical, for a (relatively)
simple mathematical reason.
The formula of Löb is the key formula of the Gödel-Löbian machine's
theology. The Löb's formula ([]([]p -> p) -> []p) has been shown to
axiomatize completely the propositional logic of self-reference (of a
very large class of entities, machines or non-machines). As expected
from incompleteness, we get *two* logic G and G*, G for what the
machine can prove about its provability and consistency logic, and G*
for what is true about what the machine can prove (about its
provability and consistency logics).
If interested, see my papers, or older posts, or ask. I have
mentioned four very good book on the subject, Boolos 79, Smorynski,
Boolos 1993, + Smullyan's recreative introduction to the modal logic
of self-reference (Forever Undecided).
But you need to study a bit of logic (Mendelson, Boolos and Jeffrey,
Martin Davis).
Bruno
John K Clark
--
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 [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.
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 [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.
