단발적 기초

Univalent foundations

단발적인 기초는 수학의 기초에 대한 접근법으로서 유형이라고 불리는 물체로 수학적 구조가 형성된다.단발적 기초의 형식은 설정-이론적 기초의 어떤 것과 정확히 일치하는 것은 아니지만, 호모토피 등가 공간에 해당하는 동일한 형식과 경로에 의해 연결된 공간의 점에 해당하는 형식의 동일한 요소를 가진 공간이라고 생각할 수 있다.단발적인 기초는 헤르만 그라스만과 게오르크 칸토르의 옛 플라토닉 사상과 알렉산더 그로텐디크 양식의 "범주적" 수학에서 모두 영감을 얻는다.단발적 기초는 고전적 술어 논리학을 기본적 형식적 공제 체계로 사용하는 것에서 출발하여, 현재는 그것을 마틴 뢰프식 이론의 버전으로 대체하고 있다.단발적인 기초의 개발은 호모토피형 이론의 개발과 밀접한 관련이 있다.null

수학 구조의 적절한 (즉, 범주형) 개념을 채택하는 경우, 단발적인 기초는 구조주의와 양립할 수 있다.[1]null

역사

단발적인 재단의 주요 아이디어는 2006년에서 2009년 사이에 블라디미르 보에보드스키에 의해 공식화되었다.단발적인 기초와 초기 사상 사이의 철학적 연결고리를 위한 유일한 참조는 Voevodsky의 2014 Bernays 강연이다.[2]"단일성"이라는 이름은 보에보드스키 때문이다.[3]단발적 토대 현황에 기여하는 일부 사상의 역사에 대한 보다 자세한 논의는 호모토피형 이론의 페이지에서 확인할 수 있다.null

단발적 기초의 근본적인 특징은 그것들이 마르틴 뢰프 유형 이론과 결합되었을 때 현대 수학의 공식화를 위한 실질적인 시스템을 제공한다는 것이다.이 시스템과 코크, 아그다 같은 현대적인 증명 조교들을 이용하여 상당량의 수학이 공식화되었다."창고"라고 불리는 최초의 도서관은 2010년에 블라디미르 보보드스키에 의해 만들어졌다.[4]이제 Foundations는 UniMath라고 불리는 몇몇 작가들과 함께 더 큰 발전의 한 부분이다.[5]재단들은 또한 HoTT Coq 도서관이나[6] HoTT Agda 도서관 같은 정형화된 수학의 다른 도서관들에게 영감을 주었고,[7] 그들은 새로운 방향으로 독창적인 아이디어를 개발했다.null

단일 재단의 중요한 이정표는 2014년 6월 티에리 코퀀드의[8] 부르바키 세미나 연설이었다.null

주요개념

단발적인 기초는 상위 카테고리 이론에 근거하여 수학의 기초를 만들려는 특정한 시도에서 비롯되었다.단발적인 기초에 가장 가까운 초기 아이디어는 마이클 막카이가 FIRD로 알려진 그의 비전적인 논문에서 표현한 아이디어였다.[9]마카이가 구상하는 단발적 기초와 기초의 주요 구분은 '세트의 고차원 아날로그'가 무한대 그룹오이드에 해당하며, 범주는 부분적으로 순서가 정해진 세트의 고차원 아날로그로 보아야 한다는 인식이다.null

원래, 단발적인 기초는 블라디미르 보에보스키가 고안한 것으로, 고전 순수 수학에 종사하는 사람들이 컴퓨터를 사용하여 그들의 구성과 구조를 검증할 수 있도록 하는 것을 목표로 한다.비생산적 기초가 본질적으로 건설적이라는 사실은 파운데이션스 라이브러리(현재의 UniMath의 일부)를 집필하는 과정에서 발견되었다.현재, 단발적인 기초에서 고전 수학은 건설 수학의 "역행"으로 간주된다. 즉, 고전 수학은 배제된 중간의 법칙을 가정으로 사용하는 이론과 구성으로 이루어진 구성 수학의 부분집합이자 에 의한 건설 수학의 "양분"이다.등가성이라는 관계, 배제된 중간자의 공리null

