On 05 Jul 2017, at 16:09, John Clark wrote:
On Tue, Jul 4, 2017 at 2:26 PM, Bruno Marchal <[email protected]>
wrote:
> In the field of mathematical logic, the theories are not used
at all. The theories are the object of study.
If mathematical logic is not to be a trivial subject then
it's object of study should be the nature of reality,
?
The object of study of mathematical logic is mathematical reasoning
and mathematical theories. Notbaly what can be derived and what cannot
be derived in mathematical theories.
that's why the study of the largest prime number seems rather
silly to me.
It is just a logical point that you can't derive this from Robinson
Arithmetic theory, a bit like the Euclid postulate on parallel has
been shown non derivable from the other geometric axiom.
>> 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.
It's not just Google, even Martin Löb never knew what
a "Löbian machine" was, and you're the only one who
refers to it.
Martin Löb knew exactly what is a Löbian machine, although he would
have called it a "sufficiently rich theory" as it is often called. I
use "machine" instead of "theory" because I limit myself to the study
of machine, given my field of study (Mechanism).
Typically, RA is Turing universal, but not Löbian. PA, ZF, etc. are
Löbian, as well as all their sound extensions.
>> 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.
In other words you've explained this brilliantly elsewhere, or in
yet other words I've stumped you.
I gave you the reference. here you show again that your goal is not to
learn something, but to be negative.
> Peano Arithmetic, is *the* exemple of a Löbian Machine.
A Turing machine can do Peano Arithmetic too. Nothing new
in that.
Of course not, you seem to ignore the difference between a theory, or
a set of "believed" propositions/sentences.
A (universal) Turing machine can compute (everything computable), but
cannot prove anything.
You might tell me that you were alluding to a (minimal) first-order
logical specification of a Turing universal machine, in which case you
will get a theory equivalent with RA, not with PA, which requires the
(infinitely many) induction axioms.
PA proves much more than RA, and a fortiori than a (logical theory of)
a Turing machine.
> The most useful current definition is that a machine is
Löbian if [blah blah blah]
Turing did far more than define what his machine could do, he
explained exactly how to construct one in great detail, and that's
why other people gave it the name "Turing Machine".
Yes, he is the discoverer of the (mathematical) notion of computer,
and he was interested in building one.
I can define what a perpetual motion machine is but I can't tell you
how to build one, and that's why they're not called Clark Machines.
If you know of a computing machine that can do things a Turing
Machine can't and you can explain exactly how to build one then they
should be called Marchal Machines, and I think Martin Löb would have
agreed.
You seem to be ignorant in logic. With the Church-Turing-Post thesis,
computable is universal, but provability, by incompletness is
relative. All axiomatizable theories can be seen as machine, because
their set of theorems is computably generable. Once such a theory can
prove all true sigma_1 sentences, the theory becomes Universal, WITH
RESPECT TO COMPUTABILITY, but the theory does not become universal
with respect to PROVABILITY.
Above RA and PA, there is an infinity of more powerful machine with
respect to arithmetical provability.
RA, by being Turing universal, can emulate PA, like all humans can
emulate Einstein, but this does not mean that all humans are Einstein.
Like I said, PA cannot prove its own consistency, but PA can prove
that ZF can prove PA's consistency, without understanding or being
able to assess the proof (of course, by incompleteness).
With Mechanism, all believer, or theorem prover, are machine, but even
with mechanism, not all machine are believer or theorem prover. A
machine compute a function, a theorem prover, or a believer asserts
propositions.
So I ask again, what parts from the hardware store do I need to buy
to build one?
I said that I wrote different program for a Löbian machine, and if you
read Smullyan's book, you will find others, and they are all emulable
by a Turing machine, so you can use your computer. To implement my
program(*), you need just to buy, or find on the net, a (good) LISP
interpreter.
To implement a Löbian machine, it is very easy, you need only to
implement a theorem prover for Peano Arithmetic. It is the kind of
task I give as easy exercise to my students. Of course, it is "easy"
only if you have some amount of knowledge in logic, and know some
programming language.
Bruno
(*) http://iridia.ulb.ac.be/~marchal/bxlthesis/Volume4CC/2%20G,%20G_%20%26%20S4Grz.pdf
(of course a prover machine for G is Löbian in the sense of
respecting the second condition given yesterday. For a Löbian machine
in the full sense of yesterday, as I just said, just program a theorem
prover for Peano Arithmetic, or for any "reasonable" part of math. In
fact, all machines rich enough to prove p -> provable(p) for p sigma_1
will be Löbian).
>> 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's not powerful enough to help a third grader with his
homework then it's not in my opinion very interesting, although
there is no disputing matters of taste.
> The formula of Löb is the key formula of the Gödel-Löbian
machine's theology.
You really should buy a dictionary so you can look up that
word.
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.
