Logic and Proofs 문서 원본 보기

[[분류:계산 이론 개론]]
[[분류:컴퓨터 공학]]
상위 문서: [[계산 이론 개론#Logic and Proofs|계산 이론 개론]]

==개요==
수학적 활동은 결국 수학적 객체(objects)에 대한 명제(assertions)를 세우고 이를 증명(proof)하는 과정이다. 해당 문서에서는 이를 위해 필요한 개념들과, 증명에 필요한 구조에 대해서 다룬다.

==Classification of Theorems==
수학자들은 다양한 종류의 명제를 구분하기 위해서 다양하게 명명했다. 아래는 그 종류에 대한 표이다:
{| class="wikitable"
|+
!개념
!의미
!예시
|-
|Theorem (정리)
|중요하고 의미 있는 결과
|피타고라스 정리
|-
|Proposition (명제)
|작은 정리, 덜 중요한 결과, 또는 증명 없이 인용되는 결과
|.
|-
|Lemma (보조정리)
|더 큰 정리를 증명하기 위해 필요한 중간 결과
|조르당 보조정리
|-
|Conjecture (추측)
|아직 증명되지 않았지만, 많은 증거와 직관으로 참일 것 같다고 믿는 주장
|리만 가설
|}
이외에도 중요도가 낮은 정리를 일컫는 말로 Scholium과 같은 용어가 사용되기도 한다.

==Expressing Mathematical Assertions==
명제를 구성하기 위해서는 여러 개념들이 필요하다. 아래는 그러한 개념들을 정리한 것이다:
{| class="wikitable"
|+
!개념
!의미
!예시
|-
|Predicates(술어/조건식)
|변수에 값을 대입하면 비로소 참/거짓이 결정되는 문장의 틀
|isEven(x) 
|-
|Propositional connectives(명제 연결자)
|참/거짓이 정해진 명제들을 논리적으로 합성해 새로운 명제를 만드는 데 사용
|<math>\neg, \lor, \land, \rightarrow, \leftrightarrow</math>
|-
|Quantifiers(수량자)
|<math>\forall x P(x)</math> = “모든 x에 대해 P(x)”, <math>\exists x P(x)</math> = “어떤 x가 있어서 P(x)”.
|<math>\forall, \exists</math>
|-
|Constants(상수)
|값이 이미 정해져 있는 고정된 기호
|0, 1, 3, π, e
|-
|Variables(변수)
|맥락에 따라 값이 달라지는 기호들<ref>변수가 수량자에 묶여 있는지의 여부를 판단해야 한다. 예를 들어 <math>P(x) \land \forall x Q(x)</math>에서 앞의 x는 자유 변수이지만, 뒤의 x는 수량자에 묶여 있다.</ref>
|<math>x, y</math>
|}

===Variables and Predicates===
조건식은 대상들의 성질/관계에 대해 말해주며, 변수는 대상들을 가리키는 이름에 해당한다. 예를 들어, <math>x \ne 0</math>라는 조건식은 변수 x의 값이 무엇이냐에 따라 참/거짓이 달라진다. 또한 <math>x > y</math>라는 조건식은 x, y라는 두 변수 사이의 관계를 표현한다. 이 역시 변수의 값에 따라 참/거짓이 정해진다. 반면, <math>1+1=2</math>라는 수식은 변수가 없으므로 완전한 명제이며, 특별한 해석 없이도 참/거짓이 결정된다.

===Constants and Definitions===
상수란 고정된 대상을 가리키는 기호이고, 보통 정의(definition)을 통해 규정된다. 이때 정의 방식들 중 하나가 명시적 정의(explicit definition)이다. 명시적 정의란 이미 알려진 표현에 새로 명명하는 것이다. 예를 들면, “googol을 10^100으로 정의한다.”과 같은 방식이다.<br>
이보다 더욱 섬세하게 정의하는 방식이 있다. 먼저 암묵적 정의(implicit definition)이 있는데, 이는 대상을 그 성질로 규정하는 것이다. 예를 들면 “<math>\sqrt{3}</math>을 <math>x^2=3</math>을 만족하는 실수 x로 정의한다.”가 있다. 하지만 이러한 정의를 사용하기 위해서는 “그런 x가 존재하고(Existence), 유일하다(Uniqueness)”를 증명해야 의미가 확정된다.<br>
또다른 정의 방식은 재귀적 정의(recursive definition)으로, 이는 정의되는 대상이 정의식에 자기 자신으로 등장하도록 하는 것이다. 이를 구현하기 위해서는 1) 기초 부분과, 2) 재귀 규칙이 함께 주어져야 한다. 예를 들어:
 <math>f(n) =
 \begin{cases}
 0, & \text{if } n = 0 \\
 n + f(n-1), & \text{if } n > 0
 \end{cases}</math>
