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). 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 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. If “[]” represents the provability predicate (Gödel 1931)of some first order Turing universal theory/number, Löbian means that it can prove p -> []p for all p equivalent with a semi-computable predicate known as sigma_1 predicate). In fact “p -> []p” is equivalent with Turing universality, and if a Universal can prove this for all p sigma_1, it will not only be Turing universal, but it will know (in some technical sense) that it is Turing Universal. “[]” itself is sigma_1, which entails that []p -> [][]p is provable. Those corresponds to what is called “sufficiently rich theories” (for proving their own incompleteness theorem). Löbianity appears when you add to: 0 ≠ s(x) s(x) = s(y) -> x = y x = 0 v Ey(x = s(y)) x+0 = x x+s(y) = s(x+y) x*0=0 x*s(y)=(x*y)+x, The induction axioms: (F(0) & Ax(F(x) -> F(s(x))) -> AxF(x), with F(x) being a formula in the arithmetical language (with "0, s, +, *) F being a formula belonging to some set of formula. If you limit F to the recursive, sigma_0, formula, you don’t get Löbianity, unless you add the exponentiation axioms. You can (and I will) limit p to the sigma_1 sentences, the semi-computable predicate/function. That is enough to get Löbianity, and inherit, in the “ideal” sound case the “theology” of number/machine/combinator… beings. With p sigma_1 Universality means that p_>[]p is true, and Löbianity is when the machine/number proves p -> []p for all p (sigma_1). []p -> p, although true (by definition of sound machine/number) remains unprovable in general. Typically the Löbian machine cannot prove []f -> f. Peano is a Löbian theory/program/idea/machine/word<whatever Church-Turing Universal). ZF too, much more “crazy machine” which believes in the axiom of infinity, but then get doubt about the choice axioms! (As I stay in very elementary arithmetic (no induction axioms) I still studies the web of Löbian dreams realised in the non Löbian reality. Provability is relative, but computability is absolute. Sigma_1 completeness, that is the truth of p -> []p, for p sigma_1, is Turing universal. Löbianity is when the machine believes in enough induction axioms to prove p -> []p for each p sigma_1. It obeys to the modal logics of self-reference G and G*, which helps to summarise the “theology” of the finite universal number/machine/combinator/<whatever Church-Turing-Kleene-Post computable universal system >. Best, Bruno -- 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.
