2.1 수리논리 — 프로그램을 명세하고 추론하는 언어

자연어 요구사항("동시에 켜지면 안 된다", "모든 사용자는 승인받아야 한다")은 사람에게는 명확해 보여도 기계가 검사할 수는 없다. 수리논리는 그 요구사항을 진리 배정으로 판정 가능한 식으로 옮기는 언어이며, 이 문서는 그 언어의 구문·의미·증명 체계를 세운 뒤 SQL의 3값 논리와 배포 설정의 모순 진단으로 이어 간다.

학습 목표

• 논리식의 구문과 의미를 구분하고, 진리 배정으로 만족 가능성·타당성·논리적 함의를 서로 다른 질문으로 판정한다.
• 증명 체계의 건전성과 완전성이 정적 분석 도구의 신뢰성과 어떤 관계인지 설명한다.
• CNF 변환의 크기 문제와 Tseitin 변환이 등가(equivalence) 대신 등만족(equisatisfiability)을 선택하는 이유를 설명한다.
• 술어 논리에서 양화사의 순서를 바꿔 명세의 의미가 달라지는 사례를 식별한다.
• SQL의 3값 논리가 고전 논리와 갈라지는 지점을 조건식 사례로 분석하고, 배포 제약을 논리식으로 모델링해 모순의 원인을 진단한다.

배경: 왜 이것이 존재하는가

"신규 인증이 켜지면 레거시 인증은 꺼져야 한다"는 문장은 사람이 읽으면 명확하다. 그런데 이 문장을 코드 리뷰어, 설정 검증기, 정적 분석기에게 검사시키려면 "문장"이 아니라 계산할 수 있는 대상이 필요하다. 19세기 중반 불(Boole)이 논리적 추론을 대수 연산으로 옮긴 이래, 논리학은 자연어의 뉘앙스를 포기하는 대신 구문(syntax)이 정확히 정의되고, 그 구문에 의미(semantics)를 부여하는 방법이 고정되어 있어, 참·거짓을 기계적으로 판정할 수 있는 언어로 발전했다.

이 대가로 잃는 것도 있다. 자연어의 함축, 문맥, 예외는 형식 언어로 옮기는 순간 사라지거나 명시적으로 다시 넣어야 한다. 대신 얻는 것은 판정 가능성이다 — 타입 체커가 프로그램을 검사하고, SAT/SMT 솔버가 제약을 풀고, 질의 최적화기가 조건을 재작성하고, 모델 체커가 프로토콜을 검증하는 모든 도구는 결국 이 형식 언어 위에서 진리값을 계산한다. 이 문서는 그 계산의 공통 어휘 — 만족 가능성, 타당성, 함의, 건전성, 완전성 — 를 세운다.

핵심 개념

구문과 의미의 분리

구문은 기호를 조합하는 규칙이다. 명제 논리의 논리식은 원자 명제(atom) p, q, r, ...와 연결사 ¬(부정), ∧(논리곱), ∨(논리합), →(함의), ↔(동치)로 재귀적으로 구성된다. p → (q ∧ ¬r)는 이 규칙을 따르는 하나의 문자열 구조일 뿐, 이 자체로는 참도 거짓도 아니다.

의미는 그 구조에 진리값을 매기는 절차다. 진리 배정(truth assignment) ν는 각 원자 명제를 {참, 거짓} 중 하나로 매핑하는 함수이고, 연결사의 진리표를 따라 임의의 논리식으로 확장된다. ν가 φ를 만족한다(ν ⊨ φ)는 그 배정 아래에서 φ가 참이 된다는 뜻이고, 이런 ν를 φ의 모델(model)이라 부른다.

이 분리가 왜 중요한가. 같은 구문이 다른 배정 아래에서 다른 의미를 가질 수 있다는 사실이 이후 모든 논의의 출발점이다. p ∧ ¬p는 어떤 배정에서도 거짓이 되도록 구문이 강제하지만, p → q는 배정에 따라 참일 수도 거짓일 수도 있다. 이 구분은 2.2에서 "생성기(문법)가 만드는 것"과 "그 생성기가 정의하는 언어"의 구분으로, "정규식 표기"와 "정규식이 표현하는 정규 언어"의 구분으로 그대로 재사용된다.

