Re: join post

From: Bruno Marchal <>
Date: Wed, 26 Nov 2008 16:54:13 +0100

Hi Abram,

On 26 Nov 2008, at 00:01, Abram Demski wrote:

> Bruno,
> Yes, I have encountered the provability logics before, but I am no
> expert.

We will perhaps have opportunity to talk about this.

>>> In any given
>>> generation, the entity who can represent the truth-predicate of the
>>> most other entities will dominate.
>> Why?
> The notion of the entities adapting their logics in order to better
> reason about each other is meant to be more of an informal
> justification than an exact proof, so I'm not worried about stating my
> assumptions precisely... If I did, I might simply take this to be an
> assumption rather than a derived fact. But, here is an informal
> justification.
> Since the entities start out using first-order logic, it will be
> useful to solve the halting problem to reach conclusions about what a
> fellow-creature *won't* ever reach conclusions about. This means a
> "provable" predicate will be useful. To support deduction with this
> predicate, of course, the entities will gain more and more axioms over
> time; axioms that help solve instances of the halting problem will
> survive, while axioms that provide incorrect information will not.
> This means that the "provable" predicate has a moving target: more and
> more is provable over time.

All right.

> Eventually it will become useful to
> abstract away from the details with a "true" predicate.

Here, assuming the mechanist hypothesis (or some weakening), the way
the "truth predicate" is introduced is really what will decide if the
soul of the machine will fall in Hell, or get enlightened and go to
Heaven. The all encompassing "truth" is not even nameable or
describable by the machines.

> The "true"
> predicate essentially says "provable by some sufficiently evolved
> system". This allows an entity to ignore the details of the entity it
> is currently reasoning about.

If PA (Peano Arithmetic) deduces "I can prove that I am consistent"
from "I can prove that ZF (Zermelo Fraenkel Set Theory) proves that I
am consistent", then PA goes to hell!
If an entity refers to a more powerful entity, even if "we" trust that
more powerful entity, it just an invalid "argument of authority".
Of course if PA begins to *believe* in the axioms of ZF, then PA
becomes ZF, and can assert the consistency of PA without problem. But
then, "we" are no more talking *about* PA, but about ZF.

> This won't always work-- sometimes it
> will need to resort to reasoning about provability again. But, it
> should be a useful concept (after all, we find it to be so).

Sure. But truth is really an interrogation mark. We can only "search"

>>> Of course, this gives rise to an outlandish number of truth-values
>>> (one
>>> for each ordinal number), when normally any more than 2 is
>>> considered
>>> questionable.
>> Not really, because those truth value are, imo, not really truth
>> value, but they quantify a ladder toward infinite credibility,
>> assurance or something. Perhaps security.
> I agree that the explosion of "truth-values" is acceptable because
> they are not really truth-values... but they do not go further and
> further into absolute confidence, but rather further and further into
> meaninglessness. Obviously my previous explanation was not adequate.
> First we have "true" and "false". Dealing with these in an
> unrestricted manner, we can construct sentences such as "this sentence
> is false".

I don't think we can really do that. We cannot, I think. (And I can
prove this making the assumption
that we are ideally sound universal machines).

> We need to label these somehow as meaningless or
> pathological. I think either a fixed-point construction or the
> revision theory are OK options for doing this;

In my opinion, revision theories are useful when a machine begins to
bet on an universal environment independent of herself. Above her
Godel-Lob-Solovay correct self-reference logic, she will have to
develop a non monotonic surface to be able to handle its errors,
dreams, etc. It is a bit more close to practical artifiicial
intelligence engineering than machine theology, but I am ok with that.

> perhaps one is better
> than the other, perhaps they are ultimately equivalent where it
> matters, I don't know. Anyway, now we are stuck with a new predicate:
> "meaningless". Using this in an unrestricted manner, I can say "this
> sentence is either meaningless or false". I need to rule this out, but
> I can't label it "meaningless", or I will then conclude it is true
> (assuming something like classical logic). So I need to invent a new
> predicate, 2-meaningless. Using this in an unrestricted manner again
> would lead to trouble, so I'll need 3-meaningless and 4-meaningless
> and finitely-meaningless and countably-meaningless and so on.

Indeed. It seems you make the point.


Bruno Marchal

You received this message because you are subscribed to the Google Groups "Everything List" group.
To post to this group, send email to
To unsubscribe from this group, send email to
For more options, visit this group at
Received on Wed Nov 26 2008 - 10:54:26 PST

This archive was generated by hypermail 2.3.0 : Fri Feb 16 2018 - 13:20:15 PST