Re: Request to Bruno re modal logic

[Bruno Marchal]

On 14 Apr 2017, at 19:31, David Nyman wrote:


On 14 April 2017 at 17:59, Bruno Marchal  wrote:


On 13 Apr 2017, at 19:26, David Nyman wrote:


On 12 April 2017 at 20:59, Bruno Marchal  wrote:

2 ^(2^9) * (3^2) * (5^17) * (7^2) * (11^21) *(13^2) * (17*17)   *
3 ^ 


​Oh, I see what you mean:

3 ^(2^17) * (3^0) * (5^21) * (7^0)​ * (11^17)



Now, you see it was easy, and, like me, you go fr ... too much  
quickly.


Even without quoting the dictionary we can suspect some mistake. And  
I hope I will not put my finger where it might hurt in case you have  
been mentally abused by a sadistic mathematical teacher!


​Possibly, but I think I've recovered ​from any lingering PMSD ;)


Good!






That one would ask you what is the value of (3^0) ? and what is the  
value of (7^0)?


And you would panic, thinking like ... hmm... er... 3^2 = 3 * 3, 3^1  
= 3, 3^0 = .. !!! . gosh that one is tricky!


​Fortunately you had explained well that it was just a coding  
system.


Yes. But notice that I have tried to avoid, this time, the term  
"code", because it is more a translation, like in German or in a  
natural language. It is partly conventional, but the structural  
relations between the numbers will be isomorphic in different  
languages, and is not conventional.





In fact in the past I have managed to disabuse myself of unnecessary  
confusions of this sort by realising​ that something was simply a  
notation or naming convention. Are irrational numbers, after all,  
insane?


They are not insane, but the fact that 2xx = yy has no solutions  
(except x = 0 = y) is not conventional, and does not depend on a  
coding. That is important for having later real pain and pleasure for  
the machine, and not conventional behavior only.




And why is x^0 always 1? (that way you can always add the exponents).


Yes, it is a good theory.






Well, (a^b) * (a ^ c) = a ^(b + c), that is obvious for a, b, c  
natural numbers, and if you want keep this true for all integers,  
you will have that 3^0 = 3^(5 - 5) = 3^(5 +(-5)) = (3^5) *(3^(-5)) =  
(again to keep that law on the integers) = (3^5)/(3^5) = 1.


same reasoning for (7^0) = 1.

But 1 is not a prime number, and if we allow it in our coding, it  
would become ambiguous. In fact 1 has been thrown out of the prime  
to get a simple enunciation of the fundamental theorem of  
arithmetic: there is only one decomposition into prime factors. if 1  
was a prime number, you can add it, as a factor where you want!


That is why, normally, 0 has been represented by non null number, as  
any number ^ 0 = 1.


I say normally, I will now search the dictionary logic-arithmetic  
(seen as languages), and I pray I did not make a typo!


I said:

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,



So, I did not (at least here). 0 has been represented by 23. (If my  
glasses does not fail me). Let us verify * is 29, + is 27, s is 25,  
0 is 23.
(A chance my recent cataract surgery has succeed!  I have an  
implant!).


​I see (and so do you, I trust). Good health!


Thanks. If only we knew the jaws has much well as the eyes ... The  
human jaws articulation is less known than even the brain 





​

So you should have written:


3 ^(2^17) * (3^23) * (5^21) * (7^23)​ * (11^17)



(I guess my talk about was not necessary, .. you did just forget to  
represent 0,  with a notion known by the machine.


​Yes, I suspected I​ was ​succumbing to the use/mention  
distinction, which you warned me about​. But​ alas​ I ​looked  
too quick​ly and managed to miss where the symbol for 0 had been  
mentioned​, so I relied on the expectation that you would kindly  
correct me.​ Thanks!​


Fair enough :)










PS Are "(" and ")" meant to be the same?


Ah! Now, that is *my* error, which you should not have copied, given  
that you detect it. ts, ts, ts 


​So we were equally sloppy in this case! Mea culpa though.


The teachers can be as sloppy as the learners, but usually only the  
learners get bad notes (grin).






​

So the correct answer is


3 ^(2^17) * (3^23) * (5^21) * (7^23)​ * (11^19)



And so the proof

Ax(x=x)
(0 = 0)

is translated in arithmetic-language in the number


2 ^[(2^9) * (3^2) * (5^17) * (7^2) * (11^21) *(13^2) * (17*17)]
*   3 ^ [(2^17) * (3^23) * (5^21) * (7^23)​ * (11^19)]