만족 가능성, 타당성, 함의 — 세 가지 다른 질문

같은 논리식을 두고 실무에서 실제로 묻는 질문은 셋으로 나뉜다.

• 만족 가능성(satisfiability, SAT): φ를 참으로 만드는 배정이 적어도 하나 존재하는가? "이 설정 조합은 실행 가능한가?"에 대응한다.
• 타당성(validity): φ가 모든 배정에서 참인가(항진명제, tautology)? "이 조건은 항상 성립하는가?"에 대응한다.
• 논리적 함의(entailment, Γ ⊨ φ): 전제 집합 Γ의 모든 모델이 φ의 모델이기도 한가? "이 전제들이 참이라면, 이 결론도 항상 참인가?"에 대응한다.

세 질문은 서로 환원된다. φ가 타당하다는 것은 ¬φ가 만족 불가능(unsatisfiable)하다는 것과 같다 — φ를 거짓으로 만드는 배정이 하나도 없다는 뜻이기 때문이다. Γ ⊨ φ도 마찬가지로 Γ ∪ {¬φ}가 만족 불가능한지로 바꿔 물을 수 있다 — "전제가 참인데 결론이 거짓인 경우가 하나도 없다"는 말이기 때문이다. 이 환원이 실무적으로 중요한 이유는, SAT 솔버 하나로 타당성 검사와 함의 검사를 모두 처리할 수 있다는 뜻이기 때문이다. "이 시스템이 이 안전 조건을 항상 만족하는가"를 증명하는 실무 도구(모델 체커 포함)는 대개 "반례가 존재한다고 가정하면 모순이 나온다"는 형태로, 즉 부정을 SAT 솔버에 넣어 unsatisfiable을 확인하는 형태로 동작한다.

증명 체계 — 건전성과 완전성

진리 배정을 전부 따져 SAT·타당성을 판정하는 것(진리표 방법)은 원리적으로 항상 가능하지만 변수 수만큼 배정이 늘어난다(이 문서의 미니 실험과 2.4에서 다시 다룬다). 증명 체계(proof system)는 진리표 전체를 만들지 않고, 공리와 추론 규칙(예: p와 p → q에서 q를 유도하는 전건 긍정, modus ponens)만으로 결론에 도달하는 절차다. Γ로부터 φ를 유도할 수 있다는 것을 Γ ⊢ φ로 쓴다.

⊢(구문적 유도)와 ⊨(의미적 함의)는 다른 것이고, 둘의 관계를 규정하는 것이 증명 체계의 핵심 성질이다.

• 건전성(soundness): Γ ⊢ φ이면 Γ ⊨ φ이다. 증명 체계가 거짓을 증명하지 않는다는 보장이다.
• 완전성(completeness): Γ ⊨ φ이면 Γ ⊢ φ이다. 증명 체계가 참인 것을 놓치지 않는다는 보장이다.

명제 논리는 건전하고 완전한 증명 체계를 가진다는 것이 알려져 있다 — 유한한 진리표로 판정 가능한 범위에서는 증명 절차가 진리표와 정확히 일치하는 답을 낼 수 있다. 이 두 성질을 실무 도구의 언어로 옮기면 이렇게 읽힌다: 건전한 도구가 "문제없음"이라고 하면 실제로 문제가 없고, 완전한 도구가 조용하면 실제로 놓친 문제가 없다. 타입 체커, 린터, 정적 분석기는 모두 근사적인 증명 체계이고, 어떤 도구가 둘 중 무엇을 지향하는지가 그 도구의 경고를 얼마나 믿어야 하는지를 결정한다 — 이 판단 기준을 챕터 5의 정적 분석이 이미 도구 정책의 언어로 사용하고 있고, 2.3은 왜 비자명한 프로그램 성질에서는 건전성·완전성·항상 종료를 동시에 가질 수 없는지를 원리적으로 보인다.

정규형 — CNF와 크기 문제

