On 28 Nov 2017, at 11:56, Lawrence Crowell wrote:
On Monday, November 27, 2017 at 12:19:53 PM UTC-6, Bruno Marchal
wrote:
On 26 Nov 2017, at 21:56, Lawrence Crowell wrote:
and in modal logic it is □p → p.
No, that is the reflexion formula, typically not provable in general
(for exemple Bf -> f, with f representing the constant falsity, or
"0 = 1") expresses consitency (~Bf), which is not provable.
Löb's theorem asserts that the machine will say Bp -> p only when
she actually prove p, which is a statement of modesty. Obviously if
she proves p, she can prove Bp -> p, because p / (q -> p) is a valid
rule in classical logic. But the machine, by Löb's theorem says the
converse, if ever she proves Bp -> p, she proves p.
The formal modal formula is B(Bp -> p) -> Bp.
You are right, it has been a long time since I looked at this.
OK. No problem. I am already glad when people can say "I was wrong".
It means that they have a bit of the scientific attitude.
It looks also like wishful thinking. If you succeed in convincing a
Löbian entity (whose beliefs are close for the Löb rule, or having
Löb's theorem for its bewesibar predicate) that if she ever believes
that some medication will work, then it work, then she will believe
the medication works!
It solves Henkin's problem about the status of the proposition
asserting their own provability: p <-> Bp. We know with Gödel that
those asserting their own non-provability to a consistent system
must be true and unprovable by the system, that is not obvious for
the Löbian sentences, as they could a priori be false and non
provable, or true and provable, but it happens that they are always
true (and provable).
The modus tolens is ⌐p → ⌐□p (⌐ = NOT) which is not the
same as p → □p. The □ means necessarily and ⌐□⌐ means not
necessarily not or possibly abbreviated as ◊ and so ⌐p →
◊⌐p. Godel's theorem illustrates a case where p → □p is false;
Indeed: ~Bf -> ~B (~Bf) (consistency implies non-provability of
consistency).
And so this is an aspect of Gödel's theorem or one way of thinking
about it. I will be honest with physics and information theory I
have found the computation or Turing machine approach more useful.
Gödel's is concerned with the provability notion, Turing was concerned
with the computability notion. In fact Gödel missed the Church-thesis,
and was very close to it, by its use of what we call now the
"primitive recursive functions".
Computability is the only "absolute" notion here (if you are willing
to believe in the Church-Turing thesis). provability is a relative
notion which depends on the formal system under concern. Yet, there
are important relation between provability and computatibility. The
main one is that the restricted sigma_1-provability is equivalent
with Turing universality. But provability in general is not concerned
by this restriction. Simulation and emulation is on the type
computation, not of the type proof. A weak system like Robinson
arithmetic can emulate (simulate exactly) Peano arithmetic, like I can
in principle emulate Einstein's brain, and this without understanding
what the simulation of Einstein explains to me. For example Robinson
Arithmetic can prove that Peano Arithmetic can prove Robinson's
arithmetic consistent, but that cannot convince Robinson Arithmetic.
I has been a while again since I looked at Penrose's approach to
these matters. As I recall he leans heavily on the Cantor
diagonalization.
The whole of Recursion Theory (Turing, Post, Kleene, ...) and
Mathematical logic (Gödel, ...) relies on diagonalisation. It is used
all the times everywhere. Most are constructive, some are not
constrtuctive, and in theoretical AI, like in theoretical theology,
most are necessarily (provably) not constructive.
Turing's demonstration of no universal Turing machine
Turing on the countrary proved the existence of a universal machine
(in math, and later in arithmetic). Then he begun to build one. But
the war arrived and he build only a decoder machine for fighting the
Nazis ... Babbage can arguably be considered as the first one
understanding that "universality" notion, but Turing is the first to
make that explicit and precise.
and the Gödel first theorem on predicates enumerating their Gödel
numbers are a form of diagonalization.
Well, once you can enumerate things (constructively or not like with
Cantor), you can diagonalize the enumeration (constructively or not ).
I can come back on this. few people know that incompleteness is a two
lines consequence from Church-Turing thesis, by a simple constructive
diagonalization. I have already explain this about 5 times on this
list, but it is so short and elegant that I might not resist coming
back to this. It is the starting point of theoretical computer science.
What does concern me is that these mathematics involve infinite
systems, and with physics we can only measure finite quantities.
The universal machine is a finite object. The "infinite tape" was a
pedagogical error. It helps the engineer, but confuse the philosopher.
Once you have an enumeration of all semi-computable functions (of one
argument) f_1, f_2, f_3, .... , a universal machine/number is the
machine/number u such that f_u(x,y) = f_x(y). U is called a computer
(although that term is sometimes only for the physical implementation
of it), x is called the program, and y is the data. (x,y) is supposed
to be one number, coding the list of the two number x and y. You can
code (x,y) by 2^x times 3^y for example.
I has been a thought that somehow physical systems might in effect
approximate Univeral TMs
Not approximate, but emulate them exactly. That is what your laptop is
doing right now. Well, you can say "approximate" in the sense that you
could run out of memory, but the human can run out of memory too and
in that case they will use the wall of the cavern, or a magnetic
disk .... The infinite tape does not need to be actually infinite, but
need to extensible. It is not thought as a part of the machine, which
is really the universal finite code. Wolfram did organize a challenge
of finding the simplest Universal Turing machine, for example. It is
the smallest (if possible) number u such that u applied on the Turing
machine x, with input y, will mimic x behavior on y. Mechanism leads
indeed to a finitism. We need to assume the (finite) natural numbers,
and nothing else. But the machine's internal phenomenology will needs
all the infinities available ... in the mind.
or Gödel's theorem in a truncated or finite manner. This might be at
the intersection of P vs NP and prvability vs undecidability. I am
though not versed enough in these matters to push on with it.
It is above the P/NP problem, which concerns efficiency, not the
existence, or not, of some computations.
Best,
Bruno
LC
a proposition about an math system is true, but is not necessarily
or provably true.
Well the Löbian systems are completely captured by G, for the
provable statement on provability, and G* for the true statement on
provability.
G has axioms
B(p -> q) -> (Bp -> Bq)
Bp -> BBp (redundant, follows from Löb).
B(Bp -> p) -> Bp (Löb)
With the rule of modus ponens and necessitation a/Ba.
G* has as axioms all theorem of G, +
Bp -> p
But lost the necessitation rule. I let you show that G* is
inconsistent if you add the necessitation rule.
If that is false then ⌐□p → ⌐p is false or ◊⌐p → ⌐p
is false. We can then only say that p being true is "possible." This
seems to have some connection with quantum measurement and the
update on knowledge of a system with prior probabilities =
plausible estimates.
I wrote a paper involving Gödel's theorem, but it was not that well
received. I will take a look at the paper on the web. I have a
certain cautionary issue with these sorts of issues. I have learned
lots of physicists take some umbrage with it.
Penrose has repeated old errors in the field, already well addressed
in the literature. That a great mathematician could be wrong on
Gödel wary a bit the physicists. I decided to do mathematics and
mathematical logic to masteries metamathematics, as it solved
already many problem I was interested in in biology and genetics. I
can give you reference on this. Gödel's theorem is only a first big
theorem in a very rich field, and it has important relation with
computer science, and, by consequence, in the computationalist
approach of the mind-body problem.
Bruno
LC
...
--
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 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 everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.
