# Re: The limit of all computations

```
On 28 May 2012, at 11:35, Russell Standish wrote:```
```
```
```On Mon, May 28, 2012 at 10:37:53AM +0200, Bruno Marchal wrote:
```
```
On 28 May 2012, at 04:00, Russell Standish wrote:

```
```On Sun, May 27, 2012 at 06:20:29PM +0200, Bruno Marchal wrote:
```
```
On 27 May 2012, at 12:15, Russell Standish wrote:
```
I still don't follow. If I have proved a is true in some world, why
```should I infer that it is true in all worlds? What am I missing?
```
```
I realize my previous answer might be too long and miss your
question. Apology if it is the case.

Here is a shorter answer. The idea of proving, is that what is
```
proved in true in all possible world. If not, a world would exist as
```a counter-example, invalidating the argument.
```
```
I certainly missed that. Is that given as an axiom?
```
```
That would be a meta-axiom in a theory defining what is logic. But
that does not exist. It is just part of what logic intuitively
consists in.
```
```
Well, I can tell you, it is not intuitive! Perhaps there is some
background understanding that is missing.
```
```
```
Yes. Logic, I am afraid. Logic the field, not logic as we use it everyday. Don't worry, virtually all non professional logicians miss it. And logicians miss that non logician miss it. It is a very technical field.
```
```
But the idea that proof, or Bp, entails truth in all world/model is given by the completeness theorem of GĂ¶del, or by Kripke semantics (with "all worlds" becoming "all accessible worlds"). See my previous post.
```

```
```
```
```Logicians are not interested of truth or interpretation of
statements. They are interested in validity. What sentences follow
from what sentences, independently of interpretations, and thus true
in all possible worlds.

```
```It seems like that
would be written p -> []p.
```
```
This means that if p then p is provable. "p -> Bp", if B = provable,
```
```
[]p means (primarily) true in all worlds. In Kripke semantics, it is
relativised to mean true in all accessible worlds.
```
```
Yes.

```
```
The meaning of provability is a different interpretation.
```
```
```
Yes. But then there are relations linking them. See my previous post on Solovay theorem which makes such a relation, and which can be sum up by: G is the modal logic of provability.
```

```
```

```
```

```
```
When I say p is true in a world, I can only prove that p is true in
that world.
```
```
I don't think so. If p is true, that does not mean you can prove it,
neither in your world, nor in some other world.
```
```
```
p may be true, but if I don't know it (or can't prove it), I shouldn't be
```asserting it :).
```
```
```
OK. But the fact is that p might be true in your world, and you can know or not that fact, independently of the fact that you can prove it or not. We have to distinguish "p is true" with "p is proved", "p is known", "p is observed", etc. All those modalities obeys different logics. Besides, if you can prove p, this does not make it true in your world, as Bp -> p, might be non provable, or even false. In that cse your world is not accessible from your world: the accessibility relation is not reflexive (that is the case for G). In a cul-de-sac world, Bf -> f is false for example. Typically, a cul- de-sac world does not access to itself, indeed it accesses to no world at all.
```

```
```
```
```

```
```I am mute on the subject of whether p is true in any other
world (unless I can use an axiom like the above).
```
```
By the logicians notion of proof, if you prove a proposition, it is
true in all worlds/model/interpretation.

```
```
Even if the proof relied upon some facet that may or may not be true
in all worlds?
```
```
```
Yes, because that facets will need to be 'conditionalized upon' in your world ... to have a proof. A world is a semantic notion, and you cannot refer to it in a proof (an error well illustrated by Craig, with all my respect).
```
Bruno

```
```
```
```
```
```
In what class of logics would such an axiom be taken to be true.
```
```
All.

```
```
--

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