모든 논리 문제에
언제나 정답을 내는 계산법을
만들 수 있을까?

함수를 계산하는 규칙

처치의 계산 개념과 람다식의 대입을 실제로 따라갑니다.

6. 처치는 '계산법'이라는 말을 어떻게 좁혔을까요?

'사람이 요령껏 풀면 계산할 수 있다'는 표현만으로는 계산 방법의 범위를 정할 수 없습니다. 처치는 함수를 기호로 만들고 규칙에 따라 바꾸는 람다 계산법(λ-calculus, 함수를 만들고 적용하는 형식 체계)을 사용했습니다. 같은 시기의 재귀함수 연구도 효과적으로 계산할 수 있는 함수가 어떤 것인지 따지게 했습니다. 그 결과 어떤 함수는 주어진 규칙으로 계산할 수 있지만, 어떤 분류 문제에는 모든 입력을 처리하는 함수가 존재하지 않음을 증명할 수 있었습니다.

먼저 간단한 함수를 생각해 봅시다. 학생 이름 x를 받으면 그대로 돌려주는 함수는 λx.x로 적습니다. 입력 이름이 '민지'라면 결과도 '민지'입니다. λx는 '뒤의 식에서 x를 입력 변수로 쓰겠다'는 표시이고, 점 뒤의 x는 함수가 내놓는 값입니다. 수학 기호가 낯설어도 핵심은 입력을 받아 정해진 규칙으로 값을 낸다는 것입니다.

처치가 제시한 계산 가능성의 범위와 튜링이 기계 동작으로 정의한 계산 가능성의 범위는 뒤에 같은 것으로 확인되었습니다. 그렇다고 처치–튜링 명제가 다른 수학 정리와 똑같은 방식으로 증명된 법칙이라는 뜻은 아닙니다. 수학적으로 정확히 정의된 두 계산 모형이 같은 함수를 계산한다는 동치 정리와, 일상적인 의미의 '어떤 알고리즘도' 그 모형에 담긴다는 폭넓은 주장은 구분해야 합니다. 후자는 '효과적인 계산'이라는 비형식적 개념의 분석에 관한 명제입니다.

7. 람다 계산법의 실제 대입을 두 번 해 봅시다

(λx.x) A → A라고 쓰면, A가 어떤 값이든 그 값을 그대로 반환한다는 뜻입니다. 이번에는 (λx. x x) (λz.z)를 생각합시다. 먼저 x가 나타난 자리에 λz.z라는 함수를 넣으면 (λz.z) (λz.z)가 됩니다. 이 결과의 왼쪽 함수 역시 입력을 그대로 내놓으므로 마지막에는 λz.z가 남습니다. 람다 계산법에서 이런 대입에 따른 변형을 베타 축약(β-reduction, 함수 적용에 따른 치환)이라고 부릅니다.

여기서 λx.x의 x와 λz.z의 z는 각각 자신이 속한 함수 안에서만 쓰는 이름입니다. 예를 들어 λx.x와 λu.u는 변수 이름만 다를 뿐 같은 동작을 합니다. 어떤 입력이 들어왔는지, 어느 변수 이름이 그 함수에 묶여 있는지 분명하게 추적해야 합니다. 복잡한 식을 변형할 때는 다른 함수 안의 같은 철자 변수에 실수로 붙잡히지 않도록 이름을 바꿔 주기도 합니다. 논리학에서 기호의 뜻을 먼저 정하는 이유가 여기에 있습니다.

람다 계산법의 동작을 끝낼 수 없는 경우도 있습니다. Ω = (λx. x x)(λx. x x)라고 놓아 보겠습니다. 왼쪽 함수에 오른쪽 함수를 대입하면 다시 똑같은 Ω가 나옵니다. 한 번 바뀌고, 다시 바뀌고, 또 바뀌지만 최종 값에는 도달하지 못합니다. 이 현상은 특정 방식의 축약이 끝없이 반복되는 예입니다. 모든 람다식이 결과까지 간다는 보장은 없다는 사실을 눈으로 확인할 수 있습니다.

다만 Ω 하나가 멈추지 않는다는 사실만으로 '모든 프로그램의 종료 여부를 결정할 수 없다'는 정리를 증명한 것은 아닙니다. 모든 식을 입력받아 정답을 내는 일반 판정 절차가 없다는 결론에는 별도의 논증이 필요합니다. 이번 글에서 중요한 것은 규칙에 따라 한 단계씩 진행할 수 있음과 임의의 입력에 대해 언제나 끝을 판정할 수 있음 사이의 차이입니다.

