Bruno:
is there a free version of Theoretical computer science and the
natural
sciences?
Ronald
On Feb 4, 2:45 pm, Bruno Marchal <marc...@ulb.ac.be> wrote:
> 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 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-4GX6J4...
>
> > 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, ...
>
> read more »- Hide quoted text -
>
> - Show quoted text -
--
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.
