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.
Scheme in Dr. Dobb's