With a T a theory that admits diagonalization and for Bew(x) a formula with a free x,.we have
├_T S ↔ Bew(gn(S)). The Löb theorem involves the diagonalization in T D(x,y) such that for any D(x,y) = k is the Gödel number diag(x) = k and y = k. This corresponds I think to the φ_u(x,y). It is some algebra to show this leads to the equation above. The Löb theorem if├_T Bew(gn(S)) → S then├_T S has parallels with the modal logical □(□S → S) → □S, which is a way of saying that if □S → S then S. This is a fancy way of just saying that if a statement S is provable then S holds. In part this corroborates with what you write. I would say the axiom of reflection, if I recall the name for it, □S → S is usually thought of as an axiom. In the Löb theorem we appear to have instances where maybe this might not hold. If we think of the complement, with ¬ = NOT, is ¬□S → ¬□(□S → S) equal to ¬□¬¬S → ¬□¬¬(□S → S) or for ¬□¬ = ◊, non necessarily not = possibly, we then have ◊¬S → ◊¬(□S → S) or ◊¬S → ◊(¬S → ¬□S) or ◊¬S → ◊(¬S → ◊¬S) with the conclusion that ¬S → (¬S → ◊¬S). The ◊ = possibly means we have an open door of sorts. We do not have the falsity of S implying logically some proof thereof. 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.