자연 연역

"오늘의AI위키"는 AI 기술로 일관성 있고 체계적인 최신 지식을 제공하는 혁신 플랫폼입니다.
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.

1. 개요
2. 역사
3. 자연 연역 논리
4. 형식적 정의
5. 판단과 명제
6. 도입과 소거
7. 가설적 도출
8. 일관성, 완전성, 정규형
9. 고차 논리로의 확장
10. 표기법의 역사 (영어 문서)
11. 겐첸 스타일 명제 논리 (영어 문서)
- 11.1. 겐첸 스타일 추론 규칙
- 11.2. 겐첸 스타일 증명 예시
12. 서페스-레몬 스타일 명제 논리 (영어 문서)
- 12.1. 서페스-레몬 스타일 추론 규칙
참조

1. 개요

자연 연역은 20세기 초 명제 논리의 공리화에 대한 문제점을 해결하기 위해 등장한 논리 체계이다. 게르하르트 겐첸은 1935년 자연 연역 체계를 개발하여 현대 자연 연역의 기반을 마련했으며, '자연 연역'이라는 용어를 처음 사용했다. 이 체계는 추론 규칙만을 사용하여 주어진 식에 변화를 가하며, System L과 같은 다양한 규칙들을 포함한다. 자연 연역은 명제의 유한 열을 통해 연역을 정의하고, 증명의 형식화를 위해 가설적 유도를 사용한다. 또한, 일관성, 완전성, 정규형과 같은 속성을 가지며, 고차 논리로 확장될 수 있다.

더 읽어볼만한 페이지

연역 - 마음
마음은 의식, 사고, 지각, 감정, 동기, 행동, 기억, 학습 등을 포괄하는 심리적 현상과 능력의 총체이며, 다양한 분야에서 연구되고 인간 삶의 중추적인 역할을 한다.
연역 - 통계적 추론
통계적 추론은 표본 데이터를 통해 모집단에 대한 결론을 도출하는 방법론으로, 추정과 가설 검정을 포함하며, 다양한 접근 방식과 통계 모델을 기반으로 여러 분야에서 활용된다.
논리학 - 모순
모순은 논리학, 철학, 과학 등 다양한 분야에서 사용되는 개념으로, 서로 상반되는 두 가지 주장이나 사실이 동시에 존재하는 상태를 의미하며, 특히 헤겔과 마르크스의 변증법적 유물론에서 사물의 내재적 대립으로서 역사 발전의 원동력으로 간주된다.
논리학 - 특수
특수는 철학에서는 개별적이고 구체적인 존재를, 언어학에서는 눈에 띄는 또는 예외적인 의미를 가지며, 사회적으로 특별함이 중요하게 여겨지기도 한다.

자연 연역
개요
종류	증명 이론
분야	논리학
다른 이름	젠첸 시스템
역사적 맥락
창시자	게르하르트 젠첸 스타니스와프 야시코프스키
창시 시기	1930년대
영향 받은 분야	증명 이론 타입 이론 구성적 논리
주요 특징	추론 규칙을 사용하여 논리적 주장을 구축
구조 및 규칙
기본 개념	가정 결론 추론 규칙
주요 규칙	도입 규칙 제거 규칙
예시
명제 논리 예시	가정: A → B, A 결론: B
술어 논리 예시	가정: ∀x P(x) 결론: P(a) (a는 임의의 대상)
활용 분야
논리적 추론	복잡한 논리적 주장의 정당성 검증
프로그램 검증	프로그램의 정확성 증명
지식 표현	지식 기반 시스템 구축
장점 및 단점
장점	직관적인 추론 과정 다양한 논리 시스템에 적용 가능
단점	복잡한 증명 구성의 어려움 자동화된 증명 시스템 개발의 어려움
관련 개념
관련 개념	힐베르트 스타일 연역 시스템 시퀀트 계산 증명 탐색
참고 문헌
주요 참고 문헌	Gentzen, G. (1935). Untersuchungen über das logische Schliessen. Mathematische Zeitschrift, 39, 176-210, 405-431. Prawitz, D. (1965). Natural Deduction: A Proof-Theoretical Study.
외부 링크
외부 링크	Internet Encyclopedia of Philosophy: Natural Deduction

2. 역사

자연 연역은 20세기 초 힐베르트, 프레게, 러셀 등이 제시한 명제 논리의 공리화 방식(힐베르트 시스템 등)에 대한 문제의식에서 비롯되었다. 이러한 공리화 방식의 대표적인 예는 러셀과 화이트헤드가 저술한 『수학 원리』(Principia Mathematica)에서 찾아볼 수 있다.

1926년 폴란드에서 열린 세미나에서 얀 우카시에비치(Jan Łukasiewicz)는 논리를 보다 자연스러운 방식으로 다룰 필요성을 제기했다. 이에 영향을 받은 스타니스와프 야시코프스키(Stanisław Jaśkowski)는 1929년 다이어그램 기법을 활용한 자연스러운 연역 방식을 처음으로 시도했고, 이후 1934년과 1935년에 걸쳐 발표한 논문들을 통해 자신의 아이디어를 발전시켰다.^[2] 야시코프스키의 연구는 이후 피치 스타일 미적분(Fitch-style calculus)이나 패트릭 서피스(Patrick Suppes)의 방법론으로 이어졌으며, 존 레몬(John Lemmon)은 이를 변형하여 서피스-레몬 표기법(Suppes-Lemmon notation)을 제시하기도 했다. 그러나 당시 야시코프스키의 연구는 널리 알려지지 못했다.

