On 06 Apr 2017, at 22:57, Brent Meeker wrote:
On 4/6/2017 12:35 AM, Bruno Marchal wrote:
On 05 Apr 2017, at 20:46, Brent Meeker wrote:
On 4/5/2017 1:54 AM, Bruno Marchal wrote:
On 04 Apr 2017, at 16:47, David Nyman wrote:
I've been thinking about the Lucas/Penrose view of the purported
limitations of computation as the basis for human thought. I
know that Bruno has given a technical refutation of this
position, but I'm insufficiently competent in the relevant areas
for this to be intuitively convincing for me. So I've been
musing on a more personally intuitive explication, perhaps along
the following lines.
The mis-step on the part of L/P, ISTM, is that they fail to
distinguish between categorically distinct 3p and 1p logics
which, properly understood, should in fact be seen as the stock-
in-trade of computationalism. The limitation they point to is
inherent in incompleteness - i.e. the fact that there are more
(implied) truths than proofs within the scope of any consistent
(1p) formal system of sufficient power. L/P point out that
despite this we humans can 'see' the missing truths, despite the
lack of a formal proof, and hence it must follow that we have
access to some non-algorithmic method inaccessible to
computation. What I think they're missing here - because they're
considering the *extrinsic or external* (3p) logic to be
exclusively definitive of what they mean by computation - is the
significance in this regard of the *intrinsic or internal* (1p)
logic. This is what Bruno summarises as Bp and p, or true,
justified belief, in terms of which perceptual objects are
indeed directly 'seen' or apprehended. Hence a computational
subject will have access not only to formal proof (3p) but also
to direct perceptual apprehension (1p). It is this latter which
then constitutes the 'seeing' of the truth that (literally)
transcends the capabilities of the 3p system considered in
isolation.
I don't think so. It is not direct perceptual "seeing the truth";
it is an inference in language and depends on language.
?
It is not an inference, but the recognition of a fact, like when a
smoke detector detect smoke.
But the fact that is "recognized" is that the Goedel sentence is (in
Goedel's language which he has encoded in arithmetic) says it cannot
be proven - and then one infers that the axiomatic system cannot be
completed. I don't see how any of this can even be considered
without language and inferences.
I am not sure why you say this. I was talking about the p in "[]p &
p". You can't apply Gödel on this because the truth of p cannot be
defined in arithmetic. That is how the first-person escapes
incompleteness and can believe consistently to be consistent (or even
complete). S4Grz does prove <>t. The problem is that its reference to
truth makes it mute on basically any question. Indeed, it cannot use
language or inference. Axiomatically, it is a knower, and knower are
not machine from their own point of view. Only G* knows that []p = []p
& p, the machine can't know that.
Let us write [m]p for the machine proves p, and [1]p by I know p. f is
for "0=1", say. The error by Lucas and Penrose is that we know that
the machine is consistent (even correct) so we can say
[m]f -> f
But the machine cannot, so I am superior to that machine. But if we
are machine, we can't say [m]f -> f with m being my body-machine. Oh,
said Penrose, but we, human, knows [1]f -> f, and we would know that
[1] = [m] if we believe in mechanism. But that is wrong, we don't know
that [1] = [m]. We can only bet on it, and the machine can do that bet
too. In fact the machine can define its own knowledge for each
particular proposition by [1]p = [m]p & p, like us, and realise that
this can only belong to its own G* minus G, by *assuming* its own
correctness at the metalevel. Then she is computationalist, but remain
consistent only if she does not assume this at the ground level. She
has to admit that to enter the telportation box, his hope to survive
cannot be justified, making its own belief in computationalist into an
act of faith. Its modesty requires it mentionning it is theology.
There is an implicit assumption of being awake, or not dreaming,
but still no inference, nor does it use language,
Who does proofs without language?
The experiencer, or intuitionists mathematicians. Not to confuse with
the metamathematics of intuitionism. When you put your hand in the
fire, you don't say: I don't understand could you elaborate on the
proof? You just put your hand quickly of the fire, without needing to
verify a proof.
at least not necessarily. The smoke detector detects smoke through
it senses, and so believe in some representational sense that there
is smoke (the [](smoke)), and ... there is smoke (the p of []p & p).
Which is an instance of physical perception - not logical proof.
Yes. That's the point. And when we do informal proof, like in math,
physics, etc., there is always a stage when that happens. The personal
conviction is always beyond language, and as such non communicable/
justifiable. It is relatively communicable in between entities
agreeing on some intuitive truth, like 0 ≠ s(x). That requires some
faith in at least one reality, like the standard model of number
theory, or a physical world, or Zeus, whatever.
Bruno
Brent
--
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.
