증명에 “고차 추론 기술”이 필요한지 여부를 결정하는 방법은 무엇입니까? 가정합니다 (즉, 관련된 증거 문제는 모든 공리가

질문:

공리와 목표로 구성된 문제에 대한 사양이 있다고 가정합니다 (즉, 관련된 증거 문제는 모든 공리가 주어지면 목표를 충족시킬 수 있는지 여부입니다). 또한 문제가 공리들 사이에 불일치 / 모순이 포함되어 있지 않다고 가정하자. 문제를 증명하는 데 “고차 추론”이 필요한지 미리 결정하는 방법이 있습니까 (즉, 완전한 증거를 먼저 작성하지 않고)?

“고차 추론”이란 고차 논리를 기록해야하는 증명 단계를 적용하는 것을 의미합니다. “고차 추론”의 전형적인 예는 귀납 일 것입니다 : 귀납 체계를 원칙적으로 쓰려면 고차 논리를 사용해야합니다.

예:

증명 문제를 지정할 수 있습니다. “두 개의 자연수에 대한 추가는 정류입니까?” 1 차 로직 사용 (즉, “plus”함수를 재귀 적으로 정의하는 공리와 함께 표준 공리와 함께 생성자 zero / succ를 통해 자연수를 정의) 이 문제를 증명하려면 “plus”의 첫 번째 또는 두 번째 인수의 구조에 대한 유도가 필요합니다 ( “plus”의 정확한 정의에 따라 다름). 증명하기 전에 입력 문제의 본질을 분석하여 이것을 알 수 있었습니까? (물론 이것은 설명을위한 간단한 예일뿐입니다. 실제로, 이것은 플러스의 commutativity보다 더 어려운 증명 문제에 흥미로울 것입니다.)

더 많은 맥락 :

내 연구에서, 나는 종종 뱀파이어, 이프 로버 등과 같은 자동화 된 1 차 정리 프로 버를 적용하여 증명 문제 (또는 증명 문제의 일부)를 해결하려고 시도하는데, 그 중 일부는 고차 추론이 필요할 수 있습니다. 종종, 증명 자들은 증거를 제시하는 데 꽤 많은 시간이 필요합니다 (일차 추론 기술 만 필요한 증거가 있다면). 물론, 고차 추론이 필요한 문제에 1 차 정리를 적용하려고하면 일반적으로 시간 초과가 발생합니다.

따라서 증명 문제가 고차 추론 기법을 필요로하는지 여부를 사전에 알려줄 수있는 방법 / 기술이 있는지 궁금합니다 ( “1 차 정리 증명 자에게 전달하는 데 시간을 낭비하지 마십시오”). ) 또는 그렇지 않은 경우, 적어도 특정 입력 문제 일 수 있습니다.

나는 문학에서 내 질문에 대한 답을 찾고 정리에 관한 일부 동료 연구원들에게 그 사실을 입증 해달라고 요청했지만 지금까지는 좋은 답을 얻지 못했습니다. 내 기대는 대화식 정리 증명과 자동 정리 증명 (Coq community? Isabelle community (Sledgehammer)?)을 결합하려는 사람들의 주제에 대한 연구가 있지만 지금까지는 아무것도 찾을 수 없었습니다.

나는 일반적으로 여기에 설명 된 문제가 결정 불가능한 것 같습니다 (그렇습니까?). 그러나 문제의 개선 된 버전에 대한 좋은 대답이있을 수 있습니다 …?



답변

간단히 말해서, 1 차 논리에 언급 된 모든 정리는 1 차 증거를가집니다.

Peter B. Andrews는 자신의 저서 인 “수학적 논리와 유형 이론에 대한 소개”에서 1 차 논리와 고차 논리 Q 0 시스템을 개발합니다 . 이는 일반적으로 현대의 고차 계급의 이론적 근거로 간주됩니다 . (예를 들어 HOL 로직 소개를 참조하십시오.)

Q 0 및 이와 유사한 시스템의 경우 Andrews는 자신이 설명하는 고차 논리가 1 차 논리의 보수적 인 확장으로 간주 될 수 있으며 다음과 같이 기록합니다 (제 2 판, 259 페이지). 유형 이론에는 1 차 증거가 있습니다. “

그러나 실제적인 관심사를 감안할 때 다음 단락도 인용합니다.

“그러나, 고차 논리로만 표현 될 수있는 개념을 사용함으로써 1 차 논리의 일부 이론이 가장 효율적으로 입증 될 수있다. 예는 [Andrews and Bishop, 1996] 및 [Boolos, 1998, Chapter 25] Statman은 1 차 논리 wff의 1 차 논리 증명의 최소 길이가 동일한 wff 증거의 최소 길이보다 엄청나게 길 수 있음을 입증했다 [Statman, 1978, 법안 6.3.5]. 2 차 논리 : Godel의 관련 결과 [Godel, 1936]는 일반적으로 ‘다음 고차의 논리를 전달하는 것이 이전에 입증 할 수 없었던 특정 명제를 제시하는 것뿐만 아니라 이미 사용 가능한 많은 증거를 엄청나게 줄일 수 있습니다. ‘이에 대한 완전한 증거는 [버스,1994]. “