증명과 참은 어떻게 이어지나요?

이번에는 우리가 쓰던 도구 자체를 살펴보겠습니다. 규칙에 맞게 증명한 결론은 왜 전제가 참일 때 참일까요? 전제들이 참인 모든 경우에 따라오는 결론이라면, 그 결론의 증명도 반드시 있을까요? 이런 질문을 논리 체계에 관한 연구, 메타논리라고 부릅니다.

맞습니다. 한편 기호를 한 줄씩 쓰지 않고도, 두 전제가 모두 참인 상황에서는 아라가 도장을 받지 않은 경우가 불가능하다고 설명할 수 있습니다. 두 방법이 어떤 기준을 사용하는지 나누어 보겠습니다.

Γ는 “감마”라고 읽습니다. 전제들을 모아 놓은 집합의 이름으로 쓰겠습니다. 이번에는 Γ={∀x(P(x)→Q(x)), P(a)}입니다. 중괄호 안에 전제 두 개를 적었지요. 이번 편의 Γ는 유한한 수의 닫힌 문장으로 이루어진 모음으로 한정합니다. 자유변수가 없는 문장을 “닫힌 문장”이라고 부릅니다.

이 설명에서 A는 문장 전체를 대신하는 말입니다. P나 Q처럼 대상에 적용할 새로운 술어를 넣는 것은 아닙니다. Γ도 등록부 속 사람을 가리키는 이름이 아닙니다. 기호로 쓴 문장에 대해 이야기하기 위한 표시라고 이해하세요.

Γ ⊢ Q(a)는 “전제 Γ에서 Q(a)를 증명할 수 있다”라고 읽겠습니다. 중급에서 사용한 자연연역 규칙을 고정하고, 그 규칙에 맞는 유한한 증명 하나가 존재한다는 뜻입니다. 마지막에 해제되지 않은 가정은 Γ에 들어 있는 것들만 허용합니다.

네. 다른 증명에서는 임시 가정을 열어도 됩니다. 다만 마지막까지 남겨 둔 가정이 Γ 밖에 있다면, 그 증명만으로 Γ ⊢ Q(a)를 주장할 수 없습니다. 예를 들어 Q(a) 자체를 새 가정으로 쓰고 그대로 끝내면, Γ만으로 얻은 결론이 되지 않습니다.

Γ ⊨ Q(a)는 “Q(a)가 Γ의 의미적 귀결이다”라고 읽습니다. 쉽게 풀면, Γ의 모든 전제가 참인 해석에서는 언제나 Q(a)도 참이라는 뜻입니다. 규칙표의 줄이 아니라 해석에서의 참을 기준으로 합니다. Γ를 모두 참으로 만드는 해석을 Γ의 모형이라고 부르겠습니다.

Γ를 참으로 만드는 아무 해석이나 생각해 보세요. P(a)가 참이므로 a가 가리키는 대상은 서류를 낸 대상입니다. 또 ∀x(P(x)→Q(x))가 참이므로 그 대상을 포함한 모든 제출자는 Q를 만족합니다. 따라서 Q(a)가 참입니다. 대상이 몇 명인지, 다른 사람의 도장 여부가 어떤지는 이 이유에 영향을 주지 않습니다.

M을 하나의 해석 이름으로 쓰면 M ⊨ Q(a)는 “해석 M에서 Q(a)가 참이다”라는 뜻입니다. Γ는 전제 문장들의 모음이고 M은 그 문장에 뜻과 값을 주는 세계입니다. 왼쪽에 무엇이 오는지 확인하면 같은 ⊨ 표시를 어떻게 읽을지 알 수 있습니다.

정확합니다. “모형”이라는 말 뒤에는 무엇의 모형인지가 필요합니다. 같은 M₁은 Γ를 참으로 만들지만, Γ와 ∀xQ(x)를 모두 포함한 더 큰 문장 모음은 참으로 만들지 않습니다.

⊢ A는 빈 전제 모음에서 A를 증명할 수 있다는 뜻이며, 이런 A를 그 체계의 정리라고 부릅니다. ⊨ A는 모든 허용 해석에서 A가 참이라는 뜻이며, 이런 문장을 타당식이라고 부릅니다. 하나는 증명의 존재, 다른 하나는 모든 해석에서의 참으로 정의합니다.

그 가정은 3번에서 해제되었습니다. 마지막에 남은 가정이 없으므로 정리를 얻었습니다. 4번에서는 d에 관한 열린 가정이 없고 d를 모두 안전하게 x로 바꾸므로 전칭 도입 조건도 충족합니다. 의미 쪽으로 보면 P(x)→P(x)는 각 대상에게 참이고, 따라서 그 전칭문은 모든 해석에서 참입니다.

의미적 귀결은 그 전제들이 참인 경우의 결론을 보장합니다. 전제가 실제 기록과 맞는지는 조사해야 합니다. 가령 아라가 서류를 냈지만 도장을 받지 않은 실제 기록을 확인했다면, 이번 전제 중 ∀x(P(x)→Q(x))가 그 기록에서는 거짓이 됩니다. 그래도 두 전제에서 Q(a)로 가는 논증의 형식적 타당성은 그대로입니다.

그렇습니다. 건전한 증명 체계로 어떤 거짓 전제에서 조건부 결론을 도출할 수도 있습니다. 체계의 건전성은 그 전제를 현실의 사실로 만들어 주는 성질이 아닙니다. 전제 모음을 참으로 만드는 해석에서 결론의 참을 지킨다는 성질입니다.

어떤 전제 모음 Γ와 결론 A에 대해서도, Γ ⊢ A이면 Γ ⊨ A라는 조건입니다. 증명할 수 있는 모든 결론이 전제들의 의미적 귀결이어야 합니다. 이 방향을 증명 체계의 건전성이라고 부릅니다.