현대 자연 연역의 기반은 독일의 수학자 게르하르트 겐첸(Gerhard Gentzen)이 1935년 괴팅겐 대학교 수학부에 제출한 학위 논문에서 독립적으로 개발하여 제시한 체계이다.^[3] '자연 연역'(natürliches Schließen|나튀를리헤스 슐리센^de)이라는 용어 역시 이 논문에서 처음 사용되었다. 겐첸은 논문에서 다음과 같이 밝혔다.

: "처음 나는 실제 추론에 최대한 가까운 형식을 만들고 싶었다. 그리하여 '자연 연역의 미적분'(Kalkül des natürlichen Schließens^de)이 생겨났다."^[4] (원문: Ich wollte nun zunächst einmal einen Formalismus aufstellen, der dem wirklichen Schließen möglichst nahe kommt. So ergab sich ein "Kalkül des natürlichen Schließens".^de)

겐첸은 수론(페아노 공리계)의 일관성을 증명하기 위해 자연 연역을 활용하고자 했으나, 증명의 복잡성 때문에 어려움을 겪었다. 이 문제를 해결하기 위해 그는 1938년 시퀀트 계산(sequent calculus)이라는 새로운 증명 체계를 고안하여 고전 논리와 직관주의 논리 모두에 대한 단절 제거 정리(Hauptsatz)를 증명했다.

이후 1961년과 1962년에 열린 세미나를 통해 다그 프라비츠(Dag Prawitz)는 자연 연역을 포괄적으로 정리하기 시작했다. 그의 1965년 저서 『자연 연역: 증명 이론적 연구』(Natural deduction: a proof-theoretical study)^[5]는 자연 연역에 대한 중요한 참고 자료로 자리 잡았으며, 양상 논리와 2차 술어 논리 등 다양한 분야로의 응용 가능성을 제시하며 현대 자연 연역의 최종적인 형태를 구축하는 데 기여했다. 현재 사용되는 자연 연역 시스템은 겐첸과 프라비츠의 형식을 따르면서도, 페르 마틴-뢰프(Per Martin-Löf)의 논리적 판단과 연결사에 대한 설명 방식의 영향도 받은 형태이다.^[6]

3. 자연 연역 논리

자연 연역은 명제 논리의 공리화에 대한 대안으로 등장했으며, 대표적인 예로 존 레몬이 개발한 체계 L이 있다. 이 체계는 공리를 가지지 않고, 주어진 식에 정해진 변화를 가하는 추론규칙만을 사용한다. System L은 증명의 구문 규칙에 관한 9가지 기본 추론 규칙을 가진다.^[2]^[3]

System L의 9가지 기본 추론 규칙
번호	규칙명 (영문명)	약자
1	가정 규칙 (The Rule of Assumption)	A
2	전건 긍정 (Modus Ponendo Ponens)	MPP
3	이중 부정 규칙 (The Rule of Double Negation)	DN
4	조건 증명 규칙 (The Rule of Conditional Proof)	CP
5	∧-도입 규칙 (The Rule of ∧-introduction)	∧I
6	∧-제거 규칙 (The Rule of ∧-elimination)	∧E
7	∨-도입 규칙 (The Rule of ∨-introduction)	∨I
8	∨-제거 규칙 (The Rule of ∨-elimination)	∨E
9	귀류법 (Reductio Ad Absurdum)	RAA

System L에서 증명은 다음 조건들을 만족하는 것으로 정의된다.

# 정형논리식 (wff)의 유한한 열(sequence)로 이루어진다.

# 각 행은 L의 추론 규칙에 의해 정당화된다. 즉, 규칙에 따라 논리적으로 타당하게 도출되어야 한다.

# 증명의 마지막 행이 '결론'이 되며, 이 결론은 증명 과정에서 도입된 '전제'(들)만을 사용하여 유도되어야 한다. 전제는 없을 수도 있다.

만약 어떤 증명이 전제를 가지지 않는다면, 그 증명의 결론을 정리(theorem)라고 부른다. 즉, L에서 정리는 공집합인 전제 집합으로부터 L의 규칙만을 사용하여 증명 가능한 논리식을 의미한다.

증명을 표기할 때는 각 행 옆에 해당 논리식이 어떤 규칙과 어떤 이전 행들을 근거로 도출되었는지 명시한다. 다음은 System L을 이용한 증명의 예시이다.

'''후건 부정 (Modus Tollens, MTT) 증명 예시'''

전제 번호	행 번호	논리식 (wff)	근거가 되는 규칙 및 행
p → q, ¬q ⊢ ¬p
1	(1)	(p → q)	A
2	(2)	¬q	A
3	(3)	p	A (for RAA)
1, 3	(4)	q	1, 3, MPP
1, 2, 3	(5)	q ∧ ¬q	2, 4, ∧I
1, 2	(6)	¬p	3, 5, RAA
증명 완료 (Q.E.D)

'''배중률 증명 예시'''

전제 번호	행 번호	논리식 (wff)	근거가 되는 규칙 및 행
⊢ p ∨ ¬p
1	(1)	¬(p ∨ ¬p)	A (for RAA)
2	(2)	¬p	A (for RAA)
2	(3)	(p ∨ ¬p)	2, ∨I
1, 2	(4)	(p ∨ ¬p) ∧ ¬(p ∨ ¬p)	1, 3, ∧I
1	(5)	¬¬p	2, 4, RAA
1	(6)	p	5, DN
1	(7)	(p ∨ ¬p)	6, ∨I
1	(8)	(p ∨ ¬p) ∧ ¬(p ∨ ¬p)	1, 7, ∧I
	(9)	¬¬(p ∨ ¬p)	1, 8, RAA
	(10)	(p ∨ ¬p)	9, DN
