The Evolution of Type Theory in Logic and Mathematics

ftp://ftp.win.tue.nl/pub/techreports/laan/proefschrift.ps.gz

ftp://ftp.win.tue.nl/pub/techreports/laan/errata.ps.gz

Twan Dismas Laurens Laan

Eindhoven University of Technology, 1997

happy holidays!

(above is why I am asking about Skolem connection?)

I read the article by Philip Wadler "Proofs are Programs"

with interest. I am creating a webpage about Skolem,

Diophantine equations, lambda calculus, Godel, Turing

which deals with the primitive origins of programming

languages, incompleteness and randomness.

Because of your interest in the topic I would like to ask

you a few questions. I gathered the following information

from the Nordic Journal of Philosophical Logic and in

particular the article by Herman Jervell which in part:

Diophantine equations and logic

I believe that Skolem considered Diophantine equations and

logic as one subject. Let me indicate a little speculatively

how Skolem's thought might have been. The theory of

Diophantine equations considers questions about

satisfiability of equations like

4x^3y^4 +3y^3 -13z^5 = 0

This is really not far from questions about satisfiability of

logical statements. A statement can be seen as a

``Diophantine equation'' where we have

true 1

false 0

not F 1-F

F and G min(F,G)

F or G max(F,G)

In addition, we have to indicate how the quantifiers are to be

interpreted. This is of course more complicated. So Skolem's

first work was to see how the quantifiers could be interpreted.

________________________________________________

Skolem in fact gives two systems: One for defining objects,

objects defined by primitive recursion, and one for proving

properties of such objects. This would be quantifier-free

statements with free variables, and with the possibility of

proving theorems using (quantifier-free) induction. These

two systems were developed in parallel. Skolem was able to

develop a substantial part of number theory. For example,

prime numbers were introduced.

Here Skolem comes very close to problems in contemporary

computer science. Let us for the moment skip over the fact

that Skolem considers only natural numbers. His two systems

could be considered as a programming language--for defining

objects--and a programming logic--for proving properties

about the objects. This is in fact of great interest for

contemporary computer science. Especially so if data

structures other than natural numbers are admitted.

Skolem's idea works equally well for data structures with

more than one base element and more than one generator.

--And so we are in business, with an interesting programming

language and its corresponding programming logic. I believe

that Skolem would have considered this as the same idea as

in 1923a. (Below is a reference starting with subtopic#3)

^^^^^^^^^

http://www.hf.uio.no/filosofi/njpl/vol1no2/pioneer/index.html

_______________________________________________

1. Are you familar with the content of "1923a" mentioned above?

Next in reference to my website:

I want to be able to say something which is correct, probably known

by experts, but which is accessible to the general reader and might

surprise the semi-expert comp.ai.philosophy denizen.

Which is that Diophantine representations can be utilized as a

simple programming language with equal computation capacity to

the other acknowledged equivalent computational approaches.

(even if it would be more difficult){end of quote}

I received a clarification/approval in email correspondence:

"In fact every RE set, A, can be defined as:

A = { n | for some i, a(n, i) = 0}

where a(n, i) = 0 is a Diophantine equation.

The reverse statement is also true.

We can turn Diophantine equations into a

computational language if for each

Diophantine equation, a, we add a

search operator, mu, such that

mu(a, n) = the smallest i such that a(n, i) = 0

Of course mu may not always find an i, which is

what prevents Diophantine equations from being

totally recursive. {end of his reply quote}

Quote:

SH writes:

So I think this is a confirmation and he is commenting

that this may not terminate unlike primitive recursion.

I am not sure what "we add a search operator, mu,

such that mu(a, n) = the smallest i such that a(n, i) = 0"

(^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^)

means exactly. I came across this from mu-calculus

Set

is a group of articles that results from a search command.

Operators can act on sets or words.

We obtain finitary complete axiom system for the $\mu$-caculus.

It can be roughly described as a system for propositional modal

logic with the addition of a induction rule to reason about least

fixpoints.

2. Could you clarify this? Does least fixpoints = "the smallest i"

3. This would mean that a Diophantine representation could

be used to implement a program which would prove theorems?

4. How would you philosophically characterize the evolution

of mathematical logic from an agenda to have a complete formal

basis for mathematics to ever stronger results of incompleteness

which now appear as randomness in Chaitin's omega variable.

Any thoughts about the connection between randomness and Inc.?

5. Would you consider Diophantine equations a meta-language?

Resolution and Discovery,

Stephen

Sent via Deja.com http://www.deja.com/

Before you buy.