On 5/29/2013 9:52 AM, Bruno Marchal wrote:
On 29 May 2013, at 18:37, Bruno Marchal wrote:
On 29 May 2013, at 17:47, Quentin Anciaux wrote:
http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems#Construction_of_a_statement_about_.22provability.22
2013/5/29 John Clark <johnkcl...@gmail.com <mailto:johnkcl...@gmail.com>>
On Wed, May 29, 2013 at 2:37 AM, Bruno Marchal <marc...@ulb.ac.be
<mailto:marc...@ulb.ac.be>> wrote:
>> If you want to communicate why should I need to search at all? And
if
even Google doesn't know what the hell Bp&p is then it's ridiculous to
expect
your readers to know what you're talking about.
> Come on, John. Search for "true opinion". Bp & p is a formula using
some
notation for this,
So when I read your post and you said "Bp & p" I should have said to myself
"obviously if I Google "true opinion" it will tell me what Bp & p means.
Well,
that is not obvious to me at all but it doesn't matter because I just
Googled
"true opinion" and I still can't find a damn thing about Bp & p.
Bp = I believe in p, or 'my opinion is that it is the case that p', or, in the context
of ideally correct (and simple machine): Beweisbar('p').
p, when produced by some system, means, in all books on logic, that p is true (from
the system pov).
So Bp & p is a ay to model true opinion, in some system.
When I write I always ask myself if anybody will understand what I say, I
may not
always be successful in making myself clear but at least I try. You're not
even
trying.
I have explained this more than one times on this list, to different people, because
once you get it you can't forget.
You have come perhaps too much recently, but you can always ask question. You should
not focus on the formula, but on what it represents. It is also explained in sane04,
and basically, in all my papers on this subject. Probably with different notations.
Or perhaps you just agree with what Niels Bohr said "I refuse to speak more
clearly than I think".
Bp is for "I believe p", produced by some machinery (machine, formal system,
...).
In particular, it is an expression in some modal logic. 'Belief' obeys usually
the axioms:
1. B(p->q) -> B(p -> Bq)
2. Bp -> BBp
Bp & p means "(I believe in p) and p". P alone, in the assertative mode of some entity
means "it is the case that p". (independently of the veracity of p).
For knowledge, we use the axiom:
3. Bp -> p
As Gödel saw in 1933, beweisbar, or provability, does not obey to that third axiom, and
so provability cannot model knowledgeability. Indeed no consistent machine can prove
B('0=1') -> 0=1, which is equivalent with ~B('0=1'), which is self-consistency.
I'm not sure I understand this. Are you saying we cannot take "(Bp->p) for all p" as an
axiom because it would entail Bf ->f and then ~f->~Bf, and since ~f is true by definition
it would entail that the machine is consistent?
Brent
But it is trivial that the new connector Kp, defined by Bp & p, verifies the axiom 3.
So we get a way to associate a knower to a machine. But it cannot be defined in
arithmetic, as you would need to define a predicate like B('p') & true('p'), which
cannot exist by a theorem of Tarski saying that true is not definable. We can only
simulate it by the modal trick of Theaetetus, for each arithmetical formula. For example,
"I know that 1+1=2" can be emulated by B('1+1=2') & 1+1=2. But you cannot find a
general arithmetical predicate for knowledge, and this makes such kind of knowledge
confirming many studies by philosophers and theologian, in the computer science setting.
Here belief is always a form of rational belief, which is basically the meaning of the
axiom 1 above.
Is is clearer? Ask anything.
I have already given such explanation here, and I will at some point later explain this
again on FOAR. No need to be angry or something,
Bruno
Oops!
Of course I was talking to J. Clark, not Quentin.
Sorry,
Bruno
http://iridia.ulb.ac.be/~marchal/ <http://iridia.ulb.ac.be/%7Emarchal/>
--
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+unsubscr...@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?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.
http://iridia.ulb.ac.be/~marchal/ <http://iridia.ulb.ac.be/%7Emarchal/>
No virus found in this message.
Checked by AVG - www.avg.com <http://www.avg.com>
Version: 2013.0.3343 / Virus Database: 3184/6366 - Release Date: 05/29/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?hl=en.
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?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.
