- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: Abram Demski <abramdemski.domain.name.hidden>

Date: Tue, 25 Nov 2008 18:01:29 -0500

Bruno,

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

*>> 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. Eventually it will become useful to

abstract away from the details with a "true" predicate. 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. 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).

*>> 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". 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; 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.

--Abram

On Mon, Nov 24, 2008 at 5:03 PM, Bruno Marchal <marchal.domain.name.hidden> wrote:

*>
*

*>
*

*> On 24 Nov 2008, at 21:52, Abram Demski wrote:
*

*>
*

*>>
*

*>> Hi Bruno,
*

*>>
*

*>>> I am not sure I follow you here. All what Godel's incompleteness
*

*>>> proves is that no machine, or no axiomatisable theory can solve all
*

*>>> halting problems.
*

*>>> The undecidability is always relative to such or such theory or
*

*>>> machine prover. For self-modifying theorem prover, the undecidable
*

*>>> sentence can evolve. (extensionaly, and yet remain the same
*

*>>> intensionally)
*

*>>
*

*>> I agree with everything you say there, so I'm not sure where you
*

*>> aren't following me. I definitely agree with the idea of a
*

*>> self-modifying theorem prover that becomes stronger over time-- I
*

*>> think it is the right model. What I am saying in the paragraph you
*

*>> quoted is that one "way out" is to claim that when we add axioms to
*

*>> strengthen our system, we can choose either the axiom or the negation
*

*>> arbitrarily, since either is consistent with the system so far. I've
*

*>> argued with people who explicitly claim this. My opinion is that there
*

*>> is only one correct choice for each addition.
*

*>
*

*> I agree, for a category of pure machine, not yet confronted to some
*

*> "bigger or older" universal machine.
*

*>
*

*>
*

*>> In the case of the
*

*>> halting problem, we want to reflect the actual truth about halting; in
*

*>> the (equivalent) domain of undecidable numerical statements, we still
*

*>> want the actual truth.
*

*>
*

*> Well some of them, like you, equivalent or bigger machine, will never
*

*> know, unless you are infinitely patient.
*

*> Insolubility here is hard, but it makes the mathematical world
*

*> necessarily ever surprising.
*

*> You can hope for a theory of everything, which preserves the mystery,
*

*> which makes it even more mysterious.
*

*>
*

*>
*

*>>
*

*>>
*

*>> Also, I should mention that the arithmetical hierarchy shows that some
*

*>> problems are "more undecidable" than halting: if we had a halting
*

*>> oracle, we would still be unable to decide those problems.
*

*>> Schmidhuber's super-omegas are a perfect example.
*

*>
*

*>
*

*> That is why the computationalist hypothesis is non trivial. It gives a
*

*> prominent role to Sigma_1 completeness. The oracle can still play an
*

*> important role "from inside", but even this is not sure. (and then
*

*> comp gives importance to sigma_1 completeness relatively to an oracle).
*

*>
*

*>
*

*>
*

*>>
*

*>>
*

*>> http://www.idsia.ch/~juergen/kolmogorov.html
*

*>>
*

*>> But you probably knew that already.
*

*>>
*

*>>>
*

*>>> For such machine the self-stopping problem become "absolutely-yet-
*

*>>> relatively-to-them" undecidable.
*

*>>> Actually I am very happy with this, because , assuming comp, this
*

*>>> could explain why humans fight on this question since so long. And we
*

*>>> can bet it is not finished!
*

*>>
*

*>> This argument is given in longer form elsewhere? Perhaps that paper
*

*>> you mention later on?
*

*>
*

*>
*

*> I have not publish this. I explain it informally in my french thesis
*

*> long version. But it is obvious I think, especially assuming comp. It
*

*> is implicit in my Plotinus paper (still on my first page of my url I
*

*> think).
*

*> Finite machine are limited. But finite machine which believes in the
*

*> induction axioms can know that they are limited, and can build
*

*> theories explaining those limitation. Formally this gives autonomous
*

*> progression. The correct one have to converge to some "non convergence
*

*> possible" in the horizon ...
*

*>
*

*>
*

*>>
*

*>>
*

*>>>
*

*>>> Tarski 's theorem is even more "religious", in the computationalist
*

*>>> setting. It means that the concept of truth (about a machine) acts
*

*>>> already like a "god" for that machine. No (sound) machine can givee a
*

*>>> name to its own proof predicate.
*

*>>
*

*>> To extend the model of the self-modifying theorem prover... the
*

*>> scenario I use when thinking about truth is a population of entities
*

*>> which, among other things, need to reason properly about each other.
*

*>> (I could perhaps reduce this to one entity that, among other things,
*

*>> needs to reason about itself; but that is needlessly recursive.) The
*

*>> logic that these entities use evolves over time.
*

*>
*

*> Relatively to some universal machine. I see subtle difficulties I
*

*> don't want to bore you with.
*

*>
*

*>
*

*>> In any given
*

*>> generation, the entity who can represent the truth-predicate of the
*