증명 완료 (Q.E.D)

System L의 각 규칙은 입력으로 받아들일 수 있는 논리식의 형태와 그 입력에 사용된 전제를 처리하는 방식이 정해져 있다. 증명 표기법으로는 위 예시에서 사용된 표(tabular) 형식 외에도 Fitch diagram 등이 사용되지만, 근본적인 논리 체계는 동일하다. 자연 연역 체계는 게르하르트 겐첸과 프라비츠의 연구를 통해 발전했으며, 현대 논리학에서 중요한 위치를 차지한다.^[5]^[6]

4. 형식적 정의

형식 언어 $\mathcal{L}$ 은 명제 논리의 재귀적 정의를 통해 정의되는 경우가 많다. 예를 들어 데이비드 보스톡은 다음과 같이 정의한다.^[18]

# 각 명제 변수는 식이다.

# " $\top$ " (참) 와 " $\bot$ " (거짓)는 식이다.

# 만약 $\varphi$ 가 식이라면, $\neg\varphi$ (부정)도 식이다.

# 만약 $\varphi$ 와 $\psi$ 가 식이라면, $(\varphi \land \psi)$ (논리곱), $(\varphi \lor \psi)$ (논리합), $(\varphi \to \psi)$ (함의), $(\varphi \leftrightarrow \psi)$ (동치)도 식이다.

# 위에 해당하지 않는 것은 식이 아니다.

이 외에도 BNF 문법 $\phi ::= a_1, a_2, \ldots ~ | ~ \neg\phi ~ | ~ \phi ~ \land ~ \psi ~ | ~ \phi \vee \psi ~ | ~ \phi \rightarrow \psi ~ | ~ \phi \leftrightarrow \psi$ 와 같은 다른 방법들이 있다.^[19]^[21]

'''연역'''(또는 '''증명''')은 명제 논리와 같은 형식 체계의 문맥에서 정확하게 정의할 수 있다. 명제의 유한한 열 ''β₁ ,..., β_n''이 전제 집합 Σ로부터 결론 α의 '''연역'''이라는 것은 다음이 성립하는 경우이다.

''β_n = α'' 이고,
모든 1 ≤ ''i'' ≤ ''n''에 대하여, ''β_i''가 전제이거나(즉, ''β_i'' ∈ Σ) 또는 ''β_i''가 그 이전에 출현한 명제에 어떠한 추론 규칙을 적용한 결과이다.

공리적 명제 논리의 버전에 따라 채택하는 공리와 추론 규칙이 다르다. 예를 들어, 고틀로프 프레게는 6개의 공리와 2개의 규칙을 채택했고, 버트런드 러셀과 알프레드 노스 화이트헤드는 프린키피아 마테마티카에서 5개의 공리로 구성된 체계를 제시했다.

얀 우카시에비치에 의한 공리적 명제 논리의 버전에서는, 다음과 같은 공리군 ''A''를 채택했다.

[PL1] ''p'' → (''q'' → ''p'')
[PL2] (''p'' → (''q'' → ''r'')) → ((''p'' → ''q'') → (''p'' → ''r''))
[PL3] (¬''p'' → ¬''q'') → (''q'' → ''p'')

그리고, 추론 규칙 ''R''로는, 전건긍정(Modus Ponens, MP)을 채택했다.

[MP] α와 α → β로부터, β를 추론한다.

추론 규칙에 의해, Σ에 포함된 논리식과 공리군으로부터 새로운 논리식을 도출할 수 있다.

다음은 가장 일반적인 논리 연결자의 표기 변형을 나타낸 표이다.^[8]^[9]

연결자의 표기 변형
연결자	기호
AND (그리고)	$A \land B$ , $A \cdot B$ , $AB$ , $A \& B$ , $A \&\& B$
동치 (같음)	$A \equiv B$ , $A \Leftrightarrow B$ , $A \leftrightharpoons B$
함축 (이면)	$A \Rightarrow B$ , $A \supset B$ , $A \rightarrow B$
NAND (AND 부정)	$A \overline{\land} B$ , $A \mid B$ , $\overline{A \cdot B}$
비동치 (같지 않음)	$A \not\equiv B$ , $A \not\Leftrightarrow B$ , $A \nleftrightarrow B$
NOR (OR 부정)	$A \overline{\lor} B$ , $A \downarrow B$ , $\overline{A+B}$
NOT (아님)	$\neg A$ , $-A$ , $\overline{A}$ , $\sim A$
OR (또는)	$A \lor B$ , $A + B$ , $A \mid B$ , $A \parallel B$
XNOR (동치 부정)	$A$ XNOR $B$
XOR (배타적 OR)	$A \underline{\lor} B$ , $A \oplus B$

5. 판단과 명제

판단이란 지식의 대상, 즉 인식 가능한 것을 의미한다. 어떤 지식이 실제로 알려져 있다면, 그것은 자명하다고 할 수 있다. 예를 들어 "비가 내리고 있다"는 판단이며, 실제로 비가 내리는 것을 아는 사람에게는 자명한 사실이다. 이때 증거는 직접 관찰을 통해 쉽게 얻을 수 있다. 하지만 수리 논리학에서는 증거가 직접 관찰 불가능한 경우가 많으며, 대신 더 기본적인 자명한 판단들로부터 연역 과정을 통해 유도된다. 이 연역 과정이 바로 증명을 구성하며, 어떤 판단은 그 증명을 알 때 자명해진다.

