모든 참을 판별하는 프로그램을 만들 수 있나요?

우선 문제를 정확하게 정해야 합니다. 결정 절차는 입력으로 받은 문장 또는 논리식이 정해진 성질을 갖는지 모든 입력에 대해 유한 시간 안에 예·아니요를 정확히 답합니다. 예를 들어 ‘명제논리식이 모든 진리값 배정에서 참인가?’라는 문제에는 진리표라는 결정 절차가 있습니다. 변수의 수가 유한하므로 모든 행을 검사한 뒤 반드시 끝납니다.

빠름과 결정 가능성은 다른 개념입니다. 아주 오래 걸려도 모든 입력에서 유한 시간 안에 끝나면 결정 절차입니다. 반대로 많은 사례에서 즉시 답하더라도 어떤 입력에서 끝나는지 보장하지 못하면 아직 결정 절차가 아닙니다.

한 성질을 만족하는 입력에 대해서는 반드시 언젠가 ‘예’라고 정답을 내고 멈추지만, 성질을 만족하지 않는 입력에서는 영원히 실행될 수도 있는 절차입니다. 이것을 반결정 가능 또는 재귀적으로 열거 가능이라고 부릅니다. 모든 입력에서 ‘아니요’의 결론까지 내리겠다고 약속하지 않습니다.

실행 중이라는 사실만으로 정답이 ‘아니요’라고 결론 내릴 수 없습니다. 단지 아직 ‘예’를 확정하지 못했다는 뜻입니다. 종료 보장이 없는 탐색을 판정기처럼 사용하면 오류가 생깁니다.

p가 참이고 q가 거짓인 배정에서 p→q는 거짓입니다. 따라서 타당하지 않습니다. 두 명제변수의 경우 네 배정을 모두 계산하면 종료합니다. 명제변수가 n개라면 진리표는 2ⁿ개 행으로 이루어지므로 유한합니다. n이 커지면 계산량은 커져도 판정은 언제나 가능합니다.

입력된 식의 길이는 유한하므로 그 식에 실제 나타나는 명제변수의 수 또한 유한합니다. 이런 성질 때문에 임의의 유한한 명제논리식을 입력받는 판정기를 만들 수 있습니다.

일차논리식의 참은 전체 영역의 크기와 각 기호의 해석에 의존합니다. 보편 양화사는 가능한 모든 대상과 구조를 고려합니다. 임의의 일차논리식이 모든 구조에서 참인지 알려면 단순히 입력 기호에 대한 유한 진리값 배정만 조사하는 것으로는 충분하지 않습니다. ‘모든 유한 모형을 차례로 검사하면 언젠가 타당성도 알 수 있다’는 주장 역시 일반적으로 성립하지 않습니다.

특정한 반모형을 찾으면 타당하지 않다는 결론을 바로 낼 수 있습니다. 하지만 반모형을 찾지 못했다는 사실만으로 모든 구조에서 참이라는 일반 결론은 나오지 않습니다. 유한 검산과 일반 증명을 구분합니다.

통상적인 효과적 형식 증명 체계에서는 모든 유한한 기호열을 길이 순서로 나열하고, 각각이 올바른 증명인지 기계적으로 확인할 수 있습니다. 합격한 증명들의 결론을 출력하면 증명 가능한 일차논리 문장을 빠짐없이 열거합니다. 괴델의 완전성 정리에 의해 전제 없는 논리적 타당성은 곧 증명 가능성과 일치하므로, 타당한 문장은 언젠가 반드시 목록에 나타납니다.

증명을 계속 찾았지만 아직 없다는 사실만으로는 제외할 수 없습니다. 다음 길이에서 증명이 나타날 가능성을 탐색만으로 제거할 수 없기 때문입니다. 이 절차는 타당성을 반결정하지만 모든 입력에서 멈추는 결정 절차는 아닙니다.

네. 충분히 풍부한 일반 일차논리 언어에서 모든 문장이 논리적으로 타당한지 매번 정확하게 종료하며 판정하는 알고리즘은 존재하지 않습니다. 처치의 정리 또는 일차논리 타당성의 결정 불가능성이라고 부릅니다. 특정한 좁은 문법이나 술어 형태에 제한을 두면 판정 가능한 부분 체계도 있으므로, ‘일차논리의 모든 작은 조각이 불가능하다’고 확대하면 안 됩니다.

