증명 규칙은 왜 참을 지켜 주나요?

네. 가령 P(a) → Q(a)와 P(a)에서 Q(a)를 얻는 규칙을 익혔지요. 오늘은 “어떤 해석에서도 앞의 두 문장이 참이면 마지막 문장도 참인가?”를 묻습니다. 문장의 뜻으로 증명 규칙을 살펴보는 질문입니다.

규칙의 이름을 정확히 적었다는 사실과 그 규칙이 참을 보존한다는 사실을 연결해 보겠습니다. 그 연결이 여러 단계의 증명에서도 유지되면, 전제를 모두 만족하는 모형에서 결론도 참이라고 말할 수 있습니다.

오늘은 ∧, ∨, →, ¬, ⊥를 다루는 명제논리 규칙에 집중합니다. ⊥는 모순을 나타내며 어느 모형에서도 참으로 평가하지 않습니다. 고전논리의 이중부정 제거도 살펴보겠습니다. 쌍조건문 A ↔ B는 (A → B) ∧ (B → A)로 풀어 읽습니다.

양화사가 든 닫힌 문장도 하나의 문장으로 놓고 연결사 규칙을 적용할 수 있습니다. 다만 오늘은 양화사를 도입하거나 제거하는 규칙을 증명에 사용하지 않습니다. 그 규칙의 건전성과 동일성 규칙은 다음 편에서 이어 살펴봅니다.

그런 업무 규칙을 가정하려면 p → q를 전제로 적어야 합니다. 제출했다는 술어의 뜻만으로 확인까지 끝났다고 정하지는 않습니다. 조건을 명시해야 우리가 어느 전제를 이용했는지 알 수 있습니다.

맞아요. A, B, C는 문장 전체를 가리키는 메타언어의 글자입니다. A를 p ∨ q로 정하면 같은 규칙 안의 모든 A 자리에 그 문장 전체를 넣습니다. 중간에 뜻을 바꾸지 않습니다.

연결사의 진리표는 A와 B의 가능한 참거짓 조합을 다룹니다. 실제로 어떤 A와 B가 의미상 연관되어 일부 조합이 생기지 않더라도, 네 조합 전체에서 안전한 연결사 규칙은 실제 생길 수 있는 조합에서도 안전합니다.

증명은 주어진 전제가 참일 때 결론이 어떻게 따라오는지 보여 줍니다. 전제를 실제 조사로 확인했는지는 별도의 일입니다. 가정 A만으로 이루어진 가장 짧은 도출은 A ⊢ A입니다. A를 참으로 만드는 모형에서는 A가 참이므로, 이 시작 단계가 안전합니다.

앞서 얻은 줄을 다시 쓰는 반복 규칙도 그 줄을 사용할 수 있는 가정 범위 안에서 적용합니다. 이미 닫힌 부분 증명 안의 줄을 밖에서 그냥 가져오지는 않습니다.

A를 얻는 데 필요한 미해제 가정들이 Γ이고, B를 얻는 데 필요한 미해제 가정들이 Δ라고 합시다. Γ는 감마, Δ는 델타라고 읽습니다. 두 결과를 함께 사용하려면 두 쪽 가정을 모두 유지해야 합니다. 그 모음을 Γ ∪ Δ라고 씁니다. ∪는 합집합 기호입니다.

예를 들어 한 줄은 p라는 가정에, 다른 줄은 q라는 가정에 기대고 있다면, 둘을 합쳐 얻은 p ∧ q는 p와 q 양쪽 가정에 기대게 됩니다. 어느 하나를 기록에서 없애면 보장 내용이 달라집니다.

그 자연스러운 생각을 의미론의 정의로 적어 봅시다. 같은 모형 M에서 A ∧ B가 참일 조건은 A와 B가 둘 다 참이라는 것입니다. 그래서 A와 B를 각각 확보했을 때 A ∧ B를 얻는 연언 도입 ∧I가 참을 보존합니다.

A가 Γ에서, B가 Δ에서 따라온다면 Γ와 Δ를 모두 만족하는 임의의 모형을 잡습니다. 그 모형에서 A도 참이고 B도 참이므로 연언도 참입니다. 이로써 Γ ∪ Δ ⊨ A ∧ B를 얻습니다.

네. 연언 제거 ∧E는 A ∧ B에서 A를 얻거나 B를 얻습니다. 연언 전체가 참인 경우는 표의 첫 줄뿐이므로 어느 쪽도 거짓일 수 없습니다.

규칙을 적용하려는 문장의 가장 바깥 연결사가 ∧인지 확인해야 합니다. p ∨ (q ∧ r) 전체는 선언문입니다. 그 안에 ∧가 보인다고 q나 r을 바로 꺼내지는 못합니다.

