Abstract
We develop a functional abstraction principle for the type-free algorithmic logic introduced in our earlier work. Our approach is based on the standard combinators but is supplemented by the novel use of evaluation trees. Then we show that the abstraction principle leads to a Curry fixed point, a statement C that asserts C ⇒ A where A is any given statement. When A is false, such a C yields a paradoxical situation. As discussed in our earlier work, this situation leaves one no choice but to restrict the use of a certain class of implicational rules including modus ponens.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Aitken, W. and Barrett, J. A.: Computer implication and the Curry paradox, Journal of Philosophical Logic 33(6) (2004), 631–637.
Aitken, W. and Barrett, J. A.: Stability and paradox in algorithmic logic, Journal of Philosophical Logic 36(1) (2007), 61–95.
Beeson, Michael J.: Foundations of Constructive Mathematics, Springer, Berlin Heidelberg New York, 1985.
Hindley, J. R. and Seldin, J. P.: Introduction to Combinators and λ-calculus, Cambridge University Press, Cambridge, UK, 1986.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Aitken, W., Barrett, J.A. Abstraction in Algorithmic Logic. J Philos Logic 37, 23–43 (2008). https://doi.org/10.1007/s10992-007-9051-5
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10992-007-9051-5