논리에서 가장 중요한 판단은 "A는 참이다"라는 형태이다. 여기서 A는 어떤 명제를 나타내는 표현으로 대체될 수 있다. 이 참/거짓 판단은 더 기본적인 판단, 즉 "A는 명제이다"라는 판단을 필요로 한다. 자연 연역에서는 이 두 기본적인 판단을 각각 "''A'' prop" (A는 명제이다)와 "''A'' true" (A는 참이다)라는 약자로 표기한다. 그 외에도 "A는 거짓이다"(논리학), "A는 시각 t에서는 참이다"(시상 논리), "A는 참이어야 한다" 또는 "A는 참일 수 있다"(양상 논리학), "프로그램 M의 형은 τ이다"(프로그래밍 언어와 형 이론), "A는 이용 가능한 자원으로부터 달성할 수 있다"(선형 논리) 등 다양한 판단이 연구되고 있다.

명제를 구성하는 규칙을 '''형성 규칙'''(formation rule)이라고 부른다. 형성 규칙은 이미 자명한 판단들(전제)로부터 새로운 판단(결론)을 이끌어내는 방법을 제시한다. 일반적인 형태는 다음과 같다.

: $\frac{J_1 \qquad J_2 \qquad \cdots \qquad J_n}{J}\ \hbox{name}$

여기서 $J_1, J_2, ..., J_n$ 은 '''전제'''(premise)라 불리는 이미 알려진 판단들이고, $J$ 는 이들로부터 도출되는 '''결론'''(conclusion)이다. "name"은 이 추론 규칙의 이름이다.

예를 들어, ''A''와 ''B''가 이미 명제임이 알려져 있을 때 (즉, "''A'' prop"와 "''B'' prop"가 자명할 때), 이 둘을 결합하여 새로운 복합 명제인 논리곱 $A \wedge B$ 를 형성할 수 있다. 이를 형성 규칙으로 나타내면 다음과 같다.

: $\frac{A\hbox{ prop} \qquad B\hbox{ prop}}{(A \wedge B)\hbox{ prop}}\ \wedge_F$

형성 규칙은 단지 명제가 올바르게 구성될 수 있음을 보여줄 뿐, 그 명제가 참임을 의미하지는 않는다. 마찬가지로 논리합( $A \vee B$ ), 부정( $\neg A$ ), 함의( $A \supset B$ )와 같은 다른 논리 연산자들과 논리 상수인 참( $\top$ )과 거짓( $\bot$ )에 대해서도 형성 규칙이 존재한다.

: $\frac{A\hbox{ prop} \qquad B\hbox{ prop}}{A \vee B\hbox{ prop}}\ \vee_F \qquad \frac{A\hbox{ prop} \qquad B\hbox{ prop}}{A \supset B\hbox{ prop}}\ \supset_F$

: $\frac{\hbox{ }}{\top\hbox{ prop}}\ \top_F \qquad \frac{\hbox{ }}{\bot\hbox{ prop}}\ \bot_F \qquad \frac{A\hbox{ prop}}{\neg A\hbox{ prop}}\ \neg_F$

6. 도입과 소거

참인 명제로부터 참인 명제를 이끌어내는 생성규칙을 '''추론 규칙'''(inference rules)이라 부른다.

참인 명제에서 더 복합적인 참인 명제를 구성하는 추론규칙을 '''도입 규칙'''(introduction rules)이라 한다. 예를 들어 논리곱을 도입하는 연언 도입은 명제 "A가 참이다"와 "B가 참이다"에서 "A 그리고 B가 참이다"라는 결론을 이끌어낸다. 이를 추론규칙으로 표기하면 다음과 같다. 이때 각 대상이 명제라는 것은 자명하다고 본다.

: $\frac{A\hbox{ true} \qquad B\hbox{ true}}{(A \wedge B)\hbox{ true}}\ \wedge_I$

정확히 표현하면 다음과 같다.

: $\frac{A\hbox{ prop} \qquad B\hbox{ prop} \qquad A\hbox{ true} \qquad B\hbox{ true}}{(A \wedge B) \hbox{ true}}\ \wedge_I$

아래는 여러 도입 규칙들이다.

논리곱을 도입하는 연언 도입:

::

\frac{A \qquad B}{(A \wedge B)}\ \wedge_I

논리합을 도입하는 선언 도입. 명제의 진리치가 세워지는 과정이 1가지가 아니므로 선언 도입은 사실 2가지 규칙의 총칭이다:

::

\frac{A}{(A \vee B)}\ \vee_I\qquad\frac{B}{(A \vee B)}\ \vee_I

항진 도입. 항진(참, ⊤)은 전제가 전혀 없는 경우에도 도출된다:

::

\frac{\ }{\top\hbox{ true}}\ \top_I

한편, 아무 전제도 없이 모순(거짓, ⊥)을 도입하는 도입규칙은 존재하지 않는다. 따라서 더 단순한 판단으로부터 거짓을 추론해내는 것은 불가능하다.

도입규칙의 반대 꼴이 되는 '''소거 규칙'''(elimination rules)이라는 것이 존재하는데, 이는 거꾸로 복합적인 명제를 해체해내는 추론규칙이다. 예를 들어 논리곱을 제거하는 연언 소거가 있다. "''A ∧ B'' true"로부터 "''A'' true"와 "''B'' true"를 결론으로 할 수 있다.

:

\frac{A \wedge B\hbox{ true}}{A\hbox{ true}}\ \wedge_{E1}\qquad\frac{A \wedge B\hbox{ true}}{B\hbox{ true}}\ \wedge_{E2}

혹은 간단히 다음과 같이 표기한다.

:

\frac{A \wedge B}{A}\ \wedge_E\qquad\frac{A \wedge B}{B}\ \wedge_E

추론규칙들을 적용하여 다음과 같이 논리곱의 교환 법칙을 증명할 수 있다. 즉, ''A ∧ B''가 참이면, ''B ∧ A''도 참임을 보이는 과정이다.

:

\cfrac{\cfrac{A \wedge B\hbox{ true}}{B\hbox{ true}}\ \wedge_{E2}\qquad\cfrac{A \wedge B\hbox{ true}}{A\hbox{ true}}\ \wedge_{E1}}{B \wedge A\hbox{ true}}\ \wedge_I

7. 가설적 도출

논리학에서는 어떤 주장이 참이라고 가정하고 그로부터 다른 주장을 이끌어내는 추론 방식을 사용하는데, 이를 가설적 도출(hypothetical derivation)이라고 한다. 이는 "가정으로부터의 추론(reasoning from assumptions)"에 해당한다.

만약 'A가 참'이라고 가정했을 때 'B가 참'이라는 결론을 얻었다면, 이를 다음과 같이 표기한다.

$\begin{matrix}[A] \\\vdots \\B \\\end{matrix}$

여기서 대괄호 `[A]`는 'A를 가정한다'는 의미이며, 이 가정(가설)은 추론 과정 중에 사용되고 결론에 도달하면 해제(discharge)될 수 있다. 예를 들어, ''A ∧ (B ∧ C)''가 참이라고 가정하면 ''B''가 참임을 도출할 수 있는데, 이는 ''B true''라는 판단이 ''A ∧ (B ∧ C) true''라는 판단에 의존함을 보여준다.

$\begin{matrix}A \wedge \left ( B \wedge C \right ) \ true \\\vdots \\B \ true\end{matrix}$

이것의 의미는 "'B true'는 'A ∧ (B ∧ C) true'로부터 도출 가능하다"가 된다.

가설적 도출의 일반적인 형태는 다음과 같다. 맨 윗줄에는 여러 전건(antecedent derivations, D_i)이, 마지막 줄에는 하나의 후건 판단(succedent judgement, J)이 온다.

$\begin{matrix}D_1 \quad D_2 \cdots D_n \\\vdots \\J\end{matrix}$

이와 관련된 중요한 추론 규칙은 함의 도입(Implication introduction)이다. 'A가 참'이라고 가정하여 'B가 참'임을 성공적으로 도출했다면, '만약 A이면 B이다' 즉, '(A ⊃ B)'가 참이라고 결론 내릴 수 있다. 도입 규칙에서 가설 ''u''는 결론에 나타나지 않는데, 이는 가설의 "범위"를 한정하여 해당 가설이 오직 "''B true''"를 확립하는 데에만 사용되었음을 명확히 한다.

$\cfrac{\begin{matrix}\cfrac{}{A \ true} u \\\vdots \\B \ true\end{matrix}}{A \supset B \ true} \supset I^u\qquad \cfrac{A \supset B \ true \quad A \ true}{B \ true} \supset E$

예시로, ''A ⊃ (B ⊃ (A ∧ B)) true''의 도출 과정은 다음과 같다. 여기서 ''u''와 ''w''는 각각 ''A true''와 ''B true'' 가설을 나타내며, 각 단계에서 해제된다.

$\cfrac{\cfrac{\cfrac{}{A \ true} u \quad \cfrac{}{B \ true} w}{A \wedge B \ true}\wedge I}{\cfrac{B \supset \left ( A \wedge B \right ) \ true}{A \supset \left ( B \supset \left ( A \wedge B \right ) \right ) \ true} \supset I^u} \supset I^w$

가설적 도출은 증명을 더 형식적으로 다룰 때 유용하다. 이를 위해 가설에 '증명 변수'(예: ''u'', ''w'')를 부여하고, 가정(Γ)과 결론(J)을 '턴스타일'(⊢) 기호로 구분하여 `Γ ⊢ J` ('가설 Γ로부터 결론 J를 도출할 수 있다')와 같이 표기하기도 한다. 이를 '국소화된 가설'(localized hypotheses)이라고 부르기도 한다.

⇒

증명을 명시적으로 나타낼 때는 "π : ''A''"와 같이 표기하며, 이는 "π는 ''A''의 증명이다"라는 의미이다. 가장 간단한 증명은 레이블이 붙은 가설 자체를 사용하는 것이다.

이러한 형식화는 Curry–Howard 동형 사상을 통해 증명과 람다 대수의 계산 과정을 연결 짓는다. 예를 들어, 함의 도입 규칙(⊃I)은 람다 추상화(λu. π)에, 함의 제거 규칙(⊃E)은 함수 적용(π₁ π₂)에 대응된다.

마찬가지로, 논리곱(∧)의 도입(∧I)은 증명의 쌍 ((π₁, π₂)) 생성에, 제거(∧E)는 쌍의 첫 번째(fst) 또는 두 번째(snd) 요소를 추출하는 것에 대응된다.

가설적 도출은 다른 논리 연산자의 추론 규칙에서도 사용된다.

논리합 (∨): 논리합 제거 규칙(∨E)은 ''A ∨ B''가 참이고, 'A를 가정했을 때 C가 도출'되며 'B를 가정했을 때도 C가 도출'된다면, C가 참이라고 결론짓는다. 여기서 ''A true''나 ''B true'' 자체가 보증되는 것은 아니다.

