posted on 2010-12-01, 00:00authored byMatthew P. Szudzik
We consider two applications of recursive functionals. The first application concerns
Gödel’s theory T , which provides a rudimentary foundation for the formalization
of mathematics. T can be understood as a theory of the simply-typed lambda
calculus that is extended to include the constant 0N, the successor function S, and
the operator RT for primitive recursion on objects of type T . It is known that the
functions from non-negative integers to non-negative integers that can be defined in
this theory are exactly the <ε0-recursive functions of non-negative integers. But it
is not well-known which functionals of arbitrary type can be defined in T . We show
that when the domain and codomain are restricted to pure closed normal forms, the
functionals of arbitrary type that are definable in T are exactly those functionals that
can be encoded as <ε0-recursive functions of non-negative integers. This result has
many interesting consequences, including a new characterization of T .
The second application is concerned with the question: “When can a model
of a physical system be regarded as computable?” We provide the definition of a
computable physical model to answer this question. The connection between our
definition and Kreisel’s notion of a mechanistic theory is discussed, and several examples
of computable physical models are given, including models which feature
discrete motion, a model which features non-discrete continuous motion, and nondeterministic
models such as radioactive decay. We show how computable physical
models on effective topological spaces can be formulated with recursive functionals
in the theory of type-two effectivity (TTE). Various common operations on
computable physical models are described, such as the operation of coarse-graining
and the formation of statistical ensembles. The definition of a computable physical
model also allows for a precise formalization of the computable universe hypothesis—
the claim that all the laws of physics are computable.
History
Date
2010-12-01
Degree Type
Dissertation
Department
Mathematical Sciences
Degree Name
Doctor of Philosophy (PhD)
Advisor(s)
Richard Statman,Jeremy Avigad,Robert Batterman,Lenore Blum