CNF(conjunctive normal form, 논리곱 표준형)는 리터럴(원자 명제 또는 그 부정)의 논리합(clause, 절)들을 논리곱으로 묶은 형태다. 예: (p ∨ ¬q) ∧ (¬p ∨ r). SAT 솔버, 정적 분석기의 제약 인코딩, 하드웨어 검증 도구는 대부분 입력으로 CNF를 요구한다 — 절 단위로 "지금 이 절이 위반됐는가"를 독립적으로 확인할 수 있어 탐색 알고리즘(2.4의 DPLL/CDCL)을 구현하기 쉽기 때문이다.

문제는 임의의 논리식을 CNF로 바꾸는 직접적인 방법(드모르간 법칙으로 부정을 안으로 밀어넣고, 분배 법칙으로 ∨를 ∧ 밖으로 밀어내는 것)이 식의 크기를 지수적으로 불릴 수 있다는 점이다. (a₁ ∧ b₁) ∨ (a₂ ∧ b₂) ∨ ... ∨ (aₙ ∧ bₙ) 같은 식을 분배 법칙으로 펼치면 각 항에서 하나씩 고르는 모든 조합, 즉 2ⁿ개의 절이 나온다. 원래 식은 n에 선형으로 컸는데 CNF는 지수적으로 커진 것이다.

Tseitin 변환은 이 문제를 다른 방식으로 우회한다. 식을 통째로 펼치는 대신, 부분식마다 새 변수를 하나씩 도입해 그 부분식과 새 변수가 같은 값을 갖도록 강제하는 절만 추가한다. 예를 들어 c가 a ∧ b를 나타내는 새 변수라면 다음 세 절로 c ↔ (a ∧ b)를 인코딩한다.

(¬c ∨ a) ∧ (¬c ∨ b) ∧ (¬a ∨ ¬b ∨ c)

이 절들은 원래 변수 a, b만 놓고 보면 c가 추가된 것이므로 원래 식과 논리적으로 동치(equivalent)는 아니다 — 모델의 집합이 정확히 같지 않다(원래 변수 위에서 같은 진리값을 내지만, 확장된 변수 집합에서는 c값이 고정된 특정 모델만 허용된다). 대신 두 식은 **등만족(equisatisfiable)**이다 — 원래 식이 만족 가능하면 새 식도 만족 가능하고, 그 역도 성립한다. 등가성을 등만족성으로 낮춘 대가로 크기가 부분식 개수에 선형으로만 커진다. 실무 SAT 인코더(모델 체커, 회로 검증기, 스케줄링 솔버의 프런트엔드)가 CNF를 만들 때 실제로 쓰는 방법이 이것이다.

술어 논리 — 양화사의 순서가 명세의 의미를 바꾼다

명제 논리는 "이 배포는 카나리아다" 같은 원자 명제를 쪼갤 수 없는 덩어리로 다룬다. 술어 논리(predicate logic)는 그 안으로 들어가 대상과 관계를 다룬다. Approve(a, u)("관리자 a가 사용자 u를 승인할 수 있다") 같은 술어에 전칭 양화사 ∀(모든)와 존재 양화사 ∃(존재)를 붙여 "모든 x에 대해...", "어떤 x가 존재해서..."를 표현한다.

양화사가 두 개 이상 겹치면 순서가 의미를 바꾼다. 다음 두 식을 비교하자.

∀u ∃a. Approve(a, u)   // 모든 사용자마다, 그를 승인할 수 있는 관리자가 (사용자별로 다를 수 있게) 존재한다
∃a ∀u. Approve(a, u)   // 어떤 한 관리자가 존재해서, 그 관리자가 모든 사용자를 승인할 수 있다

첫 문장은 사용자마다 다른 관리자가 있어도 만족된다. 둘째 문장은 단 한 명의 관리자가 모든 사용자를 커버해야 만족된다. 둘째가 참이면 첫째도 항상 참이지만(그 한 관리자를 모든 사용자의 승인자로 고르면 된다), 역은 성립하지 않는다 — 첫째가 참이라고 둘째가 참이라는 보장은 없다. 접근 제어 정책을 설계할 때 "모든 사용자는 승인자가 있어야 한다"는 요구사항을 팀 안에서 어떤 사람은 첫 번째 뜻으로, 어떤 사람은 두 번째 뜻으로 이해하고도 아무도 이상함을 못 느낄 수 있다 — 둘 다 자연어로는 "사용자는 승인받을 수 있어야 한다"로 뭉뚱그려지기 때문이다. 술어 논리는 이 차이를 기호 순서로 강제로 드러낸다.

