On 08 Mar 2015, at 23:47, meekerdb wrote:
On 3/8/2015 2:07 PM, LizR wrote:
On 9 March 2015 at 05:36, Bruno Marchal <marc...@ulb.ac.be> wrote:
On 07 Mar 2015, at 09:36, LizR wrote:
I thought <>P meant P was possible?
In the alethic interpretation of modal logic, <> means possible,
and [] means necessary.
Before I get lost in logic, just going by the verbal descriptions...
Am I right in thinking that "p" means "p is true" ?
So p -> <>p would mean "p is true implies that it's possible p is
true"
In the temporal interpretation of modal logic, <> means sometime,
and [] means always.
p is true implies that p is sometimes true
In the locus interpretation of modal logic, <> means somewhere, and
[] means everywhere.
...somewhere...
In the deontic interpretation of modal logic, <> means permitted,
and [] means obligatory.
p is permitted (by whom?!)
etc.
Note that all "<>" interpretation are form of possibility (alethic,
temporal, locative, ...).
In our interview of the Löbian machine, <> is translated in
arithmetic with Gödel beweisbar predicate:
In particular: <>t is consistency.
<>t = ~[] f = ~ beweisbar ("0 = 1"), with "0=1" being a number
coding the sentence "0 = s(0)".
OK, so this is saying that p -> <>p would mean "if p is true then
that implies that p is consistent" - which, roughly speaking, is
what Godel showed to be wrong.
Beweisbar(x) = Ey proof(y, x), that is: it exist a proof (y) of x.
Proof must be mechanically checkable, and so, like sentences, they
can be coded into numbers, and the predicate proof just decode the
proof named by y and looks if it proves the sentence coded by x.
<>t = ~[] f means intuitively, as said by PA: "PA does not prove
the false", or "PA is consistent".
So to summarize you don't want p->[]p as a modal axiom because it
particularizes to t->[]t which says all true propositions are
provable, contrary to Godel's theorem.
I guess there are typo error here. You mean p -> <>p.
I just have no choice, p are for arbitrary arithmetical proposition,
and <> is for ~beweisbar ~p.
Now G* proves p -> <>p, and this means that this is true for the
machine, bu G does not prove it, which means that the machine cannot
alway justify that fact.
And if you know Gödels theorem, you know that already with t, we don't
have t -> <>t. If G proves that G would prove <>t, and the machine
would prove its consistency, which she can't.
Godel proved PA incompleteness by diagonalization on classes of
numbers. But this applies to PA, not to every axiom set.
It applies on every axiom set rich enough to define what is computation.
So why not conclude there is something wrong with PA?
It applies to all recursively enumerable extension of PA. It applies
to us, by comp, and assuming we are consistent "enough" (which is the
case in the ideal case by construction).
To me it seems more intuitively compelling to say p-><>p than to say
every number has a successor and deny p-><>p.
You confuse the non intuitive truth about us, with the intuition of
the first person. yes, they do oppose, that is why []p, []p & p, []p &
<>t, []p & <>t & p, obey different logic.
The first person, S4Grz does prove p -> <>p. And, yes, it is very hard
to her to bet she is a machine, and she is correct by doing so. So the
machine's soul, in some sense, is not a machine. I explained this to
Craig sometimes ago.
But I don't defend comp, I just show that with comp, physics and
theology become branch of number theory. This makes comp testable,
just compare the computer-physics with nature.
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/d/optout.
http://iridia.ulb.ac.be/~marchal/
--
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.