증명을 찾는 일과 언제나 판정하는 일

괴델의 완전성 정리와 정지 문제를 연결하면서 질문의 차이를 밝힙니다.

8. 기계는 정답의 증거를 찾을 수 있는데도 왜 끝내지 못할까요?

여기서 제09회의 괴델 완전성 정리를 떠올릴 수 있습니다. 1차 논리에서 형식적 증명 규칙이 올바르게 구성되어 있다면 어떤 식이 모든 모형에서 참일 때 그 식의 유한한 형식적 증명이 존재합니다. 기호로는 ⊨ φ ⇒ ⊢ φ입니다. 건전성은 반대 방향 ⊢ φ ⇒ ⊨ φ를 보장하므로 둘을 함께 쓰면 ⊨ φ ⇔ ⊢ φ입니다.

형식적 증명은 유한하게 많은 기호와 규칙 적용으로 이루어집니다. 컴퓨터는 길이가 짧은 증명 후보부터 길이가 긴 후보까지 차례로 만들어 각 단계가 규칙에 맞는지 검사할 수 있습니다. 주어진 φ의 올바른 증명을 찾으면 '모든 모형에서 참'이라고 정답을 내고 멈춥니다. 증명이 실제로 존재하는 경우라면 언젠가 찾습니다.

그렇다면 φ가 타당하지 않을 때는 어떻게 될까요? 증명 후보를 백만 개 검사해도 실패했다는 사실만으로 앞으로 나올 모든 후보가 실패한다고 확정할 수는 없습니다. '아직 발견하지 못했다'와 '존재하지 않는다'는 서로 다른 판단입니다. 완전성 정리는 타당한 식에 증명이 존재함을 보장하지만, 타당하지 않은 식에 대해 컴퓨터가 언제 검사를 끝내고 아니요라고 답해야 하는지 알려 주지 않습니다.

그래서 1차 논리의 타당성 문제는 반결정 가능합니다. 타당한 식에는 유한한 시간 안에 긍정 답을 줄 수 있는 절차가 있지만, 타당하지 않은 식까지 모두 다루는 종료 보장은 없습니다. 이는 완전성 정리와 처치의 결정불가능성 정리가 서로 충돌하지 않는 가장 중요한 이유입니다.

9. 이미 알고 있는 정지 문제를 그대로 다시 증명할 필요는 없습니다

제12회에서 살펴본 튜링의 정지 문제를 간단히 떠올려 봅시다. 임의의 프로그램 M과 입력 w가 주어질 때, M이 w를 실행한 뒤 언젠가 멈추는지 모든 경우에 맞히는 종료 보장 판정기는 존재하지 않습니다. 이 결론을 얻는 논증은 가상의 판정기가 자기 자신의 동작을 예측하도록 만든 뒤 모순을 이끌었습니다.

이번 회차의 목표는 그 증명을 반복하는 것이 아닙니다. 서로 다른 문제를 연결하는 방법을 보여 주려는 것입니다. 첫 번째 문제는 프로그램의 종료 여부를 묻습니다. 두 번째 문제는 논리식이 모든 모형에서 참인지 묻습니다. 무엇을 입력받는지부터 다르므로 두 문제가 같다고 선언할 수 없습니다. 필요한 것은 첫 번째 문제의 모든 입력을 두 번째 문제의 입력으로 정해진 절차에 따라 바꾸는 번역입니다.

이 번역을 환원(reduction, 한 문제를 다른 문제의 입력으로 효과적으로 변환하는 방법)이라고 부릅니다. 종료 판정이 어려운 프로그램을 논리식 φ에 바꾸되, 프로그램이 멈출 때와 φ가 타당할 때가 정확히 일치하도록 만들면 됩니다. 만약 타당성을 언제나 판정하는 기계가 있다면 그 기계가 번역된 φ를 검사하도록 하여 종료 문제까지 풀 수 있게 됩니다. 하지만 종료 문제의 일반 판정기는 없다는 사실을 알고 있으므로 처음 가정했던 타당성 판정기도 존재할 수 없습니다.

앞에서부터는 현대적인 환원 증명의 설명입니다. 1936년 처치의 원증명은 람다식의 변환 가능성, 재귀성, 적절한 형식 체계의 판정 불가능성을 이용했습니다. 이를 뒤의 두 계산기 모형과 같은 문장으로 동일시하지 않겠습니다.

