고차 논리

Higher-order logic

수학과 논리학에서, 고차 논리는 부가적인 수량화, 때로는 더 강한 의미론에 의해 1차 논리와 구별되는 술어 논리의 한 형태이다.표준 의미론을 가진 고차 로직은 표현력이 더 높지만, 모델 이론적 특성은 1차 로직보다 덜 잘 동작합니다.

HOL로 축약된 "고차 논리"라는 용어는 일반적으로 고차 단순 술어 논리를 의미하기 위해 사용됩니다.여기서 "단순"은 기본 유형 이론이 단순한 유형의 이론이라는 것을 나타냅니다(단순 유형 이론 참조).리언 취스텍프랭크 램지알프레드 노스 화이트헤드와 버트랜드 러셀이 쓴 프린키피아 매스매티카에 명시된 복잡하고 서투른 유형의 이론의 단순화로 이것을 제안했다.오늘날 단순형은 다형종속형[1]제외하는 의미도 있습니다.

수량화범위

1차 로직은 개인을 넘는 변수만 수량화합니다.또한 2차 로직은 집합 전체를 수량화합니다.또한 3차 로직은 집합 전체를 수량화합니다.

고차 로직은 1차, 2차, 3차, ..., n차 로직의 결합입니다.즉, 고차 로직은 임의로 깊이 중첩된 집합에 대한 정량화를 허용합니다.

의미론

고차 로직에는 두 가지 의미론이 있습니다.

표준 또는 전체 의미론에서 상위 유형의 개체에 대한 수량자는 해당 유형의 가능한 모든 개체에 걸쳐 있습니다.예를 들어, 개인 집합에 대한 수량식은 개인 집합의 전체 파워셋에 걸쳐 있습니다.따라서, 표준 의미론에서, 일단 개체 집합이 지정되면, 이것은 모든 수량화자를 지정하기에 충분합니다.표준 의미론을 가진 HOL은 1차 논리보다 표현력이 높습니다.예를 들어, HOL은 1차 논리로는 불가능자연수실수의 범주적 공리화를 허용합니다.그러나, Kurt Gödel의 결과로, 표준 의미론을 가진 HOL은 효과적이고 건전하며 완전한 증명 [2]미적분을 인정하지 않는다.표준 의미론을 가진 HOL의 모델 이론 특성은 1차 논리보다 더 복잡합니다.예를 들어, 2차 논리의 뢰벤하임 수는 그러한 기수가 [3]존재하는 경우 첫 번째 측정 가능한 기수보다 이미 큽니다.반면 1차 로직의 뢰벤하임 수는 최소 무한 기수인 뢰벤하임0 수이다.

헨킨 의미론에서는 각 고차 유형에 대해 개별 도메인이 각 해석에 포함됩니다.따라서, 예를 들어, 개인 집합의 수량화자는 개인 집합의 파워셋의 하위 집합에만 적용될 수 있다.이러한 시멘틱스를 가지는 HOL은, 1차 논리보다 강하지 않고, 다량 정렬된 1차 로직과 동등합니다.특히 Henkin semantics를 가진 HOL은 1차 논리의 모든 모델 이론 속성을 가지고 있으며 1차 논리로부터 계승된 완전하고 건전하며 효과적인 증명 시스템을 가지고 있다.

특성.

고차 논리학은 교회의 단순한 유형[4] 이론과 다양한 형태의 직관적 유형 이론을 포함한다.제라드 휴트는 3차 [5][6][7]논리의 유형 이론적 풍미에서는 통일성결정할 수 없다는 것을 보여주었다. 즉, 3차(임의적인 고차) 항 사이의 임의의 방정식이 해답을 가지고 있는지 아닌지를 결정하는 알고리즘이 있을 수 없다.

동형의 특정 개념까지, 파워셋 연산은 2차 논리로 정의할 수 있다.이 관찰을 이용하여, Jaakko Hintikka는 1955년에 2차 논리가 고차 논리학의 모든 공식에 대해 2차 [8]논리학의 동등한 공식을 찾을 수 있다는 의미에서 고차 논리학을 시뮬레이션할 수 있다는 것을 확립했다.

"고차 논리"라는 용어는 고전적인 고차 논리를 지칭하는 것으로 가정됩니다.그러나 모달 고차 논리도 연구되고 있다.몇몇 논리학자들에 따르면, 괴델의 존재론적 증거는 그러한 [9]맥락에서 가장 잘 연구된다.

「 」를 참조해 주세요.

메모들

  1. ^ 제이콥스, 1999, 5장
  2. ^ 샤피로 1991, 87페이지
  3. ^ 메나헴 마지도르와 주코 베내넨.미타그-레플러 연구소의 보고서 No. 15(2009/2010) "1차 논리 확장을 위한 뢰벤하임-스콜렘-타르스키 숫자에 대하여"
  4. ^ Alonzo Church, 단순한 유형 이론의 공식, 기호 논리 저널 5(2): 56–68(1940)
  5. ^ Huet, Gérard P. (1973). "The Undecidability of Unification in Third Order Logic". Information and Control. 22 (3): 257–267. doi:10.1016/s0019-9958(73)90301-x.
  6. ^ Huet, Gérard (Sep 1976). Resolution d'Equations dans des Langages d'Ordre 1,2,...ω (Ph.D.) (in French). Universite de Paris VII.
  7. ^ Huet, Gérard (2002). "Higher Order Unification 30 years later" (PDF). In Carreño, V.; Muñoz, C.; Tahar, S. (eds.). Proceedings, 15th International Conference TPHOL. LNCS. Vol. 2410. Springer. pp. 3–12.
  8. ^ HOL에서의 엔트리
  9. ^ Fitting, Melvin (2002). Types, Tableaus, and Gödel's God. Springer Science & Business Media. p. 139. ISBN 978-1-4020-0604-3. Godel's argument is modal and at least second-order, since in his definition of God there is an explicit quantification over properties. [...] [AG96] showed that one could view a part of the argument not as second-order, but as third-order.

레퍼런스

외부 링크