On 11 Apr 2017, at 18:21, David Nyman wrote:
On 10 April 2017 at 18:32, Bruno Marchal <[email protected]> wrote:
On 10 Apr 2017, at 12:58, David Nyman wrote:
Over the years there have been many references to various modal
logics deployed in support of the comp theory, in particular for
the analysis of categorical distinctions between third-person and
first-person logical consequences. Trouble is, when Bruno refers to
these logics in explanation of his points, the presentation is so
technical that I for one have never been able to follow these
technicalities sufficiently well for them to become intuitively
obvious. Hence I've had to come up with my own amateur versions.
As David Hilbert famously said "A mathematical theory is not to be
considered complete until you have made it so clear that you can
explain it to the first man whom you meet on the street.". I wonder
whether it would be possible, Bruno, for you to contrive some sort
of "man in the street" presentation of the key logics deployed in
your arguments and why indeed you regard them as so central. I
suspect that this is closely related to the process you describe as
interviewing the machine.
Propositional modal logic is classical propositional logic with one
symbol more, usually, written with a box "’[]". It denotes an unary
operation. This means that if A is some formula, like (p -> p), []A
is also a "grammatically correct formula", meaning that [](p -> p)
is a formula.
Originally, modal logic was conceived, like logic itself, by
Aristotle, although he did not use any special symbol, but he used
the word "necessary" and "possibly", and used it to make his famous
"Aristotelian square":
Necessary -------------- not-necessary
necessary-not ---------- not-necessary-not
Now, not-necessary-not is the same as possibly. It is not necessary
that man is not rational is the same as "it is possible that man is
rational". "Possibly" is the dual of necessary, and is usually
abbreviated by the symbol diamond "<>". By definition it is ~[]~. We
could have used <> as primitive, and define [] by ~[]~, and write
Arstotle's square in the following way:
Not-possibly-not -------------- possibly-not
Not-possibly ------------ possibly
When the box [] and diamond <> are used to denote "necessity " and
"possibly" in some metaphysical, sense, we say that it is alethic
modal logic. Leibniz, much later, will provide a sort of semantic
for it by interpreting the necessity by "truth in all possible
world", and the possibility by "truth in at least one world". This
can help to agree that alethic modal logic, see as a theory (set of
axioms), can admit as axioms the following formula:
[]p -> p (if p is necessary, then it is true)
[]p -> [][]p (if p is necessary then it is necessary that it is
necessary)
<>p -> []<>p (if p is possible, then it is necessary that it is
possible)
Now a theory is not just a set of axioms. It is a set of axioms
together with inference or deduction rules. Most logic have the
modus ponens rule, from a proof of A and a proof of A -> B, you can
deduce B.
The so-called *normal* modal logic have the modus ponens rule and
the necessitation rule, which says that if you have a proof of A,
you can deduce []A. They have also (by definition of normal modal
logic, the axiom [](p -> q) -> ([]p -> []q). In Leibniz theory,/
semantics, you can verify that if (p -> q) is true in all words, and
if p is true in all worlds, then q is true in all worlds. OK?
OK
Different modal notion will have different axioms, and sometimes
different inference rules.
Now, modal logic is used in the "machine interview" to simplify a
lot the situation. The real difficulty, which is more demanding in
term of lengthy formalities, is the provability logic. Gödel
succeeded in translating "A is provable", with A put for some
arithmetical formula (like "s(0) = 0") in an arithmetical formula.
That is longer to explain, I will proceed later.
Tell me if you are OK up to now. We might also need to revise a bit
"simple" classical propositional logic, and to illustrate the
difference between
- this theory proves A (for A some being a classical proposition
formula, like (p -> q))
- this model satisfies A.
OK so far.
The idea that we can explain things to the man in the street is a
bit inapt in this context, because the difficulty of logic is that
it is necessary to NOT understand the formula, and to see that they
are manipulated formally only.
Yes, I do see the difference. Important point.
So logicians start from what the first man in the street already
know, and he makes it incomprehensible.
Good, only the incomprehensible is worth our time and effort!
For example take the formula (p -> p). the man in the street will be
OK with that formula being a tautology, that is an always true
formula. (p -> p) seems obviously true whatever proposition is
represented by p. If p = "it rains", it seems obvious that if it
rains then it rains, etc. OK?
Yes, I think this is equivalent to Tarski's criterion of
correspondence with the facts, or what I called perceptual
correspondence.
Actually I was just saying that it is obvious that (p -> p), but only
by alluding to the truth table, or that anyone will accept that IF it
rains THEN it rains, which is not clearly something we can percept, or
perhaps (but I was not thinking to Tarski here).
For the propositional calculus, truth, or a model, is defined by a
function from the set of propositional letters to the set {0, 1}. So a
model, in the sense of logician is an assignment of 0 or 1 to each of
p, q, r, p1, q1, r1, p2, q2, ...
So truth is an abstract notion. To give a concrete example, we can
interpret p by Hillary Clinton won the 2016 election, q by "Donald
Trump" won the 2016 election. Then we will say that (p & q), for
example, is true or satisfied, in the model where both Hillary won and
Donald won. At that level, in the concrete illustration, we will refer
to some perceptual judgment indeed. I am just no sure how we could
perceive an implication except by using the equivalence between (p->q)
and (~p V q), but that assumes either the truth table or some
intuition, and the proof of (p->p) was given to illustrate a way to
proceed which do not refer to any intuition, nor any notion of truth,
but only formal rule.
In fact, you cannot perceive the truth of (p -> p), because p is
abstract, and eventually intended for all proposition. You would need
to perceive all proposition like If there is a unicorn on the planet
venus then there is a unicorn on the planet venus, and this for all
imaginary and real animals, on all planets in the whole multiverse.
Yet, if the current theory is the giving of the two axioms:
A1 p -> (q -> p)
A2 (p -> (q -> r) ) -> ((p -> q) -> (p -> r))
With the inference rules modus ponens, and some substitution rule,
it will be rather difficult to find a proof of (p -> p).
But here, all what the man in the street is asked is in 1)
understanding that this is difficult, and 2) being able to verify if
a proof is indeed a proof, that is, a sequence of formula which
starts from some axiom, and use only axiom, or formula derived from
the axioms using only the given inference rule. Even that can be
very complex, and usually we add comment to help (like the comment
in a program).
Yes, this is important. Failing to do this, even in informal
reasoning, leads directly to question begging, as I'm fond of
pointing out.
The informal reasoning is at the level of the comment. We can only
hope to be enough clear. The formal reasoning iis at the object level:
it is the deep engine. No biologist will ever claim that you have to
write a book in biology using only strings of A, T, G, and C. The
study of those is done formally in english.
When you see someone begging the question, usually it is just because
they made an non valid informal reasoning.
Don't worry, I am aware I have not been clear enough, on this subtle
point. Russell and Whitehead missed it too, and physicists never
understand. In fact, biologist have less problem in general.
And just to make pleasure to John Clark, that is a point missed by the
greeks, and even the earlier modern logician.
All the more pernicious when (as is usual) the smuggling in of
auxiliary assumptions is almost always tacit and unrecognised.
Here is a proof of (p -> p):
1) (p -> ((p -> p) -> p) Axiom A1, with q substituted by (p -
> p).
2) (p -> ((p -> p) -> p) -> ((p -> (p -> p)) -> (p -> p)) Axiom
A2 applied on "1)", that is axiom A2 with q substituted by (p ->p)
and r by p.
3) ((p -> (p -> p)) -> (p -> p)) (by modus ponens on 1) and 2) ),
4) (p -> (p -> p) (Axiom A1 with q substituted by p),
5) (p -> p) By modus ponens on 4) and 3).
You might ask: why do you logician makes things obvious looks
becoming so complicated? Why not use a truth table and settle the
matter in less than a second?
The answer is that in most theories there are no simple method to
find a proof or to show that a model satisfy a formula, and the
modus ponens will be the main engine that we will have to describe
to translate "provable" later in arithmetic.
Yes, and also because it calibrates or tests that the formal
mechanism actually shadows or mirrors the informal correspondence.
In simple case, luckily. But later we will see that no machine can
ever proves that such a correspondence is satisfied. The machine will
still be able to hope, pray, ...
*We* will able to believe in such correspondence for simpler (than us)
machine, because we do have some intuition on numbers that we share,
but we lost the "obviousness" of the correspondence for machines whose
complexity or probability power will match our's.
We could perhaps say that Theatatus criterion of justified+true
(i.e. believes correctly that it is true + it is true) is reconciled
with the Tarski criterion of (perceptual) correspondence with the
facts (e.g. where snow being white is perceived as "analytically"
true in face of the facts).
Yes. It enforces it, and we can make sense of it for the simple
machines we trust.
The proof 1-5 given above is not given to convince anyone that (p-
>p) is a tautology. It is given to illustrate a proof, and to see
that some very simple theory embedded in some machine can prove it.
Calibration again?
Not sure. See above. And don't get nervous, logic is a science which
has the most complex beginning. I see that you still want to interpret
the logical formula (which is normal giving the role they will have).
But the point is that they are not interpreted at all. They have
intended interpretation, of course, that is why we use symbol
reminding the goal, but that is why people introduced to logic can
miss the first step. You need to look at (p->p) like you would look at
O9ç!.è§.
You must look at such proof as like it was a piece of DNA, and it
will be the main object that we will have to represent in arithmetic
later, to define provability in arithmetic, and see what this or
that theories can prove about it, and if that is not captured by
some modal logic (and you know that the answer will be affirmative,
as we will get G and G*, two very special modal logics describing
what machine can say about themselves, in the 3p ways first, and
later, why we will have that although G* proves (([]p & p) <->
[]p), yet G does not, making the "knower" existing, in some sense,
yet not being *any* machine from its points of view. But I guess
now, I have accelerate too much.
Yes, but this is the nub of my question, so let's not forget it.
I am not. I am just trying to make myself sure that you do not try to
understand the syntax, except for the procedural modus ponens rule.
You need only to agree that the following is a valid proof of
O9ç!.è§.
axiom a
##&!çç -> O9ç!.è§
axiom b
##&!çç
Proof of O9ç!.è§
1) ##&!çç (by axiom a)
2) ##&!çç -> O9ç!.è§ (by axiom b)
O9ç!.è§ (by the modus ponens rule applied on line 1) and 2).
To be sure, when we have proved (p -> p) we have used another rule
(substitution), but let us forget it for now.
Perhaps, in my language, G* "knows" truths relating to "perceptual"
facts (where perceptual stands for informally true in this context);
IOW truth here, informally, is whatever can be seen to correspond
with those facts. Then the capacity of the machine, in some sense,
to navigate by means of G* renders it an informal knower with
respect to the "facts" it perceives. But the informality of this
logic (and hence unavailability of formal proof procedures) means
that G* cannot recapitulate it mechanically and consequently cannot
appreciate itself as a machine in this sense.
G and G* knows truth about the machine. In the case of G, the machine
can prove them. But G* extends it with the whole truth (limited to
some special statement). G* knows what G knows, but incompleteness
makes G* minus G non empty (and quite large). G* knows G and the truth
in the corona G* minus G.
We will believe/prove that such truth corresponds to informal
arithmetical "fact" that we are willing to take as true, indeed. Each
one has to ask himself if they really believe things like the
irrationality of sqrt(2), which is equivalent with ~(ExEy(x*x = 2
*y*y). The legend is that Pythagorus sacirficed many cows to celebrate
the discovery. And that was kept secret; it seems a pythagorean get
killed for having explain this out of the circle of initiate ....
The "informal" will be captured "meta-formally" by S4Grz, and G* will
"see" that this makes sense. The machine will not see this. Neither
its 3-self (which will be described by G and G*) nor its 1-self, which
will be captured by S4Grz, will ever make complete sense, except the
day she bet on computationnalism and also self-correctness at the meta-
level.
G* will prove ([]p) <-> ([]p & p)
But neither G, nor S4Grz will ever be able to prove that. Here the
machine will discover that there are truth about her that would make
her inconsistent if she took such truth as axiom.
So you are close to right: G will justify later that some truth, from
the 1 and 3 view of the machine can only remain informal. Ineffable
even.
But for this, I have to explain more about PA's provability. It will
work for all mechanist extension of PA, as long as they are
arithmetically sound.
G will be the normal modal logic with the Löb formula []([]p -> p) -
> []p. It axiomatizes completely the logic of any mechanical
extension of PA.
G* will be the non normal modal logic, loosing the necessitation
rule, extending G, + the formula []p -> p.
Likewise, S4Grz, the "universal soul", the logic of a new box [o]p
defined by ([]p & p), will be axiomatised by a normal modal logic
with the (strange looking) formula:
[]([](p -> []p) -> p) -> p
due to Grzegorczyk. Gödel incompleteness makes "provability" into a
notion of belief (it can be wrong), the theaetetus idea makes it
into a logic of knowledge, and it obeys Brouwer axioms for the
"first person knower": it cannot be defined in arithmetic or in the
language of the machine, it has a temporal dimension, and it makes
possible to build an arithmetical interpretation of intuitionist
logic.
Need more on this!
Let us fix one or some simple machines: RA or PA, or even an unknown M
talking the same *language* (perhaps unsound, or inconsistent in its
belief (the axiom and their consequences)
The language is the arithmetical language. That means that RA's or
PA's assertion are grammatically correct sequences of symbols
belonging to two sorts of symbol;
- the logical one: v, &, ->, ~, E, A, t, f, plus the variables x, y,
z, u, v, ... (plus the parentheses)
- the arithmetical one: +, *, s, 0
Exemple
Ex(s(0) +s(0) = s(0)) is a grammatically correct arithmetical sentence
(intuitively false, but we should not care about this at this stage).
Note that the quantifier Ex is dummy, as x is not in the formula, but
this is allowed.
EEx(s(0) +s(0) = s(0)) is not grammatically correct, because EE is not
allowed,
Ex(x + x = x) is grammatically correct.
Ey(x+x = x) also, again Ey is dummy, but we allow it just because this
will simplify our lives.
(x+x=x), likewise, this is grammatically correct
x++x=* is NOT grammatically correct.
To define cautiously what is a grammatical correct sentence would be
long, and can frighten the beginners, especially that the math
involved here might used more than what RA can prove, or as much than
what PA can prove.
Now, the difference between RA, PA and M, is that they have different
axioms, and perhaps different inference rules. We can address them
later.
Gödel's beweisbar predicate. It is supposed to be an arithmetical
formula translating the statement asserting that PA proves F, with F
some arithmetical formula, *in* the language of PA. beweisbar(F)
should mean F is provable by PA, written in the language of arithmetic.
It is what I usually denote by "[]A", and it is the one whose logic
will be axiomatized by G and G*.
At first sight that seems impossible. PA or M seems to talk only
about numbers, and says think like Ex( s(s(0) + x = 0) or alike.
There is no miracle, nor magic. To explain to a German how to make a
pizza, you need to express yourself in german. It is the same with PA,
RA or any machine M which has only the language described above.
Beweisbar means provable in german, but PA does not know german, and
so Gödel was forced to explain what is a proof to PA.
We have defined a proof by a sequence of formula such that the formula
is either an axiom or derived by modus ponens from axiom or from
formula previously derived. And what is a formula: it is a
grammatically correct sequence of symbol. And what is a symbol?
To explain what is a symbol to PA, we will simply proceed like we do
with human. As PA knows only the term/object 0, s(0), ...We will just
say that this number and that number will be used for the symbols. The
intended meaning will be provided by the use of those symbols, later
by PA, RA, or M.
So let us denote the logical and arithmetical symbols v, &, ->, ~, E,
A, t, f, "(", ")" =, 0, s, +, *
by the first odd numbers: 1, 3, 5, 7, 9, 11, 13, 15, 17, 19, 21, 23,
25, 27, 29,
You have the lexicon
English French Logician Arithmetic
or ou v 1
and et & 3
if then si alors -> 5
not pas ~ 7
it exists Il existe E 9
For all pour tout A 11
..
..
plus plus + 27
times times * 29
The number 1, 3, 5 appearing there abbreviates s(0), s(s(s0))),
s(s(s(s(s(0))))), ... (the arithmetic language does not contain the
symbol "1", "3", ...
We can denote the countably (but infinite) many variables by the even
numbers
x is denoted by 2
y by 4
z by 6
x1 by 8,
x2, by 10
x3 by 12,
etc.
So you see, now PA, is able to get what a variable is, it is
informally captured by the formal predicate even(x), that is Ey(x =
s(s(0)) * y).
Here I do use the fact that you can understand such formula, and PA,
thanks to its axiom, can too, but this is for later.
You might prefer Variable(x) = Even(x) & (x ≠ 0), that is Ey(~(x = 0)
& x = s(s(0)) * y), to avoid like above to use 0 as a variable, which
might lead to some bugs ...
You can define Arithmetical-symbol(x) by: ((x = 23) v (x = 25) v (x
= 27) v (x = 29))
OK? Humans do not know much. If you ask what is a variable, they will
say something like "letters at the end of the alphabet, or the same
with subscript) a long time before digging on possible deeper meaning
on such a notion. It is good pedagogy to do the same with RA, PA, M.
Now what is a formula? It is a sequence of symbols (obeying some
grammar)
So we need to define a sequence of symbols. We cannot just say that
Ex(x=x) is represented by 9 (the symbol for "E") followed by 2 (the
symbol for "x", followed by 17 (the symbol for "("), 2 again for x,
21 ("="), 2 again, and 19 (to close the parenthesis 17).
This does not work, because we don't have defined "follow".
There are many ways, and Gödel will use the fundamental theorem of
arithmetic for this task. That theorem say that all natural numbers
admits one and only one decomposition into product of primes (up to
the order of the multiplication). This suggests representing the
formula Ex(x=x) by
(2^9) * (3^2) * (5^17) * (7^2) * (11^21) *(13^2) * (17*17),
At the left of the exponentiation, "^" you see the ascendent prime
numbers, and at the right of the exponentiation ^, you have the
variable, in a language that PA, RA and M can "understand".
To define the predicate (adjective, property, or relation) like
Formula(x), capable of defining, you need to define "grammatically
correct" in terms of those numbers and using addition, multiplication,
and what has been just define (variable(x), sequence(x), etc.). I skip
this for now.
Note we don't have the symbol "^" in our language. It is "easy" to
define it "recursively", but, alas, to explain "recursively" to PA we
need the finite sequence. So it is a bit more tricky to do that. Gödel
did use an Antic (Sorry John) Chinese insight in modular arithmetic
(known as the Chinese Remainder Lemma. Hmm... if you want, later.
There are many other ways, some very beautiful, like by Smullyan, and
others.
Well, beweisbar will be the translation of provable in the
arithmetical language (this does not depends on any axiom or belief by
the machines, as a matter of translating a definition into a language.
Then RA, PA, Me, and You, will differ by our basic belief, and have
our own beweisbar predicate. Human have a big non monotonic layer,
which does not obey to any of this, but to extract the theology and
the physics, that does not matter (for the evolutionary biology and
psychology, that does matter).
Now, a proof made by machine M, or PA, or RA, is a sequence of
formula, so that each one is an axiom (with respect to each system of
axioms) or a formula obtained by the preceding one by modus ponens.
But a sequence of formula is just a sequence of sequence of symbols,
so a proof will be translated by reapplying the idea above.
For example, the proof (where a typical first order logical inference
rule is used, "known" by RA, PA and M (and some humans, if they remind
that I use Ax with the intended meaning "for all x".
Ax(x=x)
(0 = 0)
is represented/translated in arithmetic by
2 ^ (the number representation of Ax(x=x)) * 3 ^ (the number
representation of (0 =0))
That is
2 ^(2^9) * (3^2) * (5^17) * (7^2) * (11^21) *(13^2) * (17*17) * 3
^ <exercise! :) >
Sorry have to go,
Bruno
We will have a theorem (by Solovay) that G proves a modal logic
formula if and only if its translations in arithmetic, with []A
becoming beweisbar(gödel-number-encoding of A), A being any
arithmetical sentence, is provable. And G* will proves all such
provability statements which are true, even when non provable by PA
or the mechanical extension concerned. G and G* sum up infinities of
interview of the machines and their mechanical descendent, as long
as they are arithmetically sound.
And this!
There is a beautiful tryptic between G, G* and S4Grz. Let us call
[]p -> p reflexion (formula):
G has Löb and necessitation, but lack reflexion,
G¨has Löb and reflexion, but lacks necessitation,
S4Grz has reflexion and necessitation, but lacks Löb.
No system can have Löb, necessitation and reflexion. Indeed, with
those three we would have, with f put for some false formula, like 0
= s(0), that is 0 = 1:
1) []f -> f by reflexion,
2) []([]f -> f) by necessitation,
3) []([]f -> f) -> []f by Löb, with p substituted by f,
4) []f by modus ponens on 2) and 3),
5) f (by modus ponens on 4) and 1).
Löb is enforced for all *machine* which are correct, and believe in
elementary operation and enough induction axioms. We can come back
on this.
I let you rest a bit.
Phew!
I have just made a little grand tour. Feel free to ask any question
or make any critics. I insist, the main difficulty in the beginning
of logic, is to understand that you should not understand the
symbols. You need only to be able to verify some formal very
elementary mechanical comparison. Then the semantic will also be
treated "formally" using powerful mathematics (sets, trees,
topological space, Hilbert spaces, etc.).
Good, but I guess I was also asking for some sort of shortcut to
the intuitive power of all this, because if the only route to this
is more of the above (however interesting in itself) then the point
will go on being lost not only on the majority in this forum (unless
I'm very much mistaken) but a fortiori on any possible wider
audience. Which would be a pity.
David
Bruno
PS I guess you have missed my early introduction to modal logic on
this list, many years ago! No problem.
Thanks in advance.
David
--
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 everything-
[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.
--
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.
