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?
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.
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. So logicians start from what the first man
in the street already know, and he makes it incomprehensible. 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? 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).
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.
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.
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.
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.
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.
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. 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.).
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 [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.
