The Harmony of Identity
- 16 Downloads
The standard natural deduction rules for the identity predicate have seemed to some not to be harmonious. Stephen Read has suggested an alternative introduction rule that restores harmony but presupposes second-order logic. Here it will be shown that the standard rules are in fact harmonious. To this end, natural deduction will be enriched with a theory of definitional identity. This leads to a novel conception of canonical derivation, on the basis of which the identity elimination rule can be justified in a proof-theoretical manner.
KeywordsIdentity Natural deduction Definition
Unable to display preview. Download preview PDF.
The justification of =-elim given here is an adaptation to natural deduction of the justification of the corresponding rule in Martin-Löf’s type theory given in . Correspondence with Per Martin-Löf pertaining to the latter work suggested to me the conception of canonical derivation that lies at the basis of the current work. While writing the paper I have been financially supported by grant nr. 17-18344Y from the Czech Science Foundation, GAČR.
- 1.Curry, H.B. (1963). Foundations of mathematical logic. New York: McGraw-Hill.Google Scholar
- 2.Curry, H.B., & Feys, R. (1958). Combinatory logic Vol. 1. Amsterdam: North-Holland.Google Scholar
- 3.Fitch, F.B. (1952). Symbolic logic. New York: The Ronald Press.Google Scholar
- 6.Kleene, S.C. (1952). Introduction to metamathematics. New York: Van Norstrand.Google Scholar
- 7.Klev, A. (2017). The justification of identity elimination in Martin-Löf’s type theory. Topoi. Online First. https://doi.org/10.1007/s11245-017-9509-1.
- 8.Lemmon, E.J. (1965). Beginning logic. London: Nelson.Google Scholar
- 9.Martin-Löf, P. (1971). Hauptsatz for the intuitionistic theory of iterated inductive definitions. In Fenstad, J.E. (Ed.) Proceedings of the second Scandinavian logic symposium (pp. 179–216). Amsterdam: North-Holland.Google Scholar
- 10.Martin-Löf, P. (1975). About models for intuitionistic type theories and the notion of definitional equality. In Kanger, S. (Ed.) Proceedings of the third Scandinavian logic symposium (pp. 81–109). Amsterdam: North-Holland.Google Scholar
- 11.Martin-Löf, P. (1998). An intuitionistic theory of types. In Sambin, G., & Smith, J. (Eds.) Twenty-five years of constructive type theory. First published as preprint in 1972 (pp. 127–172). Oxford: Clarendon Press.Google Scholar
- 13.Prawitz, D. (1965). Natural deduction. Stockholm: Almqvist & Wiksell.Google Scholar
- 14.Prawitz, D. (1971). Ideas and results in proof theory. In Fenstad, J.E. (Ed.) Proceedings of the second Scandinavian logic symposium (pp. 235–307). Amsterdam: North-Holland.Google Scholar
- 15.Prawitz, D. (1973). Towards a foundation of a general proof theory. In Suppes, P., Henkin, L., Joja, A., Moisil, G.C. (Eds.) Logic, methodology and philosophy of science IV (pp. 225–250). Amsterdam: North-Holland.Google Scholar