이 정의는 삼각수 <math>f(n) = \frac{n(n+1)}{2}</math>를 만든다. 이는 겉보기에는 순환 논리 같지만, 결국 n이 줄어드는 잘 기초화된(well-founded) 순서 위에서라면 모순이 아니다.<ref>본문 예시에서는 f(n)을 정의할 때 항상 더 작은 인자(n-1)를 참조한다.</ref> 이러한 정의를 정당화하기 위해서는 해가 모든 입력 n에 대해 존재하며, 그러한 해가 유일하다는 것을 증명해야 한다.

===Propositional Connectives===
명제를 논리 기호로 결합하여 더욱 복잡한 명제를 만들 수 있다. 예를 들면 아래와 같다:
* <math>x \le 3</math>
* <math>x > 0 \land y < 1</math>
* <math>P \rightarrow Q</math>
이때 복합 명제(compound assertions)의 참/거짓은 진리표에 따라 결정된다.

===Quantifiers===
수량자는 명제 내에서 적용되는 자유 변수의 개수를 줄인다. 예를 들어,
* <math>\forall x. x^2\ne y</math>: 모든 x에 대해 성립하므로, 명제의 참/거짓은 y에만 의존한다.
* <math>\exists x. x^2=y</math>: 어떤 x에 대해 성립하므로, 명제의 참/거짓은 y에만 의존한다.
즉, 수량자가 사용된 명제의 참 거짓은 “남은 변수(여기선 y)”의 값과 정의역에 따라 달라진다. 이때 아래와 같이 유의해야 할 규칙 두가지가 존재한다.
* 수량자의 부정: <math>\neg\forall x. P \equiv \exists x. \neg P</math> / <math>\neg\exists x. P \equiv \forall x. \neg P</math>
* 수량자의 순서: <math>\forall x \exists y. x < y</math>는 참이지만, <math>\exists y \forall x. x < y</math>
수량자는 변수를 묶는 역할을 하기 때문에 제한자(Binders)라고 불리기도 한다. 이때 묶인 변수(bound variable)는 이름을 바꿔도 의미가 유지된다는 특징이 있다:
* 안전한 바꿈(동치): <math>\exists x. x^2 = y \equiv \exists z. z^2 = y</math>
* 의미가 바뀜(동치가 아님): <math>\exists x. x^2 = y \not\equiv \exists y. y^2 = y</math>
** 오른쪽 명제는 기존의 자유 변수였던 y를 새로 묶어버려서 자유 변수 y의 의미가 완전히 바뀌었다.

== Rule of Inference ==
이에 대한 설명은 아래 figure 1으로 대체한다.
[[파일:Figure 1. Rule of Inference.png|대체글=Figure 1. Rule of Inference|가운데|섬네일|1000x1000픽셀|Figure 1. Rule of Inference]]

==[[Mathematical Induction]]==
이에 대한 자세한 설명은 [[Mathematical Induction]] 문서를 참조해 주십시오.

==각주==