\cfrac{    A \vee B \hbox{ true}    \quad    \begin{matrix}    \cfrac{}{A \ true} u \\    \vdots \\    C \ true    \end{matrix}    \quad    \begin{matrix}    \cfrac{}{B \ true} w \\    \vdots \\    C \ true    \end{matrix}    }{C \ true} \vee E^{u,w}

거짓 (⊥): 거짓 제거 규칙(⊥E), 또는 폭발 원리(Principle of Explosion)는 거짓(모순)이 참이라면 어떤 명제 C든 참이라고 추론할 수 있음을 나타낸다.

\frac{\perp true}{C \ true} \perp E

부정 (¬): 부정은 함의와 유사하게 다뤄지며, 종종 ''¬A''를 ''A ⊃ ⊥'' (A이면 모순이다)로 정의한다.
부정 도입(¬I): 'A가 참'이라고 가정했을 때 모순(⊥, 또는 임의의 명제 ''p''와 그 부정 ¬''p''가 동시에 참인 상황)이 도출된다면, 'A는 거짓(¬A)'이라고 결론 내릴 수 있다. 규칙에서 가설 ''u''와 모순을 나타내는 후건 ''p''는 결론에 나타나지 않는다.

\cfrac{        \begin{matrix}        \cfrac{}{A \ true} u \\        \vdots \\        p \ true \quad (\text{where } p \text{ represents contradiction, e.g., } \perp)        \end{matrix}        }{\lnot A \ true} \lnot I^{u,p}

부정 제거(¬E): '¬A'와 'A'가 모두 참이라면 모순이 발생하므로, 어떤 명제 C든 참이라고 결론 내릴 수 있다 (거짓 제거 규칙과 유사).

\cfrac{\lnot A \ true \quad A \ true}{C \ true} \lnot E

이 규칙들을 통해 ''¬A''와 ''A ⊃ ⊥''가 논리적으로 동등함(서로 도출 가능함)을 쉽게 알 수 있다.

8. 일관성, 완전성, 정규형

수리논리에서 어떤 형식적 이론이 모순을 추론할 수 없을 때 그 이론은 일관적(consistent) 또는 무모순적이라고 한다. 또한, 참인 모든 문장을 추론 규칙을 통해 도출할 수 있을 때 그 이론은 완전하다(complete)고 한다. 이러한 개념들은 주로 모델론적 방식으로 이해되지만, 증명론에서는 제한된 의미의 일관성과 완전성을 순수하게 구문론적인 방식으로 확인할 수도 있다.
국소적 일관성(Local consistency) 또는 국소적 환원 가능성은 어떤 연결사의 도입 규칙 바로 뒤에 같은 연결사의 소거 규칙이 사용된 경우, 이러한 '우회'가 없는 동등한 유도 과정으로 변환될 수 있음을 의미한다.^[24] 이는 소거 규칙이 불필요하게 강력하여 전제에 없던 정보를 만들어내지 않는다는 것을 보여준다. 예를 들어, 논리곱(∧)의 경우, A와 B로부터 'A ∧ B'를 도입한 뒤 바로 소거하여 A를 얻는 과정은 단순히 처음부터 A를 사용하는 과정으로 축약될 수 있다.

: $\begin{aligned}\cfrac{\cfrac{\cfrac{}{A\ }u\qquad\cfrac{}{B\ }w}{A \wedge B\ }\wedge_I}{A\ }\wedge_{E1}\end{aligned}\quad\Rightarrow\quad\cfrac{}{A\ }u$
국소적 완전성(Local completeness)은 국소적 일관성과 쌍대적인 개념으로, 소거 규칙이 충분히 강력하여 원래의 연결사를 다시 구성(도입)할 수 있음을 의미한다.^[24] 즉, 소거 규칙을 적용하여 얻은 요소들로부터 다시 원래의 연결사를 도입 규칙을 통해 만들어낼 수 있다는 것이다. 예를 들어, 'A ∧ B'라는 식에 논리곱 소거 규칙을 적용하여 A와 B를 각각 얻고, 이 둘로부터 다시 논리곱 도입 규칙을 사용해 'A ∧ B'를 만드는 과정으로 변환할 수 있다.

: $\cfrac{}{A \wedge B\ }u \quad \Rightarrow \quad \begin{aligned}\cfrac{\cfrac{\cfrac{}{A \wedge B\ }u}{A\ }\wedge_{E1} \qquad \cfrac{\cfrac{}{A \wedge B\ }u}{B\ }\wedge_{E2}}{A \wedge B\ }\wedge_I\end{aligned}$

커리-하워드 대응에 따르면, 국소적 일관성은 람다 계산에서의 β-축약에 해당하고, 국소적 완전성은 η-변환에 해당한다.^[24]

모든 소거 규칙이 모든 도입 규칙보다 먼저 나타나도록, 즉 소거 후에 도입이 이루어지는 순서로 구성된 유도를 정규 유도(normal derivation)라고 한다. 대부분의 논리 체계에서는 어떤 유도 과정이든 그와 동등한 정규 유도로 변환할 수 있으며, 이렇게 변환된 유도를 정규형(normal form)이라고 부른다.^[24] 정규형의 존재는 자연 연역 체계 내에서 직접 증명하기는 다소 복잡하지만, 1961년 다그 프라비츠의 연구 등 여러 방법을 통해 증명되었다.^[24] 특히, 컷 규칙(cut rule)이 없는 시퀀트 계산을 이용하면 정규형의 존재를 간접적으로 더 쉽게 보일 수 있다.^[24]

