수리논리

Mathematical logic

수리논리는 수학 에서 형식논리를 연구하는 학문이다.주요 하위 영역에는 모델 이론, 증명 이론, 집합 이론, 그리고 재귀 이론이 포함됩니다.수학 논리학의 연구는 일반적으로 표현력이나 연역력과 같은 논리학의 형식적인 시스템의 수학적 속성을 다룬다.그러나 올바른 수학적 추론을 특징짓거나 수학의 기초를 확립하기 위해 논리를 사용하는 것도 포함될 수 있다.

그것의 시작 이래로, 수학 논리는 수학의 기초에 대한 연구에 기여했고 그것들에 의해 동기부여되었다.이 연구는 19세기 후반에 기하학, 산술, 해석위한 자명한 틀의 개발과 함께 시작되었다.20세기 초에 그것은 기초 이론의 일관성을 증명하는 데이비드 힐버트프로그램에 의해 형성되었다.Kurt Gödel, Gerhard Gentzen 등의 결과는 프로그램에 대한 부분적인 해결을 제공하고 일관성 입증에 관련된 문제를 명확히 했습니다.집합론에서의 연구는 집합론에 대한 공통 공리 체계에서 증명될 수 없는 이론들이 있지만, 거의 모든 일반 수학이 집합의 관점에서 공식화될 수 있다는 것을 보여주었다.수학의 기초에서의 현대 연구는 종종 수학의 어떤 부분이 모든 수학이 발전될 수 있는 이론을 찾으려고 하기 보다는 특정한 형식적인 체계에서 공식화될 수 있는지를 규명하는 데 초점을 맞춘다.

서브필드 및 범위

1977년의 수리논리[1] 핸드북은 현대 수리논리를 대략 네 가지 영역으로 분류한다.

  1. 집합론
  2. 모델 이론
  3. 재귀 이론 및
  4. 증명 이론과 구성 수학(단일 영역의 일부로 간주)

추가적으로, 때때로 계산 복잡도 이론의 분야도 수학 [2]논리의 일부로 포함된다.많은 기술과 결과가 여러 영역에서 공유되지만 각 영역에는 서로 다른 초점이 있습니다.이 분야들 사이의 경계선, 그리고 수학 논리와 수학의 다른 분야를 구분하는 경계선이 항상 날카롭지는 않다.괴델의 불완전성 정리는 재귀 이론과 증명 이론의 이정표를 찍을 뿐만 아니라 모달 논리학의 뢰브 정리로 이어졌다.강제하는 방법은 직관적인 수학의 연구뿐만 아니라 집합론, 모형 이론, 재귀 이론에서도 사용된다.

범주 이론의 수학적 분야는 많은 형식적 공리 방법을 사용하며 범주 논리 연구를 포함하지만 범주 이론은 일반적으로 수리 논리의 하위 분야로 간주되지 않습니다.수학의 다양한 분야에서의 적용 가능성 때문에, 손더스 맥 레인을 포함한 수학자들은 범주 이론을 집합론과 독립적으로 수학의 기초 체계로 제안해왔다.이러한 기초는 고전적 또는 비고전적 논리를 사용할 수 있는 집합론의 일반화된 모델과 유사한 토포스를 사용합니다.

역사

수학 논리는 19세기 중반에 수학의 하위 분야로 등장하여 두 전통이 합쳐진 것을 반영했다: 형식 철학적 논리와 [3]수학.논리학, 기호논리, 논리학의 대수학, 그리고 최근에는 형식논리로도 불리는 수학논리는 인위적인 표기법과 엄밀하게 연역적인 [4]방법의 도움으로 지난 19세기 동안 정교하게 기술된 논리 이론의 집합이다.이 출현 이전에 논리학은 수사학, 계산학,[5] 삼단논법, 철학통해 연구되었다.20세기 전반에는 수학의 기초에 대한 활발한 논쟁과 함께 근본적인 결과들이 폭발적으로 증가하였다.

초기 역사

논리 이론은 중국, 인도, 그리스 그리고 이슬람 세계포함한 역사의 많은 문화권에서 발전되었다.그리스 방법들, 특히 오르가논에서 발견된 아리스토텔레스 논리학(또는 용어 논리학)은 [6]수천 년 동안 서양 과학과 수학에서 폭넓게 적용되고 받아들여졌다.스토아파, 특히 크리시푸스술어 논리의 개발을 시작했다.18세기 유럽에서는 라이프니츠와 람베르트를 포함한 철학 수학자들이 형식 논리의 연산을 상징적 또는 대수적으로 다루려는 시도를 했지만, 그들의 노력은 고립되어 거의 알려지지 않았다.

19세기

19세기 중반, 조지 불과 아우구스투스 드 모건은 논리학의 체계적인 수학적 처리를 제시했다.조지 피콕과 같은 대수학자들에 의해 만들어진 그들의 작업은 전통적인 아리스토텔레스 논리 이론을 [7]수학의 기초 연구를 위한 충분한 틀로 확장시켰다.찰스 샌더스 피어스는 나중에 관계와 수량화를 위한 논리 체계를 개발하기 위해 불의 연구를 바탕으로 1870년부터 1885년까지 여러 논문에 발표했다.

Gottlob Frege는 1879년에 출판된 그의 Begriffsschrift에서 수식어와 함께 논리학의 독립적인 발전을 제시했는데, 이것은 논리학의 역사에서 일반적으로 전환점을 나타내는 것으로 여겨진다.그러나 프레게의 작품은 베르트런드 러셀이 금세기 초에 그것을 홍보하기 시작할 때까지 불분명하게 되었다.프레게가 개발한 2차원 표기법은 널리 채택된 적이 없으며 현대 문헌에서는 사용되지 않는다.

1890년부터 1905년까지, 에른스트 슈뢰더는 세 권으로 볼레숭겐 위버 다이 대수로지크를 출판했다.이 작품은 불, 드 모르간, 피어스의 작업을 요약하고 확장한 것으로, 19세기 말에 이해된 상징 논리에 대한 포괄적인 언급이었다.

기초 이론

수학이 제대로 된 토대 위에 구축되지 않았다는 우려는 산술, 해석, 기하학과 같은 수학의 기본 영역에 대한 자명체계의 발달로 이어졌다.