조건문 제거 →E를 살펴봅시다. A → B는 A가 참이고 B가 거짓일 때만 거짓입니다. 이제 A도 참이고 조건문도 참이라고 해 봅시다. 만약 B가 거짓이라면 조건문이 거짓이어야 하므로, 처음의 조건과 맞지 않습니다. 따라서 B는 참입니다.

이 설명은 특정 등록부나 특정 사람의 성질에 의존하지 않습니다. 고전 조건문의 참거짓 조건과 두 입력이 함께 참이라는 사실만 이용합니다.

두 입력 중 A도 참이어야 하기 때문입니다. “조건문은 참이지만 A는 거짓”인 줄에서는 이 규칙의 입력 조건이 갖추어지지 않습니다.

가정까지 함께 읽으면 이렇습니다. Γ에서 A → B를 얻고 Δ에서 A를 얻었다고 합시다. Γ와 Δ를 모두 참으로 만드는 모형에서는 조건문과 A가 모두 참이므로 B도 참입니다. 결론에는 두 쪽의 미해제 가정을 유지합니다.

규칙 후보가 허용하는 추론을 먼저 검사해야 합니다. A가 거짓이고 B가 참이면 A → B도 참입니다. 그러면 후보의 두 입력은 모두 참인데 결론 A는 거짓입니다. 이 한 경우로 그 규칙은 참을 보존하지 못한다는 사실을 알 수 있습니다.

우리 언어에서는 다음의 한 사람 모형으로 실제 반모형을 만들 수 있습니다. 이전 사례의 자료를 고치는 것이 아니라 새로 정한 검사용 모형 M₀입니다.

맞아요. 전제들이 허용하는 다른 경우를 버리고 결론을 강화했기 때문입니다. 조건문은 전건이 참일 때 후건이 참이어야 한다는 제한을 두지만, 후건이 참이면 전건도 참이라는 제한이나 전건이 거짓이면 후건도 거짓이라는 제한까지 두지는 않습니다.

특정 업무에서 확인은 반드시 제출 뒤에 이루어진다는 추가 사실이 있다면 q → p 같은 새 전제로 적어 분석할 수 있습니다. 그 전제가 없는 추론 규칙 자체를 건전하게 만들어 주지는 않습니다.

조건문 도입 →I에서는 A라는 표시된 임시 가정을 열고 그 범위에서 B를 도출합니다. 부분 증명에 남은 다른 가정들을 Γ라고 합시다. 부분 증명은 “Γ의 문장들과 A가 모두 참인 모형에서는 B가 참이다”라는 보장을 제공합니다.

이제 Γ를 만족하는 임의의 모형 M을 잡습니다. A가 거짓이면 조건문의 뜻에 따라 A → B는 참입니다. A가 참이면 M은 Γ와 A를 함께 만족하므로 부분 증명의 보장에 따라 B가 참입니다. 이 경우에도 조건문은 참입니다. 따라서 Γ에서 A → B가 따라옵니다.

그렇습니다. 해제한 가정은 조건문의 전건에 들어갑니다. 다른 미해제 가정 Γ는 그대로 남습니다. 부분 증명에서 B를 얻었다는 이유로 B만 밖으로 가져오면, A가 거짓인 모형까지 다루는 데 필요한 근거가 사라집니다.

가정에는 h 같은 표지를 붙일 수 있습니다. 같은 문장이 다른 전제로 이미 있더라도 이번에 닫기로 한 임시 가정의 출현만 해제합니다. 같은 문구를 가진 모든 가정을 한꺼번에 지운다고 이해하지 마세요.

전제는 p → q와 q → r입니다. 목표가 p → r이므로 p를 임시 가정하고 r을 얻은 뒤 조건문을 만들겠습니다. 아래에서 1과 2는 전제의 표지이고, h는 3줄의 임시 가정 표지입니다.

5줄에서 r을 얻을 때는 p라는 임시 가정이 필요했습니다. 6줄에서는 그 가정을 닫으며 조건문 전체를 얻습니다. 따라서 두 전제가 참인 모든 모형에서 p → r은 참이지만, r이 반드시 참이라는 말까지 얻지는 않았습니다.

이를 확인하려면 한 사람 모형에서 P, Q, S의 외연을 모두 공집합으로 두세요. p, q, r이 모두 거짓이어도 두 전제와 결론 조건문은 모두 참입니다. 이 모형은 r만 밖으로 가져오는 잘못을 드러냅니다.

선언 도입 ∨I에서는 A가 참이면 A ∨ B가 참이라는 뜻을 이용합니다. B가 참일 수도 거짓일 수도 있지만 적어도 A가 참입니다. B를 확보한 경우에도 A ∨ B를 얻을 수 있습니다. 여기의 “또는”은 둘 다 참인 경우를 포함합니다.

