마틴뢰프의 직관주의적 유형론의 중요 사항들을 설명하고, 그 체계의 가장 중요한 특성 중의 하나인 명제와 판단의 구분에 관해 검토한다. 1절에서 문제를 도입한 후, 2절에서 직관주의적 유형론의 명제개념은 직관주의적 명제개념의 발전된 형태임을 보이고, 3절에서는 직관주의적 유형론에서 가장 기본적인 판단개념을 설명한 후, 4절에서 직관주의적 유형론의 기본적인 추론규칙들을 설명하고 그 적용의 한 사례를 검토할 것이다. 마지막으로 5절에서, 직관주의적 유형론에서 명제와 판단의 구분이 차지하는 중요성을 부연한 후, 기초론적 체계에서 명제와 판단의 구분이 필수적인지의 문제와 관련하여, 통상적인 프레게적 구분으로부터 시작하여 직관주의적 유형론에서와 같은 구분에 이르기 위해서는 어떤 것들이 전제되거나 정당화되어야 하는지 검토할 것이다.
마틴뢰프의 직관주의적 유형론의 중요 사항들을 설명하고, 그 체계의 가장 중요한 특성 중의 하나인 명제와 판단의 구분에 관해 검토한다. 1절에서 문제를 도입한 후, 2절에서 직관주의적 유형론의 명제개념은 직관주의적 명제개념의 발전된 형태임을 보이고, 3절에서는 직관주의적 유형론에서 가장 기본적인 판단개념을 설명한 후, 4절에서 직관주의적 유형론의 기본적인 추론규칙들을 설명하고 그 적용의 한 사례를 검토할 것이다. 마지막으로 5절에서, 직관주의적 유형론에서 명제와 판단의 구분이 차지하는 중요성을 부연한 후, 기초론적 체계에서 명제와 판단의 구분이 필수적인지의 문제와 관련하여, 통상적인 프레게적 구분으로부터 시작하여 직관주의적 유형론에서와 같은 구분에 이르기 위해서는 어떤 것들이 전제되거나 정당화되어야 하는지 검토할 것이다.
We explain some basic elements of Martin-L$\ddot{o}$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 intuiti...
We explain some basic elements of Martin-L$\ddot{o}$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.
We explain some basic elements of Martin-L$\ddot{o}$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.
이른바 ‘커리-하워드 동형(Curry-Howard Isomorphism)’은 BHK 해석 및 정형화 정리와 더불어 직관주의적 유형론의 배경이 되는 중요한 발견이다. 이 동형은 명제와 유형 (혹은 집합) 간의 대응 및 증명과 확장된 람다 연산의 항 간의 대응을 나타낸다.
ZF와 같은 표준적 집합론이나 단순 유형론은 고전수학의 기초적 체계로 간주되는 이유는 무엇인가요?
ZF와 같은 표준적 집합론이나 단순 유형론(Simple Type Theory)은 흔히 고전 수학의 기초적 체계로 간주된다. 그 한 이유는, 그 적절성에 관한 논란이 없지 않지만, 고전 수학의 개념들이 그런 체계에서 정의될 수 있고 고전 수학의 논증들이 그런 체계에서 형식화될 수 있기 때문이다. 유사한 의미에서 직관주의 수학의 기초적 체계로 의도된 몇 가지 형식체계들 중 마틴뢰프(P.
명제 혹은 집합에 관한 규칙들의 네 가지 종류는 무엇인가요?
명제 혹은 집합에 관한 규칙들은 형성규칙(Formation Rules), 도입규칙(Introduction Rules), 제거규칙(Elimination Rules), 동등성규칙(Equality Rules)의 네 가지 종류로 나누어진다. 형성규칙은 통상적으로 메타언어에서 제시되는 구문론적 규칙과 유사하지만, 이런 통상적인 구문론적 규칙은 특정한 언어표현을 정의하는데 반해, 여기서의 형성규칙은 특정 언어와 무관하게 집합(명제)을 형성하는 규칙이다.
※ AI-Helper는 부적절한 답변을 할 수 있습니다.