판단(수학적 논리)
Judgment (mathematical logic)수학적 논리학에서 판단(또는 판단)이나 주장은 금속어의 진술이나 발음이 된다. 예를 들어, 1차 논리에서의 전형적인 판단은 끈이 잘 형성된 공식이거나 명제가 참이라는 것이다. 이와 유사하게, 판단은 대상 언어의 표현에서 자유 변수의 발생이나 명제의 가능성을 주장할 수 있다. 일반적으로 판단은 메타테고리 내에서 귀납적으로 정의 가능한 주장이 될 수 있다.
판단은 추론 체계를 공식화하는 데 사용된다: 논리 공리는 판단을 표현하고, 추론 규칙의 전제는 판단의 순서에 따라 형성되며, 그 결론 역시 판단이다(즉, 증거의 가설과 결론은 판단이다). 힐버트식 공제 시스템 변형의 특징은 자연 추론과 순열 미적분학 모두 일부 문맥 변화 규칙을 포함하고 있는 반면, 문맥은 추론 규칙에서 변경되지 않는다는 것이다. 그러므로 만약 우리가 가상적 판단이 아닌 토폴로지의 파생성에만 관심이 있다면, 우리는 힐버트식 추론 시스템을 그것의 추론 규칙들이 다소 단순한 형태의 판단만을 포함하는 방식으로 공식화할 수 있다. 다른 두 가지 공제 시스템에서도 같은 것을 할 수 없다: 일부 추론 규칙에서 맥락이 바뀌기 때문에 가상의 판단을 피할 수 있도록 공식화할 수 없다. 단지 우리가 그것들을 단지 tautology의 파생성을 증명하기 위해 사용하고 싶더라도 말이다.
다양한 캘커리들 사이의 이러한 기본적인 다양성은 그러한 차이를 허용하는데, 힐버트식 공제 체계에서 동일한 기본 사상(예: 공제 정리)이 메타테오렘으로 증명되어야 하는 반면, 자연 추론의 규칙으로서 명시적으로 선언될 수 있다.
형식 이론에서, 일부 유사한 개념은 수학 논리학에서와 같이 사용된다(예: Curry-Howard 통신과 같은 두 분야 사이의 연결을 야기한다). 수학 논리에서의 판단 개념의 추상화는 유형 이론의 기초에서도 이용될 수 있다.
참고 항목
참조
- Martin-Löf, Per (1996). "On the meanings of the logical constants and the justifications of the logical laws" (PDF). Nordic Journal of Philosophical Logic. 1 (1): 11–60. ISSN 0806-6205.
- Dybjer, Peter. "Intuitionistic Type Theory". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy.
- Pfenning, Frank; Davies, Rowan (August 2001). "A judgmental reconstruction of modal logic". Mathematical Structures in Computer Science. 11 (4): 511–540. CiteSeerX 10.1.1.43.1611. doi:10.1017/S0960129501003322.
외부 링크
- "Judgments in formal systems". Everything2.
- Pfenning, Frank (Spring 2004). "Natural Deduction" (PDF). 15-815 Automated Theorem Proving.
- Martin-Löf, Per (1983). "On the meaning of the logical constants and the justifications of the logical laws". Siena Lectures.
