커리의 역설

Curry's paradox

커리의 역설은 임의의 주장 F가 "만약 C라면 F라면"이라고 스스로 말하는 문장 C의 존재만으로 증명되는 역설로, 겉으로 보기에 무해한 몇 가지 논리적 추론 규칙만 필요합니다. F는 임의적이기 때문에 이러한 규칙을 가진 어떤 논리도 모든 것을 증명할 수 있습니다. 역설은 자연어와 특정 형태의 집합론, 람다 미적분학, 조합 논리를 포함다양한 논리로 표현될 수 있습니다.

이 역설은 논리학자 하스켈 커리의 이름을 따서 지어졌습니다. 마르틴 위고 뢰브의 이름을 따서 뢰브의 역설이라고도 불리는데,[1] 이는 뢰브의 정리와의 관계 때문입니다.

자연어로

"A이면 B이면"이라는 형식의 청구를 조건부 청구라고 합니다. Curry의 역설은 이 예에서 증명된 것처럼 특정한 종류의 자기 참조 조건문을 사용합니다.

이 문장이 사실이라면 독일은 중국과 국경을 접하고 있습니다.

비록 독일이 중국과 국경을 접하지는 않지만, 예문은 확실히 자연어 문장이기 때문에 그 문장의 진위를 분석할 수 있습니다. 이 분석을 통해 역설이 나옵니다. 분석은 두 단계로 구성됩니다.

  1. 첫째, 일반적인 자연어 증명 기법을 사용하여 예제 문장이 참임을 증명할 수 있습니다.
  2. 둘째, 예문의 진실은 독일이 중국과 국경을 접하고 있다는 것을 증명하는 데 사용될 수 있습니다.

독일은 중국과 국경을 접하지 않기 때문에 증명 중 하나에 오류가 있었음을 시사합니다. "독일은 중국과 국경을 접하고 있다"는 주장은 다른 주장으로 대체될 수 있으며, 선고는 여전히 유효할 것입니다. 따라서 모든 문장은 증명 가능한 것으로 보입니다. 증명은 잘 받아들여진 추론 방법만을 사용하기 때문에, 그리고 이 방법들 중 어느 것도 틀린 것으로 보이지 않기 때문에, 이 상황은 역설적입니다.[2]

비공식적 증명

조건부 문장('만약 A, 그럼 B'라는 형태의 문장)을 증명하는 표준 방법을 '조건부 증명'이라고 합니다. 이 방법에서는 "A이면 B이면"을 증명하기 위해 먼저 A를 가정하고 그 가정으로 B를 참으로 표시합니다.

위의 두 단계에서 설명한 바와 같이 커리의 역설을 생산하기 위해서는 "이 문장이 사실이라면 독일은 중국과 국경을 맞댄다"라는 문장에 이 방법을 적용합니다. 여기서 "이 문장은 사실"인 A는 전체 문장을 의미하는 반면, B는 "독일은 중국과 국경을 접하고 있습니다. 따라서 A를 가정하는 것은 "A이면 B"라고 가정하는 것과 같습니다. 따라서 A를 가정할 때 우리는 A와 "A이면 B"를 모두 가정했습니다. 따라서 B는 사실이고, 우리는 일반적인 방법으로 가설을 가정하고 결론을 도출함으로써 "이 문장이 사실이라면 '독일은 중국과 국경을 맞대고 있다'는 것"을 증명했습니다.

이제 "이 문장이 사실이라면 '독일은 중국과 국경을 접하고 있다'는 것이 사실이다"라는 것을 증명했기 때문에, "이 문장이 사실이다"라는 주장이 정확하다는 것을 알기 때문에 우리는 다시 양태 포넨스를 적용할 수 있습니다. 이런 식으로 독일이 중국과 국경을 접하고 있다는 것을 추론할 수 있습니다.

형식적 증명

센텐셜 로직

