Re: AUDA and pronouns
On 23 Oct 2013, at 22:57, Russell Standish wrote: On Wed, Oct 23, 2013 at 03:02:55PM +0200, Bruno Marchal wrote: On 22 Oct 2013, at 22:50, Russell Standish wrote: On Tue, Oct 22, 2013 at 03:09:03PM +0200, Bruno Marchal wrote: On 21 Oct 2013, at 23:03, Russell Standish wrote: In fact p- []p characterizes sigma_1 completeness (by a result by Albert Visser), and that is why to get the proba on the UD*, we use the intensional nuance []p t (= proba) starting from G extended with the axiom p- []p (limiting the proposition to the UD). proba? Sorry - I was actually asking what you meant by the word proba. OK. Sorry. It was an abbreviation for probability. []p t doesn't seem like a probability. It is a probability 1. von Neumann once argued, if you have a good quantum logic (which means automatically a good axiomatic for the probability 1 (the box in a modal axiomatic) and the ~probability = 0, (the diamond in the modal approach), all the other probabilities should be derivable from it. Assuming three dimension, and the Hilbert space structure for the quantum state, Gleason theorem get the probabilities from the logic. I thought some years that I could derive a Temperley Lieb algebra of projection operators in the logic Z1*, but the math get too much complex for me. That would have provided the 3 dimensions (by relation between Temperley-Lieb Algebra and 3D knots), and the Hilbert Space structure, and in that case, the rest is done by Gleason theorem. Did you mean certainty? In our context certainty might be a bit fuzzy. But I am not against calling a probability one a certainty, in case it is an ideal relative certainty, based on the assumption of comp for example, the correct choice of the substitution level, the perfect ability of the doctor/teleportation-machine, all the default hypotheses. IIRC, one of your hypostases was interpreted as probability=1 (ie certain) events. The key is more that []p is not a probability. And that we get an abstract probability (a modal logic of probability or credibility) when we add the consistency (semantically = the existence of at least one accessible reality) condition. So yes, []p t is an arithmetical predicate which behaves like a probability one. Also, is []p t == []p p ? Yes. Those are definition made in G (and thus in arithmetic), which is a normal modal logic. t implies the existence of an accessible world (by Kripke semantics). []p implies p is true in all accessible world. So there will a world, and p is true in it, so we have p when we have []p t . And, of course the reverse is more easy. if we have p, we have an accessible world (the one with p true in that world), and t is true there too, as t is true in all world. Careful! the new logic obtained (with the new box defined by []p t), we lost the necessitation rule, and in that logic, there is no more a Kripke semantics. But we have still a notion of worlds- neighborhoods, which fit better the apparition of topologies, continuua, ... and thus with the UDA way to derive physics. Bruno -- Prof Russell Standish Phone 0425 253119 (mobile) Principal, High Performance Coders Visiting Professor of Mathematics hpco...@hpcoders.com.au University of New South Wales http://www.hpcoders.com.au -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out. 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 23 Oct 2013, at 23:42, meekerdb wrote:
On 10/23/2013 5:53 AM, Bruno Marchal wrote:
On 22 Oct 2013, at 19:01, meekerdb wrote:
On 10/22/2013 5:48 AM, Bruno Marchal wrote:
On 21 Oct 2013, at 20:07, meekerdb wrote:
On 10/20/2013 11:12 PM, Russell Standish wrote:
On Sun, Oct 20, 2013 at 08:09:59PM -0700, meekerdb wrote:
Consistency is []p ~[]~p. I was saying []p ~p, ie
mistaken belief.
ISTM that Bruno equivocates and [] sometimes means believes
and sometimes provable.
And I'm doing the same. It's not such an issue - a
mathematician will
only believe something if e can prove it.
But provable(p)==p and believes(p)=/=p, so why equivocate on
them?
Both provable('p') - p, and believe('p') - p, when we limit
ourself to correct machine.
(And incidentally mathematicians believe stuff they can't prove
all the time - that's how they choose things to try to prove).
Then it is a conjecture. They don't believe rationally in
conjecture, when they are correct.
They believe it in the real operational sense of believe, they
will bet their whole professional lives on it. How long did it
take Andrew Wiles to prove Fermat's last theorem? Since one can
never know that one is a correct machine it seems to me a
muddling of things to equivocate on provable and believes.
On the contrary. It provides a recursive definition of the beliefs,
by a rational agent accepting enough truth to understand how a
computer work.
We can define the beliefs by presenting PA axioms in that way
Classical logic is believed,
'0 ≠ s(x)' is believed,
's(x) = s(y) - x = y' is believed,
'x+0 = x' is believed,
'x+s(y) = s(x+y)' is believed,
'x*0=0' is believed,
'x*s(y)=(x*y)+x' is believed,
and the rule: if A - B is believed and A is believed, then (soon
or later) B is believed.
But the point of Seth Lloyd's paper was that later can effectively
be never and since given any time horizon, t, almost all B will not
be believed earlier than t.
But Seth Loyd assumes some physical universe. In the arithmetic
context from which we start (and have to start by UDA, at some
recursive equivalence) soon or later means once. It never means
never.
So really you call it believe, but you use it as provable.
You miss the point. The incompleteness forces the provability logic to
behave like a believability logic.
After Gödel, provable (which was for many the best case of knowledge)
becomes only 'believable'.
That's why I agree with Popper, that science = only belief, because
the big difference between a belief and a knowledge, is that the first
is corrigible and the second is incorrigible.
(Popper and Deutsch uses non-standard vocabulary here, but I agree
with them).
Then the theory will apply to any recursively enumerable extensions
of those beliefs, provided they don't get arithmetically unsound.
The believer can be shown to be Löbian once he has also the beliefs
in the induction axioms.
Not really. You have add another axiom that the believer is correct.
Why would I need to do that? It is not a new axiom, it is that I limit
the interview to correct machines. (Everett does the same, it is
natural. If you predict that a comet will appear in the sky, you will
not be refuted by a paper explaining that when astronomers are
sufficiently drunk, they miss to see it. You don't have to assume that
the observer is not drunk, sane of mind, etc. (At the level of the
scientific paper, in real life you know that a talk after dinner, at
some conference, will count for nothing, as people are full, and
sleepy!).
He doesn't believe any false propositions - which means it is an
idealization that doesn't apply to anyone.
To derive physics, that is enough. Theoretical approach starts from
the simpler assumptions, and change them, or improves them only if
needed.
If not, you would have rejected Newton's at once, as he consider the
sun being a point, when recovering Keepler laws from his gravitation
theory.
The interesting happening, I think, is that by G* proving []f,
somehow, the laws of physics and the whole machine's theology have to
take into account the consistency of incorrectness, at some basic
fundamental level. The idealization makes justice itself of your
remark, somehow.
Bruno
Brent
Bruno
--
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 http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
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
Re: AUDA and pronouns
On 22 Oct 2013, at 19:01, meekerdb wrote:
On 10/22/2013 5:48 AM, Bruno Marchal wrote:
On 21 Oct 2013, at 20:07, meekerdb wrote:
On 10/20/2013 11:12 PM, Russell Standish wrote:
On Sun, Oct 20, 2013 at 08:09:59PM -0700, meekerdb wrote:
Consistency is []p ~[]~p. I was saying []p ~p, ie mistaken
belief.
ISTM that Bruno equivocates and [] sometimes means believes
and sometimes provable.
And I'm doing the same. It's not such an issue - a mathematician
will
only believe something if e can prove it.
But provable(p)==p and believes(p)=/=p, so why equivocate on
them?
Both provable('p') - p, and believe('p') - p, when we limit
ourself to correct machine.
(And incidentally mathematicians believe stuff they can't prove
all the time - that's how they choose things to try to prove).
Then it is a conjecture. They don't believe rationally in
conjecture, when they are correct.
They believe it in the real operational sense of believe, they
will bet their whole professional lives on it. How long did it take
Andrew Wiles to prove Fermat's last theorem? Since one can never
know that one is a correct machine it seems to me a muddling of
things to equivocate on provable and believes.
On the contrary. It provides a recursive definition of the beliefs, by
a rational agent accepting enough truth to understand how a computer
work.
We can define the beliefs by presenting PA axioms in that way
Classical logic is believed,
'0 ≠ s(x)' is believed,
's(x) = s(y) - x = y' is believed,
'x+0 = x' is believed,
'x+s(y) = s(x+y)' is believed,
'x*0=0' is believed,
'x*s(y)=(x*y)+x' is believed,
and the rule: if A - B is believed and A is believed, then (soon or
later) B is believed.
Then the theory will apply to any recursively enumerable extensions of
those beliefs, provided they don't get arithmetically unsound.
The believer can be shown to be Löbian once he has also the beliefs in
the induction axioms.
Bruno
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 http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
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 http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 22 Oct 2013, at 19:07, meekerdb wrote:
On 10/22/2013 6:19 AM, Bruno Marchal wrote:
[]p - p is correctness. It is trivially true for the machine I
consider, because they are correct by definition/choice.
Consistency is correctness on the f: []f - f. It is a very
particular case of correctness.
There are machines which are not correct, yet consistent. For
example Peano-Arithmetic + the axiom beweisbar('f').
Believing '0=1', does not make you inconsistent. Only non correct.
?? But in ordinary logic a false proposition allows you to prove
anything. So if I prove '0=1' then I can prove any proposition -
which is the definition of inconsistency.
OK. I should have written Believing '0=1', does not make you
inconsistent. Only non correct.
Or if your prefer: believing believing '0=1' does not make you
inconsistent. Only non correct.
If you add the axiom 0=1 to PA, it get inconsistent, as, like you
say, ordinary logic will imply that you can prove all proposition.
But here I was not adding 0=1 as an axiom to PA, I was adding
believe 0=1 as an axiom, and from this you cannot prove all
propositions. In particular you cannot prove 0=1. You can only prove
that you can prove all propositions. That might make you stupid, and
certainly unsound, but not inconsistent.
Just keep in mind that Bf - f is not provable by PA. And keep well
the difference between PA asserts (proves, believes) p, and PA asserts
Bp.
Bruno
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 http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
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 http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 22 Oct 2013, at 22:50, Russell Standish wrote: On Tue, Oct 22, 2013 at 03:09:03PM +0200, Bruno Marchal wrote: On 21 Oct 2013, at 23:03, Russell Standish wrote: In fact p- []p characterizes sigma_1 completeness (by a result by Albert Visser), and that is why to get the proba on the UD*, we use the intensional nuance []p t (= proba) starting from G extended with the axiom p- []p (limiting the proposition to the UD). proba? Sorry - I was actually asking what you meant by the word proba. OK. Sorry. It was an abbreviation for probability. Best, Bruno 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On Wed, Oct 23, 2013 at 03:02:55PM +0200, Bruno Marchal wrote: On 22 Oct 2013, at 22:50, Russell Standish wrote: On Tue, Oct 22, 2013 at 03:09:03PM +0200, Bruno Marchal wrote: On 21 Oct 2013, at 23:03, Russell Standish wrote: In fact p- []p characterizes sigma_1 completeness (by a result by Albert Visser), and that is why to get the proba on the UD*, we use the intensional nuance []p t (= proba) starting from G extended with the axiom p- []p (limiting the proposition to the UD). proba? Sorry - I was actually asking what you meant by the word proba. OK. Sorry. It was an abbreviation for probability. []p t doesn't seem like a probability. Did you mean certainty? IIRC, one of your hypostases was interpreted as probability=1 (ie certain) events. Also, is []p t == []p p ? -- Prof Russell Standish Phone 0425 253119 (mobile) Principal, High Performance Coders Visiting Professor of Mathematics hpco...@hpcoders.com.au University of New South Wales http://www.hpcoders.com.au -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 10/23/2013 5:53 AM, Bruno Marchal wrote:
On 22 Oct 2013, at 19:01, meekerdb wrote:
On 10/22/2013 5:48 AM, Bruno Marchal wrote:
On 21 Oct 2013, at 20:07, meekerdb wrote:
On 10/20/2013 11:12 PM, Russell Standish wrote:
On Sun, Oct 20, 2013 at 08:09:59PM -0700, meekerdb wrote:
Consistency is []p ~[]~p. I was saying []p ~p, ie mistaken belief.
ISTM that Bruno equivocates and [] sometimes means believes and sometimes
provable.
And I'm doing the same. It's not such an issue - a mathematician will
only believe something if e can prove it.
But provable(p)==p and believes(p)=/=p, so why equivocate on them?
Both provable('p') - p, and believe('p') - p, when we limit ourself to
correct machine.
(And incidentally mathematicians believe stuff they can't prove all the time - that's
how they choose things to try to prove).
Then it is a conjecture. They don't believe rationally in conjecture, when they are
correct.
They believe it in the real operational sense of believe, they will bet their whole
professional lives on it. How long did it take Andrew Wiles to prove Fermat's last
theorem? Since one can never know that one is a correct machine it seems to me a
muddling of things to equivocate on provable and believes.
On the contrary. It provides a recursive definition of the beliefs, by a rational agent
accepting enough truth to understand how a computer work.
We can define the beliefs by presenting PA axioms in that way
Classical logic is believed,
'0 ≠ s(x)' is believed,
's(x) = s(y) - x = y' is believed,
'x+0 = x' is believed,
'x+s(y) = s(x+y)' is believed,
'x*0=0' is believed,
'x*s(y)=(x*y)+x' is believed,
and the rule: if A - B is believed and A is believed, then (soon or later) B
is believed.
But the point of Seth Lloyd's paper was that later can effectively be never and since
given any time horizon, t, almost all B will not be believed earlier than t. So really you
call it believe, but you use it as provable.
Then the theory will apply to any recursively enumerable extensions of those beliefs,
provided they don't get arithmetically unsound.
The believer can be shown to be Löbian once he has also the beliefs in the
induction axioms.
Not really. You have add another axiom that the believer is correct. He doesn't believe
any false propositions - which means it is an idealization that doesn't apply to anyone.
Brent
Bruno
--
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 http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 21 Oct 2013, at 17:59, Platonist Guitar Cowboy wrote:
On Mon, Oct 21, 2013 at 4:26 PM, Bruno Marchal marc...@ulb.ac.be
wrote:
On 21 Oct 2013, at 08:24, Russell Standish wrote:
On Mon, Oct 21, 2013 at 04:48:42AM +0200, Platonist Guitar Cowboy
wrote:
Disclaimer: No idea if I am even on the same planet on which this
discussion is taking place. So pardon my questions and confusions:
You and me both - we're all students here :).
I'm just rather doubtful about an axiomatisation of proof that assumes
we can prove that we can prove something, as with that we can know
that we (Theatetically) know something (since truth is usually
inherently unknowable).
It reminds me of a 3 year old's question but why? Ultimately, you
will not be able to answer a question like that.
It is quite possible I haven't drunk enough Kool-Aid.
Question for Bruno (raised from PGC's earlier comments):
Is axiom 4, ie []p - [][]p, called a fixed point theorem?
No. PGC is a bit unclear/mysterious when referring to the fixed
point theorem here.
But I don't refer to fixed point theorem there.
Concerning []p - [][]p, I just stated it is a theory of G, used in
all manner of proofs fruitfully.
I remember something like if []p - [][]p weren't a theory of G as
proven by some usual suspect, Kripke I think, then we would extend
GL sufficiently until it was!
And that shows how often this is used; almost axiomatically in
practice. Boolos at least seems addicted to it. PGC
No problem. Minor vocabulary details. I guess you mean theorem of G
(or is in the theory G).
By Solovay theorem, G is complete and sound for the arithmetical
provability, and wht is really oimprtant is that for all arithmetical
proposition beweisbar('p') - beweisbar('beeisbar('p')') is a theorem
of (Peano) arithmetic.
If G was not proving []p - [][]p, it would not be arithmetically
complete.
Bruno
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 http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 21 Oct 2013, at 20:07, meekerdb wrote:
On 10/20/2013 11:12 PM, Russell Standish wrote:
On Sun, Oct 20, 2013 at 08:09:59PM -0700, meekerdb wrote:
Consistency is []p ~[]~p. I was saying []p ~p, ie mistaken
belief.
ISTM that Bruno equivocates and [] sometimes means believes and
sometimes provable.
And I'm doing the same. It's not such an issue - a mathematician will
only believe something if e can prove it.
But provable(p)==p and believes(p)=/=p,
Both provable('p') - p, and believe('p') - p, when we limit ourself
to correct machine.
so why equivocate on them? (And incidentally mathematicians believe
stuff they can't prove all the time - that's how they choose things
to try to prove).
Brent
But if you like to subsitute mistaken proof for mistaken
belief, go ahead.
--
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 http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
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 http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 21 Oct 2013, at 20:07, meekerdb wrote:
On 10/20/2013 11:12 PM, Russell Standish wrote:
On Sun, Oct 20, 2013 at 08:09:59PM -0700, meekerdb wrote:
Consistency is []p ~[]~p. I was saying []p ~p, ie mistaken
belief.
ISTM that Bruno equivocates and [] sometimes means believes and
sometimes provable.
And I'm doing the same. It's not such an issue - a mathematician will
only believe something if e can prove it.
But provable(p)==p and believes(p)=/=p, so why equivocate on them?
Both provable('p') - p, and believe('p') - p, when we limit ourself
to correct machine.
(And incidentally mathematicians believe stuff they can't prove all
the time - that's how they choose things to try to prove).
Then it is a conjecture. They don't believe rationally in conjecture,
when they are correct.
Bruno
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 http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 21 Oct 2013, at 23:03, Russell Standish wrote: On Mon, Oct 21, 2013 at 03:52:14PM +0200, Bruno Marchal wrote: On 20 Oct 2013, at 23:15, Russell Standish wrote: On Sun, Oct 20, 2013 at 06:22:15PM +0200, Bruno Marchal wrote: On 20 Oct 2013, at 12:01, Russell Standish wrote: Obviously, one cannot prove []p p, for very many statements, ie []p p does not entail []([o]p) []p - [][]p OK? Why? This is not obvious. It translates as being able to prove that you can prove stuff when you can prove it. You are right, this is not so easy to prove. It follows from the provable sigma_1 completeness, that is the fact that if p is a sigma_1 formula, then Peano Arithmetic can prove p - Bp. (That is not easy to prove, but it is done in Hilbert-Bernays, also in the books by Boolos). It is the hard part of the second incompleteness theorem. It presupposes some induction axioms, like in Peano Arithmetic (PA). Then Bp is itself a sigma_1 arithmetical proposition, so []p - [] []p. i.e If p is the result of a computer program, then there exists a program that proves p is correct? If p is the result of a computer program P, then p is the result of a computer program P is itself the result of a computer program (it can be P itself in case P is sigma_1 complete). No notion of correctness is involved here. And thus you've proven that for everything you know, you can know that you know it. This seems wrong, as the 4 colour theorem indicates. I would not trust my intuition about this. In choosing axioms, intuition is all we have to go by. But you say below that 4 is in fact a redundant axiom ... which makes it not so clear cut. The axiom 4 ([]p - [][]p) is indeed an axiom in the classical theory of knowledge (the modal logic 4). But, then, in arithmetic, when we define knowledge with the Theaetetus's method, it becomes a theorem (a scheme of theorems, for each arithmetical p) of arithmetic. That's why we can say that we recover the classical theory of knowledge in arithmetic. We can prove the 4 colour theorem by means of a computer program, and it may indeed be correct, so that we Theatetically know the 4 colour theorem is true, but we cannot prove the proof is correct (at least at this stage, proving program correctness is practically impossible). It should be easy once we have a concrete formal proof. As far as I know, we don't have this for the 4 colour theorem. But once we have such proofs, it should be trivial to prove that the proof exists, making []p - [][]p easy to prove for the particular case of p = 4- color. How does it make it easy? Because if the proof is formal, the proof that the proof is formal is easily made itself formal, and can be checked mechanically. The case of the 4 colour theorems is not easy, because there thousand of lemma, checked by many different computers, by humans not using exactly the same software. The last thing I heard was that some lemma have been discovered not having been checked at all. A correct machine is automatically Löbian if she is sigma_1 complete, and has enough induction axioms to prove its own sigma_1 completeness (in the sense of proving all formula p - []p, for p sigma_1). In fact p- []p characterizes sigma_1 completeness (by a result by Albert Visser), and that is why to get the proba on the UD*, we use the intensional nuance []p t (= proba) starting from G extended with the axiom p- []p (limiting the proposition to the UD). proba? What prevent []p to define a proba is only the existence of cul-de-sac worlds. For a modal axiomatization of proba we want the axiom []p - p. But we don't have that in arithmetic (with [] = Gödel beweisbar). But we get it with the nuance ([]p p). (or Bp Dp, or Bp Dt) Example. I said yesterday to John Clark that P(W xor M) = 1, in Helsinki, because (W xor M) is true in the two accessible (from helsinki) realities W and M. This makes sense only because I assume comp, that is, I assume I will survive the teletransportation, that is, I assume that Helsinki is not a cul-de-sac world. The nuance Bp Dp is only that: an implcit assumption that we are not in a cul-de-sac world. It contains a little bit of comp already. Bp is true for all p, true and false, in the cul-de-sac world (world in Kripke sense, here, not yet in Everett sense!). Bruno -- Prof Russell Standish Phone 0425 253119 (mobile) Principal, High Performance Coders Visiting Professor of Mathematics hpco...@hpcoders.com.au University of New South Wales http://www.hpcoders.com.au -- 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
Re: AUDA and pronouns
On 21 Oct 2013, at 23:34, meekerdb wrote:
On 10/21/2013 7:25 AM, Bruno Marchal wrote:
On 21 Oct 2013, at 05:09, meekerdb wrote:
On 10/20/2013 2:15 PM, Russell Standish wrote:
On Sun, Oct 20, 2013 at 06:22:15PM +0200, Bruno Marchal wrote:
On 20 Oct 2013, at 12:01, Russell Standish wrote:
On Sun, Oct 20, 2013 at 08:52:41AM +0200, Bruno Marchal wrote:
We have always that [o]p - [o][o]p (like we have also always
that
[]p - [][]p)
There may be things we can prove, but about which we are in fact
mistaken, ie
[]p -p
That is consistent. (Shit happens, we became unsound).
Consistency is []p ~[]~p. I was saying []p ~p, ie mistaken
belief.
ISTM that Bruno equivocates and [] sometimes means believes and
sometimes provable.
But I am allowed to do that, because []p - p is not a theorem (for
some p, by incompleteness)
Isn't incompleteness ~(p-[]p) ?
Yes.
And you assume the machine is consistent, so doesn't that entail []p-
p ?
[]p - p is correctness. It is trivially true for the machine I
consider, because they are correct by definition/choice.
Consistency is correctness on the f: []f - f. It is a very particular
case of correctness.
There are machines which are not correct, yet consistent. For example
Peano-Arithmetic + the axiom beweisbar('f').
Believing '0=1', does not make you inconsistent. Only non correct.
and thus (rational formal) provability behaves like believability.
A mathematician told me that I was dead mad by saying this, but
that is standard in mathematical logic (ignored by most
mathematicians). It is counter-intuitive. Most people believes that
formal proof guaranties truth, when starting from true theorem (and
that is true for the ideally correct machine, but no machine can
know she is correct, and her probability does behave like a
believability, indeed one on Which the application of Theaetus'
definition leads to the classical knowledge logic (the modal logic
S4).
That still seems like equivocation to me. Even if they obey the
same modal logic, that only means they have the axioms and rules of
inference. It doesn't follow that the true but unprovable
propositions are the same propositions as the true but not-
believable ones.
It depends of your theory of belief. I agree that this concerns a form
of rational beliefs, extending the belief in Peano Axiom (or
combinators axioms, etc.) in a correct and recursively enumerable way
(using comp).
The hypostases will work for any correct machine whose beliefs
extend soundly the beliefs in elementary arithmetic.
The key is in the mathematical trick to limit us to correct
machine, with enough beliefs (about machines or numbers) so that
they are under the spell of the second incompleteness theorem, or
Löb, and can prove that.
But doesn't limiting us to a correct machine mean the []p-p ; isn't
that what correct means?
Yes.
The key point is that the machine itself cannot prove []p - p.
[]p-p is true, about the machine, but not provable in general by the
machine (which can already not prove
[]f-f).
Bruno
Brent
In the literature such machine/theories are qualified as being
sufficiently rich, but Löbian is shorter, (and then the Löb
formula also characterize their provability logic).
Bruno
Brent
Obviously, one cannot prove []p p, for very many statements, ie
[]p p does not entail []([o]p)
[]p - [][]p OK?
Why? This is not obvious. It translates as being able to prove that
you can prove stuff when you can prove it.
If this were a theorem of G, then it suggests G does not capture
the nature of proof.
Oh, I see that you are just restating axiom 4. But how can you
prove
that you've proven something? How does Boolos justify that?
(and []p - []p, and p - p) + ([](p p) - []p []q)
(derivable
in G)
Did you mean [](pq) - []p []q? That theorem at least sounds
plausable as being about proof.
so[]p p - [][]p ([]p p)
- []([]p p) ([]p p),
thus ([]p p) - [][o]p( [o]p : thus [o]p - [o][o]p)
Therefore, it cannot be that [o]p - [o]([o]p) ???
Something must be wrong...
I hope I am not too short above, (and that there is not to much
typo!)
Bruno
And thus you've proven that for everything you know, you can know
that
you know it. This seems wrong, as the 4 colour theorem indicates.
We
can prove the 4 colour theorem by means of a computer program,
and it
may indeed be correct, so that we Theatetically know the 4 colour
theorem is true, but we cannot prove the proof is correct (at
least at
this stage, proving program correctness is practically impossible).
--
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
Re: AUDA and pronouns
On 10/22/2013 5:48 AM, Bruno Marchal wrote:
On 21 Oct 2013, at 20:07, meekerdb wrote:
On 10/20/2013 11:12 PM, Russell Standish wrote:
On Sun, Oct 20, 2013 at 08:09:59PM -0700, meekerdb wrote:
Consistency is []p ~[]~p. I was saying []p ~p, ie mistaken belief.
ISTM that Bruno equivocates and [] sometimes means believes and sometimes
provable.
And I'm doing the same. It's not such an issue - a mathematician will
only believe something if e can prove it.
But provable(p)==p and believes(p)=/=p, so why equivocate on them?
Both provable('p') - p, and believe('p') - p, when we limit ourself to
correct machine.
(And incidentally mathematicians believe stuff they can't prove all the time - that's
how they choose things to try to prove).
Then it is a conjecture. They don't believe rationally in conjecture, when they
are correct.
They believe it in the real operational sense of believe, they will bet their whole
professional lives on it. How long did it take Andrew Wiles to prove Fermat's last
theorem? Since one can never know that one is a correct machine it seems to me a
muddling of things to equivocate on provable and believes.
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 http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 10/22/2013 6:19 AM, Bruno Marchal wrote:
[]p - p is correctness. It is trivially true for the machine I consider, because they
are correct by definition/choice.
Consistency is correctness on the f: []f - f. It is a very particular case of
correctness.
There are machines which are not correct, yet consistent. For example Peano-Arithmetic +
the axiom beweisbar('f').
Believing '0=1', does not make you inconsistent. Only non correct.
?? But in ordinary logic a false proposition allows you to prove anything. So if I prove
'0=1' then I can prove any proposition - which is the definition of inconsistency.
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 http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On Tue, Oct 22, 2013 at 3:52 PM, Bruno Marchal marc...@ulb.ac.be wrote: On 22 Oct 2013, at 03:21, Platonist Guitar Cowboy wrote: On Mon, Oct 21, 2013 at 4:15 PM, Bruno Marchal marc...@ulb.ac.be wrote: On 21 Oct 2013, at 04:48, Platonist Guitar Cowboy wrote: Disclaimer: No idea if I am even on the same planet on which this discussion is taking place. So pardon my questions and confusions: On Sun, Oct 20, 2013 at 11:15 PM, Russell Standish li...@hpcoders.com.au wrote: On Sun, Oct 20, 2013 at 06:22:15PM +0200, Bruno Marchal wrote: On 20 Oct 2013, at 12:01, Russell Standish wrote: On Sun, Oct 20, 2013 at 08:52:41AM +0200, Bruno Marchal wrote: We have always that [o]p - [o][o]p (like we have also always that []p - [][]p) There may be things we can prove, but about which we are in fact mistaken, ie []p -p That is consistent. (Shit happens, we became unsound). Consistency is []p ~[]~p. I was saying []p ~p, ie mistaken belief. Why Isn't mistaken belief here merely unsound because it's propositional variable, assuming we're speaking generally about all systems? Yes, []p —p, makes the machine on which [] applies, unsound. But still consistent. Such machines will believe (prove) an arithmetical false (but consistent) sentence. OK. Obviously, one cannot prove []p p, for very many statements, ie []p p does not entail []([o]p) Isn't that a rule for any modal sentence though, independent of system? [o]p is ([]p p) Isn't []p p = []([o]p) the definition of fixed point theorem? That, plus modalization conditionals to remove p from the G sentence so that every sentence H is a fixed point of it? This is a bit unclear. A fixed point is when a proposition says something about herself (like p - []p, p - [] ~p, etc.). The fixed point will be a proposition in which p does no more occur. The main one are: Ok, that is clearer. But this is a general rule in provability logic of every modal system, right? You can consider formula like p - [] (... p ...) in all modal logic, but few will have solution. This can be said: any K4 reasonner will have the fixed point in case he visit Knave/ Knight island. And that K4 reasonner will becaome a G reasonner (a Lôbian entity). Any K4 consistent machines rich enough (like PA, ZF, but unlike RA) will become Löbian too, and got the G-like fixed point. The Gödel diagonalization lemma will somehow emulate the Knight-Knaves island. [](p - ~[]p) - [](p - ~[]f) Gödel fixed point [](p - [] ¬p) = [](p- []⊥) Yes, that's the kind of thing I think we're talking about. OK. An important one is: [](p - p) - [](p - f) (all machines/sentences asserting their own consistency can prove 0=1) And the one related to Löb's theorem: [](p - []p) - [](p - t) That is very amazing: all machines/sentences asserting their own provability are true and provable. That's a sort arithmetical placebo. So that you get that list of instances with (G sentence on left and H on right) examples like the following: []p corresponds to T ¬[]p corresponds to ¬[]⊥ []¬p corresponds to []⊥, which is pretty cool because you get a provability statement that is arithmetically equivalent to its own non-provability iff the statement is equivalent to the statement that arithmetic is inconsistent. Because G proves in this fashion: [o](p = [] ¬p) = [o](p= []⊥) OK. This is the kind of thing that clarifies the pronoun issue imho. In arithmetic. But in UDA I think that the definition of first person/third person in term of reconstitution/annihilation is clear enough for the indeterminacy purpose, and the necessity of deriving physics from arithmetic. it is just not precise enough to get the actual technical beginning of the derivation of physics. []p - [][]p OK? Why? This is not obvious. It translates as being able to prove that you can prove stuff when you can prove it. If this were a theorem of G, then it suggests G does not capture the nature of proof. Oh, I see that you are just restating axiom 4. But how can you prove that you've proven something? How does Boolos justify that? But it nonetheless is everywhere in Boolos: []p - [][]p IS a theorem of G, and useful, unless Bruno shoots the cowboy, because he cannot prove it or find his damned Boolos book. What? You don't find your sacred manual? You will have to do some penitences or something :) Let me give you a difficult exercise: derive []p - [][]p in *any* normal modal logic satisfying Löb's formula (that is derive []p - [][]p from []([]p -p) - []p (and [](p-q)-([]p-[]q). Hmm, I'll try but feel free to ignore if there is too much bs in my attempt to remember from Boolos, for anything to be saved; find the book, return to earlier chapters will suffice). I choose GL from fuzzy memory as normal modal logic for the exercise: *GL derives []p - [][]p in a confused
Re: AUDA and pronouns
On Tue, Oct 22, 2013 at 03:09:03PM +0200, Bruno Marchal wrote: On 21 Oct 2013, at 23:03, Russell Standish wrote: In fact p- []p characterizes sigma_1 completeness (by a result by Albert Visser), and that is why to get the proba on the UD*, we use the intensional nuance []p t (= proba) starting from G extended with the axiom p- []p (limiting the proposition to the UD). proba? Sorry - I was actually asking what you meant by the word proba. Cheers -- Prof Russell Standish Phone 0425 253119 (mobile) Principal, High Performance Coders Visiting Professor of Mathematics hpco...@hpcoders.com.au University of New South Wales http://www.hpcoders.com.au -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On Sun, Oct 20, 2013 at 08:09:59PM -0700, meekerdb wrote: Consistency is []p ~[]~p. I was saying []p ~p, ie mistaken belief. ISTM that Bruno equivocates and [] sometimes means believes and sometimes provable. And I'm doing the same. It's not such an issue - a mathematician will only believe something if e can prove it. But if you like to subsitute mistaken proof for mistaken belief, go ahead. -- Prof Russell Standish Phone 0425 253119 (mobile) Principal, High Performance Coders Visiting Professor of Mathematics hpco...@hpcoders.com.au University of New South Wales http://www.hpcoders.com.au -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On Mon, Oct 21, 2013 at 04:48:42AM +0200, Platonist Guitar Cowboy wrote: Disclaimer: No idea if I am even on the same planet on which this discussion is taking place. So pardon my questions and confusions: You and me both - we're all students here :). I'm just rather doubtful about an axiomatisation of proof that assumes we can prove that we can prove something, as with that we can know that we (Theatetically) know something (since truth is usually inherently unknowable). It reminds me of a 3 year old's question but why? Ultimately, you will not be able to answer a question like that. It is quite possible I haven't drunk enough Kool-Aid. Question for Bruno (raised from PGC's earlier comments): Is axiom 4, ie []p - [][]p, called a fixed point theorem? Cheers -- Prof Russell Standish Phone 0425 253119 (mobile) Principal, High Performance Coders Visiting Professor of Mathematics hpco...@hpcoders.com.au University of New South Wales http://www.hpcoders.com.au -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 20 Oct 2013, at 23:15, Russell Standish wrote:
On Sun, Oct 20, 2013 at 06:22:15PM +0200, Bruno Marchal wrote:
On 20 Oct 2013, at 12:01, Russell Standish wrote:
On Sun, Oct 20, 2013 at 08:52:41AM +0200, Bruno Marchal wrote:
We have always that [o]p - [o][o]p (like we have also always that
[]p - [][]p)
There may be things we can prove, but about which we are in fact
mistaken, ie
[]p -p
That is consistent. (Shit happens, we became unsound).
Consistency is []p ~[]~p. I was saying []p ~p, ie mistaken belief.
I was saying that ( []p ~p) is consistent. ( []p ~[]~p) is p is
provable and p is consistent).
Mistaken belief is consistent with arithmetic.
Obviously, one cannot prove []p p, for very many statements, ie
[]p p does not entail []([o]p)
[]p - [][]p OK?
Why? This is not obvious. It translates as being able to prove that
you can prove stuff when you can prove it.
You are right, this is not so easy to prove. It follows from the
provable sigma_1 completeness, that is the fact that if p is a
sigma_1 formula, then Peano Arithmetic can prove p - Bp. (That is not
easy to prove, but it is done in Hilbert-Bernays, also in the books by
Boolos). It is the hard part of the second incompleteness theorem. It
presupposes some induction axioms, like in Peano Arithmetic (PA).
Then Bp is itself a sigma_1 arithmetical proposition, so []p - [][]p.
If this were a theorem of G, then it suggests G does not capture
the nature of proof.
PA, ZF, all Löbian machines prove []p - [][]p. That is why they are
intrspective enough. When they prove something, they can prove that
can prove that something.
Robinson Arithmetic, which has no induction axiom at all, cannot. It
is still sigma_1 complete, but cannot prove its own sigma_1
completeness, nor []p - [][]p. RA is typically NOT Löbian.
sigma_1 completeness = a provability characterization of Turing
universality. Löbian machines are universal, like RA, but unlike RA,
thay can prove (heir universality (in some weak sense).
Oh, I see that you are just restating axiom 4. But how can you prove
that you've proven something? How does Boolos justify that?
As I say, by showing that PA proves all instances of p - []p, for p
sigma_1. This is long and subtle to show.
Boolos 1979 sums it rather well, and Boolos 193, gives all the details
(but it is more messy).
(and []p - []p, and p - p) + ([](p p) - []p []q) (derivable
in G)
Did you mean [](pq) - []p []q?
Yes.
That theorem at least sounds
plausable as being about proof.
OK.
[]p - [][]p is not so astonishing, because the induction axioms
provides strong provability power to the theories.
Let me try to say a bit more. If PA proves p, PA will proves []p. This
is much more easy to prove, and is indeed captured by the
necessaitation rule p/[]p. That is almost obvious, because if PA
proves p, such a proof exists, and thus has a Gödel number, and the
machines will prove it (provable('p') is sigma_1, and the theories are
sigma_1 complete).
That is true for both RA and PA. But PA, like ZF, can internalise that
rule (p/[]p), they can proof in general that []p - [][]p. This will
be proved by induction on the complexity of the formula p, and well,
it is not easy at all to see that.
so[]p p - [][]p ([]p p)
- []([]p p) ([]p p),
thus ([]p p) - [][o]p( [o]p : thus [o]p - [o][o]p)
Therefore, it cannot be that [o]p - [o]([o]p) ???
Something must be wrong...
I hope I am not too short above, (and that there is not to much
typo!)
Bruno
And thus you've proven that for everything you know, you can know that
you know it. This seems wrong, as the 4 colour theorem indicates.
I would not trust my intuition about this.
We
can prove the 4 colour theorem by means of a computer program, and it
may indeed be correct, so that we Theatetically know the 4 colour
theorem is true, but we cannot prove the proof is correct (at least at
this stage, proving program correctness is practically impossible).
It should be easy once we have a concrete formal proof. As far as I
know, we don't have this for the 4 colour theorem. But once we have
such proofs, it should be trivial to prove that the proof exists,
making []p - [][]p easy to prove for the particular case of p = 4-
color.
A correct machine is automatically Löbian if she is sigma_1 complete,
and has enough induction axioms to prove its own sigma_1 completeness
(in the sense of proving all formula p - []p, for p sigma_1).
In fact p- []p characterizes sigma_1 completeness (by a result by
Albert Visser), and that is why to get the proba on the UD*, we use
the intensional nuance []p t (= proba) starting from G extended
with the axiom p- []p (limiting the proposition to the UD).
Bruno
--
Prof Russell Standish Phone 0425
Re: AUDA and pronouns
On 20 Oct 2013, at 21:03, John Mikes wrote: Brent: I like to write insted of we know - we THINK we know and it goes further: Bruno's provable' - in many cases - applies evidences (to 'prove') from conventional science (reductionist figments) we still THINK we know. Not when doing science. (pseudo-science and pseudo-religion only). I don't think I use the term T R U E at all - in my agnosticism. You still need some notion of possible truth, without which 'agnosticism lost his meaning. This can lead to instrumentalism. You had a remark lately to remind me that our 'imperfect' worldview resulted in many many practical achievements so far. I did not respond the missing adjective almost - meaning the many failures and mishaps such achievements are involved with. We approach the practical usability. Another chapter includes math - the result of certain HUMAN logic - in which 17 is defined as a 'prime'. A different logic may devise a different math with different number-concept in which the equivalent of 17 is NOT a prime. You will need a theory with more forms of absolute to develop the idea that 17 is prime is a human logic relative idea. Bruno I find it a mathematically impressed concept that the 'world' is describable by numbers (arithmetic series) and not vice versa. Nobody showed me so far a natural occurrence where arithmetic connotations were detectable by non-arithmetic trains of thought. JohnM On Sat, Oct 19, 2013 at 6:16 PM, meekerdb meeke...@verizon.net wrote: On 10/19/2013 3:08 PM, Russell Standish wrote: On Tue, Oct 08, 2013 at 08:17:17PM +0200, Bruno Marchal wrote: On 08 Oct 2013, at 11:51, Russell Standish wrote: I understand Bp can be read as I can prove p, and Bpp as I know p. But in the case, the difference between Bp and Bpp is entirely in the verb, the pronoun I stays the same, AFAICT. Correct. Only the perspective change. Bp is Toto proves p, said by Toto. Bp p is Toto proves p and p is true, as said by Toto (or not), and the math shows that this behaves like a knowledge opertaor (but not arithmetical predicate). It's the same Toto in both cases... What's the point? The difference is crucial. Bp obeys to the logic G, which does not define a knower as we don't have Bp - p. At best, it defines a rational believer, or science. Not knowledge. But differentiating W from M, is knowledge, even non communicable knowledge. You can't explain to another, that you are the one in Washington, as for the other, you are also in Moscow. Knowledge logic invite us to define the first person by the knower. He is the only one who can know that his pain is not fake, for example. You've hinted at fixed points being relevant here for the concept of I. So to have an 'I', you need the statement []p-p to be a theorem? and Bpp as he knows p, so the person order of the pronoun is also not relevant. Yes, you can read that in that way, but you get only the 3-view of the 1-view. Let us define [o]p by Bp p I am just pointing on the difference between B([o]p) and [o]([o]p). ??? B([o]p) is the statement made by the ideal rationalist believer (B) on a first person point of view ([o]). Here [o]p can be seen as an abbreviation for Bp p. In English, the first statement is that I believe I know something, and the second is that I know I know somthing. [o]([o]p is the first person statement ([o]) on a first person point of view ([o]). So, according to you, knowledge is a first person point of view. What I still get stuck on is that we may know many things, but the only things we can know we know are essentially private things things, such as the fact that we are conscious, or what the colour red seems like to us. Bruno seems to equate know with provable and true. So we know that 17 is prime. In fact we *know* infinitely many theorems that are provable, but which no one will ever prove - which seems like a strange meaning of know. Brent Are these all things you would say satisfy the proposition [o]([o]p) -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out. -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out. http://iridia.ulb.ac.be/~marchal/ -- You received this message
Re: AUDA and pronouns
On 21 Oct 2013, at 05:09, meekerdb wrote: On 10/20/2013 2:15 PM, Russell Standish wrote: On Sun, Oct 20, 2013 at 06:22:15PM +0200, Bruno Marchal wrote: On 20 Oct 2013, at 12:01, Russell Standish wrote: On Sun, Oct 20, 2013 at 08:52:41AM +0200, Bruno Marchal wrote: We have always that [o]p - [o][o]p (like we have also always that []p - [][]p) There may be things we can prove, but about which we are in fact mistaken, ie []p -p That is consistent. (Shit happens, we became unsound). Consistency is []p ~[]~p. I was saying []p ~p, ie mistaken belief. ISTM that Bruno equivocates and [] sometimes means believes and sometimes provable. But I am allowed to do that, because []p - p is not a theorem (for some p, by incompleteness) and thus (rational formal) provability behaves like believability. A mathematician told me that I was dead mad by saying this, but that is standard in mathematical logic (ignored by most mathematicians). It is counter-intuitive. Most people believes that formal proof guaranties truth, when starting from true theorem (and that is true for the ideally correct machine, but no machine can know she is correct, and her probability does behave like a believability, indeed one on Which the application of Theaetus' definition leads to the classical knowledge logic (the modal logic S4). The hypostases will work for any correct machine whose beliefs extend soundly the beliefs in elementary arithmetic. The key is in the mathematical trick to limit us to correct machine, with enough beliefs (about machines or numbers) so that they are under the spell of the second incompleteness theorem, or Löb, and can prove that. In the literature such machine/theories are qualified as being sufficiently rich, but Löbian is shorter, (and then the Löb formula also characterize their provability logic). Bruno Brent Obviously, one cannot prove []p p, for very many statements, ie []p p does not entail []([o]p) []p - [][]p OK? Why? This is not obvious. It translates as being able to prove that you can prove stuff when you can prove it. If this were a theorem of G, then it suggests G does not capture the nature of proof. Oh, I see that you are just restating axiom 4. But how can you prove that you've proven something? How does Boolos justify that? (and []p - []p, and p - p) + ([](p p) - []p []q) (derivable in G) Did you mean [](pq) - []p []q? That theorem at least sounds plausable as being about proof. so[]p p - [][]p ([]p p) - []([]p p) ([]p p), thus ([]p p) - [][o]p( [o]p : thus [o]p - [o][o]p) Therefore, it cannot be that [o]p - [o]([o]p) ??? Something must be wrong... I hope I am not too short above, (and that there is not to much typo!) Bruno And thus you've proven that for everything you know, you can know that you know it. This seems wrong, as the 4 colour theorem indicates. We can prove the 4 colour theorem by means of a computer program, and it may indeed be correct, so that we Theatetically know the 4 colour theorem is true, but we cannot prove the proof is correct (at least at this stage, proving program correctness is practically impossible). -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out. 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 10/20/2013 11:12 PM, Russell Standish wrote: On Sun, Oct 20, 2013 at 08:09:59PM -0700, meekerdb wrote: Consistency is []p ~[]~p. I was saying []p ~p, ie mistaken belief. ISTM that Bruno equivocates and [] sometimes means believes and sometimes provable. And I'm doing the same. It's not such an issue - a mathematician will only believe something if e can prove it. But provable(p)==p and believes(p)=/=p, so why equivocate on them? (And incidentally mathematicians believe stuff they can't prove all the time - that's how they choose things to try to prove). Brent But if you like to subsitute mistaken proof for mistaken belief, go ahead. -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On Mon, Oct 21, 2013 at 11:07:04AM -0700, meekerdb wrote: On 10/20/2013 11:12 PM, Russell Standish wrote: On Sun, Oct 20, 2013 at 08:09:59PM -0700, meekerdb wrote: Consistency is []p ~[]~p. I was saying []p ~p, ie mistaken belief. ISTM that Bruno equivocates and [] sometimes means believes and sometimes provable. And I'm doing the same. It's not such an issue - a mathematician will only believe something if e can prove it. But provable(p)==p and believes(p)=/=p, so why equivocate on them? (And incidentally mathematicians believe stuff they can't prove all the time - that's how they choose things to try to prove). Brent An unproven theorem is a conjecture. I don't think a mathematician would formally say that they believe in a conjecture, they would say something like assume for the present argument. Of course, when they take their mathematician's hat off, they would say they believe in all sorts of unprovable things, like democracy, free speech, etc. Anyway, this is probably getting a little off topic. Bruno's answer is probably better. -- Prof Russell Standish Phone 0425 253119 (mobile) Principal, High Performance Coders Visiting Professor of Mathematics hpco...@hpcoders.com.au University of New South Wales http://www.hpcoders.com.au -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On Mon, Oct 21, 2013 at 03:52:14PM +0200, Bruno Marchal wrote: On 20 Oct 2013, at 23:15, Russell Standish wrote: On Sun, Oct 20, 2013 at 06:22:15PM +0200, Bruno Marchal wrote: On 20 Oct 2013, at 12:01, Russell Standish wrote: Obviously, one cannot prove []p p, for very many statements, ie []p p does not entail []([o]p) []p - [][]p OK? Why? This is not obvious. It translates as being able to prove that you can prove stuff when you can prove it. You are right, this is not so easy to prove. It follows from the provable sigma_1 completeness, that is the fact that if p is a sigma_1 formula, then Peano Arithmetic can prove p - Bp. (That is not easy to prove, but it is done in Hilbert-Bernays, also in the books by Boolos). It is the hard part of the second incompleteness theorem. It presupposes some induction axioms, like in Peano Arithmetic (PA). Then Bp is itself a sigma_1 arithmetical proposition, so []p - [][]p. i.e If p is the result of a computer program, then there exists a program that proves p is correct? And thus you've proven that for everything you know, you can know that you know it. This seems wrong, as the 4 colour theorem indicates. I would not trust my intuition about this. In choosing axioms, intuition is all we have to go by. But you say below that 4 is in fact a redundant axiom ... which makes it not so clear cut. We can prove the 4 colour theorem by means of a computer program, and it may indeed be correct, so that we Theatetically know the 4 colour theorem is true, but we cannot prove the proof is correct (at least at this stage, proving program correctness is practically impossible). It should be easy once we have a concrete formal proof. As far as I know, we don't have this for the 4 colour theorem. But once we have such proofs, it should be trivial to prove that the proof exists, making []p - [][]p easy to prove for the particular case of p = 4-color. How does it make it easy? A correct machine is automatically Löbian if she is sigma_1 complete, and has enough induction axioms to prove its own sigma_1 completeness (in the sense of proving all formula p - []p, for p sigma_1). In fact p- []p characterizes sigma_1 completeness (by a result by Albert Visser), and that is why to get the proba on the UD*, we use the intensional nuance []p t (= proba) starting from G extended with the axiom p- []p (limiting the proposition to the UD). proba? -- Prof Russell Standish Phone 0425 253119 (mobile) Principal, High Performance Coders Visiting Professor of Mathematics hpco...@hpcoders.com.au University of New South Wales http://www.hpcoders.com.au -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
Bruno wrote *Not when doing science. (pseudo-science and pseudo-religion only).* * * Science as applied to the so far learned fraction of the infinite complexity? If there ever was a 'pseudo-science' - that is one (I mean the conventional pretension used for those ALMOST perfect technicalities Brent was mentioning to me.) Our 'model' (science?) is constantly growing. So: NEWER arguments are emerging and older ones are rejected. I appreciate your parallel between science and religion. Our world is a fractional model so far cleared to the capabilities of the human mentality. Are you thinking of SCIENCE (all caps) of the infinite Universal M., not reachable presently for us weak-minded humans? *You still need some notion of possible truth, without which 'agnosticism lost his meaning. This can lead to instrumentalism.* *** *You will need a theory with more forms of absolute to develop the idea that 17 is prime is a human logic relative idea.* * * Agnosticism - for me - is not a philosophical theorem: it is just marking our ignorance about 'all of it' except for the few we already GOT and adjusted to the meek capabilities of the developing human mind. I am also at a loss how I would driven towards 'instrumentalism'. In my (virgin?) agnosticism I even leave open what kind of content could be - and HOW - intertwined in the (unknowable) infinite complexity, which has SOME influence upon - how we visualize at all our 'model-world content'. Absolutes are scientific/religious belief items we try to hold on to. Possible truth is our figment. About 17? I am no mathematician, so a fantasy of math-systems is free to me. I figure a dynamic number-world flipping between series of its own integers, like the base of 'your' arithmetic and another one like expressable as 1.7, 3.4, 5.1... in which 17 is a tenfold of the first one, not a prime. This would be with all the 'primes' in our primitive number-world. Flip-flop. (Just musing!) Not so incredible for an Infinite Universal Machine. (I have imagination). As for now I am not (yet?) asking for a patent on this system. Have a good Halloween John Mikes On Mon, Oct 21, 2013 at 9:56 AM, Bruno Marchal marc...@ulb.ac.be wrote: On 20 Oct 2013, at 21:03, John Mikes wrote: Brent: I like to write insted of we know - we THINK we know and it goes further: Bruno's provable' - in many cases - applies evidences (to 'prove') from conventional science (reductionist figments) we still THINK we know. Not when doing science. (pseudo-science and pseudo-religion only). I don't think I use the term T R U E at all - in my agnosticism. You still need some notion of possible truth, without which 'agnosticism lost his meaning. This can lead to instrumentalism. You had a remark lately to remind me that our 'imperfect' worldview resulted in many many practical achievements so far. I did not respond the missing adjective almost - meaning the many failures and mishaps such achievements are involved with. We approach the practical usability. Another chapter includes math - the *result* of certain HUMAN logic - in which 17 is defined as a 'prime'. A different logic may devise a different math with different number-concept in which the equivalent of 17 is NOT a prime. You will need a theory with more forms of absolute to develop the idea that 17 is prime is a human logic relative idea. Bruno I find it a mathematically impressed concept that the 'world' is describable by numbers (arithmetic series) and not vice versa. Nobody showed me so far a natural occurrence where arithmetic connotations were detectable by non-arithmetic trains of thought. JohnM On Sat, Oct 19, 2013 at 6:16 PM, meekerdb meeke...@verizon.net wrote: On 10/19/2013 3:08 PM, Russell Standish wrote: On Tue, Oct 08, 2013 at 08:17:17PM +0200, Bruno Marchal wrote: On 08 Oct 2013, at 11:51, Russell Standish wrote: I understand Bp can be read as I can prove p, and Bpp as I know p. But in the case, the difference between Bp and Bpp is entirely in the verb, the pronoun I stays the same, AFAICT. Correct. Only the perspective change. Bp is Toto proves p, said by Toto. Bp p is Toto proves p and p is true, as said by Toto (or not), and the math shows that this behaves like a knowledge opertaor (but not arithmetical predicate). It's the same Toto in both cases... What's the point? The difference is crucial. Bp obeys to the logic G, which does not define a knower as we don't have Bp - p. At best, it defines a rational believer, or science. Not knowledge. But differentiating W from M, is knowledge, even non communicable knowledge. You can't explain to another, that you are the one in Washington, as for the other, you are also in Moscow. Knowledge logic invite us to define the first person by the knower. He is the only one who can know that his pain is not fake, for example. You've hinted at fixed points being relevant here for the concept of I. So to have an
Re: AUDA and pronouns
On 22 October 2013 10:51, John Mikes jami...@gmail.com wrote: About 17? I am no mathematician, so a fantasy of math-systems is free to me. I figure a dynamic number-world flipping between series of its own integers, like the base of 'your' arithmetic and another one like expressable as 1.7, 3.4, 5.1... in which 17 is a tenfold of the first one, not a prime. This would be with all the 'primes' in our primitive number-world. Flip-flop. (Just musing!) The point about 17 being prime is that it's prime within a certain system of maths, and *that* fact is invariant across all possible universes. There are other mathematical systems in which 17 isn't prime, and those will also hold true across all possible universes. Universes don't come with different systems of maths attached. At least that's the idea, and the point, of arithmetical realism. -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On Tue, Oct 22, 2013 at 03:21:48AM +0200, Platonist Guitar Cowboy wrote: On Mon, Oct 21, 2013 at 4:15 PM, Bruno Marchal marc...@ulb.ac.be wrote: [](p - ~[]p) - [](p - ~[]f) Gödel fixed point [](p = [] ¬p) = [](p= []⊥) Yes, that's the kind of thing I think we're talking about. Talk about hazards of doing things by email. I was going to ask what a bare [] means, then when I opened up the editor (which supports unicode), I see that the original sentence was []⊥ ([]f) -- Prof Russell Standish Phone 0425 253119 (mobile) Principal, High Performance Coders Visiting Professor of Mathematics hpco...@hpcoders.com.au University of New South Wales http://www.hpcoders.com.au -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 10/19/2013 9:21 PM, Platonist Guitar Cowboy wrote: On Sun, Oct 20, 2013 at 12:16 AM, meekerdb meeke...@verizon.net mailto:meeke...@verizon.net wrote: Bruno seems to equate know with provable and true. I'm not sure that is precise. To me, Bruno's use mostly mirrors the use in the Plato dialogues as knowledge is true belief accounted for. So X knows p is true iff: p is true, X believes p, X can account for or justify their belief. PGC I've suggested that: knowledge = justified true belief. But apparently that leaves out too much or is too vague for him. Brent So we know that 17 is prime. In fact we *know* infinitely many theorems that are provable, but which no one will ever prove - which seems like a strange meaning of know. Brent Are these all things you would say satisfy the proposition [o]([o]p) -- 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 mailto:everything-list%2bunsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com mailto:everything-list@googlegroups.com. Visit this group at http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out. -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out. No virus found in this message. Checked by AVG - www.avg.com http://www.avg.com Version: 2014.0.4158 / Virus Database: 3614/6756 - Release Date: 10/16/13 -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 20 Oct 2013, at 00:08, Russell Standish wrote: On Tue, Oct 08, 2013 at 08:17:17PM +0200, Bruno Marchal wrote: On 08 Oct 2013, at 11:51, Russell Standish wrote: I understand Bp can be read as I can prove p, and Bpp as I know p. But in the case, the difference between Bp and Bpp is entirely in the verb, the pronoun I stays the same, AFAICT. Correct. Only the perspective change. Bp is Toto proves p, said by Toto. Bp p is Toto proves p and p is true, as said by Toto (or not), and the math shows that this behaves like a knowledge opertaor (but not arithmetical predicate). It's the same Toto in both cases... What's the point? The difference is crucial. Bp obeys to the logic G, which does not define a knower as we don't have Bp - p. At best, it defines a rational believer, or science. Not knowledge. But differentiating W from M, is knowledge, even non communicable knowledge. You can't explain to another, that you are the one in Washington, as for the other, you are also in Moscow. Knowledge logic invite us to define the first person by the knower. He is the only one who can know that his pain is not fake, for example. You've hinted at fixed points being relevant here for the concept of I. Yes. So to have an 'I', you need the statement []p-p to be a theorem? Yes. ([o]p - p). It is the main axiom of knowledge. We can know, by definition, only truth. If we realize we were wrong, we realize that it was not knowledge but belief. We can never be sure if we know or belief, except for consciousness here and now. and Bpp as he knows p, so the person order of the pronoun is also not relevant. Yes, you can read that in that way, but you get only the 3-view of the 1-view. Let us define [o]p by Bp p I am just pointing on the difference between B([o]p) and [o]([o]p). ??? B([o]p) is the statement made by the ideal rationalist believer (B) on a first person point of view ([o]). Here [o]p can be seen as an abbreviation for Bp p. In English, the first statement is that I believe I know something, and the second is that I know I know somthing. OK. [o]([o]p is the first person statement ([o]) on a first person point of view ([o]). So, according to you, knowledge is a first person point of view. Yes. Knowledge is given by the beliefs that we share with God (Truth). What I still get stuck on is that we may know many things, but the only things we can know we know are essentially private things things, such as the fact that we are conscious, or what the colour red seems like to us. Are these all things you would say satisfy the proposition [o]([o]p) Yes. for the correct machines. Of course we don't know that we are correct, so in practice, it is less easy, far less easy. But we don't need that to get the physics. Bruno 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 10/19/2013 11:38 PM, Bruno Marchal wrote: What I still get stuck on is that we may know many things, but the only things we can know we know are essentially private things things, such as the fact that we are conscious, or what the colour red seems like to us. Are you leaving out the axioms and theorems of arithmetic? Are they not things we know and are public? Brent Are these all things you would say satisfy the proposition [o]([o]p) Yes. for the correct machines. Of course we don't know that we are correct, so in practice, it is less easy, far less easy. But we don't need that to get the physics. -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 20 Oct 2013, at 00:48, Russell Standish wrote: On Sat, Oct 19, 2013 at 03:16:52PM -0700, meekerdb wrote: Bruno seems to equate know with provable and true. So we know that 17 is prime. In fact we *know* infinitely many theorems that are provable, but which no one will ever prove - which seems like a strange meaning of know. I agree that it is strange, but acknowledge that the definition does have some history. ATM, I'm trying to just understand why he says certain things, given the definitions he uses. Assuming 17 is prime, then yes - we know that 17 is prime. But do we know that we know 17 is prime? [o][o] (17 is prime) is true, because [o] ([] 17 is prime 17 is prime) That is [] ([] 17 is prime 17 is prime)[] (17 is prime) 17 is prime On the other hand, if p is prime, then p is divisible only by 1 and p. This statement is indisputably true, as it is the definition of prime. So we can know this, and we know we know this. We have always that [o]p - [o][o]p (like we have also always that []p - [][]p) Which is an example of an x satisfying [o]([o]x), that is not of subjective character. Hmmm ? Sometimes we know objective things. The knowledge is subjective, but the known thing can be objective. Bruno 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On Sun, Oct 20, 2013 at 08:52:41AM +0200, Bruno Marchal wrote: We have always that [o]p - [o][o]p (like we have also always that []p - [][]p) There may be things we can prove, but about which we are in fact mistaken, ie []p -p Obviously, one cannot prove []p p, for very many statements, ie []p p does not entail []([o]p) Therefore, it cannot be that [o]p - [o]([o]p) ??? Something must be wrong... -- Prof Russell Standish Phone 0425 253119 (mobile) Principal, High Performance Coders Visiting Professor of Mathematics hpco...@hpcoders.com.au University of New South Wales http://www.hpcoders.com.au -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 20 Oct 2013, at 12:01, Russell Standish wrote: On Sun, Oct 20, 2013 at 08:52:41AM +0200, Bruno Marchal wrote: We have always that [o]p - [o][o]p (like we have also always that []p - [][]p) There may be things we can prove, but about which we are in fact mistaken, ie []p -p That is consistent. (Shit happens, we became unsound). In that case we can prove Bf. From this we still cannot prove f (Bf - f = ~Bf = I am consistent (3p self-reference). Obviously, one cannot prove []p p, for very many statements, ie []p p does not entail []([o]p) []p - [][]p OK? (and []p - []p, and p - p) + ([](p p) - []p []q) (derivable in G) so[]p p - [][]p ([]p p) - []([]p p) ([]p p), thus ([]p p) - [][o]p( [o]p : thus [o]p - [o][o]p) Therefore, it cannot be that [o]p - [o]([o]p) ??? Something must be wrong... I hope I am not too short above, (and that there is not to much typo!) Bruno -- Prof Russell Standish Phone 0425 253119 (mobile) Principal, High Performance Coders Visiting Professor of Mathematics hpco...@hpcoders.com.au University of New South Wales http://www.hpcoders.com.au -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out. 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On Sun, Oct 20, 2013 at 06:22:15PM +0200, Bruno Marchal wrote: On 20 Oct 2013, at 12:01, Russell Standish wrote: On Sun, Oct 20, 2013 at 08:52:41AM +0200, Bruno Marchal wrote: We have always that [o]p - [o][o]p (like we have also always that []p - [][]p) There may be things we can prove, but about which we are in fact mistaken, ie []p -p That is consistent. (Shit happens, we became unsound). Consistency is []p ~[]~p. I was saying []p ~p, ie mistaken belief. Obviously, one cannot prove []p p, for very many statements, ie []p p does not entail []([o]p) []p - [][]p OK? Why? This is not obvious. It translates as being able to prove that you can prove stuff when you can prove it. If this were a theorem of G, then it suggests G does not capture the nature of proof. Oh, I see that you are just restating axiom 4. But how can you prove that you've proven something? How does Boolos justify that? (and []p - []p, and p - p) + ([](p p) - []p []q) (derivable in G) Did you mean [](pq) - []p []q? That theorem at least sounds plausable as being about proof. so[]p p - [][]p ([]p p) - []([]p p) ([]p p), thus ([]p p) - [][o]p( [o]p : thus [o]p - [o][o]p) Therefore, it cannot be that [o]p - [o]([o]p) ??? Something must be wrong... I hope I am not too short above, (and that there is not to much typo!) Bruno And thus you've proven that for everything you know, you can know that you know it. This seems wrong, as the 4 colour theorem indicates. We can prove the 4 colour theorem by means of a computer program, and it may indeed be correct, so that we Theatetically know the 4 colour theorem is true, but we cannot prove the proof is correct (at least at this stage, proving program correctness is practically impossible). -- Prof Russell Standish Phone 0425 253119 (mobile) Principal, High Performance Coders Visiting Professor of Mathematics hpco...@hpcoders.com.au University of New South Wales http://www.hpcoders.com.au -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
Disclaimer: No idea if I am even on the same planet on which this discussion is taking place. So pardon my questions and confusions: On Sun, Oct 20, 2013 at 11:15 PM, Russell Standish li...@hpcoders.com.auwrote: On Sun, Oct 20, 2013 at 06:22:15PM +0200, Bruno Marchal wrote: On 20 Oct 2013, at 12:01, Russell Standish wrote: On Sun, Oct 20, 2013 at 08:52:41AM +0200, Bruno Marchal wrote: We have always that [o]p - [o][o]p (like we have also always that []p - [][]p) There may be things we can prove, but about which we are in fact mistaken, ie []p -p That is consistent. (Shit happens, we became unsound). Consistency is []p ~[]~p. I was saying []p ~p, ie mistaken belief. Why Isn't mistaken belief here merely unsound because it's propositional variable, assuming we're speaking generally about all systems? Obviously, one cannot prove []p p, for very many statements, ie []p p does not entail []([o]p) Isn't that a rule for any modal sentence though, independent of system? [o]p is ([]p p) Isn't []p p = []([o]p) the definition of fixed point theorem? That, plus modalization conditionals to remove p from the G sentence so that every sentence H is a fixed point of it? So that you get that list of instances with (G sentence on left and H on right) examples like the following: []p corresponds to T ¬[]p corresponds to ¬[]⊥ []¬p corresponds to []⊥, which is pretty cool because you get a provability statement that is arithmetically equivalent to its own non-provability iff the statement is equivalent to the statement that arithmetic is inconsistent. Because G proves in this fashion: [o](p = [] ¬p) = [o](p= []⊥) This is the kind of thing that clarifies the pronoun issue imho. []p - [][]p OK? Why? This is not obvious. It translates as being able to prove that you can prove stuff when you can prove it. If this were a theorem of G, then it suggests G does not capture the nature of proof. Oh, I see that you are just restating axiom 4. But how can you prove that you've proven something? How does Boolos justify that? But it nonetheless is everywhere in Boolos: []p - [][]p IS a theorem of G, and useful, unless Bruno shoots the cowboy, because he cannot prove it or find his damned Boolos book. (and []p - []p, and p - p) + ([](p p) - []p []q) (derivable in G) Did you mean [](pq) - []p []q? I'm not sure of the q and whether you can just leave out the first bit. That theorem at least sounds plausable as being about proof. so[]p p - [][]p ([]p p) - []([]p p) ([]p p), thus ([]p p) - [][o]p( [o]p : thus [o]p - [o][o]p) Therefore, it cannot be that [o]p - [o]([o]p) ??? Something must be wrong... Why? I hope I am not too short above, (and that there is not to much typo!) Bruno And thus you've proven that for everything you know, you can know that you know it. Not sure, I'd guess we're comparing G's reasoning 3rd person I with reasoning of a fixed point corresponding to some sentence of G 1st person I in a modal/qualitative provability sense. PGC This seems wrong, as the 4 colour theorem indicates. We can prove the 4 colour theorem by means of a computer program, and it may indeed be correct, so that we Theatetically know the 4 colour theorem is true, but we cannot prove the proof is correct (at least at this stage, proving program correctness is practically impossible). -- Prof Russell Standish Phone 0425 253119 (mobile) Principal, High Performance Coders Visiting Professor of Mathematics hpco...@hpcoders.com.au University of New South Wales http://www.hpcoders.com.au -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out. -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 10/20/2013 2:15 PM, Russell Standish wrote: On Sun, Oct 20, 2013 at 06:22:15PM +0200, Bruno Marchal wrote: On 20 Oct 2013, at 12:01, Russell Standish wrote: On Sun, Oct 20, 2013 at 08:52:41AM +0200, Bruno Marchal wrote: We have always that [o]p - [o][o]p (like we have also always that []p - [][]p) There may be things we can prove, but about which we are in fact mistaken, ie []p -p That is consistent. (Shit happens, we became unsound). Consistency is []p ~[]~p. I was saying []p ~p, ie mistaken belief. ISTM that Bruno equivocates and [] sometimes means believes and sometimes provable. Brent Obviously, one cannot prove []p p, for very many statements, ie []p p does not entail []([o]p) []p - [][]p OK? Why? This is not obvious. It translates as being able to prove that you can prove stuff when you can prove it. If this were a theorem of G, then it suggests G does not capture the nature of proof. Oh, I see that you are just restating axiom 4. But how can you prove that you've proven something? How does Boolos justify that? (and []p - []p, and p - p) + ([](p p) - []p []q) (derivable in G) Did you mean [](pq) - []p []q? That theorem at least sounds plausable as being about proof. so[]p p - [][]p ([]p p) - []([]p p) ([]p p), thus ([]p p) - [][o]p( [o]p : thus [o]p - [o][o]p) Therefore, it cannot be that [o]p - [o]([o]p) ??? Something must be wrong... I hope I am not too short above, (and that there is not to much typo!) Bruno And thus you've proven that for everything you know, you can know that you know it. This seems wrong, as the 4 colour theorem indicates. We can prove the 4 colour theorem by means of a computer program, and it may indeed be correct, so that we Theatetically know the 4 colour theorem is true, but we cannot prove the proof is correct (at least at this stage, proving program correctness is practically impossible). -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 10/19/2013 3:08 PM, Russell Standish wrote: On Tue, Oct 08, 2013 at 08:17:17PM +0200, Bruno Marchal wrote: On 08 Oct 2013, at 11:51, Russell Standish wrote: I understand Bp can be read as I can prove p, and Bpp as I know p. But in the case, the difference between Bp and Bpp is entirely in the verb, the pronoun I stays the same, AFAICT. Correct. Only the perspective change. Bp is Toto proves p, said by Toto. Bp p is Toto proves p and p is true, as said by Toto (or not), and the math shows that this behaves like a knowledge opertaor (but not arithmetical predicate). It's the same Toto in both cases... What's the point? The difference is crucial. Bp obeys to the logic G, which does not define a knower as we don't have Bp - p. At best, it defines a rational believer, or science. Not knowledge. But differentiating W from M, is knowledge, even non communicable knowledge. You can't explain to another, that you are the one in Washington, as for the other, you are also in Moscow. Knowledge logic invite us to define the first person by the knower. He is the only one who can know that his pain is not fake, for example. You've hinted at fixed points being relevant here for the concept of I. So to have an 'I', you need the statement []p-p to be a theorem? and Bpp as he knows p, so the person order of the pronoun is also not relevant. Yes, you can read that in that way, but you get only the 3-view of the 1-view. Let us define [o]p by Bp p I am just pointing on the difference between B([o]p) and [o]([o]p). ??? B([o]p) is the statement made by the ideal rationalist believer (B) on a first person point of view ([o]). Here [o]p can be seen as an abbreviation for Bp p. In English, the first statement is that I believe I know something, and the second is that I know I know somthing. [o]([o]p is the first person statement ([o]) on a first person point of view ([o]). So, according to you, knowledge is a first person point of view. What I still get stuck on is that we may know many things, but the only things we can know we know are essentially private things things, such as the fact that we are conscious, or what the colour red seems like to us. Bruno seems to equate know with provable and true. So we know that 17 is prime. In fact we *know* infinitely many theorems that are provable, but which no one will ever prove - which seems like a strange meaning of know. Brent Are these all things you would say satisfy the proposition [o]([o]p) -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On Sat, Oct 19, 2013 at 03:16:52PM -0700, meekerdb wrote: Bruno seems to equate know with provable and true. So we know that 17 is prime. In fact we *know* infinitely many theorems that are provable, but which no one will ever prove - which seems like a strange meaning of know. I agree that it is strange, but acknowledge that the definition does have some history. ATM, I'm trying to just understand why he says certain things, given the definitions he uses. Assuming 17 is prime, then yes - we know that 17 is prime. But do we know that we know 17 is prime? On the other hand, if p is prime, then p is divisible only by 1 and p. This statement is indisputably true, as it is the definition of prime. So we can know this, and we know we know this. Which is an example of an x satisfying [o]([o]x), that is not of subjective character. Hmmm -- Prof Russell Standish Phone 0425 253119 (mobile) Principal, High Performance Coders Visiting Professor of Mathematics hpco...@hpcoders.com.au University of New South Wales http://www.hpcoders.com.au -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On Sun, Oct 20, 2013 at 12:16 AM, meekerdb meeke...@verizon.net wrote: Bruno seems to equate know with provable and true. I'm not sure that is precise. To me, Bruno's use mostly mirrors the use in the Plato dialogues as knowledge is true belief accounted for. So X knows p is true iff: p is true, X believes p, X can account for or justify their belief. PGC So we know that 17 is prime. In fact we *know* infinitely many theorems that are provable, but which no one will ever prove - which seems like a strange meaning of know. Brent Are these all things you would say satisfy the proposition [o]([o]p) -- 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+unsubscribe@**googlegroups.comeverything-list%2bunsubscr...@googlegroups.com . To post to this group, send email to everything-list@googlegroups.**comeverything-list@googlegroups.com . Visit this group at http://groups.google.com/**group/everything-listhttp://groups.google.com/group/everything-list . For more options, visit https://groups.google.com/**groups/opt_outhttps://groups.google.com/groups/opt_out . -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 09 Oct 2013, at 22:02, meekerdb wrote: On 10/9/2013 12:26 AM, Bruno Marchal wrote: On 08 Oct 2013, at 20:35, meekerdb wrote: On 10/8/2013 2:51 AM, Russell Standish wrote: On Mon, Oct 07, 2013 at 10:20:14AM +0200, Bruno Marchal wrote: On 07 Oct 2013, at 07:36, Russell Standish wrote: ... and Bpp as he knows p, so the person order of the pronoun is also not relevant. Yes, you can read that in that way, but you get only the 3-view of the 1-view. Let us define [o]p by Bp p I am just pointing on the difference between B([o]p) and [o] ([o]p). Isn't B(Bp)=Bp so: Bp - B(Bp) but B(Bp) does not necessarly imply Bp. ?? That seems like strange logic. Certainly. It came as a shock. It is the shock of Gödel and Löb incompleteness results. Those are truly revolutionary. If you find this strange and shocking, it means you begin to grasp! How, in classical logic, can you prove that p is provable and yet not conclude that p is provable. I understand that the set of true propositions is bigger than the provable propositions, but I don't see that the set of provably provable propositions is smaller than the provable propositions? See below. B(Bp p) =? B(Bp p) (Bp P) Why would that be? [o](Bp p) = B(Bp p) (Bp p), but not B(Bp p), because B(Bp p) does not imply Bp p. Not that I wrote =? meaning is it equal?, not asserting it was equal, and I concluded below they were not equal. You think like that because you know that B is correct, but B does not know it. In particular, like Bf - f is true about B, but not provable by B, B(Bf)- Bf is also true about B, but not provable by B. Here B designates the machine/person having B as provability predicate. Bruno Brent Bp =? Bp p - false And so, this does not follow. (Keep in mind that Bp does not imply p, from the machine's point of view). Think about Bf, if it implies f, we would have that the machine would know that ~Bf, and knows that she is consistent. She can't, if she is correct. Bruno 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out. 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 08 Oct 2013, at 20:35, meekerdb wrote: On 10/8/2013 2:51 AM, Russell Standish wrote: On Mon, Oct 07, 2013 at 10:20:14AM +0200, Bruno Marchal wrote: On 07 Oct 2013, at 07:36, Russell Standish wrote: ... and Bpp as he knows p, so the person order of the pronoun is also not relevant. Yes, you can read that in that way, but you get only the 3-view of the 1-view. Let us define [o]p by Bp p I am just pointing on the difference between B([o]p) and [o]([o]p). Isn't B(Bp)=Bp so: Bp - B(Bp) but B(Bp) does not necessarly imply Bp. B(Bp p) =? B(Bp p) (Bp P) Why would that be? [o](Bp p) = B(Bp p) (Bp p), but not B(Bp p), because B(Bp p) does not imply Bp p. Bp =? Bp p - false And so, this does not follow. (Keep in mind that Bp does not imply p, from the machine's point of view). Think about Bf, if it implies f, we would have that the machine would know that ~Bf, and knows that she is consistent. She can't, if she is correct. Bruno 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 10/9/2013 12:26 AM, Bruno Marchal wrote: On 08 Oct 2013, at 20:35, meekerdb wrote: On 10/8/2013 2:51 AM, Russell Standish wrote: On Mon, Oct 07, 2013 at 10:20:14AM +0200, Bruno Marchal wrote: On 07 Oct 2013, at 07:36, Russell Standish wrote: ... and Bpp as he knows p, so the person order of the pronoun is also not relevant. Yes, you can read that in that way, but you get only the 3-view of the 1-view. Let us define [o]p by Bp p I am just pointing on the difference between B([o]p) and [o]([o]p). Isn't B(Bp)=Bp so: Bp - B(Bp) but B(Bp) does not necessarly imply Bp. ?? That seems like strange logic. How, in classical logic, can you prove that p is provable and yet not conclude that p is provable. I understand that the set of true propositions is bigger than the provable propositions, but I don't see that the set of provably provable propositions is smaller than the provable propositions? B(Bp p) =? B(Bp p) (Bp P) Why would that be? [o](Bp p) = B(Bp p) (Bp p), but not B(Bp p), because B(Bp p) does not imply Bp p. Not that I wrote =? meaning is it equal?, not asserting it was equal, and I concluded below they were not equal. Brent Bp =? Bp p - false And so, this does not follow. (Keep in mind that Bp does not imply p, from the machine's point of view). Think about Bf, if it implies f, we would have that the machine would know that ~Bf, and knows that she is consistent. She can't, if she is correct. Bruno 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
Thanks for this response. It'll take me a while to digest, but I'll get back with the inevitable questions :). On Tue, Oct 08, 2013 at 08:17:17PM +0200, Bruno Marchal wrote: On 08 Oct 2013, at 11:51, Russell Standish wrote: On Mon, Oct 07, 2013 at 10:20:14AM +0200, Bruno Marchal wrote: On 07 Oct 2013, at 07:36, Russell Standish wrote: Unfortunately, the thread about AUDA and its relation to pronouncs got mixed up with another thread, and thus got delete on my computer. Picking up from where we left off, I'm still trying to see the relationship between Bp, Bpp, 1-I, 3-I and the plain ordinary I pronoun in English. As I said, in natural language we usually mix 1-I (Bp) and 3-I (Bp p). The reason is that we think we have only one body, and so, in all practical situation it does not matter. (That's also why some people will say I am my body, or I am my brain, like Searles, which used that against comp, but if that was valid, the math shows that machines can validly shows that they are not machine, which is absurd). The difference 1-I/3-I is felt sometimes by people looking at a video of themselves. The objective situation can describe many people, and you feel bizarre that you are one of them. That video lacks of course the first person perspective. The distinction is brought when we study the mind body problem. You might red the best text ever on this: the Theaetetus of Plato. But the indians have written many texts on this, and some are chef-d'oeuvre (rigorous). OK, although I don't have time to read those ancient texts, alas :(. OK. I can understand. The Theaetetus is very short, though. I understand Bp can be read as I can prove p, and Bpp as I know p. But in the case, the difference between Bp and Bpp is entirely in the verb, the pronoun I stays the same, AFAICT. Correct. Only the perspective change. Bp is Toto proves p, said by Toto. Bp p is Toto proves p and p is true, as said by Toto (or not), and the math shows that this behaves like a knowledge opertaor (but not arithmetical predicate). It's the same Toto in both cases... What's the point? The difference is crucial. Bp obeys to the logic G, which does not define a knower as we don't have Bp - p. At best, it defines a rational believer, or science. Not knowledge. But differentiating W from M, is knowledge, even non communicable knowledge. You can't explain to another, that you are the one in Washington, as for the other, you are also in Moscow. Knowledge logic invite us to define the first person by the knower. He is the only one who can know that his pain is not fake, for example. So, the ideally correct machine will never been able to ascribe a name or a description to it. Intuitively, for the machine, that I is not assertable, and indeed such opertair refer to something without a name. What does it mean to assert an I? I was meaning to assert I, with the idea that you refer to something understandable for another. You can assert the 3-I, in this sense, but not the 1-I. Now, without duplication, it looks all the time like there is a simple link between 3-I, and 1-I, and that is why we confuse them, but with the experience of duplication, at some point, the distinction is unavoidable, and crucial, and the simple link between is broken, forcing the reversal between math and physics (arithmetic and physics). Also, switching viewpoints, one could equally say the Bp can be read as he can prove p, but the point is that it is asserted by he, in the language of he. But the statements can also be asserted by some other agent? Of course. But in that case it is no more a third person *self*-reference (3-I). My hat is green contains a third person self-reference. My wife's hat is green contains a third person self-reference. The hat of Napoleon is green does not. Only third person references. The logic of provable (third person) self-reference is given by the modal logic G (by Gödel, Löb, Solovay). The logic of true (third person) self-reference is given by G*. It always concerns, in our setting, what an ideally correct machine can rationally believe on itself. The interesting thing is that G* proves Bp - (Bp p), but G does not prove it. It shows that both the rational believer and the knower see the same (tiny) part of Arithmetic, yet see it from different points of view, and the logic will mathematically differ. The logic of B is G, and the logic of Bp p is S4Grz. and Bpp as he knows p, so the person order of the pronoun is also not relevant. Yes, you can read that in that way, but you get only the 3-view of the 1-view. Let us define [o]p by Bp p I am just pointing on the difference between B([o]p) and [o]([o]p). ??? B([o]p) is the statement made by the ideal rationalist believer (B) on a first person point of view ([o]). Here [o]p can be seen
Re: AUDA and pronouns
On Mon, Oct 07, 2013 at 10:20:14AM +0200, Bruno Marchal wrote: On 07 Oct 2013, at 07:36, Russell Standish wrote: Unfortunately, the thread about AUDA and its relation to pronouncs got mixed up with another thread, and thus got delete on my computer. Picking up from where we left off, I'm still trying to see the relationship between Bp, Bpp, 1-I, 3-I and the plain ordinary I pronoun in English. As I said, in natural language we usually mix 1-I (Bp) and 3-I (Bp p). The reason is that we think we have only one body, and so, in all practical situation it does not matter. (That's also why some people will say I am my body, or I am my brain, like Searles, which used that against comp, but if that was valid, the math shows that machines can validly shows that they are not machine, which is absurd). The difference 1-I/3-I is felt sometimes by people looking at a video of themselves. The objective situation can describe many people, and you feel bizarre that you are one of them. That video lacks of course the first person perspective. The distinction is brought when we study the mind body problem. You might red the best text ever on this: the Theaetetus of Plato. But the indians have written many texts on this, and some are chef-d'oeuvre (rigorous). OK, although I don't have time to read those ancient texts, alas :(. I understand Bp can be read as I can prove p, and Bpp as I know p. But in the case, the difference between Bp and Bpp is entirely in the verb, the pronoun I stays the same, AFAICT. Correct. Only the perspective change. Bp is Toto proves p, said by Toto. Bp p is Toto proves p and p is true, as said by Toto (or not), and the math shows that this behaves like a knowledge opertaor (but not arithmetical predicate). It's the same Toto in both cases... What's the point? So, the ideally correct machine will never been able to ascribe a name or a description to it. Intuitively, for the machine, that I is not assertable, and indeed such opertair refer to something without a name. What does it mean to assert an I? Also, switching viewpoints, one could equally say the Bp can be read as he can prove p, but the point is that it is asserted by he, in the language of he. But the statements can also be asserted by some other agent? and Bpp as he knows p, so the person order of the pronoun is also not relevant. Yes, you can read that in that way, but you get only the 3-view of the 1-view. Let us define [o]p by Bp p I am just pointing on the difference between B([o]p) and [o]([o]p). ??? Best, Bruno 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out. -- Prof Russell Standish Phone 0425 253119 (mobile) Principal, High Performance Coders Visiting Professor of Mathematics hpco...@hpcoders.com.au University of New South Wales http://www.hpcoders.com.au -- 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 08 Oct 2013, at 11:51, Russell Standish wrote: On Mon, Oct 07, 2013 at 10:20:14AM +0200, Bruno Marchal wrote: On 07 Oct 2013, at 07:36, Russell Standish wrote: Unfortunately, the thread about AUDA and its relation to pronouncs got mixed up with another thread, and thus got delete on my computer. Picking up from where we left off, I'm still trying to see the relationship between Bp, Bpp, 1-I, 3-I and the plain ordinary I pronoun in English. As I said, in natural language we usually mix 1-I (Bp) and 3-I (Bp p). The reason is that we think we have only one body, and so, in all practical situation it does not matter. (That's also why some people will say I am my body, or I am my brain, like Searles, which used that against comp, but if that was valid, the math shows that machines can validly shows that they are not machine, which is absurd). The difference 1-I/3-I is felt sometimes by people looking at a video of themselves. The objective situation can describe many people, and you feel bizarre that you are one of them. That video lacks of course the first person perspective. The distinction is brought when we study the mind body problem. You might red the best text ever on this: the Theaetetus of Plato. But the indians have written many texts on this, and some are chef-d'oeuvre (rigorous). OK, although I don't have time to read those ancient texts, alas :(. OK. I can understand. The Theaetetus is very short, though. I understand Bp can be read as I can prove p, and Bpp as I know p. But in the case, the difference between Bp and Bpp is entirely in the verb, the pronoun I stays the same, AFAICT. Correct. Only the perspective change. Bp is Toto proves p, said by Toto. Bp p is Toto proves p and p is true, as said by Toto (or not), and the math shows that this behaves like a knowledge opertaor (but not arithmetical predicate). It's the same Toto in both cases... What's the point? The difference is crucial. Bp obeys to the logic G, which does not define a knower as we don't have Bp - p. At best, it defines a rational believer, or science. Not knowledge. But differentiating W from M, is knowledge, even non communicable knowledge. You can't explain to another, that you are the one in Washington, as for the other, you are also in Moscow. Knowledge logic invite us to define the first person by the knower. He is the only one who can know that his pain is not fake, for example. So, the ideally correct machine will never been able to ascribe a name or a description to it. Intuitively, for the machine, that I is not assertable, and indeed such opertair refer to something without a name. What does it mean to assert an I? I was meaning to assert I, with the idea that you refer to something understandable for another. You can assert the 3-I, in this sense, but not the 1-I. Now, without duplication, it looks all the time like there is a simple link between 3-I, and 1-I, and that is why we confuse them, but with the experience of duplication, at some point, the distinction is unavoidable, and crucial, and the simple link between is broken, forcing the reversal between math and physics (arithmetic and physics). Also, switching viewpoints, one could equally say the Bp can be read as he can prove p, but the point is that it is asserted by he, in the language of he. But the statements can also be asserted by some other agent? Of course. But in that case it is no more a third person *self*- reference (3-I). My hat is green contains a third person self-reference. My wife's hat is green contains a third person self-reference. The hat of Napoleon is green does not. Only third person references. The logic of provable (third person) self-reference is given by the modal logic G (by Gödel, Löb, Solovay). The logic of true (third person) self-reference is given by G*. It always concerns, in our setting, what an ideally correct machine can rationally believe on itself. The interesting thing is that G* proves Bp - (Bp p), but G does not prove it. It shows that both the rational believer and the knower see the same (tiny) part of Arithmetic, yet see it from different points of view, and the logic will mathematically differ. The logic of B is G, and the logic of Bp p is S4Grz. and Bpp as he knows p, so the person order of the pronoun is also not relevant. Yes, you can read that in that way, but you get only the 3-view of the 1-view. Let us define [o]p by Bp p I am just pointing on the difference between B([o]p) and [o]([o]p). ??? B([o]p) is the statement made by the ideal rationalist believer (B) on a first person point of view ([o]). Here [o]p can be seen as an abbreviation for Bp p. [o]([o]p is the first person statement ([o]) on a first person point of view ([o]). Just to illustrate John Clark's probable confusion, roughly translated in arithmetical terms, is the confusion of B
Re: AUDA and pronouns
On 10/8/2013 2:51 AM, Russell Standish wrote: On Mon, Oct 07, 2013 at 10:20:14AM +0200, Bruno Marchal wrote: On 07 Oct 2013, at 07:36, Russell Standish wrote: ... and Bpp as he knows p, so the person order of the pronoun is also not relevant. Yes, you can read that in that way, but you get only the 3-view of the 1-view. Let us define [o]p by Bp p I am just pointing on the difference between B([o]p) and [o]([o]p). Isn't B(Bp)=Bp so: B(Bp p) =? B(Bp p) (Bp P) Bp =? Bp p - false 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 10/6/2013 10:36 PM, Russell Standish wrote: Unfortunately, the thread about AUDA and its relation to pronouncs got mixed up with another thread, and thus got delete on my computer. Picking up from where we left off, I'm still trying to see the relationship between Bp, Bpp, 1-I, 3-I and the plain ordinary I pronoun in English. I understand Bp can be read as I can prove p, and Bpp as I know p. But in the case, the difference between Bp and Bpp is entirely in the verb, the pronoun I stays the same, AFAICT. Also, switching viewpoints, one could equally say the Bp can be read as he can prove p, and Bpp as he knows p, so the person order of the pronoun is also not relevant. Notice though how different I can prove the 4-color theorem. is from The 4-color theorem is true. 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 07 Oct 2013, at 07:36, Russell Standish wrote: Unfortunately, the thread about AUDA and its relation to pronouncs got mixed up with another thread, and thus got delete on my computer. Picking up from where we left off, I'm still trying to see the relationship between Bp, Bpp, 1-I, 3-I and the plain ordinary I pronoun in English. As I said, in natural language we usually mix 1-I (Bp) and 3-I (Bp p). The reason is that we think we have only one body, and so, in all practical situation it does not matter. (That's also why some people will say I am my body, or I am my brain, like Searles, which used that against comp, but if that was valid, the math shows that machines can validly shows that they are not machine, which is absurd). The difference 1-I/3-I is felt sometimes by people looking at a video of themselves. The objective situation can describe many people, and you feel bizarre that you are one of them. That video lacks of course the first person perspective. The distinction is brought when we study the mind body problem. You might red the best text ever on this: the Theaetetus of Plato. But the indians have written many texts on this, and some are chef-d'oeuvre (rigorous). I understand Bp can be read as I can prove p, and Bpp as I know p. But in the case, the difference between Bp and Bpp is entirely in the verb, the pronoun I stays the same, AFAICT. Correct. Only the perspective change. Bp is Toto proves p, said by Toto. Bp p is Toto proves p and p is true, as said by Toto (or not), and the math shows that this behaves like a knowledge opertaor (but not arithmetical predicate). So, the ideally correct machine will never been able to ascribe a name or a description to it. Intuitively, for the machine, that I is not assertable, and indeed such opertair refer to something without a name. Also, switching viewpoints, one could equally say the Bp can be read as he can prove p, but the point is that it is asserted by he, in the language of he. and Bpp as he knows p, so the person order of the pronoun is also not relevant. Yes, you can read that in that way, but you get only the 3-view of the 1-view. Let us define [o]p by Bp p I am just pointing on the difference between B([o]p) and [o]([o]p). Best, Bruno 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
Re: AUDA and pronouns
On 07 Oct 2013, at 10:20, Bruno Marchal wrote (to Russell): Yes, you can read that in that way, but you get only the 3-view of the 1-view. I meant: you get only the 3-view ON the 1-view. Not of. Sorry, Bruno 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 http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