SAT로 연결

"논리식을 만족하는 배정을 찾는다"는 SAT의 정의는 그 자체로 제약 충족 문제(constraint satisfaction problem)의 원형이다. 피처 플래그 조합, 배포 대상 선택, 의존 버전 해석, 스케줄 배정은 모두 "이 조건들을 동시에 만족하는 값 배정이 있는가"로 바꿔 쓸 수 있고, 그 순간 SAT(또는 그 확장인 SMT, ILP)의 인스턴스가 된다. 이 문서의 미니 실험이 하는 일이 정확히 이것이다 — 배포 제약을 명제식으로 쓰고 만족 모델을 찾는다. SAT를 실제로 빠르게 푸는 알고리즘(DPLL, CDCL)과 왜 이 문제가 일반적으로 다항 시간에 풀리지 않는다고 여겨지는지는 2.4에서 다룬다. 여기서 필요한 것은 입출력 모델이다: SAT 솔버는 논리식을 받아 만족 모델 또는 "불가능"을 돌려주는 함수라는 것.

실무 관점

타입과 명제. 타입을 명제로, 프로그램을 그 명제의 증명으로 보는 관점(Curry–Howard 대응)은 이 문서가 세운 "구문·의미·증명 체계"라는 어휘를 그대로 타입 시스템에 옮겨 쓴다. 타입 체커의 건전성이 무엇을 보장하고 무엇을 포기하는지는 챕터 4의 타입 안전성에서 심화한다.

SQL의 3값 논리. 관계형 DB는 값이 없음을 NULL로 표현하고, NULL이 섞인 비교는 참도 거짓도 아닌 세 번째 값 UNKNOWN이 된다. AND, OR, NOT의 진리표가 이 세 값으로 확장된다.

AND

	T	F	U
T	T	F	U
F	F	F	F
U	U	F	U

OR

	T	F	U
T	T	T	T
F	T	F	U
U	T	U	U

NOT T = F, NOT F = T, NOT U = U다. 그리고 SQL의 WHERE는 조건이 정확히 TRUE인 행만 남긴다 — FALSE와 UNKNOWN을 구분하지 않고 둘 다 걸러낸다. 이 규칙이 고전 논리의 직관을 깨는 지점을 보자.

-- age가 NULL인 행이 있다고 하자.
SELECT * FROM users WHERE NOT (age > 30 AND age <= 30);

고전 명제 논리라면 age > 30 AND age <= 30은 어떤 age 값에서도 거짓이므로 그 부정은 항상 참인 항진명제이고, 모든 행이 반환되어야 한다. 하지만 age가 NULL인 행에서는 age > 30도 age <= 30도 UNKNOWN이고, UNKNOWN AND UNKNOWN = UNKNOWN이며, NOT UNKNOWN = UNKNOWN이다. WHERE는 UNKNOWN을 참으로 인정하지 않으므로 그 행은 조용히 제외된다. 고전 논리에서는 항진명제였던 식이 3값 논리에서는 항진명제가 아니게 된 것이다. NOT IN (SELECT ...)의 서브쿼리가 NULL을 하나라도 반환하면 바깥 NOT IN 전체가 결코 TRUE가 되지 않아 전체 결과가 통째로 비어 버리는 유명한 함정도 같은 구조다 — x <> NULL이 UNKNOWN이고, AND로 묶인 나머지 비교가 전부 TRUE여도 UNKNOWN 하나가 전체를 UNKNOWN으로 끌어내린다. 이 문제를 2값 논리처럼 다루면(모든 WHERE 조건이 참 아니면 거짓이라고 가정하면) 코드 리뷰에서 이런 쿼리가 옳아 보이고, 프로덕션에서만 틀린 결과를 낸다.

배포 제약의 모델링. feature flag, 배포 대상, 의존 버전의 제약을 명제식으로 옮기면 "이 조합이 가능한가"를 사람이 손으로 추적하는 대신 계산으로 확인할 수 있다. 다음 미니 실험이 이 모델링과 모순 진단을 실제로 수행한다.