앞 절의 예는 정형화되지 않은 자연어 추론을 사용했습니다. 커리의 역설은 형식 논리의 일부 유형에서도 발생합니다. 이러한 맥락에서 공식 문장(X → Y)이 존재한다고 가정할 때, X 자체가 (X → Y)와 동등하다고 가정하면 공식 증명으로 Y를 증명할 수 있음을 보여줍니다. 그러한 형식적인 증명의 한 예는 다음과 같습니다. 이 섹션에서 사용하는 논리 표기법에 대한 설명은 논리 기호 목록을 참조하십시오.

  1. X : = (X → Y)
    시작점, "이 문장이 참이면 Y"에 해당하는 가정
  2. X → X
  3. X → (X → Y)
    X는 X Y와 1만큼 같으므로 우변을 2로 대체합니다.
  4. X → Y
    수축에 의해 3부터
  5. X
    치환기 4, 1만큼
  6. Y
    5부터 4까지 modus ponens로

대안적인 증거는 피어스의 법칙을 통해서입니다. 만약 X = X → Y이면 (X → Y) → X입니다. 이것은 Pearce의 법칙 ((X → Y) → X와 modus ponens와 함께 X를 의미하며, 그 뒤에 Y를 의미합니다 (위의 증명에서와 같이).

따라서 Y가 형식적인 시스템에서 증명할 수 없는 문장이라면, X가 함의와 동치가 되도록 시스템에 문장 X가 없습니다 (X → Y). 대조적으로, 앞 절은 자연어(비공식화) 언어에서 모든 자연어 문장 Y에 대해 Z가 자연어에서 (Z → Y)와 동등한 자연어 문장 Z가 있음을 보여줍니다. 즉, Z는 "이 문장이 사실이라면 Y"입니다.

Y의 분류가 이미 알려진 구체적인 경우에는 모순을 드러내기 위한 단계가 거의 필요하지 않습니다. 예를 들어, Y가 "독일은 중국과 국경을 접하고 있다"라고 할 때, Y는 거짓이라고 알려져 있습니다.

  1. X = (X → Y)
    추정
  2. X = (X → false)
    알려진 Y값을 대입하다
  3. X = (¬X ∨ false)
  4. X = ¬X
    신원

순진집합론

기본적인 수학 논리가 자기 참조 문장을 인정하지 않더라도 특정 형태의 순진한 집합 이론은 여전히 커리의 역설에 취약합니다. 제한 없는 이해를 허용하는 집합론에서, 그럼에도 불구하고 집합을 조사함으로써 임의의 논리적 문장 Y를 증명할 수 있습니다.

{\\in } 및 ={\displaystyle =}이(가) 모두 → {\displaystyle \to } 및 ↔ {\displaystyle \leftrightarrow }보다 바인딩 우선 순위를 갖는다고 가정하면 증명은 다음과 같이 진행됩니다.


  1. X의 정의

  2. 구성원 자격의 동등한 집합 대체

  3. 쌍대 조건의 양쪽에 결과값 추가(2부터)

  4. 집중 법칙 (1과 3으로부터)

  5. 2 조건부 탈락(4명부터)

  6. 수축(5부터)

  7. 2 조건부 탈락(4명부터)

  8. 모드 포넨스(6 및 7부터)

  9. 모드 포넨스(8 및 6부터)

4단계는 일관된 집합 이론에서 유일하게 유효하지 않은 단계입니다. Zermelo-Frankel 집합론에서는 X가 집합이라는 추가 가설이 필요하며, 이 가설은 ZF나 확장 ZFC(선택의 공리)에서는 증명할 수 없습니다.

따라서 일관된 집합 이론에서 집합{ ∣ x ∈ x → } xin x\to Y\right\}는 거짓 Y에 대해 존재하지 않습니다. 이것은 러셀의 역설에 대한 변형이라고 볼 수 있지만, 동일하지는 않습니다. 집합론에 대한 몇몇 제안들은 러셀의 역설을 이해 규칙을 제한하는 것이 아니라 논리 규칙을 제한함으로써 그들 자신의 구성원이 아닌 모든 집합의 모순된 성질을 용인함으로써 다루려고 시도했습니다. 위와 같은 증명의 존재는 위 증명에서 사용된 연역 규칙 중 적어도 하나를 생략하거나 제한해야 하기 때문에 이러한 작업이 그리 간단하지 않음을 보여줍니다.

