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. 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. 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. 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). > 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? > > 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. 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 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! > 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 [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.