선언 제거 ∨E는 A ∨ B를 확보하고, A를 가정한 부분 증명에서 C를 얻고, B를 가정한 부분 증명에서도 같은 C를 얻을 때 사용합니다. 두 임시 가정을 각각 해제한 뒤 C를 얻습니다. 각 부분 증명에 있던 다른 미해제 가정은 모두 남습니다.

선언문을 얻는 데 필요한 가정들과 두 부분 증명의 나머지 가정들을 모두 만족하는 모형을 잡습니다. 그 모형에서 A ∨ B는 참이므로 A와 B 중 적어도 하나가 참입니다. A가 참이면 첫 부분 증명의 보장으로 C가 참입니다. B가 참이면 둘째 부분 증명의 보장으로 C가 참입니다. 둘 다 참이어도 C를 얻습니다.

이 설명에는 각 부분 증명의 보장이 필요합니다. “A와 B가 동시에 참”이라고 새로 가정한 뒤 C를 얻는 한 갈래로는 선언 제거를 대신할 수 없습니다.

바로 그 점을 정확히 읽어야 합니다. 모순 도출 ¬E는 A와 ¬A를 확보하면 ⊥를 얻습니다. 고전 이값 해석에서 A와 그 부정이 동시에 참인 모형은 없습니다. 따라서 “두 입력이 모두 참인데 결론이 거짓인 모형”도 없습니다.

가정 Γ에서 A를, Δ에서 ¬A를 얻는 부분 증명들이 안전하다고 합시다. Γ와 Δ를 함께 만족하는 모형이 있다면 A와 ¬A가 함께 참이어야 해서 불가능합니다. 그러므로 Γ ∪ Δ를 만족하는 모형은 없고, 거기에서 ⊥가 의미론적으로 따라옵니다.

부정 도입 ¬I입니다. Γ와 임시 가정 A에서 ⊥를 얻은 부분 증명이 있다고 합시다. Γ를 만족하는 모형에서 A까지 참이라면, 부분 증명의 보장 때문에 ⊥가 참이어야 합니다. 그런 모형은 없으므로 Γ를 만족하는 모든 모형에서 A는 거짓입니다. 따라서 ¬A가 참입니다. A라는 임시 가정을 해제하고 Γ만 남길 수 있습니다.

또 모순 제거 ⊥E는 ⊥에서 임의의 문장 B를 얻도록 합니다. ⊥를 도출하는 부분 증명이 안전하다면 그 미해제 가정들을 함께 만족하는 모형이 없습니다. 그러므로 그 가정들이 모두 참이면서 B가 거짓인 모형 역시 없습니다.

이중부정 제거 ¬¬E를 사용하려면 ¬¬A를 확보하고 A를 결론으로 얻습니다. 고전 이값 의미론에서 부정은 참과 거짓을 뒤집습니다. ¬¬A가 참이면 ¬A는 거짓이고, 따라서 A는 참입니다.

이 설명은 지금 정한 고전 이값 의미론을 사용합니다. 모든 논리 체계가 같은 규칙을 기본으로 채택한다고 말하지는 않습니다. 다른 논리의 증명 가능성과 의미를 비교할 때에는 어떤 의미론과 규칙을 사용하는지부터 밝혀야 합니다.

네. Γ와 임시 가정 ¬A에서 ⊥를 얻으면, 부정 도입으로 Γ에서 ¬¬A를 얻습니다. 여기에 이중부정 제거를 적용하면 A를 얻습니다. 교재에 따라 이 두 단계를 하나의 간접 증명 규칙으로 제시하기도 합니다.

참거짓으로 직접 설명해도 됩니다. Γ를 만족하는 모형에서 A가 거짓이라면 ¬A는 참이므로 부분 증명에 따라 모순이 참이어야 합니다. 이는 불가능합니다. 그러므로 그 모형에서 A는 참입니다.

네. 증명의 길이에는 정해진 상한이 없습니다. 그래서 증명 열 개를 열거하는 대신 증명의 구조에 대한 귀납을 사용합니다. 2편에서 항과 식을 만드는 방법을 따라 성질을 보였던 것과 비슷합니다. 여기서는 증명이 만들어지는 방법을 따라갑니다.

보이고 싶은 성질은 “이 도출의 모든 미해제 가정을 참으로 만드는 모형은 마지막 문장도 참으로 만든다”입니다. 시작은 가정 A 하나만 있는 도출입니다. 그 가정을 만족하는 모형에서 A는 참이므로 성질이 성립합니다.

맞아요. 도출이 어떤 규칙 적용으로 끝난다고 합시다. 그 규칙에 입력을 제공하는 부분 도출들은 전체 도출보다 작습니다. 그 작은 도출들에서 위의 성질이 성립한다고 가정합니다. 이 가정을 귀납 가정이라고 부릅니다.

