Constructive Recursive Mathematics
Jan. 13th, 2009 11:40 am![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
guslIt is my opinion that the Russian school of intuitionism, founded by A. A. Markov Jr, deserves more attention than it gets... especially among those who subscribe to "computational thinking".
The philosophical motivation for CRM is that an operation is considered "constructive" if and only if it is recursive.
I like this because it suggests new way of formalizing mathematical statements, not in terms of unconstructive foundations like set theory, but in terms of computer programs: every mathematical statement φ gets translated into a statement about a single computer program T(φ) of the form "this assert never fails for any input".
One might point out that for any given axiom set, the set of theorems is RE (since we can build a theorem pump), and conclude that by this definition, all mathematics is constructive... but this is not sound given the above definition.
A theorem statement is constructive only if all the functions it calls and all sets it quantifies over are recursive (or, in terms of functional programming languages: a function is implemented iff all the functions it calls are implemented).
Much of higher math, as it's practiced, involves doing computable things on uncomputable oracles, and vice-versa, in a soup of definitions; and much of the goal of the constructive movements (as I understand it) was to "clean out" that stuff. Perhaps their concern was epistemic hygiene. My concern is meaningfulness and effectiveness: what good is a piece of mathematics if it doesn't say anything about any imaginable situation?
Now I should discuss the status of traditional axiomatic theories (i.e. theories that state the existence of unconstructible objects, and give them names). Of course, we can imagine a universe in which mathematicians talk "meaningfully" about non-constructible objects such as higher infinities (we are in one!). It's tempting for me to say that truth of such statements is defined by their provability... but truth is normally defined in terms of models, and the model-checking procedure, while always recursive (AFAIK), may involve calling uncomputable oracles.
My current intuition is this: uncomputability creates a gap between mathematical statements, and provability (via non-constructive operations) closes this gap.
My view is that uncomputable oracles, such as usages of the full axiom of choice, are useful only to the extent that their results transfer faithfully to the computable universe. (Results in computable analysis reassure me that I don't need to spend my time computationalizing every analysis theorem that I come across)
Unfortunately, many early sources from the Markov school are only available in Russian. Since any copyright should be expired by now, I would encourage anyone who can to translate them and make them freely available. I'm happy to host.
Here are some key references, courtesy of A.S. Troelstra:
The philosophical motivation for CRM is that an operation is considered "constructive" if and only if it is recursive.
I like this because it suggests new way of formalizing mathematical statements, not in terms of unconstructive foundations like set theory, but in terms of computer programs: every mathematical statement φ gets translated into a statement about a single computer program T(φ) of the form "this assert never fails for any input".
One might point out that for any given axiom set, the set of theorems is RE (since we can build a theorem pump), and conclude that by this definition, all mathematics is constructive... but this is not sound given the above definition.
A theorem statement is constructive only if all the functions it calls and all sets it quantifies over are recursive (or, in terms of functional programming languages: a function is implemented iff all the functions it calls are implemented).
Much of higher math, as it's practiced, involves doing computable things on uncomputable oracles, and vice-versa, in a soup of definitions; and much of the goal of the constructive movements (as I understand it) was to "clean out" that stuff. Perhaps their concern was epistemic hygiene. My concern is meaningfulness and effectiveness: what good is a piece of mathematics if it doesn't say anything about any imaginable situation?
Now I should discuss the status of traditional axiomatic theories (i.e. theories that state the existence of unconstructible objects, and give them names). Of course, we can imagine a universe in which mathematicians talk "meaningfully" about non-constructible objects such as higher infinities (we are in one!). It's tempting for me to say that truth of such statements is defined by their provability... but truth is normally defined in terms of models, and the model-checking procedure, while always recursive (AFAIK), may involve calling uncomputable oracles.
My current intuition is this: uncomputability creates a gap between mathematical statements, and provability (via non-constructive operations) closes this gap.
My view is that uncomputable oracles, such as usages of the full axiom of choice, are useful only to the extent that their results transfer faithfully to the computable universe. (Results in computable analysis reassure me that I don't need to spend my time computationalizing every analysis theorem that I come across)
Unfortunately, many early sources from the Markov school are only available in Russian. Since any copyright should be expired by now, I would encourage anyone who can to translate them and make them freely available. I'm happy to host.
Here are some key references, courtesy of A.S. Troelstra:
"A constructive logic" (Russian), Usp. Math. Nauk 5(3) 1950, 187-188 (reviewed JSL 18,p.257)
"On the continuity of constructive functions" (Russian) Usp Math Nauk 9(3), 226-230 (1954), (review JSL 21, p.319).
See for bibliographical information Vol VI of the Omega-Bibliography of Mathematical Logic, edited by Gert H. Müller+ Springer Verlag, Heidelberg 1987.
A good introduction to the ideas and results of the Markov school is the book B.A. Kushner, Lectures on Mathematical Analysis, American Math. Soc.1984