I will try to get back to this with comments, but right now I am too tired out.
LC On Wednesday, April 18, 2018 at 12:11:35 PM UTC-5, 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). > > 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.
