Theorem

Original article: wikipedia:Theorem

Not to be confused with Teorema, Theorema, or Theory.

The Pythagorean theorem has at least 370 known proofs

수학(mathematics)에서. 정리(theorem)는 입증되어 왔거나 입증될 수 있는 명제(statement)입니다. 정리의 증명(proof)은 그 정리가 공리(axioms)와 이전에 입증된 정리의 논리적 결과(logical consequence)임을 확립하는 연역 시스템(deductive system)의 추론 규칙을 사용하여 논리적 논증(logical argument)입니다.

수학의 주류에서, 공리와 추론 규칙은 공통적으로 암시적으로 남아 있고, 이 경우에서, 그것들은 거의 항상 선택의 공리(axiom of choice)를 갖는 체르멜로–프렝켈 집합 이론(Zermelo–Fraenkel set theory) 또는 페아노 산술(Peano arithmetic)과 같은 덜 강력한 이론의 그것들입니다. 주목할만한 예외는 집합론에 새로운 공리를 추가해야 하는 그로텐디크 우주(Grothendieck universe)를 포함하는 페르마의 마지막 정리의 와일스의 증명(Wiles's proof of Fermat's Last Theorem)입니다. 일반적으로, 명시적으로 정리라고 불리는 주장은 다른 알려진 정리의 즉각적인 결과가 아닌 입증된 결과입니다. 더욱이, 많은 저자들은 가장 중요한 결과만을 정리로 인정하고, 덜 중요한 정리에는 보조정리(lemma), 제안(proposition), 및 따름정리(corollary)라는 용어를 사용합니다.

