> On 22 Apr 2018, at 18:04, Lawrence Crowell <goldenfieldquaterni...@gmail.com> > wrote: > > 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.
It is a way of saying that if □S → S is *provable*, then S is provable. > This is a fancy way of just saying that if a statement S is provable then S > holds. ? The Löb formula says the contrary. It says for example with S = f (false), that if the machine is consistent (~provable(f), i.e []f -> f), then f is provable. So if the machine is could prove []f -> f it would prove f and be inconsistent. > > 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. It is an axiom of the soul (SAGrz) and of the Noùs (G*), but the machine cannot prove it. That is why we can apply the idea of Theaetetus. As typically []p -> p is not provable, it makes sense to define knowledge by “[]p & p”, like in Plato. That gives a modal logic of knowledge, but by Tarski (and variants), that cannot be defined by the machine, which is nice, as it confirms Brouwer theory of the mental. > In the Löb theorem we appear to have instances where maybe this might not > hold. Not maybe. Certainly. Typical cases []f -> f is not provable. []<>[]f -> <>[]f is not provable, etc. > 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) > (that line will be false when we do the sigma_1 restriction!) > ◊¬S → ◊(¬S → ◊¬S) OK. That is almost the dual presentation of Löb’s formula, but it will not work on the sigma_1 (semi-computable) restriction. Here, out of that restriction, you could use ~S instead of S, so that you have ◊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. This means that incompleteness entails the platonic nuances []p & p, []p & <>p, … That plays a key role in the derivation of physics from arithmetic (as imposed by Digital Mechanism). Bruno > > 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 > <mailto:everything-list+unsubscr...@googlegroups.com>. > To post to this group, send email to everything-list@googlegroups.com > <mailto:everything-list@googlegroups.com>. > Visit this group at https://groups.google.com/group/everything-list > <https://groups.google.com/group/everything-list>. > For more options, visit https://groups.google.com/d/optout > <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.