두 칸 계산기의 실행을 논리식으로 옮기기

계수기 기계의 상태, 명령, 시작·증가·감소 규칙을 정의합니다.

10. 자연수 두 칸만 가진 계산기를 먼저 정의합니다

현대적인 설명에서는 두 개의 숫자 칸 A와 B를 가진 작은 계산기를 사용해도 충분합니다. 각 칸에는 0 이상의 자연수가 들어 있습니다. 계산기에는 번호가 붙은 유한 개의 명령만 있고, 한 번에 다음 셋 중 하나를 실행합니다. 어느 한 칸의 수를 1 늘린 뒤 지정된 명령으로 이동, 한 칸이 0이면 정해진 명령으로 이동, 0이 아니라면 그 칸에서 1을 빼고 다른 명령으로 이동입니다. 마지막에는 멈춤 명령이 있습니다.

처음에는 장난감처럼 보이지만, 이러한 두 계수기 기계(two-counter machine, 자연수 두 칸과 유한한 명령으로 동작하는 계산 모형)가 적절한 부호화 아래 일반 튜링 기계를 모의할 수 있다는 사실이 알려져 있습니다. 두 칸이면 여러 숫자나 기호열의 정보를 큰 자연수에 부호화하여 보관할 수 있습니다. 이 사실의 전문적인 증명은 별도의 연구가 필요합니다. 여기서는 그 표준 정리를 사용하고, 뒤에서 예시 기계 한 대를 1차 논리로 정확히 옮기는 부분을 직접 검토합니다.

상태 q₀, q₁, q₂, …는 '지금 어느 명령을 실행하는가'를 나타냅니다. qᵢ(a,b)는 '상태 qᵢ에서 첫 번째 칸의 수가 a, 두 번째 칸의 수가 b인 계산 상황에 도달할 수 있다'는 관계 기호로 사용하겠습니다. qᵢ는 참·거짓을 판단하는 두 자리 술어입니다. 0은 수 0을 가리키는 상수이고, S(x)는 x 다음 자연수, 곧 x+1을 가리키는 함수입니다. 다만 임의의 모형 안에서는 S를 '다음 수'처럼 해석하도록 강제하는 관계식이 무엇인지 별도로 확인해야 합니다. 아래의 정확한 환원은 모형 전체를 표준 자연수로 고정할 필요 없이 작동합니다.

11. 실제로 멈추는 세 단계 계산을 논리식으로 바꿔 봅시다

예시 프로그램의 첫 명령은 q₀에서 A를 1 늘리고 q₁로 이동하는 것입니다. 둘째 명령은 q₁에서 A가 0이면 q₃로 이동하고, 0이 아니면 A를 1 줄인 뒤 q₂로 이동합니다. q₂는 멈춤 상태입니다. 시작 계산 상황은 (q₀, 0, 0)입니다.

처음에는 A=0, B=0입니다. 첫 명령을 실행하면 A=1이 되어 (q₁,1,0)에 도달합니다. 둘째 명령에서는 A가 0이 아니므로 A를 하나 줄이고 q₂로 갑니다. 결과는 (q₂,0,0)이며 계산이 끝납니다. 학생이 이 경로를 종이에 추적하면 세 상태를 거쳐 끝났다는 사실을 직접 확인할 수 있습니다. 다른 시작값이나 다른 프로그램이면 경로는 달라질 수 있으나, 지금 정의한 예시는 명확하게 멈춥니다.

이제 프로그램의 동작을 네 개의 논리 규칙으로 적겠습니다. 다음 규칙은 모두 우리 예시를 위한 현대적 형식화입니다.

시작: q₀(0,0).
증가: ∀x∀y(q₀(x,y) → q₁(S(x),y)).
0일 때: ∀y(q₁(0,y) → q₃(0,y)).
1 감소: ∀x∀y(q₁(S(x),y) → q₂(x,y)).

첫 규칙은 q₀(0,0)을 출발점으로 두라는 뜻입니다. 둘째는 q₀에 도달한 수쌍 (x,y)가 있으면 A가 S(x)로 증가한 q₁ 상황에도 도달한다는 뜻입니다. 셋째는 A가 0인 q₁ 상황에서는 q₃로 이동한다는 뜻입니다. 넷째는 A가 어떤 x의 다음 수 S(x)라면 한 칸 감소한 x를 가지고 q₂에 도달한다는 뜻입니다. B는 이 예시에서 변하지 않으므로 같은 y를 사용합니다.

