범주형 논리학
Categorical logic범주형 논리학은 범주 이론에서 나온 도구와 개념을 수학 논리 연구에 적용하는 수학의 한 분야다. 이론 전산학과의 연관성도 눈에 띈다.[1] 넓은 의미에서 범주형 논리는 범주별로 구문과 의미론 모두를 나타내고, 펑터(functor)에 의한 해석도 나타낸다. 범주형 프레임워크는 논리적 구조와 유형-이론적 구조에 대한 풍부한 개념적 배경을 제공한다. 그 주제는 1970년경부터 이러한 용어로 알아볼 수 있었다.
개요
논리에 대한 범주형 접근법에는 다음과 같은 세 가지 중요한 주제가 있다.
- 범주형 의미론
- 범주형 논리는 C가 집합과 함수의 범주인 특정 경우에 나타나는 구조물의 고전적 모델 이론적 개념과 함께 범주 C에서 평가되는 구조 개념을 도입한다. 이 개념은 모형의 이론적 개념에 일반성이 결여되어 있거나 불편할 때 유용하다는 것이 입증되었다. R.A.G. 실리의 시스템 F와 같은 다양한 충동 이론 모델링은 범주형 의미론의 유용성을 보여주는 예다.
- 사전범주 논리의 연결은 부선 펑터의 개념을 사용하여 보다 명확하게 이해되었고, 부선 펑터를 사용하여 정량자를 가장 잘 이해한다는 것이 밝혀졌다.[2]
- 내국어
- 이는 도표추적 등에 의한 증거의 정형화와 일반화로 볼 수 있다. 하나는 범주의 관련 구성요소를 명명하는 적절한 내부 언어를 정의한 다음, 내부 언어에 대한 논리의 주장을 해당하는 범주형 문장으로 바꾸기 위해 범주형 의미론을 적용한다. 이것은 토포스의 내부 언어가 토포스의 직감적 고차 논리학의 의미론과 함께 토포스의 대상과 형태에 대해 "세트와 기능인 것처럼" 추론할 수 있게 해주는 토포즈 이론에서 가장 성공적이었다.[citation needed] 이것은 고전적 논리와 양립할 수 없는 성질을 가진 상투적인 것들을 다루는 데 성공적이었다. 대표적인 예가 다나 스콧이 자신의 기능 공간으로 후퇴하는 물체 측면에서 정형화되지 않은 람다 미적분학 모델이다. 또 하나는 '모기-'이다.마틴 하이랜드의 효과적인 토포스의 내부 전체 하위 카테고리에 의한 시스템 F의 하이랜드 모델.
- 용어 모델 구성
- 많은 경우에, 논리의 범주형 의미론들은 논리의 이론과 적절한 종류의 범주의 사례들 사이의 일치성을 확립하는 근거를 제공한다. 대표적인 예가 단순 타이핑된 람다 미적분학에 대한 βη 등가 논리의 이론과 데카르트 폐쇄 범주 간의 대응이다. 용어 모델 구성을 통해 이론에서 발생하는 범주는 일반적으로 적절한 보편적 속성에 의해 동등하게 특징지어질 수 있다. 이것은 적절한 범주형 대수학을 이용하여 일부 로직의 메타이론적 특성에 대한 증거를 가능하게 했다. 예를 들어, 프레이드는 이런 식으로 직관적 논리의 존재와 분리 속성에 대한 증거를 제시했다.
참고 항목
메모들
- ^ Joseph Goguen, Till Mosakowski, Valeria de Paiva, Florian Rabe, Lutz Schroder "An Institutional View on Categine Logic" International Journal of Software and Informatics, 2007, 2007, 1(1) 페이지 129~152
- ^ 윌리엄 로비어, 퀀텀스 및 쉐이브스
참조
- 책들
- Abramsky, Samson; Gabbay, Dov (2001). Handbook of Logic in Computer Science: Logic and algebraic methods. Oxford: Oxford University Press. ISBN 0-19-853781-6.
- Gabbay, Dov (2012). Handbook of the History of Logic: Sets and extensions in the twentieth century. Oxford: Elsevier. ISBN 978-0-444-51621-3.
- Kent, Allen; Williams, James G. (1990). Encyclopedia of Computer Science and Technology. New York: Marcel Dekker Inc. ISBN 0-8247-2272-8.
- Barr, M. and Wells, C. (1990), 컴퓨터 과학을 위한 범주 이론. 영국 헤멜 헴프스테드.
- Lambek, J. and Scott, P.J. (1986), 상위 순서 범주형 논리 소개. 영국 케임브리지의 케임브리지 대학 출판부.
- 로베르, F.W., 로즈브루그, R.(2003) 세트 포 수학. 영국 케임브리지의 케임브리지 대학 출판부.
- 로베레, F.W. (2000년)와 샤누엘, S.H. 개념 수학: 카테고리에 대한 첫 번째 소개. 1997년 영국 케임브리지의 케임브리지 대학 출판부. 2000년 수정본으로 다시 인쇄.
세미날 페이퍼
- Lawever, F.W., Functorial Semantics of Algebraic 이론s. 미국 국립과학원 회보 제5호(1963년 11월)에서는 869-872번이다.
- 세트 카테고리의 Lawever, F.W., 기본 이론. 미국 국립과학원 회보 제52호, 제6호 (1964년 12월), 1506년-1511년.
- 로베레, F.W., 퀀텀스, 쉐이브스. 국제수학회의(International Congress on Mathematics, Nice 1970)에서는 Gautier-Villars(1971) 329-334.
추가 읽기
- 마이클 막카이와 곤잘로 E. Reyes, 1977, First 순서 범주형 논리, Springer-Verlag.
- Lambek, J., Scott, P. J. 1986. 상위 순서 범주형 논리 소개. 꽤 쉽게 접근할 수 있는 도입부지만 다소 날짜가 잡혔다. 다형 및 종속형보다 고차 논리학에 대한 범주형 접근법은 이 책이 출판된 후 크게 개발되었다.
- Jacobs, Bart (1999). Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics 141. North Holland, Elsevier. ISBN 0-444-50170-3. 컴퓨터 과학자에 의해 쓰여진 포괄적인 모노그래프; 1차 및 고차 로직과 다형 및 종속형 모두를 다룬다. 다형성과 종속성을 다루는 데 필요한 범주형 논리학의 보편적 도구로서 섬유화된 범주에 초점을 맞추고 있다.
- 존 레인 벨 (2005) 범주형 논리학의 발전. 철학적 논리학의 지침서 제12권. 스프링거 존 벨의 홈페이지에서 온라인으로 이용 가능한 버전.
- 장피에르 마르키스와 곤살로 E. Reyes(2012). 1963-1977년 범주형 논리의 역사. 논리학의 역사 핸드북: 20세기의 세트와 연장, 6권, D. M. Gabbay, A. Kamanori & J. Woods, Eds, North-Holland, 689–800페이지. 예비 버전은 [1]에서 구할 수 있다.
