Jump to content

Mathematical logic

This is a fully translated article. Click here for more information.
From DawoumWiki, the free Mathematics self-learning
Original article: w:Mathematical logic
For Quine's theory sometimes called "Mathematical Logic", see New Foundations. For other uses, see Logic (disambiguation).
Part of a series on
Mathematics
Areas
Relationship with sciences
Mathematics Portal

수학적 논리(Mathematical logic)는 수학 내의 형식적 논리(formal logic)에 대한 연구입니다. 주요 하위 영역에는 모델 이론(model theory), 증명 이론(proof theory), 집합 이론(set theory), 및 재귀 이론(recursion theory, 계산 가능성 이론이라고도 알려져 있음)이 포함됩니다. 수학적 논리에서 연구는 공통적으로 표현력이나 연역력과 같은 논리의 형식적 시스템의 수학적 속성을 다룹니다. 어쨌든, 그것은 역시 올바른 수학적 추론을 특성화하거나 수학의 토대(foundations of mathematics)를 확립하기 위해 논리의 사용을 포함할 수 있습니다.

처음부터, 수학적 논리는 수학의 토대의 연구에 기여하고 동기를 부여해 왔습니다. 이 연구는 19세기 후반 기하학(geometry), 산술(arithmetic), 및 해석학(analysis)에 대한 공리적(axiomatic) 프레임워크의 개발과 함께 시작되었습니다. 20세기 초에서, 그것은 토대적 이론의 일관성을 입증하기 위한 다비트 힐베르트(David Hilbert)의 프로그램에 의해 형성되었습니다. 쿠르트 괴델(Kurt Gödel), 게르하르트 겐첸(Gerhard Gentzen), 및 다른 사람들의 결과는 그 프로그램에 대한 부분적인 해결책을 제공하고, 일관성 입증과 관련된 문제를 명확히 했습니다. 집합 이론에서 연구는 집합 이론에 대한 공통 공리 시스템에서 입증될 수 없는 몇 가지 정리가 있을지라도 거의 모든 보통의 수학이 집합의 관점에서 형식화될 수 있음을 보여주었습니다. 수학의 토대에서 현대적 연구는 모든 수학이 발전될 수 있는 이론을 찾으려고 노력하기보다는 (역 수학에서와 같이) 수학의 어떤 부분이 특정 형식적 시스템에서 형식화될 수 있는지를 확립하는 데 초점을 맞추는 경우가 많습니다.

Subfields and scope

1977년에 나온 수학적 논리 핸드북(Handbook of Mathematical Logic[1])은 현대 수학적 논리를 대략적으로 네 가지 영역으로 분류합니다:

  1. 집합 이론(set theory)
  2. 모델 이론(model theory)
  3. 재귀 이론(recursion theory), 및
  4. 증명 이론(proof theory)과 구성적 수학(constructive mathematics) (단일 영역의 일부로 고려됨).

추가적으로, 때로는 계산 복잡도 이론(computational complexity theory)의 분야도 수학적 논리의 일부로 포함됩니다.[2] 많은 기술과 결과가 여러 영역에서 공유되지만 각 영역에는 뚜렷한 초점이 있습니다. 이러한 분야 사이의 경계선, 및 수학적 논리와 기타 수학 분야를 구분하는 선이 항상 뚜렷한 것은 아닙니다. 괴델의 불완전성 정리(Gödel's incompleteness theorem)는 재귀 이론과 증명 이론의 이정표일 뿐만 아니라, 양상 논리에서 뢰브의 정리(Löb's theorem)로 이어져 왔습니다. 강제(forcing)의 방법은 집합 이론, 모델 이론, 및 재귀 이론은 물론 직관주의 수학 연구에도 사용됩니다.

카테고리 이론의 수학적 분야는 많은 형식적인 공리적 방법을 사용하고, 카테고리적 논리학에 대한 연구를 포함하지만, 카테고리 이론은 보통 수학적 논리의 하위 분야로 고려되지 않습니다. 다양한 수학 분야에서의 적용 가능성 때문에, 손더스 맥 레인(Saunders Mac Lan)을 비롯한 수학자들은 집합 이론과 별개로 수학에 대한 토대적 시스템으로 카테고리 이론을 제안해 왔습니다. 이들 토대는 고전적 또는 비고전적 논리를 사용할 수 있는 집합 이론의 일반화된 모델과 닮은 토포스(toposes)를 사용합니다.

History

수학적 논리는 19세기-중반 수학의 하위 분야로 등장했으며, 이는 형식적인 철학적 논리와 수학이라는 두 전통의 융합을 반영합니다.[3] '기호 논리학의(logistic)', '기호 논리(symbolic logic)', '논리의 대수(algebra of logic)', 및, 보다 최근에는, 간단히 '형식적 논리(formal logic)'라고도 불리는 수학적 논리는 지난 19세기에 인위적인 표기법과 엄격한 연역법의 도움을 받아 정교화된 논리 이론의 집합입니다."[4] 이러한 출현 이전에는, 수사학(rhetoric), 계산(calculationes),[5] 삼단논법(syllogism)을 통해, 및 철학(philosophy)과 함께 논리학을 연구했습니다. 20세기 전반에는 수학의 토대에 걸쳐 활발한 논쟁과 함께 근본적인 결과가 폭발적으로 증가했습니다.

Early history

Further information: History of logic

논리학의 이론은 중국, 인도, 그리스, 및 이슬람 세계를 포함하여 역사상 여러 문화권에서 발전했습니다. 그리스 방법, 특히 오르가논(Organon)에서 발견된 것처럼 아리스토텔레스 논리학(Aristotelian logic, 또는 용어 논리)은 수천 년 동안 서양 과학과 수학에서 폭넓게 적용되고 수용되었습니다.[6] 스토아 학파(Stoics), 특히 크리시포스(Chrysippus)는 술어 논리(predicate logic)의 개발을 시작했습니다. 18세기 유럽에서, 라이프니츠(Leibniz)와 램버트(Lambert)를 포함한 철학적 수학자들에 의해 형식적 논리의 연산을 기호적 또는 대수적 방법으로 다루려는 시도가 있어 왔지만, 그들의 작업은 고립되게 남겨지고 거의 알려지지 않았습니다.

19th century

19세기 중반에서, 조지 부울(George Boole)과 그 뒤에 오거스터스 드 모르간(Augustus De Morgan)은 논리학에 대한 시스템적인 수학적 처리를 제시했습니다. 조지 피콕(George Peacock)과 같은 대수학자들에 의한 연구를 기반으로 한 그들의 연구는 전통적인 아리스토텔레스 논리학 교리를 수학의 토대(foundations of mathematics) 연구를 위한 충분한 프레임워크로 확장했습니다.[7] 1847년에, 바트로슬라프 베르티치(Vatroslav Bertić)는 부울과 독립적으로 논리의 대수화에 관해 상당한 연구를 수행했습니다.[8] 찰스 샌더스 퍼스(Charles Sanders Peirce)는 나중에 부울의 연구를 기반으로 관계 및 한정어에 대한 논리적 시스템을 개발했으며, 이를 1870년부터 1885년까지 여러 논문에 발표했습니다.