암호 프로토콜의 형식 검증. 이 문서가 세운 만족 가능성·타당성·모델 검사의 어휘는 암호 프로토콜(키 교환, 인증 절차)이 의도한 안전성 속성을 실제로 만족하는지 자동으로 검증하는 도구(모델 체커)의 기반이기도 하다. 다만 이 어휘를 세우는 것과 검증 도구를 실제로 운용하는 것은 다른 일이다. 챕터 3의 대칭 암호와 무결성이 프리미티브의 증명 범위와 프로토콜 조립의 간극을 다루지만, 모델 체커를 사용한 프로토콜 검증 자체는 이 커리큘럼의 범위 밖이다.

더 깊이: Tseitin 변환이 절을 만드는 방식

앞서 c ↔ (a ∧ b)의 인코딩을 봤다. 이것이 어디서 나오는지 짚어 보자. c ↔ (a ∧ b)는 (c → (a ∧ b)) ∧ ((a ∧ b) → c)와 같다. 각 방향을 함의 제거(x → y ≡ ¬x ∨ y)와 드모르간으로 CNF로 바꾸면:

c → (a ∧ b)  ≡  ¬c ∨ (a ∧ b)  ≡  (¬c ∨ a) ∧ (¬c ∨ b)
(a ∧ b) → c  ≡  ¬(a ∧ b) ∨ c  ≡  ¬a ∨ ¬b ∨ c

두 결과를 합치면 앞서 본 세 절이 나온다. ∨가 하나의 ∧ 앞에 있을 때만 분배가 필요하므로 이 변환은 부분식 하나당 상수 개수의 절만 만든다. 복잡한 식 전체를 이렇게 부분식별로 새 변수를 도입해 아래에서 위로 조립하면, 전체 CNF 크기가 원래 식의 크기에 선형으로 비례한다 — 위에서 본 지수적 분배 폭발을 피하는 이유다. 실제 SAT 인코더가 사용자가 쓴 임의의 논리식을 받아 몇 초 안에 CNF로 바꿀 수 있는 것은 이 변환 덕분이다.

미니 실험: 배포 제약을 명제식으로 모델링하고 모순을 진단한다

다음 시나리오를 명제 변수 5개로 모델링한다: canary, useNewAuth, useLegacyAuth, regionEU, gdprMode. 규칙 4개와 "이번 배포가 실제로 요청한 값" 2개를 제약으로 추가하고, 2⁵ = 32개의 모든 진리 배정을 전수 열거해 만족 모델이 있는지 확인한다. Node.js 24는 타입 주석을 제거하는 방식으로 .ts 파일을 플래그 없이 직접 실행한다(enum처럼 런타임 표현이 필요한 문법은 지원하지 않지만, 이 스크립트는 그런 문법을 쓰지 않는다).

// deploy-constraints.ts — node deploy-constraints.ts 로 실행
// 배포 설정을 명제 변수로 모델링하고, 모든 진리 배정을 전수 열거해
// 만족 모델이 있는지, 없다면 어떤 제약들이 충돌하는지 확인한다.

type VarName = "canary" | "useNewAuth" | "useLegacyAuth" | "regionEU" | "gdprMode";

// 진리 배정: 5개 변수 각각에 true/false를 매긴 것 하나가 "가능한 세계" 하나다.
type Assignment = Record<VarName, boolean>;

const VARS: VarName[] = ["canary", "useNewAuth", "useLegacyAuth", "regionEU", "gdprMode"];

interface Constraint {
  name: string;
  // 명제식 하나를 함수로 표현한다: 이 배정에서 참인가?
  holds: (a: Assignment) => boolean;
  formula: string; // 사람이 읽을 명제식 표기
}

