On 24 Feb 2016, at 21:08, Brent Meeker wrote:
On 2/23/2016 12:17 AM, Bruno Marchal wrote:
On 22 Feb 2016, at 18:00, Brent Meeker wrote:
On 2/22/2016 4:38 AM, Bruno Marchal wrote:
In the formal treatment, this is recovered by the fact that G*
proves the extensional equivalence of all intensional variants of
provability, and G* proves the non intensional equivalence of
thoise variants, by constructively ascribing them different
logics (intuitionistic/epistemological for the first person
singular, quantum logic for first person plural and matter, etc.).
Interesting point, but why should we consider intensional non-
equivalence to be anything more than a difference of description?
Because G* shows them to obey to different logics.
Also, []p & p is not just a different description than []p. Not
only the first obeys to a logic of knowledge (S4Grz if you
remember) but it does not admit any 3p description in the language
of the machine (or in arithmetic, as our pet machine is PA). []p
does, it is beweisbar(x), but []p & p does not: it should be
beweisbar(x) & x; but x is a number and not a proposition, so it
should be something like []p & true(p) but true cannot be defined
in the language of the machine (by Tarski-Gödel immediate
diagonalization. And it can be shown that no such predicate can
exist for knowledge (something shown by Kaplan and Montague in
their "paradox regained" paper, reference in my theses: I can show
it if someone asks, as it is a quasi direct consequence of Gödel's
diagonal lemma, or Kleene second recursion theorem when formalized
in the language of the machine).
I'd like to see - or if you can point to a good reference.
The best reference is the original paper of Kaplan and Montague:
KAPLAN D. and MONTAGUE R., 1960, A Paradox Regained, Notre Dame
Journal of
Formal Logic, 1, pp. 79-90.
But see also
THOMASON R. H., 1980, A Note on Syntactical Treatment of Modality,
Synthese, 44,
pp. 391-395.
Let me try to explain.
Do you remember Gödel's diagonal lemma? It says that for any
predicate P definable in the language of the machine (like the
language of arithmetic for the machine or theory like PA), we can find
a sentence k such that PA will prove
k <-> P('k')
k is a self-referential sentence. k says something about itself, in
the 3p view, that is k says something about its 3p description 'k'. It
says P('k').
So,
if a predicate C(x) of knowledge was definable in arithmetic, "not
knowable" would also be definable, indeed by ~C(x), and we would be
able to find, by using Gödel's diagonal lemma, a sentence k such that
PA (or any Löbian machine) could prove
k <-> ~C('k')
In particular we would have
C('k') -> ~k (contrapositive of above)
But for knowledge we need
C('k') -> k,
so C('k') would imply k and ~k
that is C('k') -> f, that is ~C('k'), that is ... k,
and PA, or the Löbian machine would know both k and ~k, that is she
would know something false, which is rather bad for a knowledge
predicate.
QED.
Another way to see that is in the fact that you cannot have
simultaneously
1) []p -> p
2) the necessitation rule p / []p
3) and the Löb formula: []([]p -> p) -> []p. (or more generally the
fixed point property derived from Gödel diagonal lemma for all
definable predicate)
Easy exercice: show that before looking at the solution below!
Solution:
[]p -> p (by 1)
[]f -> f (by 1, specialization p => f)
[]([]f -> f) (by 2), use of the necessitation rule)
[]([]f -> f) -> []f (by 3), the Löb formula, specialization p => f))
[]f (by modus ponens)
f (by line two of this proof []f -> f)
QED
Note that:
G has the necessitation rule and the Löb formula, so it lost the
reflexion
axiom of knowledge []p -> p, as Gödel saw already in 1933.
G* has the reflexion formula and the Löb formula (indeed it extends
G), so it lost the necessitation rule.
S4, the logic of knowledge or knowledgeability, has the necessitation
rule and the reflexion formula, so it lost the Löb axiom (indeed it
lost as shown above the ability to be defined in the language of the
machine).
Machine can bet on mechanism and on a level of substitution, but
cannot justify rationally both mechanism and the choice of the
substitution level. In fact, no machine can know which machine she is.
She has no way to provably or knowingly defined something knowing
exactly what she knows: she needs some act of faith for using an
artificial brain or teleportation.
But what we can do, is for each arithmetical proposition, define
Know(p) by (prove('p') & p). That (prove('p') & p) can be shown to
obey to a logic of knowledge S4 (indeed even S4+Grz), but then the
price is that it does not correspond to any definable predicate (by
the machine). We might think to use (prove('p') & true('p')), but
true(p) itself cannot be defined in the language, for the same reason
as above: if true('p') was definable then false('p') too, (it would be
~true('p')), and by the diagonal lemma again we could find a k such
that PA would prove
k <-> ~true('k')
and PA would prove k <-> true('k') as a truth predicate should ask
for, but then PA can prove k <-> ~k, and that is a contradiction.
Truth and knowledge of a machine are not definable by that machine,
and that play some important role and is why truth will be able to
play the role of the neoplatonist ONE, and the knower will mimic the
neoplatonist notion of soul. With that vocabulary we get easily that a
machine's soul is not a machine (which is a notion definable in
arithmetic) from the machine knowledge or first person point of view.
Of course the divine intellect know that the machine's soul is a
machine, but that belong to G* minus G and is not a knowledge ever
accessible by the machine itself, as far as it remains correct or even
just consistent.
It makes also possible to define consciousness as a form of more
focused knowledge, like
[]p & <>t & p, which is also not definable, and explains why
consciousness and qualia seems so elusive when we (the machines with
comp) try to define them.
Does this help? I can explain the diagonal lemma, but I have already
prove (many times, but some times ago) Kleene second recursion
theorem, and the diagonal lemma is basically its formalization in the
language of the machine, with a proof given by the machine itself.
That lemma is of course one of the main contribution by Gödel in its
1931 paper.
Bruno
Brent
[]p & <>t does admit a description in the language, and correspond
to the "measure one" on the computations when p is restricted to
the sigma_1 sentences. So you might say here that it is "just" a
difference of description, but again, it is enough to get a
different logic, and actually this gives a quantum logic, like
S4Grz provides an intuitionist logic for the internal logic of the
knower.
I hope this answers your question. It is the interest of the G---G*
splitting that it provides different logic for all the intensional
or modal nuances already disserted by the philosophers, from Plato
to Wittgenstein (which made a similar remark to you in its latest
treatise "On uncertainty").
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 [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.
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.