고틀롭 프레게(Gottlob Frege)는 1879년에 출판된 그의 Begriffsschrift에서 한정어와 함께 논리학의 독립적인 발전을 제시했으며, 이 작품은 일반적으로 논리학 역사에서 전환점을 표시한 것으로 여겨집니다. 어쨌든, 프레게의 연구는 세기가 바뀔 무렵 버트런드 러셀(Bertrand Russell)이 이 연구를 홍보하기 시작할 때까지 알려지지 않았습니다. 프레게가 개발한 2차원 표기법은 결코 널리 채택되지 않았고 현대 텍스트에서는 사용되지 않습니다.

1890년부터 1905년까지 에른스트 슈뢰더(Ernst Schröder)는 Vorlesungen über die Algebra der Logik을 3권으로 출판했습니다. 이 연구는 부울, 드 모르간, 퍼스의 연구를 요약하고 확장했고, 19세기 말에 이해된 기호 논리학에 대한 포괄적인 참고 자료였습니다.

Foundational theories

수학이 적절한 토대 위에 구축되지 않았다는 우려로 인해 산술, 해석학, 및 기하학과 같은 수학의 토대적 영역에 대한 공리적 시스템이 개발되었습니다.

논리학에서 산술(arithmetic)이라는 용어는 자연수의 이론을 의미합니다. 주세페 페아노(Giuseppe Peano)는 부울과 슈뢰더의 논리적 시스템의 변형을 사용하지만 한정어를 추가하여 자신의 이름을 지니게 되는 산술에 대한 공리의 집합 (페아노 공리)를 출판했습니다.[9] 페아노는 당시 프레게의 연구를 알지 못했습니다. 비슷한 시기에 리하르트 데데킨트(Richard Dedekind)는 자연수가 그것들의 귀납법 속성에 의해 고유하게 특징짓는다는 것을 보여주었습니다. 데데킨트는 페아노의 공리의 형식적 논리적 특성이 부족한 다른 특성화를 제안했습니다.[10] 어쨌든, 데데킨트의 연구는 (동형까지) 자연수의 집합의 고유성과 다음수 함수( successor function)와 수학적 귀납법에서 나오는 덧셈과 곱셈의 재귀적 정의를 포함하여 페아노의 시스템에서 접근할 수 없는 정리를 입증했습니다.

19세기 중반에서, 기하학에 대한 유클리드의 공리에서 결함이 알려지게 되었습니다.[11] 1826년 니콜라이 로바쳅스키(Nikolai Lobachevsky)에 의해 확립된 평행 공준(parallel postulate)의 독립성 외에도,[12] 수학자들은 유클리드가 당연하게 여겼던 특정 정리가 실제로는 그의 공리로부터 입증될 수 없다는 사실을 발견했습니다. 그 중에는 직선이 적어도 두 개의 점을 포함하거나, 중심이 해당 반지름으로 분리되어 있는 같은 반지름의 원이 교차해야 한다는 정리가 있습니다. 힐베르트는 파쉬(Pasch)의 이전 연구를 기반으로 기하학에 대한 공리(axioms for geometry)의 완전한 집합을 개발했습니다.[13][14] 기하학을 공리화하는 것에서 성공은 힐베르트가 자연수 및 실수 직선(real line)과 같은 수학의 다른 영역에 대한 완전한 공리화를 추구하도록 동기를 부여했습니다. 이것은 20세기 전반기의 주요 연구 분야임이 입증되었습니다.

