Ultrafinitism doesn’t seem relevant here. The “type theory” you’re thinking of seems to be just the arithmetical hierarchy. A “concrete prediction” is a statement with only bounded quantifiers, “this Turing machine eventually halts” is a statement with one existential quantifier, “this Turing machine halts for every input” is a statement with one universal and one existential quantifier, and so on. Or am I missing something?
The arithmetical hierarchy is presuming a background of predicate logic; I was not presuming that. Yes, the type theory that I was gesturing towards would have some similarity to the arithmetical hierarchy.
I was trying to suggest that the answer to “what is a prediction” might look like a type theory of different variants of a prediction. Perhaps a linear hierarchy like the arithmetical hierarchy, yes, perhaps something more complicated. There could be a single starting type “concrete prediction” and a type constructor that, given source type and a destination type, gives the type of statements defining functions that take arguments of the source type and give arguments of the destination type.
The intuitive bridge for me from ultrafinitism to the question “what counts as a prediction?” is that ultrafinitists do happily work with entities like 2^1000 considered as a structure like (“^” “2” “1000″), even if they deny that those structures refer to things that are definitely numbers (of course, they can agree that they are definitely “numbers”, given an appropriately finitist definition of “number”). Maybe extreme teetotalers regarding what counts as a prediction would happily work with things such as computable functions returning predictions, even if they don’t consider them predictions.
Ultrafinitism doesn’t seem relevant here. The “type theory” you’re thinking of seems to be just the arithmetical hierarchy. A “concrete prediction” is a statement with only bounded quantifiers, “this Turing machine eventually halts” is a statement with one existential quantifier, “this Turing machine halts for every input” is a statement with one universal and one existential quantifier, and so on. Or am I missing something?
The arithmetical hierarchy is presuming a background of predicate logic; I was not presuming that. Yes, the type theory that I was gesturing towards would have some similarity to the arithmetical hierarchy.
I was trying to suggest that the answer to “what is a prediction” might look like a type theory of different variants of a prediction. Perhaps a linear hierarchy like the arithmetical hierarchy, yes, perhaps something more complicated. There could be a single starting type “concrete prediction” and a type constructor that, given source type and a destination type, gives the type of statements defining functions that take arguments of the source type and give arguments of the destination type.
The intuitive bridge for me from ultrafinitism to the question “what counts as a prediction?” is that ultrafinitists do happily work with entities like 2^1000 considered as a structure like (“^” “2” “1000″), even if they deny that those structures refer to things that are definitely numbers (of course, they can agree that they are definitely “numbers”, given an appropriately finitist definition of “number”). Maybe extreme teetotalers regarding what counts as a prediction would happily work with things such as computable functions returning predictions, even if they don’t consider them predictions.