const CONSTRAINTS: Constraint[] = [
  { name: "no-dual-auth", formula: "useNewAuth → ¬useLegacyAuth",
    holds: (a) => !a.useNewAuth || !a.useLegacyAuth },
  { name: "canary-needs-new-auth", formula: "canary → useNewAuth",
    holds: (a) => !a.canary || a.useNewAuth },
  { name: "eu-needs-gdpr-mode", formula: "regionEU → gdprMode",
    holds: (a) => !a.regionEU || a.gdprMode },
  { name: "gdpr-mode-excludes-legacy", formula: "gdprMode → ¬useLegacyAuth",
    holds: (a) => !a.gdprMode || !a.useLegacyAuth },
  // 아래 두 항목은 "규칙"이 아니라 이번 배포가 실제로 요청한 값이다.
  // 운영팀은 "카나리아 + EU 리전"을 원했고, 롤백 대비로 레거시 인증도 켜 두고 싶어했다.
  { name: "this-deploy-is-canary-in-eu", formula: "canary ∧ regionEU",
    holds: (a) => a.canary && a.regionEU },
  { name: "ops-wants-legacy-auth-too", formula: "useLegacyAuth",
    holds: (a) => a.useLegacyAuth },
];

function enumerateAssignments(vars: VarName[]): Assignment[] {
  const n = vars.length;
  const all: Assignment[] = [];
  // n개 불리언 변수의 모든 배정은 2^n개다. 비트마스크 하나가 배정 하나에 대응한다.
  for (let mask = 0; mask < 2 ** n; mask++) {
    const a = {} as Assignment;
    for (let i = 0; i < n; i++) a[vars[i]] = ((mask >> i) & 1) === 1;
    all.push(a);
  }
  return all;
}

function satisfiesAll(a: Assignment, constraints: Constraint[]): boolean {
  return constraints.every((c) => c.holds(a));
}
function describe(a: Assignment): string {
  return VARS.map((v) => `${v}=${a[v]}`).join(", ");
}

function run(constraints: Constraint[], label: string) {
  console.log(`\n=== ${label} (제약 ${constraints.length}개) ===`);
  const assignments = enumerateAssignments(VARS);
  console.log(`전수 열거한 배정 수: 2^${VARS.length} = ${assignments.length}`);
  const models = assignments.filter((a) => satisfiesAll(a, constraints));
  console.log(`만족 모델(satisfying model) 수: ${models.length}`);
  if (models.length > 0) console.log("모델 예시:", describe(models[0]));
  else console.log("만족 모델 없음 — 이 제약 집합은 unsatisfiable(모순)이다.");
}

run(CONSTRAINTS, "전체 제약");

// 진단: 제약을 하나씩 빼 보며 "이것만 없으면 만족 가능해지는가"를 확인한다.
// SAT 솔버의 unsat core 개념을 손으로 재현한 것이다 — 2.4에서 도구로 다룬다.
console.log("\n=== 진단: 어떤 제약을 빼면 만족 가능해지는가 ===");
for (const dropped of CONSTRAINTS) {
  const rest = CONSTRAINTS.filter((c) => c.name !== dropped.name);
  const models = enumerateAssignments(VARS).filter((a) => satisfiesAll(a, rest));
  console.log(
    `"${dropped.name}"(${dropped.formula})를 빼면: ` +
      (models.length > 0 ? `만족 가능 (예: ${describe(models[0])})` : "여전히 unsatisfiable"),
  );
}

Node.js v24.14.0, Apple M5 Pro, macOS 26.6.2에서 실행한 결과다.

=== 전체 제약 (제약 6개) ===
전수 열거한 배정 수: 2^5 = 32
만족 모델(satisfying model) 수: 0
만족 모델 없음 — 이 제약 집합은 unsatisfiable(모순)이다.

=== 진단: 어떤 제약을 빼면 만족 가능해지는가 ===
"no-dual-auth"(useNewAuth → ¬useLegacyAuth)를 빼면: 여전히 unsatisfiable
"canary-needs-new-auth"(canary → useNewAuth)를 빼면: 여전히 unsatisfiable
"eu-needs-gdpr-mode"(regionEU → gdprMode)를 빼면: 여전히 unsatisfiable
"gdpr-mode-excludes-legacy"(gdprMode → ¬useLegacyAuth)를 빼면: 여전히 unsatisfiable
"this-deploy-is-canary-in-eu"(canary ∧ regionEU)를 빼면: 만족 가능 (예: canary=false, ...)
"ops-wants-legacy-auth-too"(useLegacyAuth)를 빼면: 만족 가능 (예: canary=true, useNewAuth=true, ...)