람다 미적분학

커리의 역설은 제한된 최소 논리에 의해 풍부해진 유형화되지 않은 람다 미적분학으로 표현될 수 있습니다. 람다 미적분학의 구문적 제한에 대처하기 위해 은 두 매개변수를 사용하는 함의 함수를 나타내야 합니다. 즉, 람다 항 (( B (m B는 일반적인 infix 표기법 A\ B와 같아야 합니다

An arbitrary formula can be proved by defining a lambda function , and , where denotes Curry's fixed-point combinator. Then by definition of and , hence the above sentential logic proof can be duplicated in the calculus:[3][4][5]

간단히 입력된 람다 미적분학에서는 고정 소수점 결합기를 입력할 수 없으므로 허용되지 않습니다.

조합논리학

커리의 역설은 람다 미적분학과 동등한 표현력을 가진 조합 논리로도 표현될 수 있습니다. 임의의 람다 표현은 조합 논리로 번역될 수 있으므로, 람다 미적분학에서 Curry의 역설 구현에 대한 번역으로 충분할 것입니다.

X X는 조합에서(r {\로 번역되며, 여기서

따라서[6]

논의

Curry의 역설은 기본 논리 연산을 지원하는 모든 언어에서 공식화될 수 있으며, 이를 통해 자기 회귀 함수를 표현식으로 구성할 수도 있습니다. 역설의 구성을 뒷받침하는 두 가지 메커니즘은 자기 참조(문장 내에서 "이 문장"을 참조하는 능력)와 순진한 집합 이론의 제한 없는 이해입니다. 자연어는 거의 항상 다른 많은 언어와 마찬가지로 역설을 구성하는 데 사용될 수 있는 많은 기능을 포함합니다. 일반적으로 언어에 메타 프로그래밍 기능을 추가하면 필요한 기능이 추가됩니다. 수학적 논리는 일반적으로 자신의 문장에 대한 명시적인 언급을 허용하지 않습니다. 그러나 괴델의 불완전성 정리의 핵심은 다른 형태의 자기 참조가 추가될 수 있다는 관찰입니다. 괴델 수를 참조하십시오.

제한 없는 이해의 공리는 집합론에서 재귀적 정의를 구성할 수 있는 능력을 추가합니다. 이 공리는 현대 집합론에 의해 지지되지 않습니다.

증명의 구성에 사용되는 논리 규칙은 조건부 증명에 대한 가정의 규칙, 수축의 규칙, 모드 포넨스입니다. 이러한 것들은 1차 논리와 같은 가장 일반적인 논리 시스템에 포함됩니다.

일부 형식 논리에 대한 결과

1930년대에 Curry의 역설과 이와 관련된 Kleene-Rosser 역설은 자기 회귀식에 기초한 형식 논리 체계가 일관성이 없음을 보여주는 데 큰 역할을 했습니다. 여기에는 람다 미적분학조합 논리의 일부 버전이 포함됩니다.

Curry는 Kleene-Rosser 역설에서[7] 시작하여 핵심적인 문제가 이 단순한 Curry의 역설에서 표현될 수 있다고 추론했습니다.[8][9] 그의 결론은 조합 논리와 람다 미적분학이 연역적 언어로서 일관성을 가질 수는 없지만 재귀를 허용한다는 것이라고 말할 수 있습니다.

1941년[10] Curry는 비유적(추론적) 조합 논리 연구에서 이 역설의 의미를 제한 없이 조합 논리의 다음과 같은 속성이 양립할 수 없음을 암시하는 것으로 인식했습니다.

  1. 조합적 완성도. 이는 추상화 연산자가 시스템에서 정의 가능(또는 원시적)하다는 것을 의미하며, 이는 시스템의 표현력에 대한 요건입니다.
  2. 연역적 완성도. 이것은 도출 가능성에 대한 요구 사항, 즉 물질적 함의와 변증법이 있는 공식 시스템에서 Y가 가설 X로부터 증명될 수 있다면 X → Y의 증명도 있다는 원리입니다.

결의안

주의할 점은 거짓말쟁이 역설이나 러셀의 역설과 달리 커리의 역설은 완전히 부정이 없기 때문에 어떤 부정의 모델을 사용하는지에 달려 있지 않습니다. 따라서 역설적 논리는 거짓말쟁이 역설에 면역력이 있더라도 여전히 이 역설에 취약할 수 있습니다.

람다 미적분학의 분해능 없음

Alonzo Church의 람다 미적분학의 기원은 "어떻게 방정식을 풀 수 있습니까, 함수의 정의를 제공합니까?"였습니다. 이것은 이 등가성으로 표현됩니다.

이 정의는 방정식 = displaystyle f\ x = y}를 만족하는 함수 가 하나만 있으면 유효하지만 그렇지 않으면 유효하지 않습니다. 이것이 스티븐 크린해스켈 커리가 조합 논리와 람다 미적분학으로 발견한 문제의 핵심입니다.

상황은 정의하는 것과 비교될 수 있습니다.

제곱근에 대해 양의 값만 허용된다면 이 정의는 괜찮습니다. 수학에서 기존에 정량화된 변수는 여러 개의 값을 나타낼 수 있지만 한 번에 하나만 나타낼 수 있습니다. 실존적 정량화는 방정식의 많은 인스턴스를 해체하는 것입니다. 각 방정식에서 변수에 대한 값은 하나입니다.

그러나 수학에서 자유 변수가 없는 표현은 하나의 값만 있어야 합니다. 4 는) + 만 나타낼 수 있습니다 그러나 람다 추상화를 한 값으로 제한하거나 값이 있는지 확인하는 편리한 방법은 없습니다.

람다 미적분학은 매개변수로 불리는 동일한 함수를 통과시켜 재귀를 허용합니다. f x = {\ f\ x = y}에 f {\displaystyle f}에 대한 솔루션이 여러 개이거나 없는 상황이 발생할 수 있습니다.

람다 미적분학은 방정식에 대한 단일 해를 나타내는 람다 추상화만 허용되는 경우 수학의 일부로 간주될 수 있습니다. 다른 람다 추상화들은 수학에서 부정확합니다.

람다 미적분학에서 커리의 역설과 다른 역설들이 발생하는 이유는 연역 체계로 간주되는 람다 미적분학의 불일치 때문입니다. 연역 람다 미적분학도 참조하십시오.

람다 미적분학 항의 정의역

람다 미적분학은 자신의 영역에서 일관된 이론입니다. 그러나 일반 수학에 람다 추상화 정의를 추가하는 것은 일관성이 없습니다. 람다 항은 람다 미적분 도메인의 값을 설명합니다. 각 람다 항은 해당 도메인에 값이 있습니다.

수학에서 람다 미적분학으로 표현을 번역할 때 람다 미적분학 용어의 정의역이 항상 수학적 표현의 정의역과 동형인 것은 아닙니다. 이 동형화의 결여가 명백한 모순의 근원입니다.

제한 없는 언어로 해상도를 제공합니다.

해결책이 없거나 많을 수 있는 방정식을 암시적으로 호출하는 많은 언어 구조가 있습니다. 이 문제에 대한 건전한 해결책은 이러한 표현식을 기존에 정량화된 변수와 구문적으로 연결하는 것입니다. 변수는 일반적인 인간의 추론에서는 의미가 있지만 수학에서도 유효한 방식으로 다중 값을 나타냅니다.

예를 들어, Evalue 함수를 허용하는 자연어는 수학적으로 일관되지 않습니다. 하지만 자연어로 평가를 부를 때마다 일관된 방식으로 수학으로 번역될 수 있습니다. 평가를 수학으로 번역하는 것은

let x = Eval(s) in x.

여기서 = "평가(들) → y",

let x = x → y in x.

y가 거짓이면 x = x → y는 거짓이지만 이는 거짓이지 역설이 아닙니다.

변수 x의 존재는 자연어에 함축되어 있었습니다. 변수 x는 자연어를 수학으로 번역할 때 생성됩니다. 이를 통해 수학적 무결성을 유지하면서 자연스러운 의미론과 함께 자연 언어를 사용할 수 있습니다.

형식논리식 해상도

형식 논리에서 논쟁은 (X → Y)를 X로 명명하는 것의 유효성을 가정하는 것으로 시작됩니다. 그러나 이것은 유효한 출발점이 아닙니다. 먼저 명명의 타당성을 추론해야 합니다. 다음 정리는 쉽게 증명할 수 있으며 이러한 명명을 나타냅니다.

위의 문장에서 공식 A는 X로 명명됩니다. 이제 A에 대해 (X → Y)로 공식을 인스턴스화합니다. ∃ X \ X가 ∀ A {\ \forall A}의 범위안에 있기 때문에 불가능합니다. Skolemization을 사용하여 정량기의 순서를 변경할 수 있습니다.

그러나 이제 인스턴스화는

이는 증명의 시작점이 아니며 모순으로 이어지지 않습니다. 역설의 출발점으로 이어지는 A에 대한 다른 인스턴스는 없습니다.

집합론에서의 해상도

Zermelo–Frankel 집합론(ZFC)에서 제한 없는 이해의 공리는 집합의 구성을 허용하는 일련의 공리로 대체됩니다. 그래서 ZFC에서는 커리의 역설을 말할 수 없습니다. 러셀의 역설에 대응하여 ZFC는 진화했습니다.

참고 항목

참고문헌

  1. ^ Barwise, Jon; Etchemendy, John (1987). The Liar: An Essay on Truth and Circularity. New York: Oxford University Press. p. 23. ISBN 0195059441. Retrieved 24 January 2013.
  2. ^ 비슷한 예로 스탠포드 철학 백과사전에 설명되어 있습니다. 참조
  3. ^ 여기서 명명은 Curry의 고정 소수점 Y 와의 혼동을 피하기 위해 "Y" 대신 "Z"가 사용된다는 점을 제외하고는 필수 논리 증명을 따릅니다
  4. ^ Gérard Huet (May 1986). Formal Structures for Computation and Deduction. International Summer School on Logic of Programming and Calculi of Discrete Design. Marktoberdorf. Archived from the original on 2014-07-14.Gérard Huet (May 1986). Formal Structures for Computation and Deduction. International Summer School on Logic of Programming and Calculi of Discrete Design. Marktoberdorf. Archived from the original on 2014-07-14.{{cite book}}CS1 maint: 위치 누락 게시자(링크) 여기: p.125
  5. ^ Haskell B. Curry; Robert Feys (1958). Combinatory Logic I. Studies in Logic and the Foundations of Mathematics. Vol. 22. Amsterdem: North Holland.[페이지 필요]
  6. ^
  7. ^ Kleene, S. C. & Rosser, J. B. (1935). "The inconsistency of certain formal logics". Annals of Mathematics. 36 (3): 630–636. doi:10.2307/1968646. JSTOR 1968646.
  8. ^ Curry, Haskell B. (Jun 1942). "The Combinatory Foundations of Mathematical Logic". Journal of Symbolic Logic. 7 (2): 49–64. doi:10.2307/2266302. JSTOR 2266302. S2CID 36344702.
  9. ^ Curry, Haskell B. (Sep 1942). "The Inconsistency of Certain Formal Logics". The Journal of Symbolic Logic. 7 (3): 115–117. doi:10.2307/2269292. JSTOR 2269292. S2CID 121991184.
  10. ^ Curry, Haskell B. (1941). "The Paradox of Kleene and Rosser". Transactions of the American Mathematical Society. 50 (3): 454–516. doi:10.1090/S0002-9947-1941-0005275-6. MR 0005275. Retrieved 24 January 2013.
  11. ^ Stenlund, Sören (1972). Combinators, λ-terms, and Proof Theory. Dordrecht: D. Reidel. p. 71. ISBN 978-9027703057.

외부 링크