The only important things is to see that this is just one number,  
written s(s(s(s(s(s(s(s ... s(0)...), and quite huge (!). Once  
the machine believes in addition and multiplication, it will denote  
the proof, and the machine will be able to answer question like  
"does a variable occur in that proof?", etc.


Very good David, welcome to logic! (and sorry for being long, and  
probably too short in my next answer to the other posts as ... time  
flies like an 

Re: Request to Bruno re modal logic

[Bruno Marchal]

On 13 Apr 2017, at 16:23, David Nyman wrote:


On 13 April 2017 at 14:56, Bruno Marchal  wrote:

Hmm You seem to want to replace the Outer-God, by the Inner-God.  
That is a risky move toward solipsim. S4Grz does not see the gap,  
but it does not see the other minds either.


​But that's just it. We cannot ever "see" the other minds, nor even  
our own for that matter, however much we examine mechanism. But we  
can believe in them, as we do in our own.


We can feel our mind, and cannot feel the mind of the other.

We can believe in our mind, without doubt. But we cannot believe in  
other mind, without doubt. They might be p-zombie, instant-creature in  
a dream, hallucination, or something else.


S4Grz (the 1p described by S4Grz, to be precise) is indeed  
solipsistic, even close to Brouwer solipsism/intuitionism.





Perhaps the least confusing conception of this (following Hoyle's  
heuristic, which as you know I'm fond of) is to conceive the soul as  
indeed a soles ipse, though one with innumerable personifications,  
each profoundly amnesic with respect to the others.


Yes. That fits S4Grz. In the "machine theology", it plays the role of  
Plotinus "universal soul", which is below the divine intellect (here  
G*) and God (here denoted cryptically without any name by p, put for a  
generic true arithmetical proposition (you can "define" God here by  
the set of true arithmetical sentences: Warning: it is a highly non  
computable set).





But surely that must be true of any computational device capable of  
compartmentalising one program's states from another's. Is this then  
the Inner-God?


That is a slight generalization. The salvia plant is "OK" with this,  
but it makes non universal machine conscious, and then even more  
conscious than the universal machine. It is unclear how will the much  
simpler machine consciousness differentiate?


The theology of too much simple machine can degenerate, a bit like  
attempting to divide by zero. They will have "God's consciousness",  
out of time and space, and unique, in a, needless to say, highly  
dissociated state.


How frustrating, your fridge (assuming that kind of things exists)  
knows as much as God, but it flies so high that it can't hear your pray.




Perhaps, in concrete or perceptual form. But surely the abstract  
Outer-God is still evidenced in that maximally-compressed creative  
widget you call the UD?


Only after the machine's "blasphem", when she identify herself with  
god:   p <-> []p.


This is going near a death experience, near inconsistency, near []f.

With computationalism, we limit p to the sigma_1 sentences. They are  
arithmetical translation of halting computations. The creative widget  
is equivalent with Robinson Arithmetic. But the computationalist  
machine I define (in Robinson arithmetic) believes in the induction  
rules, and so it can prove that it is universal. In fact it can prove,  
like PA and ZF (where the "[]" denotes their own provability predicate):


   p -> []p

(given that we limit ourself to p sigma_1). It is a theorem of G1  
(axioms of G + (p -> []p))



Do we have []p -> p?

Well, that is trivially true, given that we study the correct machine,  
by choice. We believe also that it is true for simple machine that we  
trust, like PA, and ZF (for many).


But, and very importantly, no machine at all can prove that about  
itself. Only their divine intellect do: G* proves []p -> p (for those  
correct machine). Note that the theology is personnalized for each  
machine (as many "’[]" than machine), but are isomorphic and followes  
the G, G*, S4Grz laws for the correct machines.



So the blasphem is true (G * proves p <-> []p), but the consistent  
machine will remain silent on this,


That is a blasphem too, if said by the machine about itself.  We are  
in the corona G* minus G.


A good sum up diagram of the 8 "hypostases" or "type of points of  
view"  (make sure your window is big enough: you should se,  
coincidentally, a sort of diamond above a a sort of square):



Truth

G1 G1*   (the provable part of the provability  
logic, and G1* gives the whole bigger truth about the provability and  
consistency logic


  S4Grz1 (the 1-p, the first person, the  
universal soul, the inner-god, the "creative germ", the "terrible  
child", the solipsist)


--

Z1Z1*(intelligible matter)
X1   X1*(sensible matter)


G1* proves the seemingly ultra-blasphemic collapsing of the whole  
adventure (writing a <-> b <-> c <-> ...  for (a <-> b) & (b <-> c)  
& ...)


 G1* proves p <-> []p <-> ([]p & p) <-> ([]p & <>t) <- 
> ([]p & <>t & p).


But G proves none of those equivalence, making the machines view  
obeying quite different logic (leading from the start to some tension/ 
schizophrenia).



Take it easy. I dig toward the 

Re: Request to Bruno re modal logic

[David Nyman]

On 14 April 2017 at 17:59, Bruno Marchal  wrote:


> On 13 Apr 2017, at 19:26, David Nyman wrote:
>
> On 12 April 2017 at 20:59, Bruno Marchal  wrote:
>
> 2 ^(2^9) * (3^2) * (5^17) * (7^2) * (11^21) *(13^2) * (17*17)   *   3 ^
>> 
>
>
> ​Oh, I see what you mean:
>
> 3 ^(2^17) * (3^0) * (5^21) * (7^0)​ * (11^17)
>
>
>
> Now, you see it was easy, and, like me, you go fr ... too much
> quickly.
>
> Even without quoting the dictionary we can suspect some mistake. And I
> hope I will not put my finger where it might hurt in case you have been
> mentally abused by a sadistic mathematical teacher!
>

​Possibly, but I think I've recovered ​from any lingering PMSD ;)


> That one would ask you what is the value of (3^0) ? and what is the value
> of (7^0)?
>
> And you would panic, thinking like ... hmm... er... 3^2 = 3 * 3, 3^1 = 3,
> 3^0 = .. !!! . gosh that one is tricky!
>

​Fortunately you had explained well that it was just a coding system. In
fact in the past I have managed to disabuse myself of unnecessary
confusions of this sort by realising​ that something was simply a notation
or naming convention. Are irrational numbers, after all, insane? And why is
x^0 always 1? (that way you can always add the exponents).


> Well, (a^b) * (a ^ c) = a ^(b + c), that is obvious for a, b, c natural
> numbers, and if you want keep this true for all integers, you will have
> that 3^0 = 3^(5 - 5) = 3^(5 +(-5)) = (3^5) *(3^(-5)) = (again to keep that
> law on the integers) = (3^5)/(3^5) = 1.
>
> same reasoning for (7^0) = 1.
>
> But 1 is not a prime number, and if we allow it in our coding, it would
> become ambiguous. In fact 1 has been thrown out of the prime to get a
> simple enunciation of the fundamental theorem of arithmetic: there is only
> one decomposition into prime factors. if 1 was a prime number, you can add
> it, as a factor where you want!
>
> That is why, normally, 0 has been represented by non null number, as any
> number ^ 0 = 1.
>
> I say normally, I will now search the dictionary logic-arithmetic (seen as
> languages), and I pray I did not make a typo!
>
> I said:
>
> 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,
>
>
> So, I did not (at least here). 0 has been represented by 23. (If my
> glasses does not fail me). Let us verify * is 29, + is 27, s is 25, 0 is 23.
> (A chance my recent cataract surgery has succeed!  I have an implant!).
>

​I see (and so do you, I trust). Good health!
​

>
> So you should have written:
>
> 3 ^(2^17) * (3^23) * (5^21) * (7^23)​ * (11^17)
>
>

> (I guess my talk about was not necessary, .. you did just forget to
> represent 0,  with a notion known by the machine.
>
> ​Yes, I suspected I
​ was
​succumbing to
the use/mention distinction, which you warned me about
​. B
ut
​ alas​
I
​looked too
quick
​ly and managed to miss wh
ere the symbol for 0 had been mentioned
​, s
o I relied on the expectation that you would kindly correct me.
​ Thanks!​



>
>
> PS Are "(" and ")" meant to be the same?
>
>
> Ah! Now, that is *my* error, which you should not have copied, given that
> you detect it. ts, ts, ts 
>

​So we were equally sloppy in this case! Mea culpa though.
​

>
> So the correct answer is
>
> 3 ^(2^17) * (3^23) * (5^21) * (7^23)​ * (11^19)
>
>
> And so the proof
>
> Ax(x=x)
> (0 = 0)
>
> is translated in arithmetic-language in the number
>
>
> 2 ^[(2^9) * (3^2) * (5^17) * (7^2) * (11^21) *(13^2) * (17*17)]   *   3 ^ 
> [(2^17)
>> * (3^23) * (5^21) * (7^23)​ * (11^19)]
>
>
>
> The only important things is to see that this is just one number, written
> s(s(s(s(s(s(s(s ... s(0)...), and quite huge (!). Once the machine
> believes in addition and multiplication, it will denote the proof, and the
> machine will be able to answer question like "does a variable occur in that
> proof?", etc.
>
> Very good David, welcome to logic! (and sorry for being long, and probably
> too short in my next answer to the other posts as ... time flies like an
> arrow).
>

​And fruit flies like a banana!

David
​

>
> Bruno
>
>
>
>
> 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 everything-list+unsubscr...@googlegroups.com.
> To post to this group, send email to everything-list@googlegroups.com.
> 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 everything-list+unsubscr...@googlegroups.com.
> To post to this 

Re: Request to Bruno re modal logic

[Bruno Marchal]

On 13 Apr 2017, at 19:26, David Nyman wrote:


On 12 April 2017 at 20:59, Bruno Marchal  wrote:

2 ^(2^9) * (3^2) * (5^17) * (7^2) * (11^21) *(13^2) * (17*17)   *
3 ^ 


​Oh, I see what you mean:

3 ^(2^17) * (3^0) * (5^21) * (7^0)​ * (11^17)



Now, you see it was easy, and, like me, you go fr ... too much  
quickly.


Even without quoting the dictionary we can suspect some mistake. And I  
hope I will not put my finger where it might hurt in case you have  
been mentally abused by a sadistic mathematical teacher!


That one would ask you what is the value of (3^0) ? and what is the  
value of (7^0)?


And you would panic, thinking like ... hmm... er... 3^2 = 3 * 3, 3^1 =  
3, 3^0 = .. !!! . gosh that one is tricky!


Well, (a^b) * (a ^ c) = a ^(b + c), that is obvious for a, b, c  
natural numbers, and if you want keep this true for all integers, you  
will have that 3^0 = 3^(5 - 5) = 3^(5 +(-5)) = (3^5) *(3^(-5)) =  
(again to keep that law on the integers) = (3^5)/(3^5) = 1.


same reasoning for (7^0) = 1.

But 1 is not a prime number, and if we allow it in our coding, it  
would become ambiguous. In fact 1 has been thrown out of the prime to  
get a simple enunciation of the fundamental theorem of arithmetic:  
there is only one decomposition into prime factors. if 1 was a prime  
number, you can add it, as a factor where you want!


That is why, normally, 0 has been represented by non null number, as  
any number ^ 0 = 1.


I say normally, I will now search the dictionary logic-arithmetic  
(seen as languages), and I pray I did not make a typo!


I said:

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,



So, I did not (at least here). 0 has been represented by 23. (If my  
glasses does not fail me). Let us verify * is 29, + is 27, s is 25, 0  
is 23.

(A chance my recent cataract surgery has succeed!  I have an implant!).

So you should have written:


3 ^(2^17) * (3^23) * (5^21) * (7^23)​ * (11^17)



(I guess my talk about was not necessary, .. you did just forget to  
represent 0,  with a notion known by the machine.




PS Are "(" and ")" meant to be the same?


Ah! Now, that is *my* error, which you should not have copied, given  
that you detect it. ts, ts, ts 


So the correct answer is


3 ^(2^17) * (3^23) * (5^21) * (7^23)​ * (11^19)



And so the proof

Ax(x=x)
(0 = 0)

is translated in arithmetic-language in the number


2 ^[(2^9) * (3^2) * (5^17) * (7^2) * (11^21) *(13^2) * (17*17)]
*   3 ^ [(2^17) * (3^23) * (5^21) * (7^23)​ * (11^19)]




The only important things is to see that this is just one number,  
written s(s(s(s(s(s(s(s ... s(0)...), and quite huge (!). Once the  
machine believes in addition and multiplication, it will denote the  
proof, and the machine will be able to answer question like "does a  
variable occur in that proof?", etc.


Very good David, welcome to logic! (and sorry for being long, and  
probably too short in my next answer to the other posts as ... time  
flies like an arrow).


Bruno





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 everything-list+unsubscr...@googlegroups.com.

To post to this group, send email to everything-list@googlegroups.com.
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 everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.

Re: Request to Bruno re modal logic

[David Nyman]

On 13 Apr 2017 2:56 p.m., "Bruno Marchal"  wrote:


On 13 Apr 2017, at 13:35, David Nyman wrote:


On 13 April 2017 at 10:09, Bruno Marchal  wrote:

> Oops.
>
> Yet, you asked me about the modal logic, and I do think at some point I
> have to say precisely what the G box [] is for. It is simple, but long and
> tedious. I hope you have not too much difficulties with my previous post.
>
> To make this accessible, the universal dovetailer argument can be seen as
> a layman version of the "machine interview (the G logics and its variants
> imposed by itself). (even if it came befoe in my mind when observing the
> amoebas).  I replace the machine by a human willing to be that he is a
> machine, and the thought experiments explains the reversal. The G logics
> makes this precise, and more abstract/general, but it relies on the
> extra-ordinary works on computability and logic of Gödel and others, which
> are not that difficult, but is hard to sell without some precision. Don't
> hesitate to encourage me to rewrite a passage in some more shorter way, in
> case you lose the line.
>

​Thanks for this Bruno. I suppose I ought to say I have some special
interests here. In the first place, my interest is in understanding what
ultimately could justify characterising any phenomenon as internal,
intrinsic, or subjective; IOW what is called 1p in this forum.​ The reason
is that I think this is an extremely under-examined, not to say almost
terminally confused, notion in philosophy of mind and the one where things
tend to go wrong at the start. For example, the idea that we can appeal to
some "inner" nature of matter as in panpsychism, weaselling about
"illusion" or "seeming" in what is variously called materialism,
physicalism or naturalism, or the biological obscurantism resorted to by
Searle in the face of the Chinese Room argument. This is also part of what
I was getting at about unexamined extra presuppositions more or less
tacitly assumed in informal reasoning - in this case the implicitly assumed
"free lunch" of an inner or subjective point of view absent any explicit
supporting rationale. So one of the most interesting things about comp for
me has always been the possibility of explicating such a perspective
explicitly in terms of a logic particular to the first-person.


Always trying to go right at the heart of the problem. OK.




The reason I see this as so central is to do with the gap between syntax
and semantics, to use Searle's terminology. This gap has struck many as
unbridgeable, whether frankly so as in mysterianism (e.g. McGinn) or
implicitly in the belief that all further questioning will effectively be
terminated by a completed neuroscience.



So comp, here will go toward mysterianism. Comp gives a reason why there is
a mystery from our limited terrestrial and locally mechanical points of
view.




So what I find of particular interest in comp is the possibility of
bridging this gap in an intelligible manner.


OK.
But it is necessary a bit subtle. In a nutshell:

G cannot bridge the gap.
G* can bridge the gap (but G cannot believe in that bridge without becoming
inconsistent)
S4Grz (the first person) cannot see that there is a gap.

They have to dialog. The choice will be, like Paul Valery said, between
logic and war.




I cited Wittgenstein's idea of the explanatory ladder that is discarded
when the sought-after next level is reached. In this case the ladder is the
temporary conceptual aid of an external interpretation (aka a view from
nowhere) imposed on what is still fundamentally a third-person syntactical
procedure.


OK.


This is, or should be, a provisional "transcendence" from syntax to
semantics that is justifiable as an external prosthesis only so long as it
leads to a replacement that can do away with the need for it.


Hmm You seem to want to replace the Outer-God, by the Inner-God. That
is a risky move toward solipsim. S4Grz does not see the gap, but it does
not see the other minds either.


O
​K​
, I've been re-reading the relevant section of
​T​
he Amoeba's Secret just to check my intuition about
​what I said above
. There you remind us that in the final analysis the truth of p as distinct
from its believability can't be proved in the language of the machine.
Hence
​we
 postulate
​ it​
as true by assertion. Let us accept this
​ postulation​
​for the moment ​
as "provisionally" true. Then let us consider the case where
​ a
machine
​"​
believes
​"​
in the existence of
​​
a concrete perceptual reality, the 1-truth of which it also
​3-​
asserts, but of course cannot communicate.
​Concealed i
n
​the
 gap between the provability and communicability of the
​3-​
belief and the unprovability and incommunicability of the
​1-​
assertion is the
​elusive ​
transition from syntax to semantics. The latter we will conceive as an
​additional ​
​"​
interpretation
​"​
of the former, but - by assumption of computationalism -
any such
interpretation
​ *must be 

Re: Request to Bruno re modal logic

[David Nyman]

On 12 April 2017 at 20:59, Bruno Marchal  wrote:

2 ^(2^9) * (3^2) * (5^17) * (7^2) * (11^21) *(13^2) * (17*17)   *   3 ^
> 


​Oh, I see what you mean:

3 ^(2^17) * (3^0) * (5^21) * (7^0)​ * (11^17)

PS Are "(" and ")" meant to be the same?

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 everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.

Re: Request to Bruno re modal logic

[David Nyman]

On 12 April 2017 at 20:59, Bruno Marchal  wrote:

>
> On 11 Apr 2017, at 18:21, David Nyman wrote:
>
> On 10 April 2017 at 18:32, Bruno Marchal  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.
>>
>
> 

Re: Request to Bruno re modal logic

[Bruno Marchal]

On 13 Apr 2017, at 14:11, David Nyman wrote:


On 12 April 2017 at 20:59, Bruno Marchal  wrote:

On 11 Apr 2017, at 18:21, David Nyman wrote:


On 10 April 2017 at 18:32, Bruno Marchal  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 

Re: Request to Bruno re modal logic

[David Nyman]

On 13 April 2017 at 14:56, Bruno Marchal  wrote:

Hmm You seem to want to replace the Outer-God, by the Inner-God. That
> is a risky move toward solipsim. S4Grz does not see the gap, but it does
> not see the other minds either.


​But that's just it. We cannot ever "see" the other minds, nor even our own
for that matter, however much we examine mechanism. But we can believe in
them, as we do in our own. Perhaps the least confusing conception of this
(following Hoyle's heuristic, which as you know I'm fond of) is to conceive
the soul as indeed a soles ipse, though one with innumerable
personifications, each profoundly amnesic with respect to the others. But
surely that must be true of any computational device capable of
compartmentalising one program's states from another's. Is this then the
Inner-God? Perhaps, in concrete or perceptual form. But surely the abstract
Outer-God is still evidenced in that maximally-compressed creative widget
you call the UD?

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 everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.

Re: Request to Bruno re modal logic

[Bruno Marchal]

On 13 Apr 2017, at 13:35, David Nyman wrote:



On 13 April 2017 at 10:09, Bruno Marchal  wrote:
Oops.

Yet, you asked me about the modal logic, and I do think at some  
point I have to say precisely what the G box [] is for. It is  
simple, but long and tedious. I hope you have not too much  
difficulties with my previous post.


To make this accessible, the universal dovetailer argument can be  
seen as a layman version of the "machine interview (the G logics and  
its variants imposed by itself). (even if it came befoe in my mind  
when observing the amoebas).  I replace the machine by a human  
willing to be that he is a machine, and the thought experiments  
explains the reversal. The G logics makes this precise, and more  
abstract/general, but it relies on the extra-ordinary works on  
computability and logic of Gödel and others, which are not that  
difficult, but is hard to sell without some precision. Don't  
hesitate to encourage me to rewrite a passage in some more shorter  
way, in case you lose the line.


​Thanks for this Bruno. I suppose I ought to say I have some  
special interests here. In the first place, my interest is in  
understanding what ultimately could justify characterising any  
phenomenon as internal, intrinsic, or subjective; IOW what is called  
1p in this forum.​ The reason is that I think this is an extremely  
under-examined, not to say almost terminally confused, notion in  
philosophy of mind and the one where things tend to go wrong at the  
start. For example, the idea that we can appeal to some "inner"  
nature of matter as in panpsychism, weaselling about "illusion" or  
"seeming" in what is variously called materialism, physicalism or  
naturalism, or the biological obscurantism resorted to by Searle in  
the face of the Chinese Room argument. This is also part of what I  
was getting at about unexamined extra presuppositions more or less  
tacitly assumed in informal reasoning - in this case the implicitly  
assumed "free lunch" of an inner or subjective point of view absent  
any explicit supporting rationale. So one of the most interesting  
things about comp for me has always been the possibility of  
explicating such a perspective explicitly in terms of a logic  
particular to the first-person.


Always trying to go right at the heart of the problem. OK.





The reason I see this as so central is to do with the gap between  
syntax and semantics, to use Searle's terminology. This gap has  
struck many as unbridgeable, whether frankly so as in mysterianism  
(e.g. McGinn) or implicitly in the belief that all further  
questioning will effectively be terminated by a completed  
neuroscience.



So comp, here will go toward mysterianism. Comp gives a reason why  
there is a mystery from our limited terrestrial and locally mechanical  
points of view.





So what I find of particular interest in comp is the possibility of  
bridging this gap in an intelligible manner.


OK.
But it is necessary a bit subtle. In a nutshell:

G cannot bridge the gap.
G* can bridge the gap (but G cannot believe in that bridge without  
becoming inconsistent)

S4Grz (the first person) cannot see that there is a gap.

They have to dialog. The choice will be, like Paul Valery said,  
between logic and war.





I cited Wittgenstein's idea of the explanatory ladder that is  
discarded when the sought-after next level is reached. In this case  
the ladder is the temporary conceptual aid of an external  
interpretation (aka a view from nowhere) imposed on what is still  
fundamentally a third-person syntactical procedure.


OK.


This is, or should be, a provisional "transcendence" from syntax to  
semantics that is justifiable as an external prosthesis only so long  
as it leads to a replacement that can do away with the need for it.


Hmm You seem to want to replace the Outer-God, by the Inner-God.  
That is a risky move toward solipsim. S4Grz does not see the gap, but  
it does not see the other minds either.




The needed replacement is an intelligibly internalised semantics, or  
self-interpretation, which ISTM must be the very nub of a first- 
personal logic.


OK. And as you know, that will be given, at the meta-level, by S4Grz.  
But the machine cannot involves its own S4Grz box. From its machine's  
view, it has simply no name. It is not genuinely Turing emulable. The  
machine can discover it by *postulating* computationalism.



If this can be explicated in terms of a logic that is itself  
emulable in computation, then - on the comp assumption that we  
occupy the selfsame first-personal situation - the perceptual facts  
of an inter-subjective concrete reality can then retroactively  
illuminate the theoretical framework that has explicated them.


Through the bet in a sharable reality, but at the price of having to  
justify its physical aspect without invoking a physical reality.




Equally, denying such facts becomes an effective nullification 

Re: Request to Bruno re modal logic

[David Nyman]

On 12 April 2017 at 20:59, Bruno Marchal  wrote:

>
> On 11 Apr 2017, at 18:21, David Nyman wrote:
>
> On 10 April 2017 at 18:32, Bruno Marchal  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.
>>
>
> 

Re: Request to Bruno re modal logic

[David Nyman]

On 13 April 2017 at 10:09, Bruno Marchal  wrote:

> Oops.
>
> Yet, you asked me about the modal logic, and I do think at some point I
> have to say precisely what the G box [] is for. It is simple, but long and
> tedious. I hope you have not too much difficulties with my previous post.
>
> To make this accessible, the universal dovetailer argument can be seen as
> a layman version of the "machine interview (the G logics and its variants
> imposed by itself). (even if it came befoe in my mind when observing the
> amoebas).  I replace the machine by a human willing to be that he is a
> machine, and the thought experiments explains the reversal. The G logics
> makes this precise, and more abstract/general, but it relies on the
> extra-ordinary works on computability and logic of Gödel and others, which
> are not that difficult, but is hard to sell without some precision. Don't
> hesitate to encourage me to rewrite a passage in some more shorter way, in
> case you lose the line.
>

​Thanks for this Bruno. I suppose I ought to say I have some special
interests here. In the first place, my interest is in understanding what
ultimately could justify characterising any phenomenon as internal,
intrinsic, or subjective; IOW what is called 1p in this forum.​ The reason
is that I think this is an extremely under-examined, not to say almost
terminally confused, notion in philosophy of mind and the one where things
tend to go wrong at the start. For example, the idea that we can appeal to
some "inner" nature of matter as in panpsychism, weaselling about
"illusion" or "seeming" in what is variously called materialism,
physicalism or naturalism, or the biological obscurantism resorted to by
Searle in the face of the Chinese Room argument. This is also part of what
I was getting at about unexamined extra presuppositions more or less
tacitly assumed in informal reasoning - in this case the implicitly assumed
"free lunch" of an inner or subjective point of view absent any explicit
supporting rationale. So one of the most interesting things about comp for
me has always been the possibility of explicating such a perspective
explicitly in terms of a logic particular to the first-person.

The reason I see this as so central is to do with the gap between syntax
and semantics, to use Searle's terminology. This gap has struck many as
unbridgeable, whether frankly so as in mysterianism (e.g. McGinn) or
implicitly in the belief that all further questioning will effectively be
terminated by a completed neuroscience. So what I find of particular
interest in comp is the possibility of bridging this gap in an intelligible
manner. I cited Wittgenstein's idea of the explanatory ladder that is
discarded when the sought-after next level is reached. In this case the
ladder is the temporary conceptual aid of an external interpretation (aka a
view from nowhere) imposed on what is still fundamentally a third-person
syntactical procedure. This is, or should be, a provisional "transcendence"
from syntax to semantics that is justifiable as an external prosthesis only
so long as it leads to a replacement that can do away with the need for it.
The needed replacement is an intelligibly internalised semantics, or
self-interpretation, which ISTM must be the very nub of a first-personal
logic. If this can be explicated in terms of a logic that is itself
emulable in computation, then - on the comp assumption that we occupy the
selfsame first-personal situation - the perceptual facts of an
inter-subjective concrete reality can then retroactively illuminate the
theoretical framework that has explicated them. Equally, denying such facts
becomes an effective nullification of the sense of any framework
paradoxically adduced in their support (as in any Churchland or
Dennett-style weaselling about "illusions").

I think these aspects may be so important to communicating these ideas to a
wider appreciation, as opposed to a technical/professional audience, that
if at all possible some Hilbert-style man-in-the-street way of
encapsulating their most essential features, without involving a detailed
point for point grasp of the bulk of the technicalities, would be valuable
indeed. By the most essential features I mean for example the distinctions
between belief (or judgement) and perception, communicability and
incommunicability, formal and informal. No doubt you might point to others.
The UDA, while valuable in itself, assumes the first-person position (as
indeed it is entitled to do on the comp assumption) but without providing
any explicit rationale for it. Of course, that is the intended function of
AUDA and the machine interviews. But then that takes us immediately into
the complexities of the formidable technical batteries of mathematical
logic. Is it not possible that there might be some intermediate pedagogical
step?

David

-- 
You received this message because you are subscribed to the Google Groups 
"Everything List" group.
To unsubscribe 

Re: Request to Bruno re modal logic

[Bruno Marchal]

On 11 Apr 2017, at 18:21, David Nyman wrote:


On 10 April 2017 at 18:32, Bruno Marchal  wrote:

On 10 Apr 2017, at 12:58, David Nyman wrote:








​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.


Oops.

Yet, you asked me about the modal logic, and I do think at some point  
I have to say precisely what the G box [] is for. It is simple, but  
long and tedious. I hope you have not too much difficulties with my  
previous post.


To make this accessible, the universal dovetailer argument can be seen  
as a layman version of the "machine interview (the G logics and its  
variants imposed by itself). (even if it came befoe in my mind when  
observing the amoebas).  I replace the machine by a human willing to  
be that he is a machine, and the thought experiments explains the  
reversal. The G logics makes this precise, and more abstract/general,  
but it relies on the extra-ordinary works on computability and logic  
of Gödel and others, which are not that difficult, but is hard to sell  
without some precision. Don't hesitate to encourage me to rewrite a  
passage in some more shorter way, in case you lose the line.


Bruno







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 everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything- 
l...@googlegroups.com.

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 everything-list+unsubscr...@googlegroups.com.

To post to this group, send email to everything-list@googlegroups.com.
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 everything-list+unsubscr...@googlegroups.com.

To post to this group, send email to everything-list@googlegroups.com.
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 everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.

Re: Request to Bruno re modal logic

[Bruno Marchal]

On 11 Apr 2017, at 18:21, David Nyman wrote:


On 10 April 2017 at 18:32, Bruno Marchal  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 

Re: Request to Bruno re modal logic

[Brent Meeker]

On 4/11/2017 9:21 AM, David Nyman wrote:


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):



But why choose A1 and A2?  Why not make (p -> p) and axiom.  It's 
certainly more obvious than either A1 of A2, so if it were not a theorem 
you'd got back choose different axioms.  Actually I know why; but my 
point is that logic is intended to formalize sound inference - but 
because it's formal it is only "t" preserving, not truth preserving.


Brent

--
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 everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.

Re: Request to Bruno re modal logic

[David Nyman]

On 10 April 2017 at 18:32, Bruno Marchal  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 

Re: Request to Bruno re modal logic

[Bruno Marchal]

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 

Request to Bruno re modal logic

[David Nyman]

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.

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 everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.