> On 20 Apr 2018, at 00:38, Russell Standish <li...@hpcoders.com.au> wrote:
>
> On Wed, Apr 18, 2018 at 07:11:33PM +0200, Bruno Marchal wrote:
>> Somewhere: (and I copy my answer, as some people asked me this in this list
>> too).
>>
>>
>>>
>>> What are Lobian numbers? Can you give a reference? I know little bit about
>>> Godel’s work.
>>
>>
>> Consider any Turing universal machinery, for example the programming
>> language c++.
>>
>> N is the set of natural numbers.
>>
>> It is known that the enumeration of all programs computing a (perhaps not
>> everywhere defined) function from N to N exists, and so we get a list of all
>> partial computable function phi_i from N to N. (i.e. phi_0, phi_1, phi_2,
>> …), by enumerating the program with one natural number argument) written in
>> C++, in their lexico-graphical order (length, and alphabetical for the
>> programs with the same length).
>>
>> We can define a universal number as a number u such that phI_u(x, y) =
>> phi_x(y). We say that u implements x on y. (It is a constructive definition
>> of a computer in the language of the computer).
>
> Some niggles: You haven't defined φᵢ(x,y). You need some sort of
> composition operator ∘ (perhaps x∘y is the concatenation of the bit
> representation of the number), and define φᵢ(x,y)=φᵢ(x∘y)
You need a computable bijection <x, y> between NXN and N, in case you want the
universal function to be contained in the enumeration of the one-variable
functions.
In that case we would write that u , the universal machine/number is such that
phi_u(<x, y>) = phi_x(y). (U emulates the number/machine x
on the input y).
This provides homogeneity, but it is not necessary, as we can consider the many
enumerations of one-variable, two-variables, … semi-computable functions, and
use a two variable functions (program, input) for the universal functions.
With the combinators, each combinators in the enumeration (K, S, (K, K), …) can
be seen as a function of zero variables!
And with Davis’ definition of Turing machines, all the enumerations (of
one-variable, two variables, …functions) are all identical. You decide if you
give one or two or three arguments to the machine.
The homogeneity is required for having a good notion of extensional recursive
equivalence, but I don’t use them, as I require only intensional equivalence
(based on programs behaviour).
>
>>
>> Now, once we have a universal number, we can transform/extend it into a
>> theory, which is the first order logical specification of how u operates.
>> That is a standard mapping from, say, c++ to a Turing universal logical
>> theory.
>>
>
> I assume that is possible. How would one go about this in practice?
By axiomatising in first order logic the terms of c++, and writing enough
axioms to get the Turing universality.
>
>> I assume we have done that, so now I say that a universal number is Löbian
>> when it has enough induction axioms (added to its logical specification) so
>> that it can prove enough of some special formula.
>>
>
> Isn't it true that the actual set of universal numbers rather depends
> on one chosen enumeration? So universality is not a property of the
> numbers per se?
Indeed. It is an intensional notion, but as I have explained sometimes that we
have an intensional Church-Turing thesis (which followed from the usual
extensional one).
But, once we fix the “base” (choosing between arithmetic, combinators, c++,
etc.), universality becomes an intrinsic property of numbers. That is why we
can stay entirely in Robinson Arithmetic (ontologically) to get the internal
complete phenomenology of the more rich Löbian number that RA emulates.
Bruno
>
> --
>
> ----------------------------------------------------------------------------
> Dr Russell Standish Phone 0425 253119 (mobile)
> Principal, High Performance Coders
> Visiting Senior Research Fellow hpco...@hpcoders.com.au
> Economics, Kingston University http://www.hpcoders.com.au
> ----------------------------------------------------------------------------
>
> --
> 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 https://groups.google.com/group/everything-list.
> For more options, visit https://groups.google.com/d/optout.
--
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 https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.
