The Normalization Theorem for the First-Order Classical Natural Deduction with Disjunctive Syllogism
0
조회
0
다운로드
0
인용
0
참고문헌
키워드
초록
In the present paper, we prove the normalization theorem and the consistency of the first-order classical logic with disjunctive syllogism. First, we propose the natural deduction system SCD for classical propositional logic having rules for conjunction, implication, negation, and disjunction. The rules for disjunctive syllogism are regarded as the rules for disjunction. After we prove the normalization theorem and the consistency of SCD, we extend SCD to the system SPCD for the first-order classical logic with disjunctive syllogism. It can be shown that SPCD is conservative extension to SCD. Then, the normalization theorem and the consistency of SPCD are given.
Abstract
In the present paper, we prove the normalization theorem and the consistency of the first-order classical logic with disjunctive syllogism. First, we propose the natural deduction system SCD for classical propositional logic having rules for conjunction, implication, negation, and disjunction. The rules for disjunctive syllogism are regarded as the rules for disjunction. After we prove the normalization theorem and the consistency of SCD, we extend SCD to the system SPCD for the first-order classical logic with disjunctive syllogism. It can be shown that SPCD is conservative extension to SCD. Then, the normalization theorem and the consistency of SPCD are given.
참고문헌 (11)
- Andou, Y., "A Normalization-Procedure for the First Order Classical Natural Deduction with Full Logical Symbols", Tsukuba Journal of Mathematics, 19(1), pp.153~162 (1995)
- Dummett, M., "Logical Basis of Metaphysics" (1991), Harvard Univeristy Press
- Gentzen, G., "The Collected Papers of Gerhard Gentzen", pp.68~131 (1935), North-Holland
- Gentzen, G., "The Collected Papers of Gerhard Gentzen", pp.132~222 (1936), North-Holland
- Gentzen, G., "The Collected Papers of Gerhard Gentzen", pp.252~286 (1938), North-Holland
- Prawitz, D., "Natural Deduction: A Proof-Theoretical Study" (1965), Dover Publications
- Prawitz, D., "Ideas and Results in Proof theory", Proceedings of the 2nd Scandinavian Logic Symposium, pp.235~308 (1971), North Holland
- Prawitz, D., "Gentzen’s Centenary", pp.131~176 (2015), Springer Press
- Milne, P., "Classical harmony: rules of inference and the meaning of the logical constants", Synthese, 100, pp.49~94 (1994)
- Milne, P., "Harmony, purity, simplicity and a ‘seemingly magical fact’", The Monist, 85, pp.498~534 (2002)
- Stålmark, G., "Normalization Theorems for Full First Order Classical Natural Deduction", The Journal of Symbolic Logic, 56(1), pp.129~149 (1991)