흥미로운 관찰은 규칙 4개(no-dual-auth, canary-needs-new-auth, eu-needs-gdpr-mode, gdpr-mode-excludes-legacy) 중 어느 하나를 빼도 여전히 unsatisfiable이라는 점이다. 원인을 손으로 추적하면, 모순에 이르는 경로가 두 개 독립적으로 존재한다: canary → useNewAuth와 no-dual-auth를 이으면 "카나리아 배포는 레거시 인증을 켤 수 없다"는 결론이 나오고, eu-needs-gdpr-mode와 gdpr-mode-excludes-legacy를 이어도 "EU 리전 배포는 레거시 인증을 켤 수 없다"는 같은 결론이 나온다. 두 경로 중 하나만 끊어서는 다른 경로가 여전히 useLegacyAuth와 충돌한다. 실제로 만족 가능해지려면 두 경로 중 하나를 완전히 끊거나(규칙 두 개를 함께 제거), 애초에 이번 배포의 요청 자체(this-deploy-is-canary-in-eu 또는 ops-wants-legacy-auth-too)를 접어야 한다. unsat인 제약 집합에서 "원인이 되는 제약"이 유일하지 않을 수 있다는 것, 그리고 겉보기에 무관해 보이는 두 규칙(인증 규칙과 GDPR 규칙)이 같은 모순을 독립적으로 만들어 낼 수 있다는 것이 이 실험의 핵심 관찰이다.

변수가 5개라 2⁵ = 32가지 전수 열거가 즉시 끝났지만, 실제 배포 설정에는 변수가 수십~수백 개일 수 있다. 변수가 n개면 배정은 2ⁿ개이므로 전수 열거는 변수 30개만 되어도 10억 가지를 넘는다. 이 브루트포스가 감당 불가능해지는 지점과 그 대신 실제 SAT 솔버가 무엇을 하는지는 2.4에서 다룬다.

정리

• 논리식은 구문(구조)과 의미(그 구조에 진리값을 매기는 규칙)로 나뉘고, 같은 구문이 배정에 따라 다른 진리값을 가질 수 있다.
• 만족 가능성(모델이 존재하는가), 타당성(모든 배정에서 참인가), 함의(전제의 모델이 결론의 모델이기도 한가)는 서로 다른 질문이며, 부정을 통해 서로 SAT 문제로 환원된다.
• 건전성은 증명 체계가 거짓을 증명하지 않는다는 보장이고, 완전성은 참인 것을 놓치지 않는다는 보장이다. 정적 분석 도구의 신뢰성을 이 두 축으로 읽을 수 있다.
• 임의의 논리식을 CNF로 직접 분배하면 크기가 지수적으로 커질 수 있다. Tseitin 변환은 등가성 대신 등만족성을 택해 부분식마다 새 변수를 도입하고, 크기를 선형으로 유지한다.
• 양화사의 순서(∀∃ 대 ∃∀)는 명세의 의미를 바꾼다. 자연어로는 같은 문장으로 뭉뚱그려지는 두 요구사항이 술어 논리에서는 서로 다른 것으로 드러난다.
• SQL의 3값 논리에서 WHERE는 TRUE인 행만 남기고 UNKNOWN도 걸러낸다. 고전 논리의 항진명제가 3값 논리에서는 항진명제가 아닐 수 있다.
• 논리식이 만족 가능하다는 것은 명시된 제약끼리 모순이 없다는 뜻일 뿐, 현실의 숨은 전제까지 검증했다는 뜻은 아니다. unsat의 원인이 되는 제약도 유일하지 않을 수 있다.

확인 문제

1. 동료가 "WHERE NOT (status = 'active' AND status != 'active')는 논리적으로 항상 참이므로 모든 행을 반환해야 한다"고 주장했는데, 실제로는 status가 NULL인 행 몇 개가 결과에서 빠졌다. 원인을 설명하라.

정답과 해설

status가 NULL인 행에서는 status = 'active'와 status != 'active'가 모두 UNKNOWN이다. UNKNOWN AND UNKNOWN = UNKNOWN이고 NOT UNKNOWN = UNKNOWN이므로 전체 조건이 UNKNOWN이 된다. SQL의 WHERE는 TRUE인 행만 남기고 UNKNOWN은 FALSE와 마찬가지로 걸러내므로, 고전 명제 논리에서는 항진명제였던 이 식이 NULL이 섞인 3값 논리에서는 항진명제가 아니게 되고 그 행들이 조용히 제외된다. status IS NULL OR (조건)처럼 NULL 케이스를 명시적으로 포함해야 의도한 결과가 나온다.

