양적 이론을 위한 컴퓨팅 절차

형식 논리 조사를 위해 사용된 수학적 방법들이 수학 정리를 얻기 위한 순수한 계산 방법으로 이어질 것이라는 희망은 라이프니츠로 거슬러 올라가며, 20세기 초에 페아노에 의해, 1920년대 힐버트의 학교에 의해 되살아났습니다. 힐버트는 고전 수학의 모든 것이 양적 이론 내에서 형식화될 수 있음을 지적하며, 양적 이론의 주어진 공식이 유효한지 여부를 결정하는 알고리즘을 찾는 문제가 수학적 논리의 중심 문제라고 선언했습니다. 그리고 실제로 한때 이 "결정" 문제의 조사가 성공의 직전에 있는 것처럼 보였습니다. 그러나 처치와 튜링에 의해 이러한 알고리즘은 존재할 수 없다는 것이 밝혀졌습니다. 이 결과는 현대 디지털 컴퓨터를 사용하여 중요한 수학적 질문을 결정할 가능성에 대해 상당한 비관론을 초래했습니다. 그러나 최근에 이러한 전체 질문에 대한 관심이 되살아났습니다. 구체적으로, 양적 이론에 대한 결정 절차는 존재하지 않지만, 많은 증명 절차가 존재한다는 것이 인식되었습니다. 즉, 유효한 양적 이론의 어떤 공식에 대한 증명을 궁극적으로 찾는 균일한 절차가 있으며, 일반적으로는 유효하지 않은 공식의 경우 "영원히" 탐색해야 합니다. 그리고 이러한 증명 절차 중 일부는 현대 컴퓨팅 기계에서 사용하기에 적합할 수 있습니다. 하오 왕 9와 P. C. 길모어 3은 각각 양적 이론의 증명 절차를 사용하는 작동 프로그램을 제작했습니다. 길모어의 프로그램은 헤르브란드에 의해 주어진 수학적 논리의 기본 정리 형태를 사용하고, 왕의 프로그램은 겐첸이 연구한 양적 이론과 관련된 형식을 활용합니다. 그러나 두 프로그램 모두 유효하지 않은 양적 이론의 공식과 연결된 명제 미적 방법에 대해 가장 간단한 공식이 아닌 경우 결정적인 어려움에 직면합니다. 왕의 프로그램은 겐첸과 유사한 방법을 사용하기 때문에 진리 기능 연결자의 총 수에 대한 제곱을 포함하며, 길모어의 프로그램은 정규 형태를 사용하여 포함된 절의 수에 대한 제곱을 포함합니다. 두 방법 모두는 종종 변수의 총 수에 대한 제곱을 포함하는 진리 표 방법보다 많은 경우에 우수하며, 중요한 초기 기여를 나타내지만, 둘 다 비교적 간단한 예제에서 어려움에 직면합니다. 현재 논문에서는 비교적 복잡한 공식을 사용하는 데 적합하고 일반적으로 제곱으로 이어지지 않는 양적 이론의 균일한 증명 절차를 제시합니다. 현재 절차가 이전에 사용 가능한 절차보다 우수하다는 것은 길모어의 IBM 704 루틴이 21분 동안 결과를 얻지 못하게 한 공식이 현재 방법을 사용하여 손 계산으로 30분만에 성공적으로 작업되었다는 사실에서 일부 나타납니다. §6, 참조. 또한, “진정한” 수학에 속하는 정리의 증명을 얻기 위해 양적 이론에 대한 증명 절차를 활용할 수 있을 것이라고 기대하기 전에, 다양한 수학 분야에 대해 “짧은” 유한 공리화가 얻어져야 한다는 점을 언급해야 합니다. 이 마지막 질문은 여기서 더 이상 다루지 않을 것입니다; 그러나 데이비스와 퍼트넘 2를 참조하십시오. 이 문제에 대한 한 해결책이 제공됩니다.