On 04 Feb 2010, at 15:28, Jason Resch wrote:

On Wed, Feb 3, 2010 at 1:47 PM, Bruno Marchal <marc...@ulb.ac.be>wrote:On 03 Feb 2010, at 15:49, Jason Resch wrote:On Wed, Feb 3, 2010 at 3:14 AM, Bruno Marchal <marc...@ulb.ac.be>wrote:On 03 Feb 2010, at 03:00, Jason Resch wrote:Is your point that with addition, multiplication, and an infinitenumber of successive symbols, any computable function can beconstructed?You can say so.You could also have said that with addition + multiplication axioms+ logic, any computable function can be proved to exist.So I suppose that is what I was wondering, given at minimum, those,how is the existence of a computable function proved to exist?Could you provide an example of how a simple function, like f(x) =x*2 exists, or is it a very tedious proof?I guess you ask: how is the existence of a computable functionproved to exist in a theory T. Usually logicians use the notion ofrepresentability. The one variable function f(x) is said to berepresentable in the theory T, if there is a formula F(x, y) suchthat when f(n) = m, the theory T proves F(n, m), and usually(although not needed) that T provesAx (F(n,x) -> x = m).Here you will represent the function f(x) = x*2 by the formula F(x,y) : y = x*2. Depending on your theory the proof of the true formulaF(n, m) will be tedious or not. For example F(2, 1) is s(s(0)) =s(0) * s(s(0), and you need a theory having at least logic +equality rules, and the axioms1) x * 0 = 0 2) x* s(y) = x * y + x 3) x + 0 = 0 4) x + s(y) = s(x + y)I let you prove that s(s(0)) = s(0) * s(s(0) from those axioms(using the usual axiom for egality).s(0) * s(s(0)) = s(0) *s(0) + s(0) By axiom 2 with x = s(0)and y = s(0)s(0) *s(0) + s(0) = s(s(0) + 0) By axiom 4 with x =s(0) *s(0) and y = 0s(s(0) + 0) = s(s(0)) By substitutionof identical (logic + equality rules)s(0) * s(s(0)) = s(s(0)) Transitivity ofequality (logic + equality rules)s(s(0)) = s(0) * s(s(0)) equality rule (x= y -> y = x)And this is F(2, 1), together with its proof. Not very tedious, butF(2010, 1005) would be much more tedious! Note that from this we canalso deduce the existential sentence ExF(x, 1), a typical sigma_1sentence.Or do the relations imposed by addition and multiplication somehowcreate functions/machines?You can say so but you need logic. Not just in the (meta)background, but made explicit in the axiom of the theory, or theprogram of the machine (theorem prover).Thanks,You are welcome. Such questions help to see where the difficultiesremain. Keep asking if anything is unclear.Thanks again, things are becoming a little more clear for me. Mybackground is in computer science, in case that applies and helpsin writing an explanation for my question above.The nice thing is that a function is partial recursive(programmable) if an only if it is representable in a Sigma_1complete theory.A sigma_1 complete theory is a theory capable of proving all thetrue sentences equivalent with ExP(x) with P decidable.In particular the theory above (with some more axioms like s(x) =s(y) -> x = y, ..) is Sigma_1 complete, and thus Turing universal.All computable functions can be represented in that theory, and allcomputations can be represented as a proof of a Sigma_1 sentencelike above.To show that such a weak theory is Sigma_1 complete is actually longand not so easy. But then, to prove that the game of life is turinguniversal is rather long also. For weak system, such proof asks forsome "machine language programming", and the meticulous verificationthat everything works well. Always tedious, and there are somesubtle points. It is well done in the book by Epstein and Carnielli,or Boolos, Burgess and Jeffrey.Here is another very short Turing universal theory (a purelyequational logic-free theory!) :((K x) y) = x (((S x) y) z) = ((x z)(y z)) (x = x) (x = y) ==> (y = x) (x = y) ; (y = z) ===> (x = z) (x = y) ===> ((x z) = (y z))(x = y) ===> ((z x) = (z y)) "===>" is informal deduction, and";" is the informal "and".You may look at my paper "Theoretical computer science and thenatural sciences" for more on this theory, and its probableimportance in deriving the shape of physics from numbers.http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B75DC-4GX6J45-1&_user=532047&_coverDate=12%2F31%2F2005&_rdoc=1&_fmt=&_orig=search&_sort=d&view=c&_acct=C000026678&_version=1&_urlVersion=0&_userid=532047&md5=e087a268f1a31acd7cd9ef629e6dc543Hmm... It is 32 $ ... You may look at my older posts on thecombinators (Smullyan's birds!). It is not important, I wanted justto show you another example.Bruno http://iridia.ulb.ac.be/~marchal/So then it seems the integers, addition, and multiplication (plussome logic) are the minimum axioms needed to represent and provetrue any computable function, and it is through thisrepresentability that the functions are said to exist. Is thiscorrect?

`The rule of addition and the rule of multiplication, with some amount`

`of logic provides a universal programming language. That's correct.`

`And at the same time this provides a tiny formal theory of arithmetic.`

`A generator of a tiny subset of Arithmetical Truth (the set of all`

`true arithmetical sentences, written in first order arithmetical`

`language).`

`Tiny, but already equivalent with a "block- description" of a`

`universal dovetailing.`

`You cannot prove true a computable function. You can only prove`

`proposition. A theory is just a set of formula closed for inference`

`rule. Effective theory have a recursively enumerable set of theorems.`

`Theories proves propositions. And those are true when the theory is`

`sound.`

Universal systems computes functions. But a priori don't prove anything.

`I hope your believe that any closed formula of arithmetic is either`

`true or false. A logician would add "in the standard model of`

`Arithmetic", but this can lead to confusion.`

`I can recall you exactly what is an arithmetical formula if you`

`desire, but be patient the next days are rather time occupied, so just`

`be patient.`

Could the connection be made between mathematically provable truestatements, and functions?

`Of course. mathematical logic studies mainly that. A formula F(x, y)`

`represent a function when it verifies the functionnal condition, i.e.`

`AxAyAz F(x,y) & F(x, z) ->. y = z.`

`Actually you can see functions as particular case of relations, like`

`above.`

`But you can see relations as a particular case of functions, by taking`

`the characteristic function of the set of n-uples in the relation.`

`But you have to understand well the difference between a true`

`arithmetical proposition, and a provable arithmetical proposition, by`

`me or you or that formal system, or that other one. Provable is always`

`related to a theory.`

`And provable(p) -> p systematically for all proposition when the`

`theory is sound (and then no rich theory can prove this, no they can`

`prove or even directly express its own correctness, by a theorem of`

`Tarski).`

For example, the product of 4 consecutive integers is 1 less than asquare, is provably true because a function exists which embiodiesthe relationship, and it can be proven to be true? Whereas withoutthe existence of a function, would it be unprovable?

`I am not sure what you mean by provably true. It is provable in Peano`

`Arithmetic, I suspect. But the function or functions you can associate`

`with such a truth exists or not independently of the fact that such or`

`other theories proves it.`

`Of course, if you believe in the axioms of some theory, you may`

`believe in the existence of a function, because you can prove it in`

`that theory you trust, but again, the truth is independent of the`

`theory. Now the truth about numbers can be managed in richer (not`

`necessarily made formal) theories like naive set theory, as everyone`

`does in practice.`

It is not clear to me what Sigma1 sentences are, I could not find agood definition anywhere.

`It is subtle. It is part of recursion theory. I will define the notion`

`of sigma_1 proposition instead. (sigma_1 sentence are defined`

`syntactically by induction. The relation between sigma_1 proposition`

`and sigma_1 sentence is that it is the same in the eyes of God`

`(arithmetical truth), but this can usually not been seen by the`

`machines, which explains a part of the subtlety).`

`Basically a sigma_1 proposition is a proposition asserting the`

`existence of a number verifying some decidable property.`

`"There exists a number x such that x is prime" = there is a prime`

`number, is a sigma_1 proposition.`

`Thanks to the existence of the zero searching algorithm for the`

`critical zero of the Riemann zeta function, it is easy to understand`

`that the negation of the Riemann conjecture is a sigma_1 proposition.`

`The propositions "There exist a stopping state for the machine u`

`starting with y and z" give you a rich set of examples of sigma_1`

`proposition.`

`When such proposition are true, they are verifiable (provable- in the`

`tiny arithmetic described above, accessible by the universal`

`dovetailer based on a sigma_1 complete theory).`

`There is a theorem (well known by logicians) that in first order logic`

`all quantified formula can be put in prenex form which means that all`

`the quantifier precede the atomic formula. They can all have the shape:`

AxEyAzEt .... Au P(x, y, z, t, ... u)

`The sigma_1 are the one having the shape ExP(x) with P decidable`

`(sigma_0).`

`The pi_1 are the negation of the sigma_1 ~Ex P(x), equivalent with`

`Ax ~P(x), and given that P is decidable ~P(x) is too, and the pi_1 are`

`thus the formula having the shape AxP(x) with P decidable.`

`f is the code of a total computable function means that for all x`

`there is a y such phi_f(x) = y.`

`Now phi_f(x) = y is decidable, so total(f) <-> AxEyP(f, x, y), so to`

`be total is pi_2 or in pi_2.`

`The insolubility ladder follows the number of alternation of`

`quantifiers in the formulas, by a theorem of Kleene.`

`Sigma_1 complete = turing universal (roughly speaking). This is known`

`as the arithmetical hierarchy.`

`If you define sigma_1-truth by the set of true sigma_1 proposition,`

`and p_1-truth accordingly, as sigma_2-truth (cf ExAyP(x,y)), etc. then`

`you can define arithmetical truth as the union of sigma_1 -truth, pi_1-`

`truth, sigma_2 truth, etc.`

`All the sigma(pi)_truth notion can be defined in Peano Arithmetic, but`

`their union cannot. The set of all truth cannot be defined in`

`arithmetic, and thus cannot be axiomatized.`

`You could study some book in mathematical logic and computability`

`(recursion) theory. Like Mendelson and Rogers.`

`It helps for auda, and tiny part of those book can help for the`

`seventh and eight step of the ud argument.`

`For auda, the book by Boolos 79, 93 help a lot! But they presume a`

`good understanding of Mendelson and Rogers, or any good textbook in`

`mathematical logic.`

Bruno http://iridia.ulb.ac.be/~marchal/ -- You received this message because you are subscribed to the Google Groups "Everything List" group. To post to this group, send email to everything-l...@googlegroups.com. To unsubscribe from this group, send email to everything-list+unsubscr...@googlegroups.com. For more options, visit this group at http://groups.google.com/group/everything-list?hl=en.