첫 번째와 두 번째 규칙으로 q₁(S(0),0)을 얻습니다. 이 식과 네 번째 규칙에 x=0, y=0을 넣으면 q₂(0,0)을 얻습니다. q₂는 멈춤 상태이므로 ∃x∃y q₂(x,y)가 따라옵니다. '언젠가 멈추는 계산 상황에 도달한다'는 결론입니다. 누가 값을 고를지 모르는 변수를 거치지 않고 두 번의 규칙 적용으로 도출할 수 있습니다.

논리식이 항상 참이라면 무엇을 뜻할까?

실제 계산이 멈추면 모든 모형에서 논리식이 참인 방향을 증명합니다.

12. 규칙을 하나로 묶어 타당성 문제로 바꿉니다

위의 네 규칙을 모두 논리곱 ∧으로 이어 붙여 A라는 식으로 만들고, H := ∃x∃y q₂(x,y)를 멈춤 상태의 도달 가능성으로 정하겠습니다. 그러면 한 개의 1차 논리식이 만들어집니다.

Φ := A → H

한국어로는 '출발 상태와 모든 이동 규칙을 만족하는 어떤 세계에서도, 멈춤 상태에 도달한다'는 뜻입니다. 우리가 살펴본 예시에서는 규칙을 적용해 q₂(0,0)를 이끌 수 있으므로 모든 모형에서 Φ가 참입니다. 가령 어떤 모형이 A를 거짓으로 만들면 함의식 A→H는 참입니다. A를 참으로 만드는 모형이라면, 앞에서 적용한 두 규칙 때문에 H도 반드시 참입니다. 따라서 그때도 Φ는 참입니다. 두 경우를 모두 확인해야 '타당하다'는 결론이 성립합니다.

여기서 A는 '지구상의 실제 기계가 이렇게 동작했다'는 경험적 관찰문이 아닙니다. 입력 기계의 명령을 일정한 기호 규칙으로 옮긴 유한한 1차 논리식입니다. 한 기계에 명령이 백 개면 대응하는 규칙도 유한하게 늘어납니다. 기계의 명령 목록과 시작 숫자가 주어지면 사람의 창의적 추측 없이도 대응하는 A와 H를 자동으로 만들 수 있습니다.

예시의 핵심을 확장하면, 임의의 두 계수기 기계 M에 대해 Φ_M = (A_M → H_M)을 만드는 규칙을 얻습니다. 질문은 이제 'M이 멈출까?'에서 'Φ_M이 모든 모형에서 참일까?'로 바뀝니다. 아직 이것만으로 일반 정리를 얻은 것은 아닙니다. 정확히 멈출 때에만 타당하다는 양방향 관계를 보여야 합니다.

13. 기계가 멈추면 논리식이 반드시 타당합니다

M이 실제로 n번 명령을 실행한 뒤 멈춘다고 가정해 봅시다. 그동안 거친 상태와 두 숫자 칸의 값은 모두 유한하게 적을 수 있습니다. A_M에는 각 명령이 다음 상태를 어떻게 만드는지 나타내는 규칙이 들어 있으므로, 출발 사실에 해당 규칙을 차례로 적용할 수 있습니다. 결국 멈춤 상태를 나타내는 술어 qₕ에 대해 qₕ(a,b)를 도출하게 됩니다. a와 b는 이 실제 계산에서 마지막에 남은 숫자입니다.

따라서 A_M ⊢ ∃x∃y qₕ(x,y)입니다. 기호 ⊢는 앞의 가정에서 형식적 증명을 만들 수 있다는 뜻입니다. 건전성에 의해 A_M을 참으로 만드는 모든 모형에서 결론도 참입니다. 그러므로 ⊨ (A_M → ∃x∃y qₕ(x,y))입니다. 이 식이 Φ_M입니다.

이 방향의 논증에서 중요한 단어는 '유한'입니다. 계산이 실제로 멈췄기 때문에 유한한 개수의 이동 규칙을 잇는 증명이 존재합니다. 아무리 큰 입력이라도 특정 실행이 멈추었다면 그 실행 기록의 길이는 자연수 하나로 정해집니다. 따라서 해당 실행 기록 전체를 1차 논리의 유한한 증명으로 옮길 수 있습니다.

이때 A_M의 모든 모형이 자연수의 표준적인 모형일 필요는 없습니다. 다른 모형에서도 출발 사실과 유한한 이동 규칙을 참으로 만들었다면, 그 유한한 규칙 적용 결과를 함께 참으로 만들어야 합니다. 그래서 모든 모형에서의 참이라는 강한 결론이 성립합니다.