*>> most other entities will dominate.
*

*>
*

*> Why?
*

*>
*

*>
*

*>
*

*>
*

*>> The question, then, is: what logic
*

*>> will the population eventually converge to?
*

*>
*

*>
*

*> If the entities believes in classical logic, and if they believe in
*

*> induction, they will converge toward the self-reference logic of
*

*> Solovay (G and G*, or GL and GLS nowadays).
*

*>
*

*>
*

*>>
*

*>>
*

*>> I think fair arguments could be given for the fixed-point or revision
*

*>> theories in this scenario, but like I said, both create reference
*

*>> gaps... so some creature could dominate over these by inventing a
*

*>> predicate to fill the gap. That creature will then have its own
*

*>> reference gaps, and yet more gap-filling predicates will be created.
*

*>
*

*> I think so.
*

*>
*

*>
*

*>
*

*>>
*

*>>
*

*>> My current thinking is that each gap-filling predicate will correspond
*

*>> to an ordinal number, so that the maximal logic will be one with a
*

*>> gap-filling predicate for each ordinal number. No gap will be left,
*

*>> because if there was such a gap, it would correspond to an ordinal
*

*>> number larger than all ordinal numbers, which is impossible. 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.
*

*> Still, you can do this constructively, and provably so, only up to a
*

*> constructive ordinal. In that case, your entire population will
*

*> develop a "last" large reference gap. Or ... your population will
*

*> "live" forever with "little gaps", and will converge toward the first
*

*> non constructive ordinal, but nobody, well no machines, will ever know
*

*> that.
*

*>
*

*> Yet, from their first person point of view, it is different. From
*

*> their first person point of view they fill all gaps immediately.
*

*> Perfectly sound machines will identify truth and proof, consistently
*

*> so, and fill the gap. Only seen from outside, for not too much complex
*

*> machine, *we* can see they are "wrong" ... from outside, and correct
*

*> from inside.
*

*> This entails that "conscious machine" will have hard time to believe
*

*> that they are machine.
*

*> It is a bit like Skolem paradox. it depends how we will interpret the
*

*> ordinal. this can lead to very difficult questions, and the
*

*> hierarchies you mentionned can be useful. To be sure this could be too
*

*> technical for the list, where we discuss very basic fundamental
*

*> question, and no so many people knows the technic in logic.
*

*>
*

*> Actually, we are discussing an argument that IF we are machine
*

*> (whatever we are, except the physical universe), then the physical
*

*> universe is not entirely computable. The physical universe cannot be
*

*> the output of a program, nor really directly generated by a program.
*

*> It has to emerge statistically from all possible computation going
*

*> through possible observers. It is generated, but only implicitly, by
*

*> the running of a universal dovetailer. A program whose existence
*

*> relies on Church thesis, which generates and executes all programs by
*

*> zigazaguing on all their executions. It has to zigzag because we are
*

*> not able, and never will be, to predict in advance which programs
*

*> stops or doesn't stop.
*

*>
*

*> My general feeling is that incompleteness is the guaranty of
*

*> seriousness of the mechanist hypothesis in the cognitive science, and
*

*> even in the physical science. The lesson of Gödel's first
*

*> incompleteness theorem is a lesson in modesty (provably so assuming
*

*> comp). The lesson of Gödel's second incompleteness theorem is a lesson
*

*> of wonder: all self-introspecting universal machine can learn the
*

*> modesty lesson!
*

*> Incompleteness is also what makes Church thesis consistent (see the
*

*> first footnote of the Plotinus paper). This has no price, because it
*

*> makes computability the first absolute mathematical epistemological
*

*> notion. We don't have this for the notion of provability, nor of
*

*> knowledge, still less of provability. But we have modal logic which
*

*> are invariant for their interpretation thanks to Gödel, Löb and
*

*> Solovay. Do you know the provability logics?
*

*>
*

*> Bruno Marchal
*

*>
*

*>
*

*> 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.domain.name.hidden

To unsubscribe from this group, send email to everything-list+unsubscribe.domain.name.hidden

For more options, visit this group at http://groups.google.com/group/everything-list?hl=en

-~----------~----~----~----~------~----~------~--~---

Received on Tue Nov 25 2008 - 18:01:47 PST

Date: Tue, 25 Nov 2008 18:01:29 -0500

Bruno,

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

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. Eventually it will become useful to

abstract away from the details with a "true" predicate. 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. 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).

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". 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; 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.

--Abram

On Mon, Nov 24, 2008 at 5:03 PM, Bruno Marchal <marchal.domain.name.hidden> wrote:

--~--~---------~--~----~------------~-------~--~----~

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.domain.name.hidden

To unsubscribe from this group, send email to everything-list+unsubscribe.domain.name.hidden

For more options, visit this group at http://groups.google.com/group/everything-list?hl=en

-~----------~----~----~----~------~----~------~--~---

Received on Tue Nov 25 2008 - 18:01:47 PST

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