논리학에서 산술이라는 용어는 자연수의 이론을 말한다.주세페[8] 페아노는 불과 슈뢰더의 논리체계의 변형을 사용하면서도 수량자를 추가하는 그의 이름을 갖게 된 산술 공리(페아노 공리)를 발표했다.페아노는 그 당시 프레게의 작품을 알지 못했다.비슷한 시기에 Richard Dedekind는 자연수가 그 유도 특성에 의해 독특하게 특징지어진다는 것을 보여주었다.데데킨드는 페아노 [9]공리의 형식적인 논리적 특성이 결여된 다른 성격 묘사를 제안했다.그러나 데데킨드의 연구는 자연수 집합의 고유성(동형사상까지)과 후속 함수와 수학적 귀납의 재귀적 정의를 포함하여 페아노의 체계에서 접근 불가능한 이론들을 증명했다.

19세기 중반에, 기하학에 대한 유클리드의 공리들의 결함이 [10]알려졌습니다.1826년 [11]니콜라이 로바체프스키에 의해 확립된 평행공식의 독립성 외에도, 수학자들은 유클리드에 의해 당연하게 받아들여진 어떤 이론들이 사실 그의 공리로부터 입증될 수 없다는 것을 발견했다.이들 중 하나는 선이 적어도 두 개의 점을 포함하거나 그 반지름에 의해 중심이 분리된 같은 반지름의 원이 교차해야 한다는 정리이다.힐버트는[12] 패쉬의 [13]이전 연구를 바탕으로 기하학에 대한 완전한 공리를 개발했다.기하학의 공리화 성공은 힐베르트가 자연수와 실선과 같은 수학의 다른 영역에 대한 완전한 공리화를 추구하도록 동기를 부여했다.이것은 20세기 전반의 주요 연구 분야로 판명될 것이다.