컷 규칙은 추론 규칙으로서는 불필요하지만, 메타 정리로서 증명될 수 있다. 컷 규칙을 제거할 수 있다는 사실(Cut 제거)은 자연 연역 연구에 중요한 의미를 가진다. 예를 들어, 어떤 명제가 자연 연역에서 증명 불가능함을 보일 때, 컷 규칙이 없는 시퀀트 계산을 사용하면 증명 탐색의 범위를 유한하게 제한할 수 있어 증명이 훨씬 용이해진다. 이는 컷 없는 시퀀트 계산에서는 모든 규칙이 결론의 부분 명제와 관련된 연결사만을 다루기 때문이다. 대표적인 예로, "거짓(⊥)은 아무 전제 없이 증명될 수 없다"는 전역적 일관성 정리는 컷 없는 시퀀트 계산에서 자명하게 확인된다.

9. 고차 논리로의 확장

(임의의 항 a에 대해 [a/x]A가 참임을 보이면, ∀x.A가 참이다. 단, a는 결론에 나타나지 않아야 한다.) $\cfrac{\forall x. A \text{ true} \qquad t \text{ term}}{[t/x] A \text{ true}} \;\forall_{E}$
(∀x.A가 참이고 t가 항이면, [t/x]A도 참이다.)존재 양화사 (∃) $\cfrac{[t/x] A \text{ true}}{\exists x. A \text{ true}} \;\exists_{I}$
(어떤 항 t에 대해 [t/x]A가 참이면, ∃x.A가 참이다.) $\cfrac{\begin{array}{cc} & \underbrace{\,\cfrac{}{a \text{ term}}\hbox{ u} \quad \cfrac{}{[a/x]A \text{ true}}\hbox{ v}\,}\\ & \vdots \\ \exists x. A \text{ true} \quad & C \text{ true} \\ \end{array}}{C \text{ true}} \;\exists_{E^{a,u,v}}$
(∃x.A가 참이고, 임의의 항 a에 대해 [a/x]A가 참이라는 가정(v) 하에 C가 참임을 보일 수 있다면, C는 참이다. 단, a는 C나 다른 가정에 나타나지 않아야 하며, 가정 u, v는 해당 증명 부분에서만 유효하다.)

규칙	설명
$\cfrac{\begin{matrix} \cfrac{}{p \text{ prop}}\hbox{ u} \\ \vdots \\ A \text{ prop} \\ \end{matrix}}{\forall p. A \text{ prop}} \;\forall_{F^u}$	명제 변수 p에 대해 명제 A가 성립하면, "모든 명제 p에 대해 A"도 명제이다.
$\cfrac{\begin{matrix} \cfrac{}{p \text{ prop}}\hbox{ u} \\ \vdots \\ A \text{ prop} \\ \end{matrix}}{\exists p. A \text{ prop}} \;\exists_{F^u}$	명제 변수 p에 대해 명제 A가 성립하면, "어떤 명제 p에 대해 A"도 명제이다.

타입	형성 규칙 (Formation)
Π-타입 (종속 함수 타입)	$\frac{\Gamma \vdash A \text{ type} \qquad \Gamma, x:A \vdash B \text{ type}}{\Gamma \vdash \Pi x:A. B \text{ type}} \;\Pi\text{-F}$
Σ-타입 (종속 곱 타입)	$\frac{\Gamma \vdash A \text{ type} \qquad \Gamma, x:A \vdash B \text{ type}}{\Gamma \vdash \Sigma x:A. B \text{ type}} \;\Sigma\text{-F}$

타입	도입 규칙 (Introduction)	제거 규칙 (Elimination)
Π-타입	$\frac{\Gamma, x:A \vdash \pi : B}{\Gamma \vdash \lambda x. \pi : \Pi x:A. B} \;\Pi\text{I}$	$\frac{\Gamma \vdash \pi_1 : \Pi x:A. B \quad \Gamma \vdash \pi_2 : A}{\Gamma \vdash \pi_1 \pi_2 : [\pi_2/x] B} \;\Pi\text{E}$
Σ-타입	$\frac{\Gamma \vdash \pi_1 : A \qquad \Gamma, x:A \vdash \pi_2 : B}{\Gamma \vdash (\pi_1, \pi_2) : \Sigma x:A. B} \;\Sigma\text{I}$	$\frac{\Gamma \vdash \pi : \Sigma x:A. B}{\Gamma \vdash \mathbf{fst}\ \pi : A} \;\Sigma\text{E}_1$ $\frac{\Gamma \vdash \pi : \Sigma x:A. B}{\Gamma \vdash \mathbf{snd}\ \pi : [\mathbf{fst}\ \pi/x] B} \;\Sigma\text{E}_2$

가정 집합	줄 번호	증명 문장	주석
1	1	$P \to Q$	A
2	2	$-Q$	A
3	3	$P$	A
1, 3	4	$Q$	1, 3 →E
1, 2	5	$-P$	2, 4 RAA

가정 집합	줄 번호	증명 문장	주석
1	1	$P \to Q$	A
2	2	$-Q$	A
3	3	$P$	A
1, 3	4	$Q$	1, 3 →E
1, 2	5	$-P$	2, 4 RAA

자연 연역

1. 개요

더 읽어볼만한 페이지

2. 역사

3. 자연 연역 논리

4. 형식적 정의

5. 판단과 명제

6. 도입과 소거

7. 가설적 도출

8. 일관성, 완전성, 정규형

