On 04 Feb 2010, at 15:28, Jason Resch wrote:
On Wed, Feb 3, 2010 at 1:47 PM, Bruno Marchal <[email protected]>
wrote:
On 03 Feb 2010, at 15:49, Jason Resch wrote:
On Wed, Feb 3, 2010 at 3:14 AM, Bruno Marchal <[email protected]>
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?
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 true
statements, 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 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?
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 a
good 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 [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/everything-list?hl=en.