그러고 나서 마지막 규칙이 무엇인지에 따라, 우리가 앞에서 검토한 의미론적 이유를 적용합니다. 연언 도입이면 두 쪽 가정을 함께 만족하는 모형에서 두 입력이 참입니다. 조건문 도입이면 부분 도출이 Γ와 A 아래에서 B를 보장한다는 사실을 사용하고 A의 참거짓을 나눕니다. 선언 제거이면 각 갈래의 보장을 사용합니다. 같은 방식으로 이번 편의 규칙들을 모두 확인했습니다.

귀납 가정은 전체 결론을 미리 믿는 순환 논증과 다릅니다. 가정 하나의 도출에서 먼저 성질을 보였고, 이미 더 작은 도출들에 성립한다면 그다음 규칙으로 만든 도출에도 성립함을 보였습니다. 모든 증명은 유한하게 많은 규칙 적용으로 만들어지므로, 이 시작 단계와 보존 단계가 모든 증명에 닿습니다.

그 결과 이번 편에서 명시한 연결사 규칙들로 만든 모든 도출은 미해제 가정에서 참인 결론으로 이어집니다. 아직 살피지 않은 양화 규칙과 동일성 규칙의 경우까지 확인해야 일차논리 전체 증명 체계의 건전성 증명이 완성됩니다.

오늘 확인한 규칙들로 이루어진 적법한 도출이라면 그렇습니다. 미해제 가정들이 Γ에 들어 있고 마지막 문장이 A이면, Γ를 만족하는 모든 모형에서 A도 참입니다. 이것이 건전성의 방향 ⊢에서 ⊨로입니다.

특히 남은 가정이 하나도 없는 증명이라면 모든 모형에서 결론이 참입니다. 그래서 ⊢ A에서 ⊨ A를 얻습니다. 증명 체계의 건전성은 전제가 실제로 참이라는 현장 조사까지 제공하지는 않습니다.

전제를 모두 참으로 만들고 결론을 거짓으로 만드는 반모형이 있다면, 건전한 규칙들만으로 그 결론을 그 전제들에서 도출하는 일은 불가능합니다. 그런 도출이 있다면 건전성에 따라 반모형에서도 결론이 참이어야 하므로 서로 맞지 않습니다.

반면 몇 시간 동안 증명을 못 찾았다는 사실은 도출이 없다는 증명이 아닙니다. 반모형을 찾지 못한 것만으로 타당성이 확인되는 것도 아닙니다. 무엇을 실제로 확보했는지 구별해야 합니다.

그렇게 진행해 보세요. 앞서 연언 제거, 조건문 제거, 부정 도입을 각각 확인했습니다. 이 세 규칙을 잇는 동안 어떤 가정을 유지하고 어떤 가정을 해제하는지 봅시다.

정확합니다. 증명에서는 허용된 규칙을 한 줄씩 적용했고, 의미론적 설명에서는 전제가 참인 임의의 모형을 살폈습니다. 건전성이 두 관점을 연결합니다.

이 전제들 자체가 만족 가능한지도 확인할 수 있습니다. 영역을 {아라}, a를 아라로 두고 P, Q, S를 모두 공집합으로 두면 p, q, r이 모두 거짓입니다. 두 조건문은 참이고 ¬r과 ¬p도 참입니다. 이번 결론은 전제들에 모형이 전혀 없어서만 성립하는 사례가 아닙니다.

문장의 뜻과 미해제 가정을 살피면 이유를 말할 수 있습니다. 도입·제거 규칙에서는 연결사의 참거짓 조건을 사용합니다. 임시 가정을 닫는 규칙에서는 부분 증명의 가정과 결론 사이의 보장을 이어받습니다. 증명 전체에 대해서는 가정 단계부터 각 규칙 적용까지 성질이 유지되는지 귀납합니다.

이제 양화사에도 같은 질문을 할 준비가 되었습니다. ∀x P(x)에서 P(a)로 가는 단계는 모든 대상이라는 뜻과 a가 가리키는 대상의 관계를 사용합니다. 열린 식에 항을 대입할 때는 4편의 대입 보조정리가 필요합니다. 전칭 도입과 존재 제거에서는 새 이름 조건이 왜 필요한지도 모형을 바꾸어 설명하게 됩니다.

∃x P(x)에서 P(a)를 바로 얻는 규칙 후보를 떠올려 보세요. 영역 {아라, 보라}, a=아라, P={보라}, Q=S=∅로 두면 존재문은 참이고 P(a)는 거짓입니다. 존재문의 증거가 특정 이름 a의 대상이라는 보장은 없습니다.

이처럼 새 규칙도 전제·결론·모형을 분명히 놓고 검토합니다. 다음 편은 양화 규칙의 올바른 조건과 동일성 규칙을 포함해, 일차논리 증명 전체의 건전성으로 이어갑니다.