멈추지 않는 계산의 반례와 최종 모순

표준 자연수 모형을 만들어 반례를 확인하고 만능 판정기 가정의 모순을 얻습니다.

14. 기계가 영원히 멈추지 않으면 타당하지 않은 모형이 있습니다

이번에는 M이 출발한 뒤 아무리 오래 실행해도 멈춤 상태로 가지 않는다고 가정해 봅시다. 우리가 알고 있는 자연수 집합 ℕ = {0,1,2,3,…}을 하나의 모형의 대상으로 사용하겠습니다. 여기서 0은 실제 자연수 0으로, S는 실제로 1을 더하는 함수로 해석합니다. 술어 qᵢ(x,y)는 M이 시작 상태에서 규칙을 따라 실행하다가 '상태 i, A=x, B=y'에 실제로 도달하는 경우에만 참으로 정합니다.

이렇게 정하면 시작 상태는 참이고, 도달한 상태에서 프로그램의 규칙대로 이동하는 다음 상태도 도달 가능하므로 A_M의 모든 이동 규칙이 참입니다. 그러나 M은 멈추지 않는다고 가정했습니다. 멈춤 상태 qₕ에 도달한 숫자쌍은 하나도 없습니다. 그러므로 H_M은 거짓입니다. 이 모형에서는 A_M은 참이고 H_M은 거짓이어서 함의식 Φ_M = A_M → H_M이 거짓입니다.

반례 모형 하나만 찾으면 '모든 모형에서 참'이라는 주장은 무너집니다. 따라서 M이 멈추지 않으면 Φ_M은 논리적으로 타당하지 않습니다. 위의 멈추는 경우와 합치면 다음 양방향 관계를 얻습니다.

M이 시작 입력에서 멈춘다 ⇔ ⊨ Φ_M

이 관계는 단순히 문장 두 개가 우연히 같은 답을 낸다는 이야기가 아닙니다. 임의의 기계 명령을 받아 유한한 기호 조작만으로 Φ_M을 만들어 내는 효과적인 번역 절차가 있기 때문에 계산 불가능성의 증명에 쓸 수 있습니다. 실제 학술 증명에서는 기계가 두 계수기 모형으로 모의될 수 있다는 사실까지 함께 사용합니다.

15. 최종 결론: 만능 타당성 판정기를 가정하면 모순이 생깁니다

잠시 D라는 기계가 있다고 가정해 보겠습니다. 입력으로 어떤 1차 논리식 φ를 받더라도 반드시 멈춰서, φ가 모든 모형에서 참이면 '예', 그렇지 않으면 '아니요'라고 정확히 답하는 기계입니다. D가 어떤 식에서는 오래 기다리라고 말하는 정도라면 출발 조건에 맞지 않습니다. 모든 입력에 대해 유한한 시간 안에 대답해야 합니다.

임의의 두 계수기 기계 M을 입력받아 위의 방식으로 Φ_M을 만들겠습니다. 그다음 Φ_M을 D에 입력합니다. D가 '예'라고 답하면 M은 멈추고, '아니요'라고 답하면 M은 멈추지 않습니다. Φ_M을 만드는 계산도 유한하고 D도 항상 끝난다고 가정했으므로, 이 조합은 모든 두 계수기 기계의 종료 여부를 알아내는 일반 판정기가 됩니다.

그런데 두 계수기 기계는 튜링 계산을 모의할 수 있고, 그 기계들의 일반적인 정지 문제는 결정할 수 없습니다. 따라서 D가 있다는 가정은 이미 확립된 계산 불가능성의 결과와 모순됩니다. 이처럼 어떤 대상이 존재한다고 가정한 뒤 그 가정에서 모순을 이끌어 존재할 수 없음을 보이는 방법을 귀류법이라고 합니다. 그러므로 임의의 1차 논리식의 타당성을 항상 유한하게 판정하는 알고리즘은 존재하지 않습니다. 이것이 오늘날 흔히 처치의 정리(Church’s theorem, 1차 논리의 일반 타당성 결정불가능성)라고 부르는 결과입니다.

마지막 한 걸음을 다시 확인합시다. 특정 논리식이 어려워서 아직 답을 모른다는 주장이 아닙니다. 해결된 공식이나 쉽게 판정할 수 있는 문장들이 얼마든지 있습니다. 그러나 가능한 모든 1차 논리식을 한꺼번에 책임지는 완전한 예·아니요 판정 절차는 어떤 방식으로 만들더라도 존재할 수 없다는 것이 수학적 결론입니다.

