> On 3 Mar 2020, at 14:12, Alan Grayson <[email protected]> wrote:
>
>
>
> On Tuesday, March 3, 2020 at 5:23:48 AM UTC-7, Bruno Marchal wrote:
>
> On 2 Mar 2020, at 14:19, Alan Grayson <[email protected] <javascript:>>
> wrote:
>
>
> Here is where I think you've tried to answer my gravity problem posed on
> another thread. You say there is an infinity of calculations, but what is
> doing the calculations? And why among those multitudes is one set chosen,
> namely our "illusion"? AG
>
>
> OK. I have begun the explanation. But here you are again already at the step
> 7 (if you take a look at my paper sane04 general public presentation(*))
>
> What is doing the computations? When you implement the computation in the
> physical reality, the computations are done by the relevant digital
> information encoded into physical relations, between physical objects.
> What is doing the computation, when there is no physical universe, is any
> relation in a model of a Turing complete theory. Elementary arithmetic is
> Turing complete, so if you are OK with 2+2=4, or with statement like “there
> is no bigger prime number”, the computation are implemented naturally by the
> representation of those computation in term of true natural number relation.
> It is a bit like a bloc-universe. Time will be accounted by the notion of
> “number of steps of a computation”.
>
> Example. The reality of, say, the computer science statement that" the
> register (a, b, c) contains a", is realised by the physical fact that
> something encoding “a" is put “physically” in a series of physical memories
> (flip-flop, or magnetic disk, etc.).
>
> That same reality is implemented, all by itself, in the arithmetical
> statement that the number
>
> 2^(“a”) * 3^(“b”) * 5^(“c”)
>
> admits only one decomposition into product of power of primes (by the so
> called fundamental theorem of arithmetic, by Euclid), and saying that “a”
> (the representation of ‘a' by some number, which I note “a”) belongs to its
> first place is arithmetically equivalent of saying that 2^”a” divides
> 2^(“a”) * 3^(“b”) * 5^(“c”) , and that 2^”a” + 1 does not divide it.
>
> Of course, that “arithmetise” only a few bit of the computation. Gödel missed
> the Church-Turing thesis, and so was unaware of arithmetising “computer
> science”, but he will got the point later. Meanwhile, he was the first one to
> arithmetise the provability predicate, and later, he will understand that his
> provability predicate is Turing equivalent (with respect to computability,;
> not with respect to provability).
>
> The best might be to download Gödel 1931, for example here:
>
> https://www.jamesrmeyer.com/pdfs/godel-original-english.pdf
> <https://www.jamesrmeyer.com/pdfs/godel-original-english.pdf>
>
> The complete arithmetization is done in 40 steps. See below(**). The step 44
> gives Gödel famous beweisbar predicate Bw(x), which is the one I wrote []x,
> and which is the subject of what I called “theology of machine”, mainly the
> mathematical theory of provability , proved complete by Solovay in 1976 (at
> the modal propositional level). The step 1 is the arithmetical definition of
> “x divides y”, OK?
>
> It has to be long and tedious, as defining provability (and thus
> computability) in arithmetic is like programming a high level language in a
> low level language.
>
> To really swallow this, it will also be necessary to understand well the
> difference between proof and truth. The computations are implemented in the
> truth of arithmetic (in the “model”, or in all models, in the logician sense
> of model (whicht will be brought by Lowenheim and Tarski, Gödel did without
> this, but refer to the intuition, which is simpler, but for our concern, we
> have to take this into account at some point)).
>
> Bruno
>
>
>
> (*) B. Marchal. The Origin of Physical Laws and Sensations. In 4th
> International System Administration and Network Engineering Conference, SANE
> 2004, Amsterdam, 2004.
> http://iridia.ulb.ac.be/~marchal/publications/SANE2004MARCHALAbstract.html
> <http://iridia.ulb.ac.be/~marchal/publications/SANE2004MARCHALAbstract.html>
>
> (**) Here are the 40 steps, for future reference. Tell me if you can read and
> understand the line 1.
>
> Yes. AG
Good. So, to be clear, we define an arithmetical formula by the formula using
only the symbols “+”, “*”, “s” (intended for the successor operation) + the
logical symbols.
>
> You might print it, and we can do them step by step too. It *looks*
> difficult, but it is not that much difficult, if you develop a bit of
> familiarisation with the notation (which are not quite standard):
>
> 1. x/y≡(∃z)[z≤x&x=y·z] x is divisible by y.
Note that (∃z)[x=y·z] is an admissible definition of “x divide y”, i.e. x/y,
but Gödel want to "bound the “∃” quantifier, to ensure that such relation
(divide) to be computable, and provable when true. Strictly speaking, this is
not even necessary for our purpose, but is nevertheless helpful, for the
explanation that the computation are executed in arithmetic.
> 2. Prim(x)≡~(∃z)[z≤x&z≠1&z≠x&x/z]&x> x is a prime number.
Are you OK with this?
> 3. 0Prx≡0
> (n+1) Pr x ≡ εy [y ≤ x & Prim(y) & x/y & y > n Pr x]
> n Pr x is the nt h (in order of magnitude) prime number contained in x.
And this? “εy” (epsilon x) means “the least y such that …
(today the use of the letter µ (mu is more standard))
Here, a difficulty is hidden, which is that we have a recursive definition,
which is not something purely written in first order logic. We can come back on
this later, but it is useful for me if you can tell me if it works for you.
> 4. 0!≡1
> (n+1)! ≡ (n+1).n!
Same problem and question here. Do you see that this defines well the factorial
function? I will explain later how to translate a “recursive definition” in
pure first order logic later.
OK? (ask any question, and of course, remind that all this is done to answer
your question: how the arithmetical reality/model satisfy the existence of
computation, and can be said to execute them, in, of course, a sort of
bloc-universe way). It helps if you are OK with a static bloc-universe view,
often used as well in General Relativity. Arithmetic will appear as a
bloc-mindscape, where all “dreams” are realised, but with different relative
frequencies.
Bruno
> 5. Pr(0) ≡ 0
> Pr(n+1) ≡ εy [y ≤ {Pr(n)}! + 1 & Prim(y) & y > Pr(n)]
> Pr(n) is the nt h prime number (in order of magnitude).
> 6. nGlx≡εy[y≤x&x/(nPrx)y &~x/(nPrx)y+1]
> n Gl x is the nt h term of the series of numbers assigned to the number x
> (for n > 0 and n not greater than the length of this series).
> 7. l(x)≡εy[y≤x&yPrx>0&(y+1)Prx=0]
> l(x) is the length of the series of numbers assigned to x.
> 8. x*y≡εz[z≤[Pr{l(x)+l(y)}]x+y &(n)[n≤l(x)⇒nGlz=nGlx] & (n)[0 < n ≤ l(y) ⇒
> {n+l(x)} Gl z = n Gl y]]
> x * y corresponds to the operation of "joining together" two finite series of
> numbers.
> 9. R(x) ≡ 2x
> R(x) corresponds to the number-series consisting only of the number x
> (for x > 0).
> 10. E(x)≡R(11)*x*R(13)
> E(x) corresponds to the operation of "bracketing" [ 11 and 13 are assigned to
> the basic signs "(" and ")"].
> 11. nVarx≡(∃z)[13<z≤x&Prim(z)&x=z n]&n≠0 x is a variable of nt h type.
> 12. Var(x)≡(∃n)[n≤x&nVarx] x is a variable.
> 13. Neg(x) ≡ R(5) * E(x)
> Neg(x) is the negation of x.
>
> 14. xDisy≡E(x)*R(7)*E(y)
> x Dis y is the disjunction of x and y.
> 15. xGeny≡R(x)*R(9)*E(y)
> x Gen y is the of y by means of the variable x
> (assuming x is a ).
> 16. 0Nx≡x
> (n+1) N x ≡ R(3) * n N x
> n N x corresponds to the operation: " n-fold prefixing of the sign ‘ f’
> before x."
> 17. Z(n) ≡ n N [R(1)]
> Z(n) is the number-sign for the number n.
> 18. Typ1′(x)≡(∃m,n){m,n≤x&[m=1∨1Varm] &x=nN[R(m)]} 34b
> x is a sign of first type.
> 19. Typn(x)≡[n=1&Typ1′(x)]∨[n>1
> & (∃v){v ≤ x & n Var v & x = R(v)}] x is a sign of nth type.
> 20. Elf(x) ≡ (∃y,z,n)[y,z,n ≤ x & Typn(y) & Typn+1(z) & x = z * E(y)] x is an
> elementary formula.
> 21. Op(x,y,z)≡x=Neg(y)∨x=yDisz ∨ (∃v)[v ≤ x & Var(v) & x = v Gen y]
> generalization
> variable
>
> 22. FR(x)≡(n){0<n≤l(x)⇒Elf(nGlx) ∨(∃p,q)[0<p,q<n&Op(nGlx,pGlx,qGlx)]} &l(x)>0
> x is a series of formulae of which each is either an
> or arises from those preceding by the operations of , disjunction and
> generalization.
> 23. Form(x) ≡ (∃n){n ≤ (Pr[l(x)2])x · [l(x)]2 & FR(n) & x = [l(n)] Gl n} 35 x
> is a formula (i.e. last term of a series of formulae n).
> 24. v Geb n,x ≡ Var(v) & Form(x)
> & (∃a,b,c)[a,b,c ≤ x & x = a * (v Gen b) * c & Form(b) & l(a)+1 ≤ n ≤
> l(a)+l(v Gen b)]
> The variable v is bound at the nt h place in x.
> 25. vFrn,x≡Var(v)&Form(x) &v=nGlx&n≤l(x)&~(vGebn,x)
> The variable v is free at the nt h place in x.
> 26. vFrx≡(∃n)[n≤l(x)&vFrn,x]
> v occurs in x as a free variable.
> 27. Sux( n⁄y )≡εz{z≤[Pr(l(x)+l(y))]x+y
> &[(∃u,v)u,v≤x&x=u*R(bGlx)*v &z=u*y*v&n=l(u)+1]} Su x( n ⁄y ) derives from x
> on substituting y in place of the nt h term of x
> (it being assumed that 0 < n ≤ l(x)).
> 28. 0Stv,x≡εn{n≤l(x)&vFrn,x &~(∃p)[n<p≤l(x)&vFrp,x]} (k+1) St v,x ≡ εn {n < k
> St v,x & v Fr n,x
> & (∃p)[n < p < k St v,x & v Fr p,x]}
> k St v,x is the (k+1) t h place in x (numbering from the end of formula x) at
> which v is free in x (and 0, if there is no such place.)
> elementary formula
> negation
>
> 29. A(v,x)≡εn{n≤l(x)&nStv=0}
> A(v,x) is the number of places at which v is free in x.
> 30. Sb0(x v⁄y )≡x
> Sbk+1(x ⁄y )≡Su{Sbk(x ⁄y )}( ⁄y )
> v v k St v, x 31. Sb(x v⁄y )≡SbA(v,x)(x v⁄y )36
> Sb(x v ⁄y ) is the concept Subst a( v ⁄b ), defined above.3 7
> 32. xImpy≡[Neg(x)]Disy
> x Con y ≡ Neg{[Neg(x)] Dis [Neg(y)]} x Aeq y ≡ (x Imp y) Con (y Imp x)
> v Ex y ≡ Neg{v Gen [Neg(y)]}
> 33. nThx≡εn{y≤x(xn) & (k)≤l(x)⇒(kGlx≤13&kGly=kGlx)∨ (kGlx>13&kGly=kGlx
> ·[1Pr(kGlx)]n)]}
> nThxisthenth type-liftofx(inthecasewhenxandnThxare formulae).
> To the axioms I, 1 to 3, there correspond three determinate numbers, which we
> denote by z1, z2, z3, and we define:
> 34. Z–Ax(x)≡(x=z1 ∨x=z2 ∨x=z3)
> 35. A1-Ax(x)≡(∃y)[y≤x&Form(y)&x=(yDisy)Impy]
> x is a formula derived by substitution in the axiom-schema II, 1. Similarly
> A2-Ax, A3-Ax, A4-Ax are defined in accordance with the axioms II, 2 to 4.
> 36. A-Ax(x) ≡ A1-Ax(x) ∨ A2-Ax(x) ∨ A3-Ax(x) ∨ A4-Ax(x)
> x is a formula derived by substitution in an axiom of the sentential calculus.
>
> 37. Q(z,y,v) ≡ ~(∃n,m,w)[n ≤ l(y) & m ≤ l(z)
> & w ≤ z & w = m Gl z & w Geb n,y & v Fr n,y]
> z contains no variable bound in y at a position where v is free.
> 38. L1-Ax(x) ≡ (∃v,y,z,n){v,y,z,n ≤ x & n Var v & Typ vn(z)
> &Form(y)&Q(z,y,v)&x=(vGeny)Imp[Sb(y ⁄z )]}
> x is a formula derived from the axiom-schema III, 1 by substitution.
> 39. L2-Ax(x) ≡ (∃v,q,p){v,q,p ≤ x & Var(v) & Form(p) & v Fr p & Form(q) & x =
> [v Gen (p Dis q)] Imp [p Dis (v Gen q)]}
> x is a formula derived from the axiom-schema III, 2 by substitution.
> ...
>
> --
> 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 [email protected]
> <mailto:[email protected]>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/everything-list/f36c292e-d92f-4e2c-a5fb-98a9a132c567%40googlegroups.com
>
> <https://groups.google.com/d/msgid/everything-list/f36c292e-d92f-4e2c-a5fb-98a9a132c567%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/everything-list/3E257E9B-7561-4BAF-80D4-A58FB6720EDF%40ulb.ac.be.