9. 고차 논리로의 확장

10. 표기법의 역사 (영어 문서)

11. 겐첸 스타일 명제 논리 (영어 문서)

11. 1. 겐첸 스타일 추론 규칙

11. 2. 겐첸 스타일 증명 예시

12. 서페스-레몬 스타일 명제 논리 (영어 문서)

12. 1. 서페스-레몬 스타일 추론 규칙

참조

규칙 이름	다른 이름	주석	가정 집합	명제
가정 규칙^[22]	가정^[17]	A^[22]^[17]	현재 줄 번호.^[17]	논증의 어느 단계에서든, 논증의 가정으로 명제를 도입한다.^[22]^[17]
결합 도입	앰퍼샌드 도입,^[22]^[17] 결합(CONJ)^[17]^[23]	m, n &I^[17]^[22]	m과 n 줄의 가정 집합의 합집합.^[17]	m과 n 줄에서 $\varphi$ 와 $\psi$ 로부터 $\varphi ~ \& ~ \psi$ 를 추론한다.^[22]^[17]
결합 제거	단순화(S),^[17] 앰퍼샌드 제거^[22]^[17]	m &E^[17]^[22]	m 줄과 같다.^[17]	m 줄에서 $\varphi ~ \& ~ \psi$ 로부터 $\varphi$ 와 $\psi$ 를 추론한다.^[17]^[22]
선언 도입^[22]	추가(ADD)^[17]	m ∨I^[17]^[22]	m 줄과 같다.^[17]	m 줄에서 $\varphi$ 로부터 $\psi$ 가 무엇이든 $\varphi \lor \psi$ 를 추론한다.^[17]^[22]
선언 제거	쐐기 제거,^[22] 딜레마(DL)^[23]	j,k,l,m,n ∨E^[22]	j,k,l,m,n 줄.^[22]	j 줄에서 $\varphi \lor \psi$ 와, k 줄에서 $\varphi$ 의 가정과, l 줄에서 $\varphi$ 로부터 $\chi$ 의 파생과, m 줄에서 $\psi$ 의 가정과, n 줄에서 $\psi$ 로부터 $\chi$ 의 파생으로부터 $\chi$ 를 추론한다.^[22]
선언적 삼단 논법	쐐기 제거(∨E),^[17] 긍정 긍정 법(MTP)^[17]	m,n DS^[17]	m과 n 줄의 가정 집합의 합집합.^[17]	m 줄에서 $\varphi \lor \psi$ 와 n 줄에서 $- \varphi$ 로부터 $\psi$ 를 추론하고; m 줄에서 $\varphi \lor \psi$ 와 n 줄에서 $- \psi$ 로부터 $\varphi$ 를 추론한다.^[17]
화살표 제거^[17]	전건 긍정(MPP),^[22]^[17] 긍정 법(MP),^[23]^[17] 조건 제거	m, n →E^[17]^[22]	m과 n 줄의 가정 집합의 합집합.^[17]	m 줄에서 $\varphi \to \psi$ 와 n 줄에서 $\varphi$ 로부터 $\psi$ 를 추론한다.^[17]
화살표 도입^[17]	조건 증명(CP),^[23]^[22]^[17] 조건 도입	n, →I (m)^[17]^[22]	선행사가 가정된 줄인 m을 제외하고, n 줄의 가정 집합의 모든 것.^[17]	m 줄에서 $\varphi$ 의 가정으로부터 유도된 n 줄에서 $\psi$ 로부터 $\varphi \to \psi$ 를 추론한다.^[17]
귀류법^[22]	간접 증명(IP),^[17] 부정 도입(−I),^[17] 부정 제거(−E)^[17]	m, n RAA (k)^[17]	k (부정된 가정)를 제외하고 m과 n 줄의 가정 집합의 합집합.^[17]	증명에 나타나는 가정의 부정(규칙의 명제를 단순화하기 위해, 여기에서 "부정"이라는 단어는 다음과 같이 사용된다: 공식 $\varphi$ 의 부정은 부정이 아닌 $- \varphi$ 이며, 부정 $- \varphi$ 는 $\varphi$ 와 $- - \varphi$ 두 가지 부정을 갖는다.^[17]) m과 n 줄에서, 가정의 부정을 추론한다 (k 줄에서).^[17]
양방향 화살표 도입^[17]	양방향 조건 정의 (Df ↔),^[22] 양방향 조건 도입	m, n ↔ I^[17]	m과 n 줄의 가정 집합의 합집합.^[17]	m과 n 줄에서 $\varphi \to \psi$ 와 $\psi \to \varphi$ 로부터 $\varphi \leftrightarrow \psi$ 를 추론한다.^[17]
양방향 화살표 제거^[17]	양방향 조건 정의 (Df ↔),^[22] 양방향 조건 제거	m ↔ E^[17]	m 줄과 같다.^[17]	m 줄에서 $\varphi \leftrightarrow \psi$ 로부터 $\varphi \to \psi$ 또는 $\psi \to \varphi$ 를 추론한다.^[17]
이중 부정^[22]^[23]	이중 부정 제거	m DN^[22]	m 줄과 같다.^[22]	m 줄에서 $- - \varphi$ 로부터 $\varphi$ 를 추론한다.^[22]
후건 부정^[22]	긍정 법(MT)^[23]	m, n MTT^[22]	m과 n 줄의 가정 집합의 합집합.^[22]	m 줄에서 $\varphi \to \psi$ 와 n 줄에서 $- \psi$ 로부터 $- \varphi$ 를 추론한다.^[22]