19세기에는 함수의 수렴 이론과 푸리에 급수 이론을 포함하여 실수 해석(real analysis) 이론이 크게 발전했습니다. 카를 바이어슈트라스(Karl Weierstrass)와 같은 수학자들은 모든 곳에서 미분-불가능한 연속 함수와 같이 직관을 확장하는 함수를 구성하기 시작했습니다. 계산에 대한 규칙으로서의 함수, 또는 매끄러운 그래프에 대한 이전 개념은 더 이상 적합하지 않았습니다. 바이어슈트라스는 자연수의 속성을 사용하여 해석학을 공리화하려고 추구했던 해석학의 산술화(arithmetization of analysis)를 옹호하기 시작했습니다. 현대의 극한의 (ε, δ)-정의와 연속 함수의 정의는 이미 1817년 볼차노(Bolzano)에 의해 개발되었지만,[15] 상대적으로 알려지지 않고 남아 있었습니다. 코시(Cauchy)는 1821년에 무한소(infinitesimals)의 관점에서 연속성을 정의했습니다 (Cours d'Analyse, 34페이지 참조). 1858년에, 데데킨트는 유리수에 대한 데데킨트 자름(Dedekind cuts)의 관점에서 실수의 정의를 제안했으며, 이 정의는 현대 텍스트에서 여전히 사용됩니다.[16]

게오르크 칸토어(Georg Cantor)는 무한 집합 이론의 토대적인 개념을 개발했습니다. 그의 초기 결과는 카디널리티(cardinality)의 이론을 발전시켰고 실수와 자연수는 서로 다른 카디널리티를 가지고 있음을 입증했습니다.[17] 그 후 20년 동안, 칸토어는 일련의 출판물을 통해 초월유한 숫자(transfinite numbers)의 이론을 개발했습니다. 1891년에, 그는 대각선 논증(diagonal argument)을 도입한 실수의 셀 수 없음에 대한 새로운 증명을 발표했고, 이 방법을 사용하여 어떤 집합도 그것의 거듭제곱-집합(powerset)과 같은 카디널리티를 가질 수 없다는 칸토어의 정리(Cantor's theorem)를 입증했습니다. 칸토어는 모든 각 집합이 바른-순서화(well-ordered)될 수 있다고 믿었지만, 이 결과에 대한 증명을 제시할 수 없어, 1895년에 열린 문제로 남겨졌습니다.[18]

20th century

20세기 초반에서, 집합 이론과 형식적 논리가 주요 연구 분야였습니다. 비형식적 집합 이론에서 역설이 발견되면서 일부 사람들은 수학 자체가 일관성이 없는지 궁금해하고, 일관성의 증명을 찾게 되었습니다.

1900년에서, 힐베르트(Hilbert)는 다음 세기를 위한 23가지 문제의 유명한 목록을 제시했습니다. 이들 중 처음 두 가지는 각각 연속체 가설(continuum hypothesis)을 해결하고 기초 산술의 일관성을 입증하는 것이었습니다; 열 번째는 정수에 걸쳐 다변수 다항 방정식이 해를 가지는지 여부를 결정할 수 있는 방법을 만드는 것이었습니다. 이들 문제를 해결하기 위한 후속 연구는 1928년에 제기된 힐베르트의 Entscheidungsproblem을 해결하려는 노력과 마찬가지로 수학적 논리의 방향을 형성했습니다. 이 문제는 형식화된 수학적 명제가 주어졌을 때, 그 명제가 참인지 거짓인지를 결정하는 절차를 요구했습니다.

Set theory and paradoxes

에른스트 체르멜로(Ernst Zermelo)는 모든 각 집합이 바른-순서화될 수 있다는 증명을 제공했으며, 게오르크 칸토어(Georg Cantor)는 얻을 수 없었던 결과를 제공했습니다.[19] 그 증명을 달성하기 위해, 체르멜로는 선택의 공리(axiom of choice)를 도입했으며, 이는 수학자와 집합 이론의 선구자들 사이에서 열띤 논쟁과 연구를 불러일으켰습니다. 그 방법에 대한 즉각적인 비판으로 인해 체르멜로는 자신의 증명에 대한 비판을 직접적으로 다루면서 그의 결과에 대한 두 번째 설명을 출판하게 되었습니다.[20] 이 논문은 수학 공동체에서 선택의 공리의 일반적인 수용으로 이어졌습니다.

선택의 공리에 대한 회의론은 최근 발견된 소박한 집합 이론(naive set theory)의 역설에 의해 강화되었습니다. 체사레 부랄리-포르티(Cesare Burali-Forti)는 역설을 처음으로 언급했습니다:[21] 부랄리-포르티 역설(Burali-Forti paradox)은 모든 순서 숫자(ordinal numbers)의 모음이 집합을 형성할 수 없음을 보여줍니다. 그로부터 얼마 지나지 않아, 1901년에 버트런드 러셀(Bertrand Russell)이 러셀의 역설(Russell's paradox)을 발견했고, 줄스 리처드(Jules Richard)가 리처드의 역설(Richard's paradox)을 발견했습니다.[22]

체르멜로는 집합 이론에 대한 공리의 첫 번째 집합을 제공했습니다.[23] 이들 공리는, 아브라함 프렝켈(Abraham Fraenkel)에 의해 제안된 추가적인 대체의 공리(axiom of replacement)와 함께, 현재 체르멜로-프렝켈 집합 이론(Zermelo–Fraenkel set theory, ZF)이라고 합니다. 체르멜로의 공리는 러셀의 역설을 피하기 위해 크기 제한(limitation of size)의 원리를 통합했습니다.

1910년에, 러셀과 알프레드 노스 화이트헤드(Alfred North Whitehead)에 의해 쓰인 Principia Mathematica의 첫 권이 출판되었습니다. 이 중요한 연구는 역설을 피하기 위한 노력으로 러셀과 화이트헤드가 개발한 완전히 형식적인 유형 이론(type theory)의 프레임워크에서 함수와 카디널리티의 이론을 발전시켰습니다. Principia Mathematica는 20세기 가장 영향력 있는 저서 중 하나로 여겨지지만, 유형 이론의 프레임워크는 수학에 대한 토대적 이론으로 대중화되지는 못했습니다.[24]

프렝켈은 선택의 공리가 원시-원소(urelements)를 갖는 체르멜로의 집합 이론의 공리로부터 입증될 수 없음을 입증했습니다.[25] 나중에 폴 코언(Paul Cohen)에 의한 연구는 원시-원소의 추가가 필요하지 않고, 선택의 공리는 ZF에서 증명할 수 없음을 보여주었습니다.[26] 코언의 증명은 강제(forcing)의 방법을 개발했으며, 이는 이제 집합 이론에서 독립성 결과(independence results)를 확립하는 데 중요한 도구입니다.[27]

Symbolic logic

레오폴드 뢰벤하임(Leopold Löwenheim)과[28] 토랄프 스콜렘(Thoralf Skolem)은[29] 일-차 논리(first-order logic)가 무한 구조의 카디널리티를 제어할 수 없다고 말하는 뢰벤하임-스콜렘 정리(Löwenheim–Skolem theorem)를 얻었습니다. 스콜렘은 이 정리가 집합 이론의 일-차 형식화에 적용될 것이고, 임의의 그러한 형식화에는 셀-수-있는 모델(model)이 있다는 것을 의미한다는 것을 깨달았습니다. 이 직관에 반하는 사실은 스콜렘의 역설(Skolem's paradox)로 알려지게 됩니다.

쿠르트 괴델(Kurt Gödel)은 박사 학위 논문에서 1-차 논리에서 구문론과 의미론 사이의 대응 관계를 확립하는 완전성 정리(completeness theorem)를 입증했습니다.[30] 괴델은 완전성 정리를 사용하여 컴팩트성 정리(compactness theorem)를 입증하고, 1-차 논리적 결과(logical consequence)의 유한-항 본성을 입증했습니다. 이들 결과는 수학자들에 의해 사용되는 지배적인 논리로서 1-차 논리를 확립하는 데 도움이 되었습니다.

1931년에, 괴델은 충분히 강력하고 효과적인 모든 1-차 이론의 (단어의 다른 의미에서) 불완전성을 입증했든 On Formally Undecidable Propositions of Principia Mathematica and Related Systems를 출판했습니다. 괴델의 불완전성 정리(Gödel's incompleteness theorem)로 알려진 이 결과는 수학의 공리적 토대에 심각한 제한을 설정하여, 힐베르트의 프로그램에 큰 타격을 입혔습니다. 그것은 산술의 임의의 형식적 이론 내에서 산술의 일관성 증명을 제공하는 것이 불가능함을 보여주었습니다. 어쨌든, 힐베르트는 한동안 불완전성 정리의 중요성을 인정하지 않았습니다.[a]

괴델의 정리는 임의의 충분히 강력하고 효과적인 공리 시스템에 대한 일관성(consistency) 증명이 시스템 자체에서 얻어질 수 없다, 만약 그 시스템이 일관되어 있으면, 어떤 약한 시스템에서도 얻을 수 없다는 것을 보여줍니다. 이로 인해 고려하는 시스템 내에서 형식화될 수 없는 일관성 증명의 가능성이 열려 있습니다. 겐첸(Gentzen)은 초월유한 귀납법(transfinite induction)의 원리와 함께 유한주의적인 시스템을 사용하여 산술의 일관성을 입증했습니다.[31] 겐첸의 결과는 증명 이론에서 핵심 도구가 된 자름 제거(cut elimination)와 증명-이론적 순서-숫자(proof-theoretic ordinals)의 아이디어를 도입했습니다. 괴델은 고전 산술의 일관성을 더 높은 유형에서 직관주의적 산술의 일관성으로 축소하는 다른 일관성 증명을 제시했습니다.[32]

일반인을 위한 기호 논리학에 관한 최초의 텍스트는 이상한 나라의 앨리스(Alice in Wonderland)의 저자 루이스 캐롤에 의해 1896년에 집필되었습니다.[33]

Beginnings of the other branches

알프레트 타르스키(Alfred Tarski)는 모델 이론(model theory)의 기초를 개발했습니다.

1935년부터 시작하여, 저명한 수학자의 그룹이 니콜라 부르바키(Nicolas Bourbaki)라는 가명으로 협력하여, 백과사전적인 수학 교과서 시리즈, Éléments de mathématique를 출판했습니다. 엄격하고 공리적인 스타일로 쓰인 이 텍스트는 엄격한 표현과 집합-이론적 토대를 강조했습니다. 전단사, 단사, 및 전사(bijection, injection, and surjection)와 같은 이들 텍스트에 의해 만들어진 용어와 텍스트에서 사용된 집합-이론적 토대는 수학 전반에 걸쳐 널리 채택되었습니다.

계산 가능성에 대한 연구는 재귀 이론 또는 계산-가능성 이론(computability theory)으로 알려지게 되는데, 왜냐하면 괴델과 클레이니에 의한 초기 형식화는 함수의 재귀적 정의에 의존했기 때문입니다.[b] 이들 정의가 튜링 기계(Turing machines)를 포함하는 튜링의 형식화와 동등한 것으로 나타났을 때, 새로운 개념 – 계산 가능한 함수(computable function) – 이 발견되었고, 이 정의가 수많은 독립적인 특성화를 허용할 만큼 충분히 견고하다는 것이 분명해졌습니다. 1931년 불완전성 정리에 관한 그의 연구에서, 괴델은 효과적인 형식적 시스템에 대한 엄격한 개념이 부족했습니다; 그는 계산 가능성의 새로운 정의가 이러한 목적으로 사용될 수 있다는 것을 즉시 깨달았고, 이를 통해 원래 논문에만 암시될 수 있었던 불완전성 정리를 일반적으로 기술할 수 있게 되었습니다.

재귀 이론에서 수많은 결과는 1940년대 스티븐 콜 클레이니(Stephen Cole Kleene)와 에밀 레온 포스트(Emil Leon Post)에 의해 얻어졌습니다. 클레이니는[34] 투링이 예시한 상대적 계산 가능성의 개념과[35] 산술 계층 구조(arithmetical hierarchy)를 도입했습니다. 클레이니는 나중에 재귀 이론을 고차 함수형으로 일반화했습니다. 클레이니와 게오르크 카이즐(Georg Kreisel)은 특히 증명 이론의 맥락에서 직관주의 수학의 형식적 버전을 연구했습니다.

Formal logical systems

핵심 부분에서, 수학적 논리는 형식적 논리 시스템(formal logical systems)을 사용하여 표현된 수학적 개념을 다룹니다. 이들 시스템은, 많은 세부 사항에서 다르지만, 고정된 형식적 언어(formal language)의 표현만 고려한다는 공통 속성을 공유합니다. 명제 논리(propositional logic)와 1-차 논리(first-order logic)의 시스템은 수학의 토대(foundations of mathematics)에 대한 적용-가능성과 바람직한 증명-이론적 속성으로 인해 오늘날 가장 널리 연구되고 있습니다.[c] 직관 논리(intuitionistic logic)와 같은 비고전적 논리(Non-classical logics)와 함께 2-차 논리(second-order logic) 또는 무한-항 논리(infinitary logic)와 같은 보다 강력한 고전 논리도 연구합니다.

First-order logic

Main article: First-order logic

일-차 논리는 논리의 특정 형식적 시스템입니다. 그 구문론(syntax)은 잘-형성된 공식(well-formed formulas)으로서 유한한 표현만을 포함하고, 반면에 그 의미론(semantics)은 모든 한정어(quantifiers)를 고정된 담화의 도메인(domain of discourse)으로의 한계에 의해 특징짓습니다.

형식적 논리로부터 초기 결과는 1-차 논리의 한계를 확립했습니다. 뢰벤하임-스콜렘 정리(Löwenheim–Skolem theorem) (1919)는 셀-수-있는 1-차 언어로 된 문장의 집합이 무한 모델을 가지면 그것은 각 무한 카디널리티에 대해 적어도 하나의 모델을 가짐을 보여주었습니다. 이것은 1-차 공리 집합이 자연수, 실수, 또는 동형(isomorphism)까지 임의의 다른 무한 구조를 특성화하는 것이 불가능하다는 것을 보여줍니다. 초기 토대적 연구의 목표는 수학의 모든 부분에 대한 공리적 이론을 생성하는 것이었기 때문에, 이러한 한계는 특히 극명했습니다.

괴델의 완전성 정리(Gödel's completeness theorem)는 1-차 논리에서 논리적 결과(logical consequence)의 의미론적 정의와 구문론적 정의 사이의 동등성을 확립했습니다.[30] 특정 문장이 공리의 특정 집합을 만족시키는 모든 각 모델에서 참이면, 공리로부터 그 문장이 유한하게 추론되어야 함을 보여줍니다. 컴팩트성 정리(compactness theorem)는 완전성 정리의 괴델의 증명에서 보조정리로 처음 등장했고, 논리학자들이 그 중요성을 파악하고 일상적으로 적용하기까지는 수년이 걸렸습니다. 그것은 문장의 집합이 모델을 가지는 것과 모든 각 유한 부분집합이 모델을 가지는 것은 필요충분 조건이다, 또는 다시 말해서, 공식의 비-일관된 공식은 유한 비-일관된 부분집합을 가져야 한다는 것입니다. 완전성 정리와 컴팩트성 정리는 1-차 논리의 논리적 결과에 대한 정교한 분석과 모델 이론(model theory)의 개발을 가능하게 하고, 그것들은 수학에서 1-차 논리가 두드러지는 핵심 이유입니다.

괴델의 불완전성 정리(Gödel's incompleteness theorems)는 1-차 공리화에 추가적인 한계를 설립합니다.[36] 첫 번째 불완전성 정리(first incompleteness theorem)는 산술을 해석할 수 있는 일관된, 효과적으로 주어진 (아래에 정의됨) 논리적 시스템에 대해, (자연수에 대해 유지된다는 의미에서) 참이지만 해당 논리적 시스템 내에서 입증할 수 없는 명제가 존재한다는 것입니다 (그리고 논리적 시스템과 일관될 수 있는 일부 산술의 비-표준 모델에서는 실제로 실패할 수 있습니다). 예를 들어, 페아노 공리(Peano axioms)를 표현할 수 있는 모든 각 논리적 시스템에서, 괴델 명제는 자연수에 유지되지만 입증될 수는 없습니다.

여기서 논리적 시스템은 시스템의 언어로 된 어떤 공식이 주어졌을 때, 그 공식이 공리인지 여부를 결정할 수 있으면 효과적으로 주어진다고 말하고, 페아노 공리를 표현할 수 있는 시스템은 "충분하게 강하다"고 불립니다. 1-차 논리에 적용될 때, 첫 번째 불완전성 정리는 충분하게 강력하고, 일관되고, 효과적인 1-차 이론이 기본적으로 동등(elementarily equivalent)하지 않은 모델, 뢰벤하임-스콜렘 정리에 의해 확립된 것보다 더 강한 한계를 가진다는 것을 의미합니다. 두 번째 불완전성 정리(second incompleteness theorem)는 산술에 대한 충분히 강력하고, 일관되고, 효과적인 공리 시스템은 그 자신의 일관성을 입증할 수 없다고 명시하며, 이는 힐베르트의 프로그램(Hilbert's program)이 도달될 수 없음을 보여주는 것으로 해석되었습니다.

Other classical logics

1차 논리 외에도 많은 논리가 연구됩니다. 여기에는 공식이 무한한 총양의 정보를 제공할 수 있는 무한-항 논리(infinitary logics)와 집합 이론의 일부를 의미론에 직접 포함하는 고차 논리(higher-order logics)가 포함됩니다.

가장 잘 연구된 무한-항 논리는 입니다. 이 논리에서, 한정어는 1-차 논리에서처럼 유한한 깊이까지만 중첩될 수 있지만, 공식에는 그들 내에 유한하거나 셀-수-있는 무한한 논리곱과 논리합이 있을 수 있습니다. 따라서, 예를 들어, 다음과 같은 의 공식을 사용하여 대상이 정수라고 말하는 것이 가능합니다:

고차 논리는 담화의 도메인(domain of discourse)의 요소뿐만 아니라 담화의 도메인의 부분집합, 그러한 부분집합의 집합, 및 기타 상위 유형의 대상의 한정어를 허용합니다. 의미론은 각 상위-유형 한정어 범위에 대해 별도의 도메인을 갖는 대신 한정어 범위가 적절한 유형의 모든 대상에 걸쳐 있도록 정의됩니다. 1-차 논리의 발전하기 전에 연구된 논리학, 예를 들어, 프레게의 논리학은 유사한 집합-이론적 측면을 가졌습니다. 고차 논리는 더 표현력이 뛰어나 자연수와 같은 구조의 완전한 공리화를 허용하지만, 그것들은 1-차 논리에서 완전성과 컴팩트성 정리의 아날로그를 만족하고, 따라서 증명-이론적 분석에 덜 적합합니다.

또 다른 유형의 논리는 원시 재귀 함수(primitive recursive functions)에 대한 작성과 같이 귀납적 정의(inductive definitions)를 허용하는 고정된-점 논리(fixed-point logic)입니다.

1-차 논리의 확장을 형식적으로 정의할 수 있습니다 — 이 개념은 특정 토대적 방법에서 10차 논리처럼 행동하기 때문에 이 섹션에서 모든 논리를 포괄하지만 일반적으로 모든 논리를 포괄하지는 않으며, 예를 들어, 그것은 직관주의적, 양상적 또는 퍼지 논리(fuzzy logic)를 포함하지 않습니다.

린드스트룀의 정리(Lindström's theorem)는 컴팩트성 정리(compactness theorem)와 하향 뢰벤하임-스콜렘 정리(downward Löwenheim–Skolem theorem)를 모두 만족시키는 1-차 논리의 유일한 확장이 1-차 논리임을 의미합니다.

Nonclassical and modal logic

Main article: Non-classical logic

양상 논리(Modal logics)에는 특정 수식이 참일 뿐만 아니라 반드시 참이라고 말하는 연산자와 같은 추가적인 양상 연산자가 포함됩니다. 비록 양상 논리가 수학을 공리화하기 위해 자주 사용되지는 않지만, 그것은 1-차 입증가능성[37] 및 집합-이론적 강제의 속성을 연구하기 위해 사용되어 왔습니다.[38]

직관주의적 논리(Intuitionistic logic)는 브라우어르 자신이 형식화를 피한 브라우어르의 직관주의 프로그램을 연구하기 위해 헤이팅에 의해 개발되었습니다. 직관주의적 논리에는 특히 각 문장이 참이거나 그 부정이 참이라는 제외된 중간의 법칙(law of the excluded middle)이 포함되지 않습니다. 직관주의적 논리의 증명 이론을 사용한 클레이니의 연구는 직관주의적 증명으로부터 건설적인 정보가 복구될 수 있음을 보여주었습니다. 예를 들어, 직관주의적 산술에서 임의의 입증-가능한 전체 함수는 계산-가능(computable)입니다; 이것은 페아노 산술(Peano arithmetic)과 같은 산술의 고전적 이론에서는 참이 아닙니다.

Algebraic logic

대수적 논리(Algebraic logic)는 추상 대수(abstract algebra)의 방법을 형식적 논리의 의미론을 연구하기 위해 사용됩니다. 토대적인 예는 고전 명제적 논리에서 진리 값(truth values)을 표현하기 위해 부울 대수(Boolean algebras)를 사용하는 것과 직관주의적 명제적 논리에서 진리 값을 표현하기 위해 헤이팅 대수(Heyting algebras)를 사용하는 것입니다. 1-차 논리와 고차 논리와 같은 보다 강력한 논리는 원통형 대수(cylindric algebras)와 같은 보다 복잡한 대수적 구조를 사용하여 연구됩니다.

Set theory

Main article: Set theory

집합 이론(Set theory)은 대상의 추상적인 모음인 집합(sets)에 대한 연구입니다. 순서 숫자와 세는 숫자와 같은 기본 개념의 대부분은 집합 이론의 형식적인 공리화가 개발되기 전에 칸토어에 의해 비형식적으로 개발되었습니다. 체르멜로에 의한,[23] 첫 번째 그러한 공리화(first such axiomatization)는 약간 확장되어 체르멜로-프랭켈 집합 이론(Zermelo–Fraenkel set theory, ZF)이 되었으며, 이는 현재 수학에 대한 토대적 이론으로 가장 널리 사용됩니다.

폰 노이만-베르나이스-괴델 집합 이론(Von Neumann–Bernays–Gödel set theory, NBG), 모스-켈리 집합 이론(Morse–Kelley set theory, MK), 및 새로운 토대(New Foundations, NF)를 포함하여 집합 이론의 다른 공식화가 제안되어 왔습니다. 이 중 ZF, NBG, 및 MK는 집합의 누적 계층-구조(cumulative hierarchy)를 설명하는 데 유사합니다. 새로운 토대는 다른 접근 방식을 취합니다; 그것은 집합-존재 공리를 제한하는 대가로 모든 집합의 집합과 같은 대상을 허용합니다. 크립키–플레이텍 집합 이론(Kripke–Platek set theory)의 시스템은 일반화된 재귀 이론과 밀접한 관련이 있습니다.

집합 이론에서 두 가지 유명한 명제는 선택의 공리(axiom of choice)와 연속체 가설(continuum hypothesis)입니다. 체르멜로에 의해 처음 언급된,[19] 선택의 공리는 프렝켈에 의해 ZF와 독립적인 것으로 입증되었지만,[25] 수학자들에 의해 널리 받아들여졌습니다. 그것은 비-빈 집합의 모음이 주어졌을 때 모음에서 각 집합으로부터 정확하게 하나의 원소를 포함하는 단일 집합 C가 있음을 나타냅니다. 집합 C는 모음에서 각 집합으로부터 하나의 원소를 "선택"한다고 말합니다. 그러한 선택이 만들어질 수 있는 능력이 일부에 의해 명백하다고 고려되지만, 왜냐하면 모음에서 각 집합은 비-빈이기 때문에, 그것에 의해 선택이 만들어질 수 있는 일반적이고 구체적인 규칙의 부족은 공리를 비구성적으로 렌드링합니다. 스테판 바나흐(Stefan Banach)와 알프레트 타르스키(Alfred Tarski)는 선택 공리를 사용하여 단단한 공을 유한한 수의 조각으로 분해하고 그런-다음 크기 조정 없이 다시 배열하여 원래 크기의 두 개의 단단한 공을 만들 수 있음을 보여주었습니다.[39] 바나흐-타르스키 역설(Banach–Tarski paradox)로 알려진 이 정리는 선택의 공리의 직관에 반하는 많은 결과 중 하나입니다.

칸토어에 의한 추측으로 처음 제안된 연속체 가설은 1900년 다비트 힐베르트(David Hilbert)에 의한 23개의 문제 중 하나로 나열되었습니다. 괴델은 연속체 가설이 유지되어야 하는 집합 이론의 구성-가능 우주(constructible universe)를 개발함으로써, 연속체 가설이 (선택의 공리와 함께 또는 없이) 체르멜로–프렝켈 집합 이론의 공리로부터 반증될 수 없음을 보여주었습니다. 연속체 가설이 유지되어야 하는 집합론의 구성 가능한 우주를 개발함으로써 가능합니다. 1963년에, 폴 코언(Paul Cohen)은 연속체 가설이 체르멜로-프렝켈 집합 이론의 공리로부터 입증될 수 없음을 보여주었습니다.[26] 어쨌든, 이 독립성 결과는 힐베르트의 문제를 완전히 해결하지는 못했는데, 왜냐하면 집합 이론의 새로운 공리가 그 가설을 해결할 수 있을 가능성이 있기 때문입니다. 이들 선에 대한 최근 연구는 W. Hugh Woodin에 의해 수행되었지만, 그 중요성은 아직 명확하지 않습니다.[40]

집합 이론에서 현대 연구에는 큰 세는-숫자(large cardinals)와 결정성(determinacy)에 대한 연구가 포함됩니다. 큰 세는-숫자는 특정 속성이 너무 강해서 ZFC에서 그러한 세는-숫자의 존재를 입증될 수 없는 세는-숫자(cardinal numbers)입니다. 전형적으로 연구되는 가장 작은 큰 세는-숫자의 세는-숫자, 비-접근가능 세는-숫자(inaccessible cardinal)의 존재는 이미 ZFC의 일관성을 암시합니다. 큰 세는-숫자는 극단적으로 높은 카디널리티(cardinality)를 가지고 있음에도 불구하고, 그것들의 존재는 실수 직선의 구조에 많은 영향을 미칩니다. 결정성(Determinacy)은 특정 2-사람 게임에서 승리 전략이 존재할 수 있음을 의미합니다 (게임은 결정되었다고 말합니다). 이들 전략의 존재는 실수 직선과 기타 폴란드 공간(Polish spaces)의 구조적 속성을 의미합니다.

Model theory

Main article: Model theory

모델 이론(Model theory)은 다양한 형식적 이론의 모델을 연구합니다. 여기서 이론(theory)은 특정 형식적 논리와 시그니처(signature)에서 형식의 집합이고, 반면에 모델(model)은 이론에 대한 구체적인 해석을 제공하는 구조입니다. 모델 이론은 보편적 대수(universal algebra)와 대수적 기하학(algebraic geometry)과 밀접하게 관련되어 있지만, 모델 이론의 방법은 해당 분야보다 논리적 고려 사항에 더 중점을 둡니다.

특정 이론의 모든 모델의 집합은 기본 클래스(elementary class)라고 불립니다; 고전적 모델 이론은 특정 기본 클래스에서 모델의 속성을 결정하거나, 구조의 특정 클래스가 기본 클래스를 형성하는지 여부를 결정하려고 합니다.

한정어 제거(quantifier elimination)의 방법은 특정 이론에서 정의-가능한 집합이 너무 복잡할 수 없음을 보여주기 위해 사용될 수 있습니다. 타르스키는 실수-닫힌 필드(real-closed fields)에 대해 한정어 제거를 확립했으며, 이 결과는 실수의 필드의 이론도 결정-가능함(decidable)을 보여줍니다.[41] 그는 역시 자신의 방법이 임의적인 특성의 대수적으로 닫힌 필드에 동일하게 적용-가능하다고 언급했습니다. 이것으로부터 발전하는 현대의 하위분야는 o-최소 구조(o-minimal structures)와 관련이 있습니다.

마이클 몰리(Michael D. Morley)에 의해 입증된,[42] 몰리의 카테고리성 정리(Morley's categoricity theorem)는 셀-수-있는 언어에서 1-차 이론이 일부 셀-수-없는 카디널리티에서 카테고리적이면, 즉, 이 카디널리티의 모든 모델이 동형적이면, 그것은 모든 셀-수-없는 카디널리티에서 카테고리적이라고 말합니다.

연속체 가설(continuum hypothesis)의 자명한 결과는 연속체보다 적은 수의 비동형적 셀-수-있는 모델을 갖는 완비 이론이 셀-수-있는 만큼만 가질 수 있다는 것입니다. 로버트 로슨 보트(Robert Lawson Vaught)의 이름을 딴 보트의 추측(Vaught's conjecture)은 이것이 연속체 가설과 심지어 독립적으로 참이라고 말합니다. 이 추측에 대한 많은 특별한 사례가 확립되어 왔습니다.

Recursion theory

Main article: Recursion theory

계산-가능성 이론(computability theory)이라고도 불리는 재귀 이론(Recursion theory)은 계산-가능한 함수(computable functions)의 속성과 비-계산가능한 함수를 같은 수준의 비-계산가능성을 가지는 집합으로 나누는 튜링 차수(Turing degrees)를 연구합니다. 재귀 이론에는 일반화된 계산-가능성과 정의-가능성에 대한 연구가 포함됩니다. 재귀 이론은 1930년대 로저 페테르(Rózsa Péter), 알론조 처치(Alonzo Church), 및 앨런 튜링( Alan Turing)의 연구에서 성장했으며, 이는 1940년대 클레이니(Kleene)와 포스트(Post)에 의해 크게 확장되었습니다.[43]

고전적 재귀 이론은 자연수에서 자연수로의 함수의 계산-가능성에 중점을 둡니다. 토대적인 결과는 튜링 기계(Turing machines), λ 계산법(λ calculus), 및 기타 시스템을 사용하여 수많은 독립적이고 동등한 특성화를 갖는 강력하고 정식의 계산-가능한 함수의 클래스를 수립합니다. 더 발전된 결과는 튜링 차수의 구조와 재귀적으로 열거-가능한 집합(recursively enumerable sets)의 격자(lattice)에 관한 것입니다.

일반화된 재귀 이론은 재귀 이론의 아이디어를 더 이상 반드시 유한하지 않은 계산으로 확장합니다. 여기에는 초산술적 이론(hyperarithmetical theory)과 α-재귀 이론(α-recursion theory)과 같은 영역뿐만 아니라 더 높은 유형의 계산-가능성에 대한 연구가 포함됩니다.

재귀 이론의 현대 연구에는 알고리즘 무작위성(algorithmic randomness), 계산-가능한 모델 이론(computable model theory), 및 역 수학(reverse mathematics)과 같은 응용 연구뿐만 아니라, 순수 재귀 이론의 새로운 결과도 포함됩니다.

Algorithmically unsolvable problems

재귀 이론의 중요한 하위 분야는 알고리즘적 비-해결가능성을 연구합니다; 문제에 대한 모든 적법한 입력에 대해 정답을 반환하는 가능한 계산-가능한 알고리즘이 없으면 결정 문제(decision problem) 또는 함수 문제(function problem)는 알고리즘적으로 비-해결가능(algorithmically unsolvable)입니다. 1936년 처치와 튜링에 의해 독립적으로 얻어진 비-해결가능성에 대한 첫 번째 결과는 결정문제(Entscheidungsproblem)가 알고리즘적으로 비-해결가능이라는 것을 보여주었습니다. 튜링은 정지 문제(halting problem)의 비-해결가능성을 수립함으로써 이를 입증했으며, 이는 재귀 이론과 컴퓨터 과학 둘 다에서 광범위한 영향을 미쳤습니다.

보통의 수학으로부터 비-결정가능한 문제에 대한 많은 알려진 예제가 있습니다. 그룹에 대한 단어 문제(word problem for groups)는 1955년 표트르 노비코프(Pyotr Novikov)에 의해, 그리고 1959년 W. Boone에 의해 독립적으로 알고리즘적으로 비-해결가능임이 입증되었습니다. 1962년 티보르 라도(Tibor Radó)에 의해 개발된 바쁜 비버(busy beaver) 문제는 또 다른 잘 알려진 예입니다.

힐베르트의 열 번째 문제(Hilbert's tenth problem)는 정수 계수를 갖는 다변수 다항 방정식이 정수에서 해를 갖는지 여부를 결정하는 알고리즘을 요구했습니다. 부분적인 진전이 줄리아 로빈슨(Julia Robinson), 마틴 데이비스(Martin Davis), 및 힐러리 퍼트넘(Hilary Putnam)에 의해 이루어졌습니다. 그 문제의 알고리즘적 비-해결가능성은 1970년에 유리 마티야세비치(Yuri Matiyasevich)에 의해 입증되었습니다.[44]

Proof theory and constructive mathematics

Main article: Proof theory

증명 이론(Proof theor)은 다양한 논리적 연역 시스템에서 형식적 증명에 대한 연구입니다. 이들 증명은 형식적인 수학적 대상으로 표현되어, 수학적 기법을 통한 분석을 용이하게 합니다. 힐베르트-스타일 연역 시스템(Hilbert-style deduction systems), 자연 연역의 시스템, 겐첸(Gentzen)에 의해 개발된 시퀀트 계산법(sequent calculus)을 포함하여 여러 연역 시스템이 공통적으로 고려됩니다.

수학적 논리의 맥락에서 구성적 수학(constructive mathematics)의 연구에는 직관적 논리와 같은 비-고전적 논리 시스템에 대한 연구뿐만 아니라 예측(predicative) 시스템에 대한 연구도 포함됩니다. 예측주의의 초기 지지자는 예측 방법만을 사용하여 실수 해석의 상당 부분을 개발하는 것이 가능하다는 것을 보여준 허르만 바일(Hermann Weyl)이었습니다.[45]

증명은 전적으로 유한항이고, 반면에 구조에서 진실은 그렇지 않기 때문에, 구성적 수학에서는 증명-가능성을 강조하는 것이 공통적입니다. 고전적 (또는 비구성적) 시스템의 증명-가능성과 직관적 (또는 각각 구성적) 시스템의 증명-가능성 사이의 관계는 특히 흥미롭습니다. 괴델-겐첸 부정 번역(Gödel–Gentzen negative translation)과 같은 결과는 고전적 논리를 직관적 논리에 삽입 (또는 번역)하여, 직관적 증명에 대한 일부 속성을 고전적 증명으로 다시 전송할 수 있음을 보여줍니다.

증명 이론의 최근 발전에는 울리히 콜린바흐(Ulrich Kohlenbach)에 의한 증명 마이닝(proof mining)의 연구와 Michael Rathjen에 의한 증명-이론적 순서-숫자(proof-theoretic ordinals) 연구가 포함됩니다.

Applications

"수학적 논리는 수학과 그 토대 (G. Frege, B. Russell, D. Hilbert, P. Bernays, H. Scholz, R. Carnap, S. Lesniewski, T. Skolem)뿐만 아니라, 물리학 (R. Carnap, A. Dittrich, B. Russell, 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. Bochenski)에도 성공적으로 적용되어 왔습니다. 역사적으로 논리학의 적용은 매우 유익한 것으로 입증되어 왔습니다 (J. Lukasiewicz, H. Scholz, B. Mates, A. Becker, E. Moody, J. Salamucha, K. Duerr, Z. Jordan, P. Boehner, J. M. Bochenski, S. [Stanislaw] T. Schayer, D. Ingalls)."[46] "적용은 신학에도 이루어져 왔습니다 (F. Drewnowski, J. Salamucha, I. Thomas)."[46]

Connections with computer science

Main article: Logic in computer science

컴퓨터 과학에서 계산 가능성 이론의 연구는 수학적 논리에서 계산 가능성 연구와 밀접한 관련이 있습니다. 어쨌든, 강조점의 차이가 있습니다. 컴퓨터 과학자들은 종종 구체적인 프로그래밍 언어와 실행-가능한 계산-가능성(feasible computability)에 초점을 맞추고, 반면에 수학적 논리에서 연구자들은 종종 이론적 개념으로서의 계산 가능성과 비-계산가능성에 초점을 맞춥니다.

프로그래밍 언어의 의미론(semantics of programming languages)의 이론은 프로그램 검증 (특히, 모델 검사)과 마찬가지로 모델 이론(model theory)과 관련이 있습니다. 증명과 프로그램 사이의 커리-하워드 대응(Curry–Howard correspondence)은 증명 이론(proof theory), 특히 직관주의적 논리(intuitionistic logic)와 관련이 있습니다. 람다 계산법(lambda calculus)과 조합론적 논리(combinatory logic)와 같은 형식적 계산법이 이제 이상화된 프로그래밍 언어(programming languages)로 연구됩니다.

컴퓨터 과학은 역시 자동화된 정리 증명화(automated theorem proving)와 논리 프로그래밍(logic programming)과 같은 자동 검사 또는 심지어 증명의 찾는 것에 대한 기술을 개발함으로써 수학에 기여합니다.

기술 복잡성 이론(Descriptive complexity theory)은 논리를 계산적 복잡성(computational complexity)과 연관시킵니다. 이 분야에서 첫 번째 중요한 결과, 피이긴의 정리(Fagin's theorem, 1974)는 NP가 실존적 2-차 논리(second-order logic)의 문장에 의해 표현될 수 있는 언어의 집합이라는 것을 확립했습니다.

Foundations of mathematics

Main article: Foundations of mathematics

19세기에서, 수학자들은 자신의 분야에서 논리적 틈과 불일치를 인식하게 되었습니다. 수세기 동안 공리적 방법의 예제로 가르쳐져 온 기하학에 대한 유클리드의 공리는 불완전하다는 것이 밝혀졌습니다. 무한소(infinitesimals)의 사용과 함수(function)의 정의 자체가 바이어슈트라스의 어디에서도 미분-불가능한 연속 함수와 같은 병리학적 예제가 발견되면서 해석학에서 의문이 제기되었습니다.

임의적인 무한 집합에 대한 칸토어의 연구도 역시 비판을 불러일으켰습니다. 레오폴드 크로네커(Leopold Kronecker)는 "신이 정수를 만들었습니다; 그 밖의 모든 것은 인간이 만든 것입니다"라고 유명하게 말하면서, 수학에서 유한하고 구체적인 대상에 대한 연구로의 복귀를 지지했습니다. 비록 크로네커의 주장이 20세기 구성론자들에 의해 추진되었을지라도, 수학 공동체 전체는 그것을 거부했습니다. 다비트 힐베르트(David Hilbert)는 "아무도 칸토어가 창조해 온 낙원에서 우리를 쫓아낼 수 없다"며 무한의 연구를 지지한다고 주장했습니다.

수학자들은 수학의 많은 부분을 형식화하기 위해 사용될 수 있는 공리적 시스템을 찾기 시작했습니다. 함수와 같은 이전의 소박한 용어에서 모호성을 제거하는 것 외에도, 이러한 공리화를 통해 일관성 증명이 가능해질 것으로 기대되었습니다. 19세기에서, 공리의 집합의 일관성을 증명하는 주요 방법은 그것에 대한 모델을 제공하는 것이었습니다. 따라서, 예를 들어, 비-유클리드 기하학(non-Euclidean geometry)은 고정된 구 위의 점을 의미하는 점(point)과 구 위의 큰 원(great circle)을 의미하는 선(line)을 정의함으로써 일관성이 입증될 수 있습니다. 타원 기하학(elliptic geometry)의 모델, 결과 구조는 평행 공준을 제외하고 평면 기하학의 공리를 만족시킵니다.

형식적 논리의 발달과 함께, 힐베르트는 공리 시스템이 그 시스템에서 가능한 증명의 구조를 분석하고, 이 분석을 통해 모순을 증명하는 것이 불가능함을 보여줌으로써 일관적인지를 입증하는 것이 가능한지 물었습니다. 이 아이디어는 증명 이론(proof theory)의 연구로 이어졌습니다. 더욱이, 힐베르트는 그가 허용하는 방법을 참조하기 위해 유한항(finitary)이라는 용어를 사용하지만 그것을 정확하게 정의하지는 않음으로써 분석이 완전하게 구체적이어야 한다고 제안했습니다. 힐베르트의 프로그램(Hilbert's progra)으로 알려진 이 프로젝트는 괴델의 불완전성 정리에 의해 심각한 영향을 받았으며, 이는 산술의 형식적 이론의 일관성이 해당 이론에서 형식화-가능한 방법을 사용하여 확립될 수 없음을 보여줍니다. 겐첸은 초월유한 귀납법(transfinite induction)의 공리로 강화된 유한항 시스템에서 산술의 일관성에 대한 증명을 생성하는 것이 가능하다는 것을 보여주었고, 이를 위해 그가 개발한 기술은 증명 이론에서 중요한 역할을 했습니다.

수학의 토대 역사의 두 번째 쓰레드는 비고전적 논리학(nonclassical logics)과 구성적 수학(constructive mathematics)을 포함합니다. 구성적 수학의 연구에는 구성적(constructive)의 다양한 정의를 갖는 많은 다른 프로그램이 포함됩니다. 가장 수용적인 목적에서, 선택의 공리를 사용하지 않는 ZF 집합 이론에서 증명은 많은 수학자에 의해 구성적이라고 불립니다. 보다 제한된 버전의 구성주의는 자연수, 숫자-이론적 함수(number-theoretic functions), 및 자연수의 집합 (이는 실수를 표현하기 위해 사용될 수 있어, 수학적 해석학의 연구를 용이하게 함)으로 제한됩니다. 공통적인 아이디어는 함수 자체가 존재한다고 말하기 전에 함수의 값을 계산하는 구체적인 수단을 알아야 한다는 것입니다.

20세기 초, 라위천 에흐베르튀스 얀 브라우어르(Luitzen Egbertus Jan Brouwer)는 수학의 철학(philosophy of mathematics)의 일부로 직관주의(intuitionism)를 창시했습니다. 처음에는 잘 이해되지 않았던 이 철학은 수학자에게 수학적 명제가 참이 되기 위해서는 그 사람이 그 명제를 직관할 수 있어야 하고, 그 진실을 믿을 뿐만 아니라 그 진실에 대한 이유를 이해할 수 있어야 한다고 말했습니다. 진리에 대한 이러한 정의의 결과는 제외된 중간의 법칙(law of excluded middle)을 거부하는 것이었는데, 왜냐하면, 브라우어르에 따르면, 그 부정도 사실이라고 주장할 수 없는 반면, 사실이라고 주장할 수 없는 명제가 있기 때문입니다. 브라우어르의 철학은 영향력이 있었고, 저명한 수학자들 사이에 격렬한 논쟁의 원인이 되었습니다. 나중에, 클레이니와 카이즐은 직관주의적 논리의 형식화된 버전을 연구했습니다 (브라우어르는 형식화를 거부하고, 그의 연구를 비형식화된 자연 언어로 발표했습니다). BHK 해석(BHK interpretation)과 크립키 모델(Kripke models)의 출현으로, 직관주의는 고전적 수학(classical mathematics)과 조화되기 쉬워졌습니다.

See also

Notes

  1. ^ In the foreword to the 1934 first edition of "Grundlagen der Mathematik" (Hilbert & Bernays 1934), Bernays wrote the following, which is reminiscent of the famous note by Frege when informed of Russell's paradox.

    "Die Ausführung dieses Vorhabens hat eine wesentliche Verzögerung dadurch erfahren, daß in einem Stadium, in dem die Darstellung schon ihrem Abschuß nahe war, durch das Erscheinen der Arbeiten von Herbrand und von Gödel eine veränderte Situation im Gebiet der Beweistheorie entstand, welche die Berücksichtigung neuer Einsichten zur Aufgabe machte. Dabei ist der Umfang des Buches angewachsen, so daß eine Teilung in zwei Bände angezeigt erschien."

    Translation:

    "Carrying out this plan [by Hilbert for an exposition on proof theory for mathematical logic] has experienced an essential delay because, at the stage at which the exposition was already near to its conclusion, there occurred an altered situation in the area of proof theory due to the appearance of works by Herbrand and Gödel, which necessitated the consideration of new insights. Thus the scope of this book has grown, so that a division into two volumes seemed advisable."

    So certainly Hilbert was aware of the importance of Gödel's work by 1934. The second volume in 1939 included a form of Gentzen's consistency proof for arithmetic.
  2. ^ A detailed study of this terminology is given by Soare 1996.
  3. ^ Ferreirós 2001 surveys the rise of first-order logic over other formal logics in the early 20th century.

References

  1. ^ Barwise (1989).
  2. ^ "Computability Theory and Foundations of Mathematics / February, 17th – 20th, 2014 / Tokyo Institute of Technology, Tokyo, Japan" (PDF).
  3. ^ Ferreirós (2001), p. 443.
  4. ^ Bochenski (1959), Sec. 0.1, p. 1.
  5. ^ Swineshead (1498).
  6. ^ Boehner (1950), p. xiv.
  7. ^ Katz (1998), p. 686.
  8. ^ "Bertić, Vatroslav | Hrvatska enciklopedija". www.enciklopedija.hr. Retrieved 2023-05-01.
  9. ^ Peano (1889).
  10. ^ Dedekind (1888).
  11. ^ Katz (1998), p. 774.
  12. ^ Lobachevsky (1840).
  13. ^ Hilbert (1899).
  14. ^ Pasch (1882).
  15. ^ Felscher (2000).
  16. ^ Dedekind (1872).
  17. ^ Cantor (1874).
  18. ^ Katz (1998), p. 807.
  19. ^ a b Zermelo (1904).
  20. ^ Zermelo (1908a).
  21. ^ Burali-Forti (1897).
  22. ^ Richard (1905).
  23. ^ a b Zermelo (1908b).
  24. ^ Ferreirós (2001), p. 445.
  25. ^ a b Fraenkel (1922).
  26. ^ a b Cohen (1966).
  27. ^ See also Cohen 2008.
  28. ^ Löwenheim (1915).
  29. ^ Skolem (1920).
  30. ^ a b Gödel (1929).
  31. ^ Gentzen (1936).
  32. ^ Gödel (1958).
  33. ^ Carroll (1896).
  34. ^ Kleene (1943).
  35. ^ Turing (1939).
  36. ^ Gödel (1931).
  37. ^ Solovay (1976).
  38. ^ Hamkins & Löwe (2007).
  39. ^ Banach & Tarski (1924).
  40. ^ Woodin (2001).
  41. ^ Tarski (1948).
  42. ^ Morley (1965).
  43. ^ Soare (2011).
  44. ^ Davis (1973).
  45. ^ Weyl 1918.
  46. ^ a b Bochenski (1959), Sec. 0.3, p. 2.

Undergraduate texts

Graduate texts

Research papers, monographs, texts, and surveys

Classical papers, texts, and collections

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.

  • Burali-Forti, Cesare (1897). A question on transfinite numbers. Reprinted in van Heijenoort 1976, pp. 104–111

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.

External links

Retrieved from "https://dawoum.duckdns.org/w/index.php?title=Mathematical_logic&oldid=82521"