Martin-Löf형 이론과 그 후손인 Calculus of In 귀납형 구조와 같은 단수형 기초에 대한 공식화 시스템에서는 세트의 고차원 아날로그가 유형별로 표현된다.유형의 집합은 h-수준(또는 호모토피 수준)의 개념에 의해 계층화된다.[10]null

h-수준 0의 유형은 1점 유형과 동일한 유형이다.그들은 계약형이라고도 불린다.null

h-수준 1의 유형은 두 원소가 동일한 유형이다.그러한 유형을 일률적인 기초에서 "제안"이라고 한다.[10]h-레벨에 대한 명제의 정의는 앞서 아워디와 바우어가 제시한 정의와 일치한다.[11]그래서 모든 명제가 유형이지만, 모든 유형이 명제인 것은 아니다.명제가 되는 것은 증거를 필요로 하는 유형의 재산이다.예를 들어, 단일기반의 첫 번째 기본구성을 iscontr이라고 한다.그것은 종류마다 함수다.X가 유형인 경우 iscontr X는 X가 계약 가능한 경우에만 객체를 갖는 유형이다.X의 경우 X형식이 h-수준 1을 가지므로 계약형식이 되는 것이 재산이라는 것은 정리(UniMath 라이브러리에서는 isapropiscontr라고 한다)이다.이러한 h-수준 1의 대상과 상위 h-수준의 대상의 대상이 목격한 구조물의 구별은 단일기초에서 매우 중요하다.null

h-level 2의 종류를 set라고 한다.[10]자연수의 종류에 h-수준 2(UniMath의 isasetnat)가 있다는 것이 정리다.마틴 뢰프형 이론에서 집합의 비생산적인 공식화는 건설적이면서도 고전적이면서도 설정 이데올로기 수학의 모든 측면에 대한 공식적인 추론을 위해 현재 이용 가능한 최상의 환경이라고 단발적 재단 설립자들에 의해 주장되고 있다.[12]null

범주는 부분적으로 순서 집합을 정의하는 h-수준 2의 구조와 매우 유사한 추가 구조를 가진 h-수준 3의 유형으로 정의된다(UniMath의 RezkCompletion 라이브러리 참조).단발적 토대에서의 범주 이론은 세트이론적 세계의 범주 이론과는 다소 다르고 풍부하며, 중요한 새로운 구분은 사전 범주와 범주의 구별이다.[13]null

독창적인 기초의 주요 아이디어와 그 기초가 건설적인 수학과의 연관성에 대한 설명은 티에리 코콴드의 자습서에서 찾을 수 있다. (2부)에서 찾을 수 있다.고전 수학의 관점에서 본 주요 사상의 프레젠테이션은 알바로 펠라요와 마이클 워렌의 리뷰 기사와 다니엘 그레이슨의 서론에서[15] 찾아볼 수 있다.[14]재단 라이브러리에 대한 기사도 참조하십시오.null

현재 개발 현황

보에보츠키가 칸 단순 집합에서 값을 가진 마르틴 뢰프형 이론의 통일된 모델을 구축한 것에 대한 설명은 크리스 카풀킨, 피터 르파누 럼스다인, 블라디미르 보보드스키의 논문에서 찾을 수 있다.[16]단순 집합의 역도 범주에 값을 갖는 단일 모델들은 Michael Shulman에 의해 만들어졌다.[17]이러한 모델들은 단일성 공리가 제안들에 대한 배제된 중간 공리에서 독립적이라는 것을 보여주었다.null

보에보스키의 모델은 불가역적인 방식으로 선택의 공리를 사용하기 때문에 비구축적인 것으로 간주된다.null

또한 자연수에 대한 단발성 공리와 카노니티를 추가로 만족시킨다는 마틴 뢰프식 이론의 규칙들에 대한 건설적인 해석을 찾는 문제는 여전히 열려 있다.마크 베젬, 티에리 코콴트, 사이먼 휴버의[18] 논문에서 부분적인 해결책이 간략히 설명되어 있으며, 핵심 남은 문제는 신원 유형의 제거기의 계산 특성이다.본 논문의 사상은 현재 입체형 이론의 전개 등 여러 방향으로 전개되고 있다.[19]null