2. 어느 팀이 "권한 요구사항: 모든 리포지토리는 승인해 줄 관리자가 있어야 한다"를 ∀r ∃a. CanApprove(a, r)로 구현했다. 이후 감사팀이 "모든 리포지토리를 승인할 수 있는 사람이 최소 한 명은 있어야 한다(백업 관리자 정책)"는 요구사항을 추가했는데, 기존 구현이 이 요구사항을 자동으로 만족한다고 착각해 별도 검증 없이 넘어갔다. 무엇이 잘못됐는가?

정답과 해설

기존 구현 ∀r ∃a. CanApprove(a, r)은 "리포지토리마다 승인자가 존재한다"는 뜻으로, 리포지토리별로 승인자가 달라도 만족된다. 감사팀의 요구사항은 ∃a ∀r. CanApprove(a, r) — "모든 리포지토리를 승인할 수 있는 한 사람"이다. ∃a∀r가 참이면 ∀r∃a는 항상 참이지만 역은 성립하지 않으므로, 기존 구현이 만족된다고 해서 백업 관리자 정책이 만족된다는 보장은 전혀 없다. 두 요구사항은 양화사 순서만 다를 뿐 자연어로는 둘 다 "승인자가 있어야 한다"로 뭉뚱그려지기 쉬우므로, 요구사항을 술어 논리로 옮겨 양화사 순서를 명시하고 별도로 검증해야 한다.

3. 이 문서의 미니 실험에서 no-dual-auth 규칙 하나만 제거해도 배포 설정은 여전히 unsatisfiable로 남았다. "충돌하는 제약을 하나 찾아 제거했으니 이제 문제가 해결됐다"는 성급한 결론이 왜 위험한지, 실험 결과를 근거로 설명하라.

정답과 해설

unsat의 원인이 유일한 제약 하나가 아니라 서로 다른 두 개의 독립된 추론 경로(인증 규칙 경로와 GDPR 규칙 경로)일 수 있기 때문이다. 실험에서 no-dual-auth를 제거해도 eu-needs-gdpr-mode와 gdpr-mode-excludes-legacy가 결합해 같은 결론(레거시 인증 불가)을 독립적으로 다시 만들어 내므로 여전히 unsatisfiable이다. 제약 하나를 제거한 뒤 재확인 없이 "고쳤다"고 결론 내리면, 겉보기에 무관한 다른 규칙 조합이 같은 모순을 계속 재생산하고 있다는 사실을 놓친다. 실제로 불일치를 해소하려면 각 독립 경로를 모두 확인하거나, 그 경로들이 공통으로 의존하는 상위 요청(this-deploy-is-canary-in-eu 또는 ops-wants-legacy-auth-too) 자체를 재검토해야 한다.

참고 자료

• Martin Davis, Hilary Putnam, "A Computing Procedure for Quantification Theory" (1960) — 진리표 전체를 만들지 않고 만족 가능성을 판정하는 절차의 원 논문. 2.4의 DPLL 계열 solver 논의의 출발점이다.
• Martin Davis, George Logemann, Donald Loveland, "A Machine Program for Theorem-Proving" (1962) — Davis–Putnam 절차를 실용적인 결정 절차(DPLL)로 다듬은 원 논문.
• Michael Huth, Mark Ryan, Logic in Computer Science 2nd ed. (Cambridge University Press, 2004) — 명제·술어 논리의 구문·의미·증명 체계를 컴퓨터 과학 응용과 함께 다루는 표준 교재.
• ISO/IEC 9075 (SQL 표준), Part 2 Foundation — NULL과 3값 논리 비교 연산의 공식 정의를 확인할 수 있는 표준 문서. 실제 검증 시에는 사용 중인 DBMS의 공식 문서와 함께 대조한다.
• PostgreSQL 공식 문서, Comparison Functions and Operators — NULL 비교와 3값 논리를 다루는 실제 구현체의 설명. NOT IN과 NULL의 상호작용을 실무 관점에서 확인할 수 있다.