On 12 Jun 2012, at 00:47, Russell Standish wrote:
On Thu, Jun 07, 2012 at 01:33:48PM +0200, Bruno Marchal wrote:
In fact we have p/p for any p. If you were correct we would have []p
for any p.
This is what I thought you said the "meta-axiom" stated?
How else do we get p/[]p for Kripke semantics?
Because if p is true in all worlds, then []p is true in all worlds OK?
If p is true in all worlds (validity) then p is true in particular in
all worlds accessible from alpha, and so []p is true in alpha, and
this works for any alpha, so []p is true in all worlds.
In a deduction, without proviso, p means that we have already proved
p, (or in some case, that it is an assumption but you have to be
careful).
The meta-semantics of a rule is dependent on the theory, and the way
we define what constitutes a proof. In modal logic it usually mean,
in "p/[]p" that p occur at the end of a proof.
Self-reference is confusing because deduction "p/q" get represented by
[](p->q), or []p->[]q.
[]p is the machine's language for the machine asserts (believes,
proves) p. All universal machine, when they asserts p, will soon or
later asserts []p. So []p -> [][]p is true about all universal
(correct) machines.
The löbian machine are those for which []p -> [][]p is not only true,
but they actually can justify why they know that []p -> [][]p. It is
the kind of truth they can communicate.
So the fact p/q is modeled by []p->[]q, in the language of the machine.
Löbian machines are close for the Löb rule. If they asserts []p -> p,
they will inevitably asserts soon or later p.
And they know that, which means they can prove []([]p->p)->[]p, for
each p arithmetical sentences, in the arithmetical interpretations.
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 post to this group, send email to everything-list@googlegroups.com.
To unsubscribe from this group, send email to everything-list+unsubscr...@googlegroups.com
.
For more options, visit this group at http://groups.google.com/group/everything-list?hl=en
.
http://iridia.ulb.ac.be/~marchal/
--
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To post to this group, send email to everything-list@googlegroups.com.
To unsubscribe from this group, send email to
everything-list+unsubscr...@googlegroups.com.
For more options, visit this group at
http://groups.google.com/group/everything-list?hl=en.