19세기에는 함수 수렴 이론과 푸리에 급수를 포함한 실해석 이론이 크게 발전했다.바이어슈트라스와 같은 수학자들은 어디에도 구분이 되지 않는 연속함수와 같이 직관을 확장시키는 함수를 만들기 시작했다.함수를 계산 규칙 또는 부드러운 그래프로 간주하는 이전의 개념은 더 이상 적절하지 않았다.바이얼스트래스는 자연수의 특성을 이용한 분석의 공리화를 추구한 분석의 산술화를 옹호하기 시작했다.한계와 연속 함수의 현대적 (ε, )) 정의는 1817년에 [14]볼자노에 의해 이미 개발되었지만, 상대적으로 알려지지 않은 채로 남아 있었다.코시는 1821년에 무한소수의 관점에서 연속성을 정의했다(34페이지 Cours d'Analyse 참조).1858년, 데데킨트는 유리수의 데데킨드 컷의 관점에서 실수의 정의를 제안했는데, 이는 현대 [15]문헌에서 여전히 사용되고 있다.

게오르크 칸토르는 무한 집합론의 기본 개념을 개발했습니다.그의 초기 결과는 카디널리티 이론을 발전시켰고 실수와 자연수가 다른 [16]기수를 가지고 있다는 것을 증명했다.이후 20년 동안, 칸토르는 일련의 출판물에서 초한수 이론을 발전시켰다.1891년, 그는 대각선 인수를 도입한 실수의 셀 수 없다는 새로운 증거를 발표했고, 어떤 집합도 그것의 거듭제곱 집합과 같은 카디널리티를 가질 수 없다는 칸토어의 정리를 증명하기 위해 이 방법을 사용했습니다.칸토르는 모든 세트가 잘 정돈될 수 있다고 믿었지만, 이 결과에 대한 증거를 제시할 수 없었고,[17] 1895년에 미해결 문제로 남겨졌다.

20세기

20세기 초, 연구의 주요 분야는 정설과 형식 논리였다.비공식 집합론에서의 역설의 발견은 수학 자체가 일관성이 없는 것이 아닌지 의문을 갖게 했고, 일관성의 증거를 찾게 했다.

1900년에 힐버트는 다음 세기를 위한 23가지 문제에 대한 유명한 목록을 제출하였다.이 중 첫 번째 두 가지는 연속체 가설을 풀고 기초 산술의 일관성을 증명하는 것이었다. 그리고 열 번째는 정수에 대한 다변량 다항식 방정식이 해답을 가지고 있는지 여부를 결정할 수 있는 방법을 만드는 것이었다.이러한 문제들을 해결하기 위한 후속 연구는 1928년에 제기된 힐베르트의 "벤체이둥슈프로블럼" 문제를 해결하기 위한 노력과 같이 수학 논리의 방향을 형성했다.이 문제는 공식화된 수학적 문장이 주어질 때 그 문장이 참인지 거짓인지를 결정하는 절차를 요구했다.

이론과 패러독스를 설정하다

Ernst Zermelo는 모든 세트가 잘 정돈될 수 있다는 증거제시했고, 그 결과 Georg Cantor[18]얻을 수 없었다.그 증거를 얻기 위해, Zermelo는 선택 공리를 도입했는데, 이것은 수학자들과 집합론의 선구자들 사이에서 뜨거운 논쟁과 연구를 이끌어냈다.이 방법에 대한 즉각적인 비판은 체르멜로를 그의 결과에 대한 두 번째 설명을 발표하게 했고, 그의 [19]증거에 대한 비판에 직접적으로 대응했다.이 논문은 수학계의 선택 공리를 일반적으로 받아들이게 했다.

선택 공리에 대한 회의론은 최근 발견된 순진한 집합론의 역설에 의해 강화되었다.Cesare Burali-Forti[20] 역설을 처음으로 진술했다: Burali-Forti 역설은 모든 서수의 집합이 집합을 형성할 수 없다는 것을 보여준다.직후인 1901년 버트런드 러셀은 러셀의 역설발견했고 줄스 리차드는 리처드의 [21][full citation needed]역설을 발견했다.

체르멜로는 집합론에 [22]대한 첫 번째 공리를 제공했다.이러한 공리는 아브라함 프랭켈이 제안대체 공리와 함께, 현재 체르멜로-프랭켈 집합론(ZF)이라고 불립니다. 체르멜로의 공리는 러셀의 역설을 피하기 위해 크기 제한의 원리를 통합했습니다.

1910년, 러셀과 알프레드 노스 화이트헤드가 쓴 프린키피아 매스매티카 제1권이 출판되었다.이 중요한 연구는 러셀과 화이트헤드가 역설을 피하기 위해 개발한 완전한 형식적인 유형 이론의 틀에서 함수와 카디널리티의 이론을 발전시켰습니다.프린키피아 매스매티카는 비록 유형 이론의 틀이 [23]수학의 기초 이론으로 인기를 끌지는 못했지만, 20세기의 가장 영향력 있는 작품 중 하나로 여겨진다.

프랭클은[24] 선택 공리가 요소와 함께 체르멜로의 집합론의 공리로부터 증명될 수 없다는 것을 증명했다.Paul[25] Cohen의 이후 연구는 요소의 추가가 필요하지 않으며 ZF에서는 선택 공리를 증명할 수 없다는 것을 보여주었다.코헨의 증명은 강제 방법을 개발했고, 이것은 이제 집합론에서 [26]독립 결과를 확립하는 중요한 도구가 되었다.

기호논리

레오폴트 뢰벤하임[27] 토랄프[28] 스콜렘은 1차 논리가 무한 구조의 기수를 제어할 수 없다는 뢰벤하임-스콜렘 정리를 얻었다.스콜렘은 이 정리가 집합론의 1차 공식화에 적용될 것이며, 그러한 공식화는 수 있는 모델을 가지고 있음을 암시한다는 것을 깨달았다.이 반직관적인 사실은 스콜렘의 역설로 알려지게 되었다.

의 박사 논문에서, Kurt Gödel은 1차 [29]논리에서 구문과 의미론 사이의 대응관계를 확립하는 완전성 정리를 증명했다.괴델은 완전성 정리를 사용하여 콤팩트성 정리를 증명하고, 1차 논리적 결과의 완전성을 증명했습니다.이러한 결과는 수학자들이 사용하는 지배적인 논리로서 1차 논리를 확립하는 데 도움을 주었다.

1931년, 괴델은 충분히 강하고 효과적인 모든 1차 이론의 불완전성을 증명한 "공식적으로 결정할 수 없는 수학 원리관련 체계"를 출판했습니다.괴델의 불완전성 정리로 알려진 이 결과는 힐베르트의 프로그램에 강한 타격을 입히면서 수학의 공리적인 기초에 심각한 한계를 설정한다.그것은 산술의 공식 이론 내에서 산술의 일관성 증거를 제공하는 것의 불가능성을 보여주었다.그러나 [a]힐베르트는 한동안 불완전성 정리의 중요성을 인정하지 않았다.

괴델의 정리는 충분히 강하고 효과적인 공리 체계에 대한 일관성 증명은 시스템이 일관성이 있는 경우 시스템 자체에서도 얻을 수 없고 약한 시스템에서도 얻을 수 없다는 것을 보여준다.이것에 의해, 검토하는 시스템내에서 공식화할 수 없는 일관성 증명의 가능성이 열려 있습니다.겐젠은 유한 [30]귀납의 원리와 함께 피니티스트 시스템을 사용하여 산술의 일관성을 증명했다.겐젠의 결과는 증명 이론의 핵심 도구가 된 절단 제거증명 이론 서수 개념을 도입했다.괴델은 다른 일관성 증거를 제시했는데, 이것은 고전적인 산수의 일관성을 더 높은 유형의 [31]직관적인 산수의 일관성으로 감소시켰다.

평신도를 위한 상징 논리에 대한 첫 번째 교과서는 1896년 [32]이상한 나라의 앨리스의 저자 루이스 캐롤에 의해 쓰여졌다.

다른 지점의 시작

알프레드 타르스키모델 이론의 기초를 발전시켰다.

1935년부터 저명한 수학자들이 니콜라 부르바키라는 필명으로 협력하여 백과사전 수학 교과서 시리즈인 '에레앙스마테마티크'를 출판했습니다.엄숙하고 자명한 문체로 쓰여진 이 문서들은 엄격한 표현과 설정 이론의 기초를 강조했다.이러한 텍스트에 의해 만들어진 용어들, 예를 들어 사출, 주입, 그리고 사출과 같은 단어들과 사용된 텍스트들이 사용하는 집합 이론의 기초들은 수학 전반에 걸쳐 널리 채택되었다.

계산가능성의 연구는 재귀이론 또는 계산가능성 이론으로 알려지게 되었는데, 이는 괴델과 클리에네에 의한 초기 공식화가 [b]함수의 재귀적 정의에 의존했기 때문이다.이러한 정의가 튜링 기계를 포함하는 튜링의 공식화와 동등한 것으로 나타났을 때, 새로운 개념, 즉 계산 가능한 함수가 발견되었고, 이 정의는 수많은 독립적인 특성화를 허용할 만큼 충분히 강력하다는 것이 분명해졌다.1931년 불완전성 정리에 대한 그의 연구에서, 괴델은 효과적인 형식 체계에 대한 엄격한 개념이 부족했다; 그는 계산가능성의 새로운 정의가 이 목적을 위해 사용될 수 있다는 것을 즉시 깨달았고, 원래의 논문에서만 암시될 수 있는 일반성의 불완전성 정리를 진술할 수 있게 했다.

1940년대에 스티븐클린에밀 레온 포스트가 재귀 이론의 많은 결과를 얻었다.클린은[33] [34]튜링에 의해 암시된 상대적 계산가능성의 개념과 산술적 위계질서를 도입했다.클린은 나중에 재귀 이론을 고차 함수로 일반화했다.클라이네와 게오르크 크라이젤은 특히 증명 이론의 맥락에서 직관 수학의 정식 버전을 연구했습니다.

정식 논리 시스템

수학 논리는 본질적으로 형식 논리 시스템을 사용하여 표현되는 수학적 개념을 다룬다.이러한 시스템은 많은 세부 사항에서 다르지만 고정된 형식 언어의 표현만을 고려한다는 공통 속성을 공유합니다.명제논리1차논리의 체계는 수학의 기초에 적용가능성과 그들의 바람직한 증명 이론 [c]특성 때문에 오늘날 가장 널리 연구되고 있다.2차 논리나 무한 논리 같은 보다 강력한 고전 논리학, 직관적 논리 같은고전적 논리학도 연구된다.

1차 논리

1차 논리는 특정한 형식적인 논리 체계이다.그것의 구문은 잘 형성된 공식으로서 유한한 표현만을 포함하는 반면, 그것의 의미론들은 모든 수량화자들고정된 담론의 영역으로 제한되는 것을 특징으로 한다.

형식 논리의 초기 결과는 1차 논리의 한계를 설정했다.뢰벤하임-스콜렘 정리(1919)는 계산 가능한 1차 언어의 문장 집합이 무한 모델을 가지고 있다면, 각각의 무한 카디널리티의 적어도 하나의 모델을 가지고 있다는 것을 보여주었다.이것은 일련의 1차 공리가 자연수, 실수 또는 동형사상까지의 다른 무한 구조를 특징짓는 것은 불가능하다는 것을 보여준다.초기 기초 연구의 목표가 수학의 모든 부분에 대한 자명한 이론을 만드는 것이었기 때문에, 이러한 제한은 특히 극명했다.

괴델의 완전성 정리는 1차 [29]논리에서의 논리적 결과의 의미적 정의와 통사적 정의 사이의 동등성을 확립했다.그것은 특정 공리 집합을 만족시키는 모든 모델에서 특정 문장이 참이라면, 공리로부터 그 문장에 대한 유한한 추론이 있어야 한다는 것을 보여준다.콤팩트성 정리는 괴델의 완전성 정리에 대한 증명에서 보조정리로 처음 나타났고 논리학자들이 그 중요성을 파악하고 일상적으로 적용하기까지는 수년이 걸렸다.그것은 모든 유한 부분 집합이 모형을 가지고 있는 경우, 또는 다른 말로, 일관되지 않은 공식 집합이 유한하게 일관되지 않은 부분 집합을 가져야 하는 경우에만 문장의 집합이 모형을 가지고 있다고 말한다.완전성과 콤팩트성 정리는 1차 논리에서의 논리적 결과의 정교한 분석과 모델 이론의 발전을 가능하게 하며, 그것들은 수학에서 1차 논리가 두드러지는 중요한 이유이다.

괴델의 불완전성 이론은 1차 공리화에 [35]추가적인 한계를 설정한다. 번째 불완전성 정리는 산술을 해석할 수 있는 (아래에 정의되어 있는) 일관되고 효과적으로 주어진 논리 시스템에 대해, (자연수에 대해 그것이 유지된다는 의미에서는) 사실이지만 그 논리 시스템 에서 입증할 수 없는 진술이 존재한다고 말한다.논리 시스템과 일치할 수 있는 f 산술).를 들어, 페아노 공리를 표현할 수 있는 모든 논리 체계에서, 괴델 문장은 자연수를 유지하지만 증명할 수 없습니다.

