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 infinite number
>> of successive symbols, any computable function can be constructed?
>>
>>
>> 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 function proved to
> exist in a theory T. Usually logicians use the notion of representability.
> The one variable function f(x)  is said to be representable in the theory T,
> if there is a formula F(x, y) such that when f(n) = m,  the theory T proves
> F(n, m), and usually (although not needed) that T proves
> Ax (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 formula F(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 axioms
>
> 1) 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 = 0
> s(s(0) + 0)  = s(s(0))                             By substitution of
> identical (logic + equality rules)
> s(0) * s(s(0)) = s(s(0))                          Transitivity of
> equality (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, but F(2010,
> 1005) would be much more tedious! Note that from this we can also deduce the
> existential sentence ExF(x, 1), a typical sigma_1 sentence.
>
>
>
>
>>
>> Or do the relations imposed by addition and multiplication somehow create
>> 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 the program of the machine
>> (theorem prover).
>>
>>
>>
>>
>> Thanks,
>>
>>
>> You are welcome. Such questions help to see where the difficulties remain.
>> Keep asking if anything is unclear.
>>
>>
>>
> Thanks again, things are becoming a little more clear for me.  My
> background is in computer science, in case that applies and helps in 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_1 complete theory.
> A sigma_1 complete theory is a theory capable of proving all the true
> 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 all computations can be
> represented as a proof of a Sigma_1 sentence like above.
> To show that such a weak theory is Sigma_1 complete is actually long and
> not so easy. But then, to prove that the game of life is turing universal is
> rather long also. For weak system, such proof asks for some "machine
> language programming", and the meticulous verification that everything works
> well. Always tedious, and there are some subtle 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 purely equational
> 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 the natural
> sciences" for more on this theory, and its probable importance 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=e087a268f1a31acd7cd9ef629e6dc543
>
> Hmm... It is 32 $ ...  You may look at my older posts on the combinators
> (Smullyan's birds!). It is not important, I wanted just to show you another
> example.
>
> Bruno
>
> http://iridia.ulb.ac.be/~marchal/
>
>
>
So then it seems the integers, addition, and multiplication (plus some
logic) are the minimum axioms needed to represent and prove true any
computable function, and it is through this representability that the
functions are said to exist.  Is this correct?

Could the connection be made between mathematically provable true
statements, and functions?  For example, the product of 4 consecutive
integers is 1 less than a square, is provably true because a function exists
which embiodies the relationship, and it can be proven to be true?  Whereas
without the existence of a function, would it be unprovable?

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

Thanks again,

Jason

-- 
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.

Reply via email to