On Thursday, April 26, 2018 at 3:09:03 AM UTC-5, Bruno Marchal wrote: > > > On 22 Apr 2018, at 18:04, Lawrence Crowell <goldenfield...@gmail.com > <javascript:>> 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. > > > > Yes, that is now S is interpreted. I do not have time to go into this discussion right now. I will try to get back in a day or so. LC > > > 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-li...@googlegroups.com <javascript:>. > To post to this group, send email to everyth...@googlegroups.com > <javascript:>. > 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.
