조사불가증

수학 철학에서, 조사 불가능한 증거는 인간 수학자가 타당성 등을 검증할 수 없는 것으로 간주되는 수학적 증거다.이 용어는 1979년 토머스 티모츠코가 케네스 아펠과 볼프강 하켄의 4색 정리에 대한 컴퓨터 지원 증명서를 비판하여 만든 것으로, 그 이후 다른 주장들, 주로 과도한 사례 분열을 가진 주장들과/또는 검증하기 어려운 컴퓨터 프로그램에 의해 파견된 부분들과 함께 적용되었다.측량성은 계산 수학에서 중요한 고려사항으로 남아 있다.

티모츠코의 주장

티모츠코는 세 가지 기준이 어떤 주장이 수학적 증거인지를 결정한다고 주장했다.

• 설득력(probability)은 합리적인 프로베이어의 결론을 설득할 수 있는 증명의 능력을 말한다.
• 인간 수학적 커뮤니티 구성원에 의한 검증에 대한 증명 접근성을 나타내는 조사 가능성
• 형식성(Formalizability)은 그 증명서가 그것의 주장을 입증하기 위해 개념들 사이의 논리적인 관계에만 호소하는 것을 말한다.^[1]

티모츠코의 견해로는, 아펠은-하켄 증명서는 실험을 공제로 대체함으로써 측량성 기준을 통과하지 못했다고 주장했다.

…우리가 [4색 정리]를 정리로 받아들인다면, 「테오렘」 즉, 보다 요점까지, 「증거」의 기본 개념의 감각을 바꾸는 데 전념하고 있다.
…[4색 정리]에서와 같이 수학에서 컴퓨터를 사용하는 것은 수학에 경험적 실험을 도입한다.우리가 [4색깔 정리]를 입증된 것으로 간주하기로 선택하든 말든, 우리는 현재의 증거가 전통적인 증거가 아니며, 전제로부터의 진술에 대한 사전 추론도 아니라는 것을 인정해야 한다.그것은 잘 생각한 실험의 결과로 채워지는 빈틈, 즉 빈틈이 있는 전통적인 증거다.

— Thomas Tymoczko, "The Four-Color Problem and its Philosophical Significance"^[1]

측량성이 없다면, 증거는 독자에게 결과를 설득하는 첫 번째 목적을 제공할 수 있지만, 그 결과가 왜 사실인지에 대해 독자를 계몽하는 두 번째 목적을 달성하지 못할 수 있다. 즉, 그것은 논쟁보다는 관찰의 역할을 할 수 있다.^[2][3]

이러한 구별은 조사 불가능한 증거들이 수학을 훨씬 더 높은 오류 잠재력에 노출시킨다는 것을 의미하기 때문에 중요하다.특히 컴퓨터 프로그램(버그가 있을 수 있음)의 사용으로 인해 조사불능이 되는 경우, 특히 그 프로그램이 발표되지 않을 경우, 결과적으로 설득력이 저하될 수 있다.^[3]타이모츠코는 다음과 같이 썼다.

어떤 슈퍼컴퓨터가 페아노 산술의 일관성을 연구하기 위해 설정되었다고 가정해 보자. 그리고 그것이 모순의 증거를 보고했다고 가정해 보자. 그것은 너무 길고 복잡해서 수학자는 가장 일반적인 용어를 넘어서서 그것을 이해할 수 없었다.우리는 이 결과를 받아들이기 위해 컴퓨터에 대한 충분한 믿음을 가질 수 있을까, 아니면 그들의 신뢰성에 대한 경험적 증거가 충분하지 않다고 말할까?

— Thomas Tymoczko, "The Four-Color Problem and its Mathematical Significance"^[1]

타이모츠코의 조사불능 주장에 대한 반론

그러나 타이모츠코의 견해는 조사하기 어려운 증거가 반드시 조사하기 불가능한 증거만큼 무효한 것은 아니라는 주장으로 인해 논란이 되고 있다.

Paul Teller는 조사가능성은 정도와 독자에 의존하는 문제이지 증거가 가지고 있거나 가지고 있지 않은 것이 아니라고 주장했다.학생들이 문제가 그들을 이해하는 것이 교정을 거부하지 않고 있기 때문에 전문적인 수학자들 열심히 지킬 것 주장이라고 생각하, 텔러, 주장하고 있지 proofs(그들은 비난 받을 수도 있다)거부되어야 한다.[4][3](텔러 Tymoczko의 평가는 "[그 Four-Color 정리]mathematicians,에 의해 확인되지 않았다고 동의하지 않았다.다른 모든 증거들이 확인되었듯이, 차근차근 차근히실제로 그런 식으로 확인할 수는 없다.)

유사한 선에 따른 논쟁은 사례분할이 허용되는 증명방법이라는 것이다.하켄 증거는 사건이 분열되는 극단적인 예에 불과하다.^[2]

조사불능에 대한 대책

반면에, 증거는 최소한 조사가 가능해야 하고, 조사하기 어려운 증명들의 오류는 정밀 조사의 대상이 될 가능성이 적다는 티모츠코의 지적은 일반적으로 논쟁의 여지가 없다; 대신에, 특히 컴퓨터 보조 증거의 조사 가능성을 향상시키기 위한 방법들이 제안되어 왔다.초기 제안들 중 하나는 병렬화였다: 검증 작업은 많은 독자들에게 나누어질 수 있었고, 각 독자들은 입증의 일부를 조사할 수 있었다.^[5]그러나 플라이스펙에 의해 유명해진 현대적 관행은 제한된 형식주의로 증거의 의심스러운 부분을 표현하고, 그 후에 그 자체가 조사에 이용 가능한 증명 검사기로 검증하는 것이다.아펠-아펠-하켄 증거는 이렇게 검증되었다.^[6]

그럼에도 불구하고, 자동화된 검증은 아직 널리 채택되지 않았다.^[7]

참조