On 13 Apr 2017, at 14:11, David Nyman wrote:
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).
OK.
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.
Here you introduce a complexity which I try to not to deal so quickly
with. With the three main hypostases, p, []p & p, there are just
beliefs, and truth (and their conjunction). To perceive require a
reality, and so should be handled with the hypostases using <>t, which
just add that there is a reality.
But I see your point, and at this stage we can temporarily entangled
the formal belief with the perceptual truth. That should not lead to
much difficulties. To equate perceptual truth with truth can lead to
confusion for those who decide that in a dream we are not conscious,
but I guess you are OK with the idea that we are conscious in dream 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).
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.
Yes, but that might be part of the problem.
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).
And also it does not work, as illustrated by the Boltzman problem. The
physical explanation use because there is an implicit thesis of
identity between or first person and body, like if only my body here
could be conscious, but this requires a unique reality. The identity
link can be made by adding infinities in the mind and in the thing
observed, but then we lost the comp hypothesis (and its explanations).
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.
Exactly. The plausibly disappointing comp possible truth is that
hoping is the best we can hope for.
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.
I am sure you do. But in Gödel's work, the difficulty is to keep it in
mind, and to formalize it. let me show you using the representation
explained below, which I cut and past here:
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 see that the symbol 0 is represented by the number 26, that is by
s(s(s(s(s(s(s(s(s(s(s(s(s ...s(0))))))...) (26 parenthesis).
The machine will reason about itself, and at some point, must
understand the difference between 0 (explained by the *use* of the
symbol represented by s(s(s(s(s(s(s(s(s(s(s(s(s ...s(0))))))...) (26
parenthesis), and the symbol, which can only be mentionned by the
represention of "s(s(s(s(s(s(s(s(s(s(s(s(s ...s(0))))))...)", which
here is given (2^27) * (3^17) * (5^27) * (7^17) * (11^27) * (13^17) *
(17^27) * (19^17) .... of length 26.
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.
Good :)
Hope you will see the fun in all this. Take your time. The magical
potion is indigestible when drank too much quickly!
Bruno
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 everything-
[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 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.