여기서 논리체계는 시스템 언어의 어떤 공식이든 주어진다면 공리인지, 그리고 페아노 공리를 표현할 수 있는 것을 "충분히 강한" 것으로 결정될 수 있는지를 효과적으로 주어진다고 한다.1차 논리에 적용되었을 때, 첫 번째 불완전성 정리는 충분히 강하고, 일관되고, 효과적인 1차 이론이 뢰벤하임-스콜렘 정리에 의해 확립된 것보다 더 강한 한계인 기초적으로 동등하지 않은 모델을 가지고 있다는 것을 암시한다. 번째 불완전성 정리는 산술에 대한 충분히 강하고 일관되고 효과적인 공리 체계가 그 자체의 일관성을 증명할 수 없다는 것을 언급하고 있는데, 이것은 힐베르트의 프로그램이 도달할 수 없다는 것을 보여주는 것으로 해석되어 왔다.

기타 고전적 논리

1차 논리 외에 많은 논리를 연구한다.여기에는 무한한 양의 정보를 공식으로 제공할 수 있는 무한 논리학과 집합론의 일부를 의미론에 직접 포함하는 고차 논리학포함됩니다.

가장 잘 연구된 무한 로직은 1 , { \ L _ { \ } , \ obega 입니다.이 로직에서는 1차 로직과 같이 수량자는 유한한 깊이까지만 중첩될 수 있지만, 공식에는 유한 또는 셀 수 있는 무한 결합 및 분리가 포함될 수 있습니다.따라서 예를 들어 다음과 같은 L 1 , { \ L _ { \ _ {1 , \ 공식을 사용하여 객체가 정수라고 할 수 있습니다.

고차 논리는 담화 영역의 요소뿐만 아니라 담화 영역의 하위 집합, 그러한 하위 집합 집합 및 기타 상위 유형의 객체의 수량화를 허용한다.시멘틱스는 각 상위 유형 수량자에 대해 개별 도메인을 갖는 것이 아니라 수량자가 적절한 유형의 모든 개체로 범위를 지정하도록 정의됩니다.예를 들어 Frege의 논리와 같은 1차 논리의 개발 이전에 연구된 논리학은 유사한 집합 이론적인 측면을 가지고 있었다.고차 논리학은 자연수와 같은 구조의 완전한 공리화를 가능하게 하는 보다 표현적이지만, 그것들은 1차 논리로부터의 완전성과 콤팩트성 이론의 유추들을 만족시키지 못하기 때문에 증명 이론 분석에 덜 순하다.

또 다른 유형의 로직은 원시 재귀 함수에 대한 쓰기처럼 귀납적 정의를 허용하는 고정 소수점 로직입니다.

1차 로직의 확장을 공식적으로 정의할 수 있다. 즉, 1차 로직이 특정 기본적인 방법으로 1차 로직처럼 동작하기 때문에 이 대분의 모든 로직을 포괄하는 개념이지만, 일반적으로 모든 로직을 포괄하는 것은 아니다(예: 직관적, 모달 또는 퍼지 로직은 포함하지 않는다).

린드스트롬의 정리콤팩트성 정리와 하향 뢰벤하임-스콜렘 정리를 모두 만족시키는 1차 논리의 유일한 확장이 1차 논리라는 것을 의미한다.

비클래식 및 모달 논리

모달 로직에는 특정 공식이 참일 뿐만 아니라 반드시 참임을 나타내는 연산자와 같은 추가 모달 연산자가 포함됩니다.비록 모달 로직은 수학을 공리화하는데 자주 사용되지 않지만, 1차 증명[36] 가능성과 집합 이론 [37]강제력의 특성을 연구하는데 사용되어 왔다.

직관주의 논리는 브루어 자신이 형식화를 피했던 브루어의 직관주의 프로그램을 연구하기 위해 헤이팅에 의해 개발되었다.직관주의 논리는 특히 각 문장이 참이거나 부정이라는 배제의 중간 법칙을 포함하지 않는다.직관주의 논리의 증명 이론에 대한 클린의 연구는 건설적인 정보가 직관적인 증명으로부터 회복될 수 있다는 것을 보여주었다.예를 들어, 직관적 산술에서 입증 가능한 모든 함수는 계산 가능하다; 이것은 페아노 산술과 같은 산술의 고전 이론에서는 사실이 아니다.

대수 논리

대수적 논리는 형식 논리학의 의미론을 연구하기 위해 추상 대수학의 방법을 사용한다.기본적인 예는 고전 명제 논리에서 진실 값을 나타내기 위해 부울 대수를 사용하고 직관적 명제 논리에서 진실 값을 나타내기 위해 헤이팅 대수를 사용하는 것입니다.1차 논리와 고차 논리와 같은 더 강력한 논리는 원통형 대수와 같은 더 복잡한 대수 구조를 사용하여 연구된다.

집합론

집합론은 추상적인 사물들의 집합인 집합의 연구이다.서수와 기수와 같은 많은 기본 개념들은 집합론의 공식적인 공리화가 개발되기 전에 칸토어에 의해 비공식적으로 개발되었다.체르멜로 [22]때문에 그러한 첫 번째 공리화체르멜로-프랭켈 집합 이론(ZF)으로 약간 확장되었고, 이것은 현재 수학에서 가장 널리 사용되는 기초 이론이다.

집합론의 다른 공식화들은 폰 노이만-베네이스-를 포함하여 제안되었다.괴델 집합론(NBG), 모르스-켈리 집합론(MK) 및 새 기초(NF)입니다.이 중 ZF, NBG 및 MK는 집합의 누적 계층을 설명하는 것과 유사합니다.New Foundations는 다른 접근 방식을 취합니다. 즉, 집합 존재 공리에 대한 제한을 감수하면서 모든 집합의 집합과 같은 개체를 허용합니다.크립케-플레이트 집합론의 체계는 일반화된 재귀 이론과 밀접하게 관련되어 있다.

집합론에서 두 가지 유명한 진술은 선택 공리연속체 가설이다.Zermelo에 [18]의해 처음 언급된 선택 공리는 Fraenkel에 [24]의해 ZF와 무관하다는 것이 증명되었지만 수학자들에 의해 널리 받아들여지고 있다.빈 집합이 아닌 집합의 집합이 주어진 경우 집합의 각 집합에서 정확히 하나의 요소를 포함하는 단일 집합 C가 있음을 나타냅니다.집합 C는 집합의 각 집합에서 하나의 요소를 "선택"한다고 합니다.그러한 선택을 할 수 있는 능력은 명백하다고 생각되는 반면, 컬렉션의 각 집합은 비어 있지 않기 때문에 선택을 할 수 있는 일반적이고 구체적인 규칙의 결여는 공리를 비건설적으로 만든다.Stefan Banach와 Alfred Tarski는 선택 공리를 사용하여 고체 공을 유한한 개수의 조각으로 분해할 수 있으며, 그 조각은 스케일링 없이 재배열하여 원래 [38]크기의 고체 공 두 개를 만들 수 있다는 것을 보여주었다.바나흐-타르스키 역설로 알려진 이 정리는 선택 공리의 많은 반직관적인 결과 중 하나이다.

칸토르가 추측으로 처음 제안한 연속체 가설은 1900년 데이비드 힐버트에 의해 그의 23가지 문제 중 하나로 열거되었다.괴델은 연속체 가설이 존재해야 하는 집합론의 구성 가능한 우주를 개발함으로써 연속체 가설이 (선택 공리 유무에 관계없이) 체르멜로-프랭켈 집합론의 공리로부터 반증될 수 없다는 것을 보여주었다.1963년 폴 코헨은 연속체 가설이 체르멜로-프랭켈 집합론의 [25]공리로부터 증명될 수 없다는 것을 보여주었다.그러나 집합론에 대한 새로운 공리가 가설을 해결할 수 있을 가능성이 있기 때문에 이 독립성의 결과는 힐베르트의 질문을 완전히 해결하지는 못했다.W사는 최근 이러한 작업을 수행하고 있습니다. Hugh Woodin, 비록 그것의 중요성은 [39]아직 확실하지 않다.

집합론에서의 현대 연구는 큰 추기경의 연구결정론을 포함한다.대형 추기경은 ZFC에서 그러한 추기경의 존재를 증명할 수 없을 정도로 강한 특성을 가진 추기경 수이다.일반적으로 연구되는 가장 작은 대형 추기경의 존재는 이미 ZFC의 일관성을 암시한다.추기경들의 카디널리티가 매우 높음에도 불구하고, 그들의 존재는 실제 라인의 구조에 많은 영향을 끼친다.결정성(determinity)은 특정 2인용 게임에서 이길 수 있는 전략이 존재할 가능성을 말합니다(게임은 결정된다고 합니다).이러한 전략의 존재는 실선과 다른 폴란드 공간의 구조적 특성을 암시한다.

모델 이론

모델 이론은 다양한 형식 이론의 모델을 연구한다.여기서 이론은 특정한 형식 논리와 서명에 있는 공식들의 집합인 반면, 모형은 이론에 대한 구체적인 해석을 제공하는 구조이다.모델 이론은 보편 대수학과 대수 기하학과 밀접하게 관련되어 있지만, 모델 이론의 방법들은 그 분야들보다 논리적 고려에 더 초점을 맞춘다.

특정 이론의 모든 모델의 집합은 초등 클래스라고 불린다; 고전적 모델 이론은 특정 초등 클래스에서의 모델의 속성을 결정하거나 특정 구조의 클래스가 초등 클래스를 형성하는지 여부를 결정하려고 한다.

양자화 제거 방법은 특정 이론에서 정의 가능한 집합이 너무 복잡할 수 없다는 것을 보여주기 위해 사용될 수 있다.Tarski는 실폐장에 대한 양자화 소거를 확립하고, 그 결과 실수의 장 이론도 파악[40]수 있다.그는 또한 그의 방법들이 임의의 특성의 대수적으로 닫힌 분야에도 동일하게 적용된다고 언급했다.여기서 발전하는 현대의 서브필드는 o-minimal 구조와 관련이 있다.

마이클 D에 의해 증명된 몰리의 범주성 정리. 몰리는 만약 [41]카운터블 언어에서 1차 이론이 어떤 셀 수 없는 카디널리티에서 범주형이라면, 즉 이 카디널리티의 모든 모델이 동형이라면, 그것은 모든 셀 수 없는 기수에서 범주형이라고 말한다.

연속체 가설의 사소한 결과는 연속체보다 작은 다수의 비동형 계수 가능 모델을 가진 완전한 이론이 셀 수 있을 정도로 많은 것을 가질 수 있다는 것이다.Robert Lawson Vaught의 이름을 딴 Vaught의 추측은 연속체 가설과는 별개로 이것이 사실이라고 말한다.이 추측의 많은 특수한 사례가 확립되었다.

재귀 이론

계산 가능성 이론이라고도 불리는 재귀 이론은 계산 가능한 함수와 튜링 정도를 연구하는데, 계산 불가능한 함수를 동일한 수준의 계산 불능을 가진 집합으로 나눈다.재귀 이론은 또한 일반화된 계산 가능성과 정의 가능성의 연구를 포함한다.재귀 이론은 1930년대 로사 페테르, 알론조 교회, 앨런 튜링의 작품에서 발전했고, 1940년대 [42]클린과 포스트에 의해 크게 확장되었다.

고전적인 재귀 이론은 자연수에서 자연수에 이르는 함수의 계산 가능성에 초점을 맞추고 있다.기본 결과는 튜링 기계, δ 미적분 및 다른 시스템을 사용하여 수많은 독립적이고 동등한 특성화를 가진 강력한 계산 가능 함수의 표준 클래스를 확립합니다.더 발전된 결과는 튜링 차수의 구조와 재귀적으로 열거할 수 있는 집합의 격자에 관한 것이다.

일반화 재귀 이론은 재귀 이론의 개념을 더 이상 유한하지 않은 계산으로 확장합니다.그것은 높은 유형의 계산 가능성과 더불어 초산술 이론과 α-재귀 이론과 같은 분야의 연구를 포함한다.

재귀 이론의 현대 연구는 알고리즘 랜덤성, 계산 가능한 모델 이론, 그리고 역수학과 같은 응용 분야에 대한 연구와 순수 재귀 이론의 새로운 결과를 포함합니다.

알고리즘적으로 해결할 수 없는 문제

재귀 이론의 중요한 하위 분야는 알고리즘의 해결 불가능성을 연구합니다. 문제에 대한 모든 법적 입력에 대한 정답을 반환하는 가능한 계산 가능한 알고리즘이 없으면 결정 문제 또는 함수 문제는 알고리즘적으로 해결할 수 없습니다.1936년 처치와 튜링에 의해 독립적으로 얻어진 해결 불가능성에 대한 첫 번째 결과는 Eentscheidungsproblem이 알고리즘적으로 해결 불가능하다는 것을 보여주었다.튜링은 재귀 이론과 컴퓨터 과학 모두에서 광범위한 의미를 지닌 결과인 정지 문제의 해결 가능성을 확립함으로써 이것을 증명했다.

일반적인 수학에서 알 수 없는 문제의 예들이 많이 있다.그룹에 대한 문제라는 단어는 1955년 표트르 노비코프에 의해 알고리즘적으로 해결할 수 없다는 것이 증명되었고 1959년 W. Boone에 의해 독립적으로 증명되었다.1962년티보르 라도가 개발바쁜 비버 문제는 또 다른 잘 알려진 예입니다.

힐베르트의 열 번째 문제는 정수 계수를 갖는 다변량 다항식 방정식이 정수에 해를 가지고 있는지 여부를 결정하기 위한 알고리즘을 요구했습니다.줄리아 로빈슨, 마틴 데이비스, 힐러리 퍼트남의해 부분적으로 진전되었다.이 문제의 알고리즘적 해결 불가능성은 1970년 [43]유리 마티야세비치에 의해 증명되었다.

증명 이론과 구성 수학

증명 이론은 다양한 논리적 추론 체계에서 형식적인 증명에 대한 연구이다.이러한 증명은 형식적인 수학적 개체로 표현되며, 수학적 기법에 의한 분석을 용이하게 합니다.힐베르트식 연역 체계, 자연 연역 체계, 겐젠에 의해 개발된 순차 미적분을 포함한 여러 연역 체계가 일반적으로 고려된다.

수학 논리학의 맥락에서 건설적인 수학의 연구는 서술적 시스템의 연구뿐만 아니라 직관적 논리학과 같은 비고전적 논리학의 체계에 대한 연구를 포함한다.고전주의의 초기 주창자는 헤르만 바일이었는데, 그는 서술적 [44]방법만을 사용하여 실제 분석의 많은 부분을 발전시키는 것이 가능하다는 것을 보여주었다.

증명은 전적으로 미결적인 반면, 구조상의 진실은 그렇지 않기 때문에, 건설적인 수학에서의 연구는 증명 가능성을 강조하는 것이 일반적이다.고전적(또는 비건설적) 시스템의 입증 가능성과 직관적(또는 건설적) 시스템의 입증 가능성의 관계는 특히 중요합니다.Gödel-Gentzen 부정 번역과 같은 결과는 직관적인 논리에 고전적인 논리를 포함(또는 번역)할 수 있다는 것을 보여주며, 직관적인 증명에 대한 일부 특성이 고전적인 증명으로 다시 옮겨지는 것을 가능하게 한다.

증명 이론의 최근 발전은 Ulrich Kohlenbach의 증명 채광 연구와 Michael Rathjen의 증명 이론 서수 연구를 포함한다.

적용들

"수학 논리는 수학과 그 기초에만 성공적으로 적용된 것이 아닙니다(G. Frege, B). 러셀, D. Hilbert, P. Bernays, H. Scholz, R. Carnap, S. Lesniewski, T. S. S. S. S. Skolem.뿐만 아니라 물리학(R. Carnap, A.디트리히, BRussell, C. E. Shannon, A. N. Whitehead, H. Reichenbach, P. Fevrier, 생물학과(J. H. Woodger, A. Tarski), 심리학(F. B. Fitch, C. G. Hempel), 법과 도덕(K. Menger, U. Klug, P. Oppenheim)는 경제학(J. Neumann, O. Morgenstern), 실제 질문(E. C. Berkeley, E. Stamm), 그리고 형이상학(J. [Jan] Salamucha, H. Scholz, J. M. Bochenskinski)에까지.논리학의 역사에 대한 응용은 매우 유익하다는 것이 입증되었다(J. Lukasiewicz, H. Scholz, B. Mates, A).Becker, E. Moody, J. Salamucha, K.Duerr, Z.조던, P. 베이너, J. M. 보첸스키, S. [스타니슬로] T.셰이어, D. "[45]신학에도 응용되고 있습니다.Drewnowski, J. Salamucha, I.토마스)."[45]

컴퓨터 과학과의 관계

컴퓨터 공학에서 계산 가능성 이론의 연구는 수리 논리에서의 계산 가능성 연구와 밀접하게 관련되어 있다.하지만 강조의 차이는 있다.컴퓨터 과학자들은 종종 구체적인 프로그래밍 언어와 실현 가능한 계산 가능성에 초점을 맞추는 반면, 수리 논리학자들은 종종 이론적 개념으로서의 계산 가능성과 계산 불가능성에 초점을 맞춘다.

프로그래밍 언어의 의미론은 프로그램 검증(특히 모델 확인)과 마찬가지로 모델 이론과 관련이 있습니다.증명과 프로그램 사이의 Curry-Howard 대응증명 이론, 특히 직관적 논리와 관련이 있다.람다 미적분과 조합 논리와 같은 형식 계산은 이제 이상적인 프로그래밍 언어로 연구됩니다.

컴퓨터 공학은 또한 자동화된 정리 증명과 논리 프로그래밍같은 자동 확인 또는 심지어 증명의 발견을 위한 기술을 개발함으로써 수학에 기여한다.

기술 복잡도 이론은 논리학과 계산 복잡도를 관련짓습니다. 영역의 첫 번째 중요한 결과는, 페이긴의 정리(1974)가 NP가 존재론적인 2차 논리의 문장으로 표현 가능한 언어의 집합이라는 을 확립했다.

수학의 기초

19세기에 수학자들은 그들의 분야에서 논리적인 차이와 불일치를 인지하게 되었다.유클리드의 기하학 공리는 수세기 동안 공리적인 방법의 예로서 가르쳐져 온 것이 불완전하다는 것을 보여주었다.무한소수의 사용, 그리고 함수의 바로 그 정의가 분석에서 의문을 갖게 된 것은 바이얼스트래스의 어디에도 구별되지 않는 연속함수와 같은 병리학적 예가 발견되었기 때문이다.

칸토르의 임의 무한 집합 연구는 또한 비판을 받았다.레오폴드 크로네커는 수학에서 유한하고 구체적인 사물에 대한 연구로의 복귀를 지지하며 "이 정수를 만들었다; 다른 모든 것은 인간의 일이다"라고 유명한 말을 했습니다.비록 크로네커의 주장은 20세기에 구성주의자들에 의해 추진되었지만, 수학계는 전체적으로 그것들을 거부했다.데이비드 힐버트는 "칸토르가 창조한 천국에서 우리를 쫓아낼 사람은 아무도 없다"며 무한에 대한 연구를 지지했다.

수학자들은 수학의 많은 부분을 공식화하기 위해 사용될 수 있는 공리 체계를 찾기 시작했다.함수와 같은 이전의 순진한 용어에서 모호성을 제거하는 것 외에, 이 공리화가 일관성 증명을 가능하게 할 것으로 기대되었다.19세기에 일련의 공리들의 일관성을 증명하는 주요 방법은 그것에 대한 모형을 제공하는 것이었다.따라서, 예를 들어, 비유클리드 기하학은 고정된 구상의 점을 의미하고 구상의 큰 원을 의미하도록 점을 정의함으로써 일관성을 증명할 수 있다.타원 기하학의 모델인 결과 구조는 평행 공식을 제외한 평면 기하학의 공리를 충족합니다.

형식논리의 발달로 힐버트는 공리체계가 일관성이 있다는 것을 증명하는 것이 가능한지 물었다.이 분석을 통해 모순을 증명하는 것은 불가능하다는 것을 보여준다.이 생각은 증명 이론의 연구로 이어졌다.게다가 힐버트는 분석을 전적으로 구체화해야 한다고 제안했는데, 이는 그가 허용하지만 정확하게 정의하지는 않는 방법을 언급하기 위해 결백하다는 용어를 사용했다.힐베르트 프로그램으로 알려진 이 프로젝트는 괴델의 불완전성 이론들에 의해 심각하게 영향을 받았는데, 이것은 산술의 형식 이론의 일관성이 그 이론들에서 공식화할 수 있는 방법들을 사용하여 확립될 수 없다는 것을 보여준다.겐젠은 초한유도의 공리로 보강된 피니터리 시스템에서 산술의 일관성에 대한 증거를 만드는 것이 가능하다는 것을 보여주었고, 그렇게 하기 위해 그가 개발한 기술은 증명 이론에서 중요한 것이었다.

수학 기초의 역사에서 두 번째 줄거리는 비고전 논리와 건설적인 수학을 포함한다.건설적인 수학의 연구는 건설적인 것의 다양한 정의를 가진 많은 다른 프로그램들을 포함한다.ZF 집합론에서 선택 공리를 사용하지 않는 증명은 많은 수학자들에 의해 건설적이라고 불립니다.더 제한된 버전의 구성주의는 자연수, 숫자이론 함수, 그리고 자연수의 집합으로 스스로제한한다.일반적인 생각은 함수의 값을 계산하는 구체적인 방법을 알고 있어야 함수가 존재한다고 말할 수 있다는 것입니다.

20세기 초에, Luitzen Egbertus Jan Brower는 수학 철학의 한 부분으로 직관주의를 창시했습니다.처음에는 잘 이해되지 않았던 이 철학은 수학자에게 수학적 진술이 진실되기 위해서는 그 진술이 진실을 믿을 뿐만 아니라 그 진실의 이유를 이해할 수 있는 직관적인 능력이 있어야 한다고 말했다.이 진실의 정의의 결과는 배제된 중간의 법칙을 거부한 것이다.Brower에 따르면, 그들의 부정 또한 진실이라고 주장될 수 없는 진술들이 있기 때문이다.브루어의 철학은 영향력이 있었고, 저명한 수학자들 사이에 격렬한 논쟁을 불러일으켰다.나중에 클라이네와 크라이셀은 직감적 논리의 정형화된 버전을 연구했다.BHK 해석크립케 모형의 등장으로 직관주의는 고전 수학과 조화되기 쉬워졌다.

「 」를 참조해 주세요.

메모들

  1. ^ 1934년판 '그룬드라겐 데르 매틱'의 서문에서 버네이는 러셀의 역설에 대해 들었을 때 프레게의 유명한 노트를 떠올리게 하는 다음과 같이 썼다.

    "Die Ausführung hat eine besentliche Verzögerung daduch erfahren, daß da in erfahren, einem Stadium, da in di die die Darstellung shon ihrem Abschu na nahe nahe durch derbrand von Arbiten von am von am von im Gédel im Gerrédern Vern Vern Vern Vern im Gern imerDabei is der Umfang des Buches angewachsen, 그래서 Zwei Bénde angeigt erschien의 da'eine Teilung.

    번역:

    "이 계획을 실행하는 것은 (수학적 논리학을 위한 증명 이론에 대한 박람회를 위해 힐버트에 의한) 필수적인 지연을 경험했습니다. 왜냐하면, 그 설명이 이미 결론에 가까워진 단계에서, 헤르브란트와 괴델의 작품 출현으로 인해 증명 이론 영역에 변화된 상황이 발생했기 때문입니다.e 새로운 통찰력에 대한 고려.그래서 이 책의 범위가 넓어졌기 때문에 두 권으로 나누어 보는 것이 좋을 것 같습니다.

    그래서 확실히 힐베르트는 1934년까지 괴델의 일의 중요성을 알고 있었다.1939년 제2권은 산술에 대한 겐젠의 일관성 증명 형식을 포함했다.
  2. ^ 이 용어에 대한 자세한 연구는 Soare 1996에 의해 제공되었습니다.
  3. ^ Ferreiros 2001은 20세기 초에 다른 공식 논리에 비해 1차 논리의 발달을 조사했습니다.

레퍼런스

  1. ^ Barwise(1989년.
  2. ^ "Computability Theory and Foundations of Mathematics / February, 17th – 20th, 2014 / Tokyo Institute of Technology, Tokyo, Japan" (PDF).
  3. ^ Ferreiros(2001), 페이지 443.
  4. ^ 보첸스키(1959), 0.1장, 페이지 1
  5. ^ Swineshead(1498)
  6. ^ 베이너(1950), 페이지 14.
  7. ^ Katz(1998), 페이지 686.
  8. ^ 페아노(1889년).
  9. ^ 데데킨트(1888년).
  10. ^ Katz(1998), 페이지 774.
  11. ^ 로바체프스키(1840).
  12. ^ 힐버트(1899년).
  13. ^ 패쉬(1882년).
  14. ^ Felscher(2000).
  15. ^ 데데킨트(1872년).
  16. ^ 칸토르(1874년).
  17. ^ Katz(1998), 페이지 807.
  18. ^ a b 체르멜로(1904년.
  19. ^ 체르멜로(1908a).
  20. ^ Burali-Forti(1897).
  21. ^ 리처드(1905).
  22. ^ a b 체르멜로(1908b).
  23. ^ 페레이로스(2001), 페이지 445.
  24. ^ a b Fraenkel (1922).
  25. ^ a b 코헨(1966년).
  26. ^ Cohen 2008 도 참조해 주세요.
  27. ^ 뢰벤하임(1915).
  28. ^ 스콜렘(1920).
  29. ^ a b 괴델(1929)
  30. ^ 겐젠(1936년).
  31. ^ 괴델(1958)
  32. ^ 캐럴(1896년).
  33. ^ 클린(1943년).
  34. ^ 튜링(1939).
  35. ^ 괴델(1931년).
  36. ^ 솔로베이(1976년).
  37. ^ Hamkins & Löwe (2007)
  38. ^ Banach & Tarski(1924).
  39. ^ 우딘(2001년).
  40. ^ 타르스키(1948).
  41. ^ 몰리(1965).
  42. ^ Soare(2011).
  43. ^ 데이비스(1973년).
  44. ^ 와일 1918년
  45. ^ a b 보첸스키(1959), 0.3장, 페이지 2

학부 교재

졸업 교재

연구 논문, 논문, 텍스트, 설문 조사

고전 논문, 텍스트 및 컬렉션

Bochenski, Jozef Maria, ed. (1959). A Precis of Mathematical Logic. Synthese Library, Vol. 1. Translated by Otto Bird. Dordrecht: Springer. doi:10.1007/978-94-017-0592-9. ISBN 9789048183296.

Cantor, Georg (1874). "Ueber eine Eigenschaft des Inbegriffes aller reellen algebraischen Zahlen" (PDF). Journal für die Reine und Angewandte Mathematik. 1874 (77): 258–262. doi:10.1515/crll.1874.77.258. S2CID 199545885. Carroll, Lewis (1896). Symbolic Logic. Kessinger Legacy Reprints. ISBN 9781163444955.

Soare, Robert Irving (22 December 2011). "Computability Theory and Applications: The Art of Classical Computability" (PDF). Department of Mathematics. University of Chicago. Retrieved 23 August 2017. Swineshead, Richard (1498). Calculationes Suiseth Anglici (in Lithuanian). Papie: Per Franciscum Gyrardengum.

외부 링크