새로운 방향

단발적 기초의 틀에서 수학의 공식화에 관한 대부분의 작업은 다양한 하위 시스템과 귀납적 구성의 확장을 이용하여 이루어지고 있다.null

많은 시도에도 불구하고 CIC를 사용하여 해결책을 구성할 수 없었던 세 가지 표준 문제가 있다.

  1. 준-심층 구조의 유형을 정의하기 위해, H형 또는 (비례,1)-형식의 범주 구조를 정의한다.
  2. 크기 조정 규칙을 실행할 수 있는 우주 관리 시스템으로 CIC를 확장한다.
  3. 단발성 Axiom의[20] 건설적 변형을 개발한다.

이러한 미해결 문제들은 CIC가 단발적 기반 개발의 초기 단계에 좋은 시스템인 반면, 그것의 보다 정교한 측면에 대한 작업에 컴퓨터 증명 보조자를 사용하는 방향으로 나아가기 위해서는 새로운 세대의 공식적인 공제 및 계산 시스템의 개발이 필요할 것임을 나타낸다.null

참고 항목

참조

  1. ^ Awodey, Steve (2014). "Structuralism, Invariance, and Univalence" (PDF). Philosophia Mathematica. 22 (1): 1–11. CiteSeerX 10.1.1.691.8113. doi:10.1093/philmat/nkt030.
  2. ^ Voevodsky, Vladimir (September 9–10, 2014). "Foundations of mathematics — their past, present and future". The 2014 Paul Bernays Lectures. ETH Zurich. Voevodsky 강의에서 항목 11 참조
  3. ^ nLab의 일변도 공리
  4. ^ 재단 라이브러리, https://github.com/vladimirias/Foundations 참조
  5. ^ UniMath 라이브러리, https://github.com/UniMath/UniMath 참조
  6. ^ HoTT Coq 라이브러리, https://github.com/HoTT/HoTT 참조
  7. ^ HoTT 아그다 라이브러리, https://github.com/HoTT/HoTT-Agda 참조
  8. ^ Coquand의 부르바키 강의 논문과
  9. ^ Makkai, M. (1995). "First Order Logic with Dependent Sorts, with Applications to Category Theory" (PDF). FOLDS.
  10. ^ a b c 2014 Pelayo & Warren 참조, 페이지 611
  11. ^ Awodey, Steven; Bauer, Andrej (2004). "Propositions as [types]". J. Log. Comput. 14 (4): 447–471. doi:10.1093/logcom/14.4.447.
  12. ^ Voevodsky 2014, 강의 3, 슬라이드 11
  13. ^ 참조
  14. ^ Pelayo, Álvaro; Warren, Michael A. (2014). "Homotopy type theory and Voevodsky's univalent foundations". Bulletin of the American Mathematical Society. 51 (4): 597–648. doi:10.1090/S0273-0979-2014-01456-9.
  15. ^ Grayson, Daniel R. (2018). "An introduction to univalent foundations for mathematicians". Bulletin of the American Mathematical Society. 55 (4): 427–450. arXiv:1711.01477. doi:10.1090/bull/1616. S2CID 32293255.
  16. ^ Kapulkin, Chris; Lumsdaine, Peter LeFanu; Voevodsky, Vladimir (2012). "The Simplicial Model of Univalent Foundations". arXiv:1211.2851 [math.LO].
  17. ^ Shulman, Michael (2015). "Univalence for inverse diagrams and homotopy canonicity". Mathematical Structures in Computer Science. 25 (5): 1203–1277. arXiv:1203.3253. doi:10.1017/S0960129514000565. S2CID 13595170.
  18. ^ Bezem, M.; Coquand, T.; Huber, S. "A model of type theory in cubical sets" (PDF).
  19. ^ Altenkirch, Thorsten; Kaposi, Ambrus, A syntax for cubical type theory (PDF)
  20. ^ V. Voevodsky, Univalent Foundation Project(NSF 보조금 애플리케이션의 수정된 버전), 페이지 9

외부 링크

  • Wiktionary에서 단발성에 대한 사전 정의
정형화된 수학의 도서관