계산 능력이나 시간의 부족이 아닙니다. 표준적인 알고리즘 개념 아래에서 어떤 알고리즘도 모든 입력에 대해 요구한 종료·정확성을 동시에 만족할 수 없다는 수학적 정리입니다.

문장 A가 만족 불가능하다는 것은 ¬A가 모든 모형에서 참이라는 뜻입니다. 따라서 증명 열거로 ¬A의 타당성을 확인할 수 있으면 A의 만족 불가능성을 반결정할 수 있습니다. 반대로 A의 만족 가능성을 일반적으로 같은 방식으로 반결정할 수 있는 것은 아닙니다. A가 무한 모형에서만 만족 가능할 때 단순한 유한 모형 열거는 끝없이 실패할 수 있습니다.

영역과 해석을 완전히 제시하고 A를 계산해 참을 확인했다면 A의 만족 가능성에 대한 올바른 긍정 증거입니다. 그러나 만족 가능한 문장이 언제나 유한 모형을 갖는다는 일반 정리는 성립하지 않습니다.

탐색 개수를 아무리 키워도 유한한 범위의 실패만 확인한 것입니다. 다음 위치에 증명이 나올 수 있습니다. 타당성 반결정기는 어떤 입력에서는 영원히 기다릴 수 있으므로, 오래된 실행은 논리적 부정의 증거가 아닙니다.

실제 사례의 상당수를 더 잘 처리할 수는 있습니다. 다만 ‘모든 입력에서 멈춘다’는 일반 보장을 만들지는 못합니다. 수학적 결정 불가능성과 실제 소프트웨어의 유용성을 함께 이해하면 두 진술을 혼동하지 않습니다.

T의 공리들이 효과적으로 나열 가능하면 T의 증명도 체계적으로 열거할 수 있습니다. 그래서 T⊢A의 긍정 사례를 반결정할 수 있습니다. 하지만 임의로 주어진 무한한 T에 대해 어떤 공리를 사용할 수 있는지조차 계산 가능한 방식으로 제공되지 않았다면 같은 주장에 추가 설명이 필요합니다.

네. 괴델–로서 불완전성의 핵심 조건 중 하나는 이론이 효과적으로 공리화되어 있다는 것입니다. 우리가 각 공리를 기계적으로 알아볼 수 있거나 열거할 수 있어야 증명을 수로 부호화하고 계산에 연결할 수 있습니다.

유한한 명제논리식의 타당성은 진리표로 결정 가능합니다. 일반 일차논리 타당성은 증명 열거로 반결정 가능하지만, 모든 입력에서 판정하는 절차는 없습니다. 일차논리 만족 불가능성 역시 부정식의 타당성을 열거하여 반결정 가능합니다. 이 셋에서 각 알고리즘이 어떤 경우에 멈추는지와 무엇을 보장하는지를 별도로 확인하는 것이 중요합니다.

⊨A는 모든 모형의 참, A의 만족 가능성은 적어도 한 모형의 참입니다. 양화 범위가 반대이므로 어떤 절차가 긍정을 확인하는지도 달라집니다.

모든 모형에서 따라오는 문장은 형식 증명을 갖는다는 의미론적 완전성을 얻었습니다. 여기서 증명이 유한한 형태로 존재하므로 그 증명을 열거하는 반결정도 얻습니다. 그러나 입력마다 ‘예’와 ‘아니요’를 모두 유한 시간 안에 판정하는 일은 별도의 문제이며, 일반 일차논리에는 해결할 수 없다는 정리가 있습니다.

효과적으로 공리화되고 충분한 기초 산술을 포함하는 일관된 이론에서는 어떤 산술 문장과 그 부정도 이론 내부에서 증명되지 않을 수 있다는 불완전성입니다. 이 정리의 대상은 특정 이론의 증명 능력이며 지금의 논리 체계 전체의 완전성과는 구별됩니다.