예를 들어 “∃xQ(x)에서 ∀xQ(x)로 가도 된다”는 규칙을 임의로 추가했다고 합시다. M₁에서 아라와 찬우는 확인받았지만 보라는 확인받지 않았습니다. 따라서 ∃xQ(x)는 참이고 ∀xQ(x)는 거짓입니다. 그 규칙을 허용한 체계는 참인 전제에서 거짓인 결론을 도출할 수 있어 건전성 조건을 어깁니다.

각 증명을 목록으로 만들어 하나씩 검토하는 방법은 끝나지 않겠지요. 대신 증명이 어떻게 만들어지는지 살펴봅니다. 시작점의 가정이 참인 해석을 잡고, 허용된 각 규칙이 그 참을 적절히 보존한다는 것을 보입니다. 그러면 짧은 부분 증명에서 더 긴 증명으로 성질을 이어 갈 수 있습니다.

그 부분은 더 조심해야 합니다. 안쪽 가정이 거짓인 해석도 있을 수 있습니다. 따라서 그 줄이 기대는 가정들이 모두 참이면 그 줄도 참이라는 형태로 성질을 이어 갑니다. 미해제 가정을 정확히 추적해야 조건문 도입과 존재 제거도 설명할 수 있습니다.

완전성은 Γ ⊨ A이면 Γ ⊢ A라는 뜻입니다. 전제들의 의미적 귀결인 결론에 증명이 있다는 보장입니다. 아무 문장이나 다 증명할 수 있다는 뜻으로 쓰지 않습니다. 전제에서 따라오지 않는 문장까지 증명하면 오히려 건전성에 문제가 생깁니다.

표준적인 고전 일차논리 자연연역은 비어 있지 않은 영역의 통상적인 의미론에 대해 건전하고 완전합니다. 이는 ⊢와 ⊨의 모양이 닮았기 때문이 아니라 별도로 증명되는 정리입니다. 여기서는 그 알려진 결과의 뜻을 먼저 소개합니다. 이 과정에서는 건전성의 근거부터 차례로 만들고 완전성이 성립하는 이유로 이어 가겠습니다.

사용하는 체계의 건전성이 확보되어 있다면 말할 수 있습니다. 만약 Γ ⊢ ∀xQ(x)라면 건전성에 의해 Γ ⊨ ∀xQ(x)여야 합니다. 그런데 M₁은 Γ의 모든 전제를 참으로 만들면서 ∀xQ(x)를 거짓으로 만듭니다. 따라서 그 체계에서는 그런 증명이 있을 수 없습니다.

그것만으로는 쓸 수 없습니다. ⊬는 아직 못 찾았다는 기록보다 강한 주장으로, 증명이 없다는 뜻입니다. 탐색이 실패했을 때에는 더 긴 증명이 있을 수도 있고 다른 전략이 필요할 수도 있습니다. 반모형과 건전성처럼 모든 가능한 증명을 배제하는 근거가 필요합니다.

이번 절에서는 원래 Γ와 별도로 Δ={P(a), ¬P(a)}를 생각하겠습니다. Δ는 “델타”라고 읽는 새 전제 모음입니다. 고전 이값 논리에서 P(a)와 ¬P(a)를 동시에 참으로 만드는 해석은 없습니다.

맞습니다. Δ의 전제를 모두 참으로 만드는 해석 자체가 없으므로, 그런 반모형도 없습니다. 의미적 귀결의 정의에 따라 Δ ⊨ Q(a)가 성립합니다. 같은 이유로 어떤 결론 A를 골라도 Δ ⊨ A입니다. 이것은 Q(a)가 모든 해석에서 참이라는 말과 다릅니다.

⊥는 모순을 표시하며 항상 거짓으로 해석합니다. 이 증명이 있다고 해서 Δ의 두 전제가 함께 실제 사실이 될 수 있는 것은 아닙니다. 서로 모순되는 정보를 넣으면 무엇이든 도출할 수 있다는 성질 때문에, 전제 모음이 함께 성립 가능한지도 따로 확인해야 합니다.

두 문장의 대상을 나누어 보겠습니다. 앞서 말한 논리의 증명 체계가 완전하다는 것은 전제의 모든 모형에서 따라오는 문장에 증명이 있다는 뜻입니다. 반면 이론 T가 완전하다는 말은, 그 언어의 각 문장 A에 대해 T에서 A를 증명하거나 T에서 ¬A를 증명할 수 있다는 뜻으로 쓰입니다. 이 두 정의는 같지 않습니다.

그럴 수 있습니다. 그런 경우에는 T의 모든 모형이 A의 값에 동의할 필요가 없습니다. 어떤 T의 모형에서는 A가 참이고 다른 T의 모형에서는 거짓일 수 있습니다. 그러면 T ⊨ A도 T ⊨ ¬A도 아니어서, 논리의 완전성이 어느 쪽의 증명을 요구하지 않습니다.

같은 P와 Q의 뜻을 쓰되, 마지막 연습의 전제 모음을 Θ={∀x(P(x)→Q(x)), ∃xP(x)}로 바꾸겠습니다. Θ는 “세타”라고 읽습니다. 특정 이름의 제출 사실 대신 제출자가 적어도 한 명 있다는 전제를 사용합니다. 첫 목표는 ∃xQ(x)입니다.

다음 2편에서는 이 문장들이 어떤 규칙으로 만들어지는지부터 다시 정리합니다. 이름·변수·함수항·식·문장을 나누고, 작은 구성에서 큰 구성으로 성질을 이어 가는 귀납의 생각을 익히겠습니다. 오늘 구별한 ⊢와 ⊨를 정확히 연결하려면 양쪽에서 다루는 대상을 먼저 분명히 해야 합니다.