완전성, 결정불가능성, 판정 가능한 부분

정리가 다루는 범위와 실제 판정 도구가 해결할 수 있는 경우를 구별합니다.

16. 괴델의 완전성과 처치의 결정불가능성은 함께 성립합니다

학생들이 가장 많이 묻는 질문을 다시 살펴봅시다. '제09회에서 모든 참인 논리식은 증명할 수 있다고 했는데, 왜 이번에는 판단할 수 없다고 하나요?' 앞 정리의 질문은 타당한 논리식에 유한한 증명이 존재하는가였습니다. 이번 정리의 질문은 논리식이 타당한지 아닌지 매번 유한한 시간 안에 알아내는 알고리즘이 있는가입니다. 증명의 존재를 보장하는 일과, 존재하지 않는 증명을 더 찾아볼 필요가 없다고 알 수 있는 일은 서로 다릅니다.

비유를 쓰자면, 자격증을 발급받은 사람은 언젠가 발급증을 제시할 수 있습니다. 그러나 아무것도 제시하지 않는 사람이 아직 증서를 찾는 중인지, 애초에 발급받지 않았는지는 '아직 제시하지 않았다'는 사실만으로 판정할 수 없습니다. 이 비유가 완전히 일치하는 것은 아닙니다. 자격증은 행정기관의 유한한 기록으로 확인할 수 있기 때문입니다. 비유에서 가져와야 할 부분은 긍정의 유한한 증거를 찾는 절차와 부정의 종료 판정을 구별한다는 점입니다.

논리적으로 더 정확하게 적으면 다음 두 문장은 동시에 참입니다.

완전성·건전성: ⊨ φ ⇔ ⊢ φ.
결정불가능성: 모든 φ에 대해 '⊨ φ인가?'를 항상 종료하며 판정하는 알고리즘은 없다.

증명 후보를 차례로 검사하는 기계는 타당한 φ에는 '예'라고 끝내 줍니다. 타당하지 않은 φ에는 언제 '아니요'라고 끝내도 되는지 일반적인 기준이 없습니다. 이것이 제09회와 이번 회차를 이어 주는 논리적인 연결입니다. 두 정리가 모순이기는커녕, 서로 다른 한계를 정밀하게 구분하게 해 줍니다.

17. 어떤 문제는 여전히 정확하게 판정할 수 있습니다

처치의 정리는 우리가 사용하는 개별 논리 학습 도구를 모두 포기하라는 뜻이 아닙니다. 명제논리식은 언제나 진리표로 판정할 수 있습니다. 1차 논리라도 사용 가능한 모형의 원소 수를 고정된 유한한 수로 제한하고, 관계·함수 기호를 유한하게 정하면 가능한 해석을 전수검사할 수 있습니다. 정확한 원소 수의 상한이 입력과 무관하게 미리 정해진 경우, 모든 해석을 열거하는 방법이 존재합니다.

또한 단항 술어만 있는 1차 논리의 적절한 단편처럼 일반적인 타당성 판정 방법이 알려진 경우도 있습니다. 이때 '단항'은 P(x)처럼 대상 한 개에만 적용하는 관계 기호를 말합니다. C(x,y)처럼 두 대상을 연결하는 관계 기호까지 무제한 허용하는 일반적인 1차 논리와는 표현할 수 있는 구조가 다릅니다. 단항 단편의 결정 가능성도 어떤 함수·관계 기호를 허용하느냐에 따라 조건을 자세히 명시해야 합니다.

반대로 '이번 검사가 백 가지 사례에서 모두 통과했다'는 사실을 전체 논리식의 결정 절차로 확대해서는 안 됩니다. 100개의 특정 식이 참인 사례를 찾은 경험은 101번째 식까지 늘 적용될 수 있는 일반적인 증명을 대신하지 않습니다. 임의의 논리식 전체를 대상으로 종료를 보장하는가, 검사 대상의 범위를 정확하게 정했는가를 확인해야 합니다.

오늘날의 자동정리증명기와 검증 도구는 이 한계 안에서도 아주 강력하게 작동합니다. 넓은 범위의 실제 문제를 빠르게 해결하고, 증명에 성공하면 기호 수준의 검증 가능한 기록을 남깁니다. 일반적인 결정 불가능성과 많은 실제 사례의 해결 가능성은 같은 도구를 평가할 때 함께 고려할 사항입니다.