On 12 April 2017 at 20:59, Bruno Marchal <[email protected]> wrote:
>
> 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).
>
Well, I was thinking that is you can *see* that it is raining, then it is
(perceptually or concretely) apparent that it is raining (i.e. it
corresponds with the facts).
>
> 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.
>
But my point was that the formal truth must somehow be entangled with the
perceptual truth, in Tarski's sense, even if not (unavoidably, as you
explain) provably so. Indeed, this idea is at the heart of the comp
explication of the mind body problem. So on that reading truth becomes both
an abstract and a perceptual "notion", as it were.
>
>
>
>
> 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.
>
Yes but that clarity is what will convince the non-specialist. Almost all
philosophy is done at this level.
> 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.
>
Sure, but often that very lack of validity is jump-started by tacitly
assuming something that the explicit explanatory framework doesn't require
or justify. For example, what is the a priori justification for materialism
to make any intelligible claim to have explicated consciousness when it has
already presented a fully-explicable transition from any physical state to
any other, which was its aim? There is no attempt to further explicate the
genesis of any "internal" or subjective position, it is merely assumed a
posteriori on the basis of an ever more detailed analysis in terms of
purely neurological processes, all of which are in principle (and it is the
principle that counts here) fully reducible to the designedly unexplained
primitive level of physics. In so doing the central question of the
relation between physical process and consciousness is "beggared" (drained
of value or impoverished, to recall the fundamental meaning of the
metaphor).
> 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.
>
And yet our ability to "act" as distinct from merely "perceive" depends on
that hope.
>
>
>
>
> 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ç!.è§.
>
Believe me, I understand the distinction. Indeed in my former career, I
was forever trying to restrain system developers under my tutelage from
confusing "understanding" a system from the application of formal methods
to test its correctness.
>
>
>
>
>
>>
>> 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,
>
Thanks for all this. I will read and peruse.
David
>
> 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 [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.
>
--
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.
