커리의 역설

**커리의 역설**(Curry's paradox)은 "C이면 F이다"라고 스스로 말하는 문장 C의 존재만으로 임의의 주장 F가 증명되는 역설이다. 이 역설은 몇 가지 명백히 무해한 논리적 추론 규칙만 필요로 한다. F는 임의적이므로, 이 규칙들을 가진 모든 논리는 모든 것을 증명할 수 있게 한다. 이 역설은 자연어와 집합론의 특정 형식, 람다 대수, 조합론적 논리를 포함한 다양한 논리학에서 표현될 수 있다. 이 역설은 1942년에 이 문제에 대해 저술한 논리학자 해스켈 커리의 이름을 따서 명명되었다. 뢰브의 정리와의 관계로 인해 마르틴 휘고 뢰브의 이름을 따 **뢰브의 역설**이라고도 불린다.access-date=24 January 2013
# 자연어에서
"A이면 B이다" 형태의 주장은 조건문이라고 불린다. 커리의 역설은 다음과 같은 예시에서 보여지듯이 특정 종류의 자기언급적 조건문을 사용한다. 이 문장이 참이면, 독일은 중국과 국경을 접한다. 독일이 중화인민공화국과 국경을 접하지 않더라도, 예시 문장은 분명히 자연어 문장이며, 따라서 그 문장의 진위를 분석할 수 있다. 역설은 이 분석에서 비롯된다. 분석은 두 단계로 구성된다. 첫째, 일반적인 자연어 증명 기법을 사용하여 예시 문장이 참임을 증명할 수 있다 [아래 1–4단계]. 둘째, 문장의 진위를 사용하여 독일이 중국과 국경을 접한다고 증명할 수 있다 [5–6단계]: # 이 문장은 "이 문장이 참이면, 독일은 중국과 국경을 접한다"라고 읽힌다. 형식 증명과 호환되는 단계 번호 매기기를 위해 정의 반복] # 이 문장이 참이면, 참이다. [명백한, 즉 항진식] # 이 문장이 참이면: 이 문장이 참이면, 독일은 중국과 국경을 접한다. ["참이다"를 문장의 정의로 대체] # 이 문장이 참이면, 독일은 중국과 국경을 접한다. [반복된 조건 축약] # 그러나 4번은 이 문장이 말하는 것이므로, 실제로 참이다. # 이 문장은 참이며 [5번에 의해], 그리고 [4번에 의해]: 이 문장이 참이면, 독일은 중국과 국경을 접한다.
따라서 독일은 중국과 국경을 접한다. [전건 긍정] 독일이 중국과 국경을 접하지 않기 때문에, 이는 증명 단계 중 하나에서 오류가 있었음을 시사한다. "독일은 중국과 국경을 접한다"라는 주장은 다른 어떤 주장으로 대체될 수 있으며, 그 문장은 여전히 증명 가능하다. 따라서 모든 문장이 증명 가능한 것처럼 보인다. 증명이 잘 받아들여지는 연역 방식만을 사용하고, 이러한 방식 중 어느 것도 틀린 것처럼 보이지 않기 때문에, 이러한 상황은 역설적이다.A parallel example is explained in the Stanford Encyclopedia of Philosophy. See date=2018
## 비형식적 증명
조건문 (형태가 "A이면 B이다"인 문장)을 증명하는 표준 방법은 "함의 도입"이라고 불린다. 이 방법에서 "A이면 B이다"를 증명하기 위해, 먼저 A가 가정되고 그 가정 하에 B가 참임이 보여진다. 커리의 역설을 생성하기 위해, 위에서 설명된 두 단계에서, "이 문장이 참이면, 독일은 중국과 국경을 접한다"라는 문장에 이 방법을 적용한다. 여기서 A, "이 문장이 참이다"는 전체 문장을 의미하고, B는 "독일은 중국과 국경을 접한다"이다. 따라서 A를 가정하는 것은 "A이면 B이다"를 가정하는 것과 같다. 그러므로 A를 가정함으로써 우리는 A와 "A이면 B이다"를 모두 가정하게 된다. 따라서 전건 긍정에 의해 B가 참이며, 우리는 가설을 가정하고 결론을 도출하는 일반적인 방식으로 "이 문장이 참이면, '독일은 중국과 국경을 접한다'가 참이다"를 증명했다. 이제, 우리는 "이 문장이 참이면, '독일은 중국과 국경을 접한다'가 참이다"를 증명했으므로, "이 문장이 참이다"라는 주장이 옳다는 것을 알기 때문에 다시 전건 긍정을 적용할 수 있다. 이런 방식으로 우리는 독일이 중국과 국경을 접한다는 것을 추론할 수 있다.
# 형식논리학에서

## 명제 논리
이전 섹션의 예시는 비형식적인 자연어 추론을 사용했다. 커리의 역설은 일부 형식논리학에서도 발생한다. 이 맥락에서, 이것은 만약 우리가 (X → Y)라는 형식 문장이 존재한다고 가정한다면, 여기서 X 자체가 (X → Y)와 동등하다면, 우리는 형식 증명으로 Y를 증명할 수 있음을 보여준다. 그러한 형식 증명의 한 예시는 다음과 같다. 이 섹션에서 사용된 논리 표기법에 대한 설명은 논리 기호 목록을 참조하라. # X := (X → Y)
가정, 시작점, "이 문장이 참이면 Y"와 동등함 # X → X
동일률 # X → (X → Y)
2의 오른쪽을 대체, 1에 의해 X는 X → Y와 동등하므로 # X → Y
3으로부터 축약 규칙에 의해 # X
4를 대체, 1에 의해 # Y
5와 4로부터 전건 긍정에 의해 대안적인 증명은 피어스의 법칙을 통한다. 만약 X = X → Y라면, (X → Y) → X이다. 이는 피어스의 법칙 ((X → Y) → X) → X 및 전건 긍정과 함께 X를, 그리고 나중에 Y를 함축한다 (위 증명에서와 같이). 위의 도출은 만약 Y가 형식 체계에서 증명 불가능한 문장이라면, 그 체계에 X가 함의 (X → Y)와 동등한 문장은 존재하지 않는다는 것을 보여준다. 즉, 이전 증명의 1단계가 실패한다. 대조적으로, 이전 섹션은 자연(비형식화된) 언어에서 모든 자연어 문장 Y에 대해, 자연어에서 Z가 (Z → Y)와 동등한 자연어 문장 Z가 존재함을 보여준다. 즉, Z는 "이 문장이 참이면 Y"이다.
## 순진한 집합론
기본적인 수학적 논리학이 어떤 자기언급 문장도 허용하지 않더라도, 순진한 집합론의 특정 형식은 여전히 커리의 역설에 취약하다. 무제한 명세를 허용하는 집합론에서, 우리는 집합 X \ \stackrel{\mathrm{def{=}\ \left\\{ x \mid (x \in x) \to Y \right\\}.를 검토함으로써 어떤 논리적 문장 Y도 증명할 수 있다. 그런 다음 X\in X가 (X\in X) \to Y와 동등하다는 것을 쉽게 보여준다. 이로부터 Y는 위에서 보여진 증명과 유사하게 추론될 수 있다. ("X\in X"는 "이 문장"을 의미한다.) 따라서 일관성 있는 집합론에서 \left\\{ x \mid (x \in x) \to Y \right\\} 집합은 거짓 Y에 대해 존재하지 않는다. 이것은 러셀의 역설의 변형으로 볼 수 있지만, 동일하지는 않다. 일부 집합론 제안은 무제한 명세 규칙을 제한하는 대신, 모든 집합이 자기 자신을 원소로 포함하지 않는 집합의 모순적 본질을 용인하도록 논리 규칙을 제한함으로써 러셀의 역설을 다루려고 시도했다. 위와 같은 증명의 존재는 그러한 작업이 그리 간단하지 않음을 보여준다. 왜냐하면 위의 증명에서 사용된 연역 규칙 중 적어도 하나는 생략되거나 제한되어야 하기 때문이다.
## 제한된 최소 논리를 가진 람다 대수
커리의 역설은 함의 명제 논리로 확장된 비형식적 람다 대수로 표현될 수 있다. 람다 대수의 구문적 제약을 다루기 위해 m은 두 매개변수를 취하는 함의 함수를 나타내며, 즉 람다 항 ((m A) B)는 일반적인 중위 표기법 A \to B와 동등하다. 임의의 공식 Z는 람다 함수 N := \lambda p.((m p) Z)와 X := (\textsf{Y} N)를 정의함으로써 증명될 수 있으며, 여기서 \textsf{Y}는 커리의 고정점 결합자를 나타낸다. 그러면 X = (N X) = ((m X) Z)는 \textsf{Y}와 N의 정의에 의해 성립하며, 따라서 위의 명제 논리 증명을 계산에서 복제할 수 있다.The naming here follows the sentential logic proof, except that "Z" is used instead of "Y" to avoid confusion with Curry's fixed-point combinator \textsf{Y}.archive-date=2014-07-14 Here: p.125 \begin{array}{cll} \vdash & ((m X) X) & \mbox{ 최소 논리 공리 } A \to A \mbox{ 에 의해 } \\\ \vdash & ((m X) ((m X) Z)) & \mbox{ } X = ((m X) Z) \mbox{ 이므로 } \\\ \vdash & ((m X) Z) & \mbox{ 최소 논리의 정리 } (A \to (A \to B)) \vdash (A \to B) \mbox{ 에 의해 } \\\ \vdash & X & \mbox{ } X = ((m X) Z) \mbox{ 이므로 } \\\ \vdash & Z & \mbox{ 전건 긍정 } A, (A \to B) \vdash B \mbox{ 에 의해 } X \mbox{ 와 } ((m X) Z) \mbox{ 로부터 } \\\ \end{array} 단순 형식 람다 대수에서는 고정점 결합자가 형식화될 수 없으므로 허용되지 않는다.
## 조합론적 논리
커리의 역설은 람다 대수와 동등한 표현력을 가진 조합론적 논리에서도 표현될 수 있다. 모든 람다 표현식은 조합론적 논리로 번역될 수 있으므로, 람다 대수에서 커리의 역설 구현을 번역하는 것으로 충분할 것이다. 위의 항 X는 조합론적 논리에서 (r \ r)로 번역되며, 여기서 r = \textsf{S} \ (\textsf{S} (\textsf{K} m) (\textsf{S} \textsf{I} \textsf{I})) \ (\textsf{K} Z); 따라서 1=(r r) 1== 1=(\textsf{S} (\textsf{S} (\textsf{K} m) (\textsf{S} \textsf{I} \textsf{I})) (\textsf{K} Z) (\textsf{S} (\textsf{S} (\textsf{K} m) (\textsf{S} \textsf{I} \textsf{I})) (\textsf{K} Z))) 1=\to 1=(\textsf{S} (\textsf{K} m) (\textsf{S} \textsf{I} \textsf{I}) (\textsf{S} (\textsf{S} (\textsf{K} m) (\textsf{S} \textsf{I} \textsf{I})) (\textsf{K} Z)) (\textsf{K} Z (\textsf{S} (\textsf{S} (\textsf{K} m) (\textsf{S} \textsf{I} \textsf{I})) (\textsf{K} Z)))) 1=\to 1=(\textsf{S} (\textsf{K} m) (\textsf{S} \textsf{I} \textsf{I}) (\textsf{S} (\textsf{S} (\textsf{K} m) (\textsf{S} \textsf{I} \textsf{I})) (\textsf{K} Z)) Z) 1=\to 1=(\textsf{K} m (\textsf{S} (\textsf{S} (\textsf{K} m) (\textsf{S} \textsf{I} \textsf{I})) (\textsf{K} Z)) (\textsf{S} \textsf{I} \textsf{I} (\textsf{S} (\textsf{S} (\textsf{K} m) (\textsf{S} \textsf{I} \textsf{I})) (\textsf{K} Z))) Z) 1=\to 1=(m (\textsf{S} \textsf{I} \textsf{I} (\textsf{S} (\textsf{S} (\textsf{K} m) (\textsf{S} \textsf{I} \textsf{I})) (\textsf{K} Z))) Z) 1=\to 1=(m (\textsf{I} (\textsf{S} (\textsf{S} (\textsf{K} m) (\textsf{S} \textsf{I} \textsf{I})) (\textsf{K} Z)) (\textsf{I} (\textsf{S} (\textsf{S} (\textsf{K} m) (\textsf{S} \textsf{I} \textsf{I})) (\textsf{K} Z)))) Z) 1=\to 1=(m (\textsf{S} (\textsf{S} (\textsf{K} m) (\textsf{S} \textsf{I} \textsf{I})) (\textsf{K} Z) (\textsf{I} (\textsf{S} (\textsf{S} (\textsf{K} m) (\textsf{S} \textsf{I} \textsf{I})) (\textsf{K} Z)))) Z) 1=\to 1=(m (\textsf{S} (\textsf{S} (\textsf{K} m) (\textsf{S} \textsf{I} \textsf{I})) (\textsf{K} Z) (\textsf{S} (\textsf{S} (\textsf{K} m) (\textsf{S} \textsf{I} \textsf{I})) (\textsf{K} Z))) Z) 1== 1=((m (r r)) \ Z) (r \ r) = ((m (r r)) \ Z).
# 논의
커리의 역설은 표현식으로 자체 재귀 함수를 구성할 수 있도록 하는 기본 논리 연산을 지원하는 모든 언어로 공식화될 수 있다. 역설 구성을 지원하는 두 가지 메커니즘은 자기언급 (문장 내에서 "이 문장"을 참조하는 능력)과 순진한 집합론의 무제한 명세이다. 자연어는 거의 항상 역설을 구성하는 데 사용될 수 있는 많은 기능을 포함하며, 다른 많은 언어도 마찬가지이다. 일반적으로 언어에 메타프로그래밍 기능을 추가하면 필요한 기능이 추가된다. 수학적 논리학은 일반적으로 자체 문장에 대한 명시적 참조를 허용하지 않는다. 그러나 괴델의 불완전성 정리의 핵심은 다른 형태의 자기언급이 추가될 수 있다는 관찰이다. 괴델 수를 참조하라. 증명 구성에 사용된 규칙은 조건부 증명의 가정 규칙, 축약 규칙, 그리고 전건 긍정이다. 이들은 1차 논리와 같은 대부분의 일반적인 논리 체계에 포함되어 있다.
## 일부 형식논리학에 대한 결과
1930년대에 커리의 역설과 커리의 역설이 개발된 관련 클레이니-로서 역설은number=2s2cid=121991184 자기 재귀 표현을 허용하는 다양한 형식 논리 체계가 모순적임을 보여주는 데 중요한 역할을 했다. 무제한 명세 공리는 현대 집합론에서 지원되지 않으며, 따라서 커리의 역설은 회피된다.