Article contents
Proofs, Snakes and Ladders
Published online by Cambridge University Press: 09 June 2010
Extract
Anyone who has worked at proving theorems of intuitionistic logic in a natural deduction system must have been struck by the way in which many logical theorems “prove themselves.” That is, proofs of many formulas can be read off from the syntactical structure of the formulas themselves. This observation suggests that perhaps a strong structural identity may underly this relation between formulas and their proofs. A formula can be considered as a tree structure composed of its subformulas (Frege 1879) and by the normal form theorem (Gentzen 1934) every formula has a normalized proof consisting of its subformulas. Might we not identify an intuitionistic theorem with (one of) its proof(s) in normal form?
- Type
- Articles
- Information
- Dialogue: Canadian Philosophical Review / Revue canadienne de philosophie , Volume 13 , Issue 4 , December 1974 , pp. 723 - 731
- Copyright
- Copyright © Canadian Philosophical Association 1974
References
- 1
- Cited by