[Phil-logic] Dennis's foundational interests

[Dennis E. Hamilton]

Answering your questions in reverse order:

1. I am talking about foundations of computation (theory) only.  I am
restricting my particular foundation concern to that.  I do not consider it
in any way comparable to a question of foundations for mathematics.

2. Church's Thesis in its essentially-original form identifies the
effectively calculable functions of positive integers with the recursive
functions (or lambda-definable functions) of positive integers.  The reason
that I put more legs on the thesis is

 - 2.1 Turing-computability has been added since the original formulation
(thereby earning designation as the Church-Turing thesis) and 
 - 2.2 Church generalized his thesis to encompass a function F to be
effectively calculable if for every positive integer m, there exists a
positive integer n such that F(m) = n is a *provable* theorem.

3. FOL= comes into it via (2.2) and also anything involving proof with
regard to a correspondence with the recursive functions. 

4. Church also considered that one could define a function as effectively
calculable if there exists an algorithm for the calculation of its value.
That may be more than four legs, but four is enough for the stool to be
wobbly already [;<).  I am not wedded to the "supporting legs" analogy if
that is found too far off from the precise relationship of Church's thesis
to algorithms and formal representations (along with lambda-definability,
recursive functions, and Turing computability).

5. I am interested in the distinction between and the useful
inter-relationship of (2.2) about representability of functions in FOL= and
(4) having algorithms for their calculation. 

6. My particular computational model is one for expressing procedures via a
particular data structure and the application of such procedures to data
structures of the same kind.  [NB: I am not talking about expressing
functions.  I would not call the description of a Turing Machine a notation
for expressing functions either, although the behavior of the machine might
be shown to enact an algorithm for some function.]

7. A computational procedure might be algorithmic in nature (with regard to
the finiteness and termination conditions) yet we might have no idea what,
if any, distinguished function(s) that procedure enacts an algorithm for.
There are, however, proof techniques that are used to establish that a given
procedure is an algorithm for some identified function, F, but as a
practical matter, we usually need a (2.2) concerning F to start from.  This
last is also something I wish to motivate in my little research pastime.


Does that help some?

 - Dennis


-----Original Message-----
From: phil-logic-bounces at philo.at [mailto:phil-logic-bounces at philo.at] On
Behalf Of Roger Bishop Jones
Sent: Monday, December 20, 2010 12:56
To: phil-logic at philo.at
Subject: [Phil-logic] Dennis's foundational interests

Here are some questions whose answers might possibly
bring me closer to understanding what Dennis is trying
to do.

As I understand it Dennis has devised something like
a model of computation, by which I understand a notation
for defining functions which is equivalent in its expressive
powers to the turing machine, the lambda-calculus etc.
i.e. a notation for the general recursive functions.

He has a point here about four pronged support for Church's 
thesis among which he includes FOL=.
My first question here is, is FOL= being offered as a 
computational model, and if so in what way is it suggested 
that the general recursive functions are expressible in 
FOL=?

I observe that, supposing the four prongs all to be 
notations for the recursive functions, I would not myself 
say that they do support Church's thesis.
They are the subject matter of Church's thesis, which 
alleges that the informal notion of effective computability 
corresponds to these formal notions of computable function.
However, this is not an important point.

[ ... ]

If you have some other notion of foundation in mind, a 
foundation for something else perhaps, then it would be 
helpful to me to know what it is.

Roger Jones
















_______________________________________________
Phil-logic mailing list
Phil-logic at philo.at
http://philo.at/cgi-bin/mailman/listinfo/phil-logic