수학적 논리(mathematical logic)에서, 정리와 증명의 개념은 그것들에 대한 수학적 추론을 허용하기 위해 형식화되어 왔습니다. 이러한 맥락에서, 명제는 일부 형식적 언어(formal language)의 잘-형성된 공식(well-formed formulas)이 됩니다. 이론은 공리(axioms)라고 하는 몇 가지 기본 명제와 몇 가지 추론 규칙(deducing rules) (때로는 공리에 포함됨)으로 구성됩니다. 이론의 정리는 추론 규칙을 사용함으로써 공리에서 유도될 수 있는 명제입니다. 이 형식화는 증명 이론(proof theory)으로 이어졌고, 정리와 증명에 대한 일반 정리를 입증하는 것을 허용합니다. 특히, 괴델의 불완전성 정리(Gödel's incompleteness theorems)는 자연수를 포함하는 모든 각 일관된(consistent) 이론이 이론의 정리가 아닌 (즉, 그것들이 이론 내에서 증명될 수 없는) 자연수에 대한 참 명제를 가지고 있음을 보여줍니다.

공리는 종종 물리적 세계의 속성에 대한 추상화이므로, 정리는 일부 진리를 표현하는 것으로 고려될 수 있지만, 실험적(experimental)인 과학 법칙(scientific law)의 개념과 달리, 정리의 진리에 대한 정당화는 순전히 연역적(deductive)입니다.

Theoremhood and truth

19세기 말과 수학의 토대적 위기(foundational crisis of mathematics)까지, 모든 수학적 이론은 자명한 것으로 여기는 몇 가지 기본 속성으로 구성되었습니다; 예를 들어, 모든 각 자연수(natural number)는 다음 수를 가지고, 두 개의 주어진 구별되는 점을 통과하는 정확하게 하나의 직선(line)이 있다, 등이 사실입니다. 절대적으로 명백한 것으로 여겨지지 않는 기본 속성은 공준(postulates)이라고 불립니다; 예를 들어, 유클리드의 공준(Euclid's postulates) 등이 있습니다. 모든 정리는 이들 기본 속성을 암시적 또는 명시적으로 사용함으로써 입증되었고, 이들 기본 속성의 증거로 인해, 입증된 정리는 증명에 오류가 없는 한 결정적인 진리로 여겨집니다. 예를 들어, 삼각형(triangle)의 내부 각도(interior angles)의 합은 180°와 같고, 이것은 의심할 여지가 없는 사실로 여겨집니다.

수학의 토대적인 위기의 한 측면은 임의의 모순으로 이어지지 않는 비-유클리드 기하학(non-Euclidean geometries)의 발견이었지만, 그러한 기하학에서, 삼각형의 각도의 합이 180°와 다릅니다. 따라서, "삼각형 각도의 합은 180°와 같다"라는 속성은 유클리드의 공준이 가정되는지 여부에 따라 참 또는 거짓입니다. 유사하게, 집합(sets)의 "명백한" 기본 속성의 사용은 러셀의 역설(Russel's paradox)의 모순으로 이어집니다. 이것은 집합을 조작하는 데 허용되는 규칙을 정교화함으로써 해결되어 왔습니다.

이 위기는 수학의 토대를 더 엄격(rigorous)하게 만들기 위해 재검토함으로써 해결되어 왔습니다. 이들 새로운 토대에서, 정리는 이론의 공리(axioms)와 추론 규칙(inference rules)에서 입증될 수 있는 수학적 이론(mathematical theory)의 잘-형성된 공식(well-formed formula)입니다. 따라서, 삼각형의 각도의 합에 대한 위의 정리는 다음과 같습니다: 유클리드 기하학의 공리와 추론 규칙 아래에서, 삼각형의 내부 각도의 합은 180°와 같습니다. 유사하게, 러셀의 역설은 공리화된 집합 이론에서, 모든 집합의 집합이 잘-형성된 공식으로 표현될 수 없기 때문에 사라집니다. 보다 정확하게, 만약 모든 집합의 집합이 잘-형성된 공식으로 표현될 수 있으면, 이것은 이론이 비-일관적(inconsistent)이고, 모든 각 잘-형성된 주장과 그 부정이 정리라는 것을 의미합니다.

이러한 맥락에서, 정리의 타당성은 증명의 정확성에만 의존합니다. 그것은 진리, 또는 심지어 공리의 중요성과도 독립적입니다. 이것은 무의미함에 있어서 공리의 중요성을 의미하는 것이 아니라, 단지 정리의 타당성이 공리의 중요성과 독립적이라는 것을 의미합니다. 이 독립성은 명백하게 관련이 없는 영역에서 수학의 일부 영역의 결과를 사용할 수 있게 함으로써 유용할 수 있습니다.

수학에 대한 이러한 사고 방식의 중요한 결과는 수학적 이론과 정리를 수학적 대상(mathematical objects)으로 정의하고, 이에 대한 정리를 증명할 수 있다는 것입니다. 예제는 괴델의 불완전성 정리(Gödel's incompleteness theorems)입니다. 특히, 더 넓은 이론에서는 증명될 수 있지만, 주변 이론의 정리가 아닌 것으로 입증될 수 있는 것보다 잘 형성된 주장들이 있습니다. 예로서 굿스타인의 정리(Goodstein's theorem)는 페아노 산술(Peano arithmetic)로 설명될 수 있지만, 페아노 산술에서는 입증될 수 없는 것으로 판명되었습니다. 어쨌든, 체르멜로-프랭켈 집합 이론(Zermelo–Fraenkel set theory)과 같은 좀 더 일반적인 이론에서 입증될 수 있습니다.

Epistemological considerations

많은 수학적 정리는 조건부 명제이며, 그 증명은 가설(hypotheses) 또는 전제(premises)로 알려진 조건에서 결론을 추론합니다. 증명을 진리의 정당화로 해석하는 관점에서, 결론은 종종 가설의 필연적인 결과(necessary consequence)로 보입니다. 즉, 더 이상의 가정 없이 가설이 참인 경우에서 결론이 참이라는 것입니다. 어쨌든, 유도 규칙과 조건부 기호 (예를 들어, 비-고전적 논리)에 할당된 의미에 따라 조건부는 특정 연역적 시스템(deductive systems)에서 다르게 해석될 수도 있습니다.

비록 정리는 완전히 기호적 형식으로 (예를 들어, 명제 계산법(propositional calculus)에서 제안으로) 작성될 수 있지만, 그것들은 더 나은 가독성을 위해 한글과 같은 자연어로 비공식적으로 표현되는 경우가 많습니다. 같은 것은 의심의 여지없이 정리의 명제가 참임을 독자들에게 확신시키기 위해 의도된, 논리적으로 조직되고 명확하게 표현된 비공식 논증으로 종종 표현되고, 형식적 상징적 증명이 원칙적으로 구성될 수 있는 증명에서도 참입니다.

가독성이 더 좋을 뿐만 아니라, 비공식 논증은 전형적으로 순수하게 기호적 논증보다 확인하기가 더 쉽습니다—실제로, 많은 수학자들은 정리의 타당성을 시연할 뿐만 아니라, 어떤 식으로든 그것이 분명히 왜 참인지 설명하는 증명을 선호할 것입니다. 어떤 경우에서, 사진을 그것의 증명으로 사용함으로써 정리를 입증할 수도 있습니다.

정리는 수학의 핵심에 있기 때문에 수학 미학(aesthetics)의 중심이기도 합니다. 정리는 종종 "자명한", 또는 "어려운", 또는 "심오한", 또는 "아름다운" 것으로 설명됩니다. 이들 주관적인 판단은 사람마다 다를 뿐만 아니라, 시대와 문화에 따라 다릅니다: 예를 들어, 증명이 확보되고, 단순화되거나 더 잘 이해되면 한때 어려웠던 정리가 사소해질 수 있습니다. 다른 한편으로, 심오한 정리는 간단하게 기술될 수 있지만, 그 증명은 수학의 이질적인 영역 사이의 놀랍고 미묘한 연결을 포함할 수 있습니다. 페르마의 마지막 정리(Fermat's Last Theorem)는 그러한 정리의 특히 잘 알려진 예제입니다.

Informal account of theorems

논리적(Logically)으로, 많은 정리는 지시적 조건부(indicative conditional)의 형식입니다: 만약 A이면, B이다. 그러한 정리는 B를 주장하지 않습니다 — B가 A의 필연적 결과라고 주장할 뿐입니다.  이 경우에서, A는 정리의 가설(hypothesis)이라고 불리고 (여기서 "가설"은 추측(conjecture)과 매우 다른 것을 의미합니다), B는 정리의 결론(conclusion)을 의미합니다. 둘은 함께 (증명 없이) 정리의 제안(proposition) 또는 명제(statement)라고 불립니다 (예를 들어, "만약 A이면, B이다"는 제안입니다). 대안적으로, A와 B는 각각 전제(antecedent)와 결론(consequent)이라고 부를 수도 있습니다. "만약 n이 짝수 자연수이면, n/2는 자연수이다"라는 정리는 전형적인 예제이며, 가설은 "n은 짝수 자연수이다"이고, 결론은 "n/2도 역시 자연수이다"입니다.

정리가 증명되기 위해, 그것은 원칙적으로 정확하고, 형식적인 명제로 표현될 수 있어야 합니다. 어쨌든, 정리는 보통 완전하게 기호적 형식이 아닌 자연어로 표현됩니다—형식적인 명제는 비공식적인 것에서 유도될 수 있다고 가정을 가집니다.

수학에서는 주어진 언어 내에서 여러 가설을 선택하고 이론이 이들 가설에서 입증할 수 있는 모든 명제로 구성되어 있다고 선언하는 것이 공통적입니다. 이들 가설은 이론의 토대적 기초를 형성하고 공리(axioms) 또는 공준이라고 불립니다. 증명 이론(proof theory)으로 알려진 수학 분야는 형식적 언어, 공리, 및 증명의 구조를 연구합니다.

A planar map with five colors such that no two regions with the same color meet. It can actually be colored in this way with only four colors. The four color theorem states that such colorings are possible for any planar map, but every known proof involves a computational search that is too long to check by hand.

일부 정리는 정의, 공리, 및 기타 정리를 명백한 방법으로 따르고 임의의 놀라운 통찰력을 포함하지 않는다는 의미에서 "자명한(trivial)" 것입니다. 다른 한편으로, 일부는 증명이 길고 어려울 수 있고, 정리 자체의 명제와 표면적으로 구별되는 수학 영역을 포함하거나, 수학의 이질적인 영역 사이에 놀라운 연결을 보여주기 때문에 "심오한" 것이라고 불릴 수 있습니다. 정리는 간단하면서도 심오할 수 있습니다. 훌륭한 예제는 페르마의 마지막 정리(Fermat's Last Theorem)이고, 다른 영역 중에서 숫자 이론(number theory)과 조합론(combinatorics)에서 단순하지만 심오한 정리의 다른 많은 예제가 있습니다.

다른 정리는 쉽게 기록될 수 없는 알려진 증명을 가집니다. 가장 눈에 띄는 예제는 네 가지 색깔깔 정리와 케플러 추측(Kepler conjecture)입니다. 이들 두 가지 정리는 모두 컴퓨터 프로그램에 의해 검증되는 계산 검색으로 줄임으로써만 참으로 알려져 있습니다. 처음에, 많은 수학자들이 이 증명 형식을 받아들이지 않았지만, 그것은 더 널리 수용되게 되었습니다. 수학자 Doron Zeilberger는 이것이 수학자들이 이제까지 증명한 유일한 비-자명한 결과일 수 있다고 주장하기까지 했습니다. 다항 항등식, 삼각 항등식, 및 초기하 항등식을 포함하여 많은 수학적 정리가 보다 간단한 계산으로 축소될 수 있습니다.

Relation with scientific theories

수학에서 정리와 과학에서 이론은 그것들의 인식론(epistemology)에서 근본적으로 다릅니다. 과학적 이론은 입증될 수 없습니다; 그 핵심 속성은 그것이 반증-가능(falsifiable)이라는 것, 즉, 그것은 실험(experiments)에 의해 테스트-가능인 자연 세계에 대한 예측()을 만드는 것입니다. 예측과 실험 사이의 불일치는 과학적 이론의 부정확성을 시연하거나, 적어도 그 정확성이나 타당성의 영역을 제한합니다. 다른 한편으로, 수학적 정리는 순전하게 추상적인 형식적 명제입니다: 정리의 증명은 과학적 이론을 뒷받침하기 위해 그러한 증거가 사용되는 것과 같은 방법으로 실험이나 다른 경험적 증거를 포함할 수 없습니다.

The Collatz conjecture: one way to illustrate its complexity is to extend the iteration from the natural numbers to the complex numbers. The result is a fractal, which (in accordance with universality) resembles the Mandelbrot set.

그럼에도 불구하고, 수학적 정리의 발견과 관련된 어느 정도의 경험주의와 데이터 수집이 있습니다. 때로는 강력한 컴퓨터를 사용하여 패턴을 설정함으로써, 수학자들은 증명하려는 것이 무엇 인지의 아이디어를 가질 수 있고, 어떤 경우에는 증명을 수행하는 방법에 대한 계획도 가질 수 있습니다. 단 하나의 반대-예제를 찾아 진술된 제안에 대해 증명의 불가능성을 확립하고, 실현 가능한 증명을 가질 수 있는 원래 제안의 제한된 형식을 제안하는 것도 가능합니다.

예를 들어, 콜라츠 추측(Collatz conjecture)과 리만 가설(Riemann hypothesis)은 모두 잘 알려진 미해결 문제입니다; 그것들은 경험적 확인을 통해 광범위하게 연구되었지만, 입증되지 않은 상태로 남아 있습니다. 콜라츠 추측은 최대 약 2.88 × 10¹⁸의 시작 값에 대해 확인되었습니다. 리만 가설은 제타 함수의 처음 10조 개의 비-자명한 영들에 대해 유지되는 것으로 확인되어 왔습니다. 대부분의 수학자들은 추측과 가설이 참이라고 가정하는 것을 용인할 수 있지만, 이러한 제안 중 어느 것도 입증된 것으로 고려되지 않습니다.

그러한 증거는 증명을 구성하지 않습니다. 예를 들어, 메르텐스 추측(Mertens conjecture)은 현재 거짓으로 알려진 자연수에 대한 명제이지만, 명시적인 반대-예제 (즉, 메르텐스 함수 M(n)이 n의 제곱근과 같거나 초과하는 자연수 n)는 알려진 것이 없습니다: 10¹⁴보다 작은 모든 숫자는 메르텐스 속성을 가지고, 이 속성을 가지지 않는 가장 작은 숫자는 오직 1.59 × 10⁴⁰의 지수(exponential)보다 작은 것으로 알려져 있으며, 이는 근사적으로 10에 4.3 × 10³⁹ 거듭제곱을 올린 것입니다. 우주에 있는 입자의 수는 일반적으로 10의 100 거듭제곱 (구골)보다 작은 것으로 여겨지지만, 철저한 검색(exhaustive search)을 통해 명시적인 반대-예제를 찾을 희망은 없습니다.

"이론"이라는 단어는 수학에도 존재하며, 예를 들어, 그룹 이론(group theory) (수학적 이론 참조)에서와 같이, 수학적 공리, 정의, 및 정리의 몸체를 나타내는 것입니다. 과학, 특히 물리학, 및 공학에도 "정리"가 있지만, 그것들은 종종 물리적 가정과 직관이 중요한 역할을 하는 명제와 증명을 가집니다; 그러한 "정리"의 기반이 되는 물리적 공리는 자체적으로 반증-가능입니다.

Terminology

수학적 명제에 대해 다양한 용어가 존재합니다; 이들 용어는 특정 주제에서 명제가 수행하는 역할을 나타냅니다. 다른 용어 사이의 구분은 때때로 다소 임의적이고, 일부 용어의 사용법은 시간이 지남에 따라 발전해 왔습니다.

• 공리(axiom) 또는 공준(postulate)은 연구 대상에 대한 근본적인 가정으로, 증명 없이 수용됩니다. 관련된 개념은 알려진 개념의 관점에서 단어 또는 구의 의미를 제공하는 정의(definition)의 개념입니다. 고전 기하학은 일반적인 명제인 공리와 기하학적 대상에 대한 공준 사이를 분별합니다. 역사적으로, 공리는 "자명한(self-evident)" 것으로 여겨졌습니다; 오늘날 그것들은 단지 사실로 가정됩니다.
• 추측(conjecture)은 사실로 믿어지는 입증되지 않은 명제입니다. 추측은 보통 공개적으로 이루어지고, 작성자의 이름을 따서 지어집니다 (예를 들어, 골드바흐의 추측 및 콜라츠의 추측). 가설(hypothesis)이라는 용어는 이러한 의미로도 사용되며 (예를 들어, 리만 가설), 증명의 전제로서 "가설"과 혼동되어서는 안 됩니다. 다른 용어도 경우에 따라 사용되며, 예를 들어 사람들이 해당 명제를 참으로 믿어야 하는지 여부를 확신할 수 없는 경우 문제(problem)라고 합니다. 페르마의 마지막 정리(Fermat's Last Theorem)는 역사적으로 정리라고 불렸지만, 수세기 동안 그것은 단지 추측에 불과했습니다.
• 정리(theorem)는 공리와 다른 정리를 기반으로 참으로 입증된 명제입니다.
• 제안(proposition)은 덜 중요한 정리, 또는 너무 기초적이거나 즉시 명백한 것으로 여겨지는 정리, 또는 증명 없이 진술될 수 있는 정리입니다. 이것은 명제 계산법(propositional logic)에서 사용되는 "proposition"와 혼동되어서는 안 됩니다. 고전 기하학에서 "제안"이라는 용어는 다르게 사용되었습니다: 유클리드의 원론 (기원전 약 300년)에서 모든 정리와 기하학적 구성은 중요성에 관계없이 "제안"이라고 불렸습니다.
• 보조-정리(lemma)는 "부속물 제안"입니다 – 특정 증명에서 사용하는 것 외에는 거의 응용가능성이 없는 제안입니다. 시간이 지남에 따라 보조-정리의 중요성이 커지고 정리로 고려될 수 있지만 "보조-정리"라는 용어는 보통 그 이름의 일부로 유지됩니다 (예를 들어, 가우스 보조정리, 조온의 보조정리, 및 기본 보조정리).
• 따름-정리(corollary)는 적은 증명 또는 요구된 증명 없이 또 다른 정리 또는 공리에서 즉시 뒤따르는 제안입니다. 따름-정리는 역시 정리를 더 단순한 형식으로 다시 기술하거나, 특별한 경우(special case)에 대한 것일 수 있습니다: 예를 들어, "직사각형에서 모든 내부 각도는 직각입니다"라는 정리는 "정사각형에서 모든 내부 각도는 직각입니다"라는 따름-정리를 가집니다 - 정사각형은 직사각형의 특별한 경우입니다.
• 정리의 일반화(generalization)는 유사한 명제를 가진 정리이지만 더 넓은 범위에서 원래의 정리가 특별한 경우 (따름-정리)로 추론될 수 있습니다.

다른 용어는 역사적 또는 관습적인 이유로 사용될 수도 있습니다. 예를 들어:

• 항등식(identity)은 그것의 도메인 내의 임의의 값에 대해 유지되는 두 표현식 사이의 상등을 나타내는 정리입니다 (예를 들어, 베주의 항등식, 방데르몽드 항등식).
• 규칙(rule)은 유용한 공식을 설립하는 정리입니다 (예를 들어, 베이즈 규칙 및 크라메르의 규칙).
• 법칙(law) 또는 원리(principle)는 넓은 응용가능성을 갖는 정리입니다 (예를 들어, 큰 숫자의 법칙, 코사인의 법칙, 콜모고로프 영–일 법칙, 하르낙의 원리, 최소-위쪽-경계 원리, 및 비둘기집 원리).

몇 가지 잘 알려진 정리는 나눗셈 알고리듬(division algorithm), 오일러 공식(Euler's formula), 바나흐-타르스키 역설(Banach–Tarski paradox)과 같이 훨씬 더 특이한 이름을 가집니다.

Layout

정리와 그 증명은 전형적으로 다음과 같이 구성됩니다:

정리 (그것을 증명한 사람의 이름, 증명의 발견 또는 출판 연도)

정리의 명제 (때때로 제안이라고 불림)

증명

증명의 설명

끝

증명의 끝은 문자 Q.E.D. (quod erat demonstrandum) 또는 기사의 끝을 표시하기 위해 잡지에서 사용한 후 Paul Halmos에 의해 도입된, "증명의 끝"을 의미하는, "□" or "∎"와 같은 묘비(tombstone) 표시 중 하나에 의해 나타낼 수 있습니다.

정확한 스타일은 저자 또는 출판물에 따라 다릅니다. 많은 출판물에서 하우스 스타일(house style)로 조판하기 위한 지침이나 매크로(macros)를 제공합니다.

정리에 사용된 용어의 정확한 의미를 설명하는 정의(definitions)가 정리 앞에 오는 것이 공통적입니다. 증명에 사용되는 많은 제안이나 보조-정리가 정리 앞에 오는 것도 일반적입니다. 어쨌든, 보조-정리는 중첩된 증명이나 정리의 증명 뒤에 제시되는 증명과 함께 정리의 증명에 삽입되는 경우가 있습니다.

정리에 대한 따름-정리는 정리와 그 증명 사이, 또는 증명 바로 뒤에 제시됩니다. 때때로, 따름-정리는 정리를 따르는 이유를 설명하는 자체 증명을 가집니다.

Lore

매년 25만 개 이상의 정리가 증명되는 것으로 추정되어 왔습니다.

"수학자는 커피를 정리로 바꾸는 장치이다(A mathematician is a device for turning coffee into theorems)"라는 유명한 격언은 아마도 Alfréd Rényi 때문일 것이지만, 이는 종종 Rényi의 동료 Paul Erdős (및 Rényi는 Erdős를 생각했을 수도 있음)에 기인하며, 그는 그가 만들어낸 많은 정리들, 그의 협업 횟수와 그의 커피 마시기로 유명합니다.

유한 단순 그룹의 분류(classification of finite simple groups)는 정리의 가장 긴 증명으로 일부에 의해 고려됩니다. 그것은 약 100명의 저자에 의해 작성된 500개의 저널 기사에 수만 페이지로 구성되어 있습니다. 이들 논문들은 함께 완전한 증명을 제공한다고 믿어지고, 여러 진행 중인 프로젝트는 이 증명을 단축하고 단순화하기를 희망합니다. 이 유형의 또 다른 정리는 컴퓨터가 생성한 증명이 인간이 읽기에 너무 긴 네 가지 색깔깔 정리(four color theorem)입니다. 그것은 일반인이 쉽게 이해할 수 있는 정리의 가장 오래 알려진 증명 중 하나입니다.

Theorems in logic

수학적 논리(mathematical logic)에서, 형식 이론(formal theory)은 형식 언어(formal language) 내의 문장의 집합입니다. 문장은 자유 변수를 가지지 않는 잘-형성된 공식(well-formed formula)입니다. 이론의 구성원인 문장은 그 정리 중 하나이고, 이론은 그 정리의 집합입니다. 보통 이론은 논리적 귀결(logical consequence)의 관계 아래에서 닫힌 것으로 이해됩니다. 어떤 설명은 이론을 의미적 귀결(semantic consequence) 관계 ($\models$) 아래에서 닫히는 것으로 정의하고, 다른 설명은 구문적 귀결, 또는 유도-가능성 관계 ($\vdash$) 아래에서 닫는 것으로 정의합니다.

This diagram shows the syntactic entities that can be constructed from formal languages. The symbols and strings of symbols may be broadly divided into nonsense and well-formed formulas. A formal language can be thought of as identical to the set of its well-formed formulas. The set of well-formed formulas may be broadly divided into theorems and non-theorems.

유도-가능성 관계 아래에서 닫히려는 이론에 대해, 그것은 정리가 유도되는 방법을 지정하는 연역적 시스템(deductive system)과 연관되어야 합니다. 연역적 시스템은 명시적으로 기술될 수도 있거나, 그것은 문맥에서 명확하게 될 수도 있습니다. 논리적 귀결의 관계 아래에서 빈 집합의 클로저는 연역적 시스템의 정리인 그들 문장만을 포함하는 집합을 산출합니다.

논리 내에서 용어가 사용되는 넓은 의미에서, 정리를 포함하는 이론은 주어진 의미론과 관련하여, 또는 놓여있는 언어의 표준 해석(interpretation)과 관련하여 불건전(unsound)할 수 있기 때문에 정리가 참일 필요는 없습니다. 불일치(inconsistent)인 이론은 모든 문장을 정리로 가지고 있습니다.

형식 언어의 문장으로 정리의 정의는 형식 증명의 구조와 증명-가능한 공식의 구조를 연구하는 수학의 한 가지인 증명 이론(proof theory) 내에서 유용합니다. 형식 이론과 해석(interpretation)을 통해 의미론을 제공할 수 있는 구조 사이의 관계와 관련된 모델 이론(model theory)에서도 중요합니다.

정리는 해석되지 않은 문장일 수 있지만, 실제로 수학자들은 문장의 의미, 즉, 문장이 표현하는 명제에 더 관심이 있습니다. 형식 정리를 유용하고 흥미롭게 만드는 것은 그것이 참 명제로 해석될 수 있고 그 유도가 그것들의 진리의 증명으로 해석될 수 있다는 것입니다. 해석이 형식 시스템에 대한 참 명제인 정리 (형식 시스템 내에서와 반대됨)를 메타-정리(metatheorem)라고 불립니다.

수학적 논리에서 몇 가지 중요한 정리는 다음과 같습니다:

• Compactness of first-order logic
• Completeness of first-order logic
• Gödel's incompleteness theorems of first-order arithmetic
• Consistency of first-order arithmetic
• Tarski's undefinability theorem
• Church-Turing theorem of undecidability
• Löb's theorem
• Löwenheim–Skolem theorem
• Lindström's theorem
• Craig's theorem
• Cut-elimination theorem

Syntax and semantics

Main articles: Syntax (logic) and Formal semantics (logic)

형식 정리의 개념은 의미론(semantics)을 도입하는 참 제한의 개념과 대조적으로 근본적으로 통사론적입니다. 다른 연역 시스템은 유도 규칙의 가정 (즉, 믿음, 정당화, 또는 기타 양식)에 따라 다른 해석을 산출할 수 있습니다. 형식 시스템의 건전성(soundness)은 그것의 모든 정리가 역시 타당성(validities)인지 여부에 달려 있습니다. 타당성은 임의의 가능한 해석 아래에서 참인 공식입니다 (예를 들어, 고전적 명제 계산법에서, 타당성은 동의어-반복(tautologies)입니다). 형식 시스템은 그것의 모든 정리가 역시 동의어-반복일 때 의미적으로 완전(semantically complete)한 것으로 여겨집니다.

Interpretation of a formal theorem

Main article: Interpretation (logic)

Theorems and theories

Main articles: Theory and Theory (mathematical logic)

See also

• List of theorems
• Fundamental theorem
• Formula
• Inference
• Toy theorem

References

• Boolos, George; Burgess, John; Jeffrey, Richard (2007). Computability and Logic (5th ed.). Cambridge University Press.
• Chiswell, Ian; Hodges, Wilfred (2007). Mathematical Logic. Oxford University Press.
• Enderton, Herbert (2001). A Mathematical Introduction to Logic (2nd ed.). Harcourt Academic Press.
• Heath, Sir Thomas Little (1897). The works of Archimedes. Dover. Retrieved 2009-11-15.
• Hedman, Shawn (2004). A First Course in Logic. Oxford University Press.
• Hinman, Peter (2005). Fundamentals of Mathematical Logic. Wellesley, MA: A K Peters.
• Hoffman, P. (1998). The Man Who Loved Only Numbers: The Story of Paul Erdős and the Search for Mathematical Truth. Hyperion, New York. ISBN 1-85702-829-5.
• Hodges, Wilfrid (1993). Model Theory. Cambridge University Press.
• Hunter, Geoffrey (1996) [1973]. Metalogic: An Introduction to the Metatheory of Standard First Order Logic. University of California Press. ISBN 0-520-02356-0.
• Johnstone, P. T. (1987). Notes on Logic and Set Theory. Cambridge University Press.
• Mates, Benson (1972). Elementary Logic. Oxford University Press. ISBN 0-19-501491-X.
• Monk, J. Donald (1976). Mathematical Logic. Springer-Verlag.
• Petkovsek, Marko; Wilf, Herbert; Zeilberger, Doron (1996). A = B. A.K. Peters, Wellesley, Massachusetts. ISBN 1-56881-063-6.
• Rautenberg, Wolfgang (2010). A Concise Introduction to Mathematical Logic (3rd ed.). Springer.
• van Dalen, Dirk (1994). Logic and Structure (3rd ed.). Springer-Verlag.

External links

• Media related to Theorems at Wikimedia Commons
• Weisstein, Eric W. "Theorem". MathWorld.
• Theorem of the Day