직관주의적 유형론에서의 명제와 판단
Propositions and Judgments in the Intuitionistic Type Theory
0
조회
0
다운로드
6
인용
0
참고문헌
키워드
초록
마틴뢰프의 직관주의적 유형론의 중요 사항들을 설명하고, 그 체계의 가장 중요한 특성 중의 하나인 명제와 판단의 구분에 관해 검토한다. 1절에서 문제를 도입한 후, 2절에서 직관주의적 유형론의 명제개념은 직관주의적 명제개념의 발전된 형태임을 보이고, 3절에서는 직관주의적 유형론에서 가장 기본적인 판단개념을 설명한 후, 4절에서 직관주의적 유형론의 기본적인 추론규칙들을 설명하고 그 적용의 한 사례를 검토할 것이다. 마지막으로 5절에서, 직관주의적 유형론에서 명제와 판단의 구분이 차지하는 중요성을 부연한 후, 기초론적 체계에서 명제와 판단의 구분이 필수적인지의 문제와 관련하여, 통상적인 프레게적 구분으로부터 시작하여 직관주의적 유형론에서와 같은 구분에 이르기 위해서는 어떤 것들이 전제되거나 정당화되어야 하는지 검토할 것이다.
Abstract
We explain some basic elements of Martin-Löf's type theory and examine the distinction between propositions and judgments. In section 1, we introduce the problem. In section 2, we explain the concept of proposition in the intuitionistic type theory as a development of the intuitionistic conception of proposition. In section 3, we explain the concept of judgment in the intuitionistic type theory. In section 4, we explain some basic inference rules and examine a particular derivation in the theory. In section 5, we examine one route from the Fregean distinction between propositions and judgments to the distinction between them in the intuitionistic type theory, paying attention to the alleged necessity for introducing different forms of judgments.
참고문헌 (36)
- 정인교, "역리와 증명", 철학, 47, pp.201~237 (1996)
- 정인교, "무한정 확장가능성과 양화", 철학연구, (38), pp.213~249 (2009), 철학연구소
- Aczel, P., "The Type theoretic Interpretation of Constructive Set Theory", Logic Colloquium'77, pp.55~66 (1978)
- Beeson, M., "Foundations of Constructive Mathematics" (1985), Springer
- Bishop, E., "Constructive Analysis" (1985), Springer-Verlag
- Curry, H., "Combinatory Logic, Vol. I" (1958), North-Holland
- Dummett, M., "Elements of Intuitionism, (second ed.)" (2000), Oxford University Press
- Frege, G., "Thoughts, In Collected Papers on Mathematics, Logic and Philosophy", pp.351~372 (1984), Basil Blackwell
- Howard, W., "The formulae-as-types notion of construction, In To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism", pp.479~490 (1980), Academic Press
- Martin-Löf, P., "An Intuitionistic Theory of Types: Predicative Part", Logic Colloquium, 통권 : 73, pp.73~117 (1975)
- Martin-Löf, P., "Constructive Mathematics and Computer Programming, In Logic, Methodology and Philosophy of Science VI", pp.153~175 (1982)
- Martin-Löf, P., "Intuitionistic Theory of Types" (1984), Bibliopolis
- Martin-Löf, P., "On the Meanings of the Logical Constants and the Justification of Logical Laws", Nordic Journal of Philosophical Logic, 1(1), pp.11~60 (1996)
- Martin-Löf, P., "Truth of a Proposition, Evidence of a Judgement, Validity of a Proof", Synthese, 73, pp.407~420 (1987)
- Martin-Löf, P., "A Path from Logic to Metaphysics", pp.141~149 (1991), CLUEB Bolgna
- Martin-Löf, P., "Analytic and Synthetic Judgements in Type Theory, In Kant and Contemporary Epistemology", pp.87~99 (1994), Kluwer Academic Publishers
- Martin-Löf, P., "Verificationism Then and Now, In The Foundational Debate: Complexity and Constructivity in Mathematics and Physics", pp.187~196 (1995), Kluwer Academic Publishers
- Martin-Löf, P., "Truth and Knowability: On the Principles C and K of Michael Dummett, In Truth in Mathematics", pp.105~114 (1996), Clarendon Press
- Martin-Löf, P., "An Intuitionistic Theory of Types, In Twenty-five Years of Constructive Type Theory", pp.127~172 (1998), Clarendon Press
- Martin-Löf, P., "100 years of Zermelo's axiom of choice: what was the problem with it", The Computer Journal, 49(3), pp.345~350 (2006)
- Nordström, B., "Programming in Martin-Löf's Type Theory: An Introduction" (1990), Clarendon Press
- Nordström, B., "Martin-Löf's Type Theory, In Handbook of Logic in Computer Science Vol. V", pp.1~37 (2000), Oxford University Press
- Prawitz, D., "Natural Deduction: A Proof-theoretical Study" (1965), Almqvist & Wiksell
- Prawitz, D., "Ideas and Results in Proof Theory", Proceedings of the Second Scandinavian Logic Symposium, pp.235~307 (1971)
- Prawitz, D., "Comments on the Papers", Theoria, 64, pp.283~337 (2000)
- Prawitz, D., "Inference and Knowledge, In Logica Yearbook 2008", pp.175~192 (2009), College Publications
- "Validity of Inferences"[URL]
- Ranta, A., "Type-Theoretical Grammar" (1994), Oxford University Press
- Sommaruga, G., "History and Philosophy of Constructive Type Theory" (2000), Kluwer Academic Publishers
- SØrensen, M. H., "Lectures on the Curry-Howard Isomorphism" (2006), Elsevier
- Sundholm, G. B., "Implicit Epistemic Aspect of Constructive Logic", Journal of Language, Logic and Information, 6, pp.191~212 (1997)
- Sundholm, G. B., "Inference, Consequence, Implication: A Constructivist's Perspective", Philosophia Mathematica, 6(3), pp.178~194 (1998)
- Sundholm, G. B., "Proof as Acts and Proof as Objects: Some Questions for Dag Prawitz", Theoria, 64, pp.187~216 (2000)
- Van der Schaar, M., "The Cognitive Act and the First-Person Perspective: An Epistemology for Constructive Type Theory", Synthese, 180(3), pp.391~417 (2011)
- Thompson, S., "Type Theory & Functional Programming" (1999), Computing Laboratory, University of Kent
- Troelstra, A. S., "Constructivism in Mathematics: An Introduction, 2 Vols" (1988), North-Holland