1차 논리: 대상, 관계, 그리고 한정사

📍 우리는 지금 여기 있습니다: 1부 · 논리를 처음부터 — 4장. 명제논리는 우리에게 참, 거짓, 그리고 연결사를 주었지만, 단 하나의 대상을 이름 붙이거나 "모든"이라고 말할 방법은 주지 못했습니다. 1차 논리는 바로 그 원자를 깨뜨려 엽니다.

명제논리는 "새롭고(novel) 정확하다(correct)"로부터 "채택된다(accepted)"가 따라 나오는지를 저울질할 수 있었습니다. 하지만 명제논리가 결코 할 수 없었던 것은 alice라는 이름을 붙이거나, 모든 교수에 대해 한 번에 참인 무언가를 말하는 일이었습니다. 각 명제는 내부가 없는 단단한 진리의 조약돌이었습니다 — ∧(그리고), ∨(또는), ¬(아님), →(함의)로 조약돌을 쌓아 올릴 수는 있었지만, 그 안을 들여다볼 수는 없었습니다. 이 장은 그 조약돌을 깨뜨려, 하나의 사실을 실제로 이루는 두 가지 요소 — 그것이 말하는 대상(object)들과, 그 대상들 사이에서 주장되는 관계(relation) — 를 드러냅니다. 우리는 이 장치를 설명하는 데서 그치지 않을 것입니다. 어떤 문장이 어떤 세계에서 참이라는 것이 정확히 무엇을 의미하는지 그 재귀적 정의를 명시적으로 적고, 그 정의의 모든 줄을 실제로 그것을 실행하는 코드의 해당 줄과 대응시킨 다음, 세 개의 실제 문장과 하나의 실제 질의를 손으로 직접 계산해 볼 것입니다 — 기계가 하는 것과 똑같이 유한한 학계 세계를 개체 하나하나씩 훑어가면서 말입니다.

쉽게 말하면

오직 통째로 참이거나 거짓인 완결된 문장만으로 말할 수 있다고 상상해 보십시오 — "비가 온다", "세미나는 정오에 있다" — 그리고 "방 안의 모든 사람이 피곤하다"를 말하려면 그 방에 있는 사람 한 명 한 명에 대해 참/거짓 문장을 따로 써야만 한다고 말입니다. 1차 논리는 한꺼번에 세 가지 새로운 힘을 건네줍니다. 개별 사물에 대한 이름(alice, 논문 p1), 그것들 사이에서 성립할 수 있는 관계(alice가 bob을 지도한다), 그리고 한 문장이 사람들 전체 무리에 대해 말할 수 있게 해 주는 두 개의 작은 한정어 "모든"과 "어떤"입니다. 그리고 그런 문장이 참인지 확인하는 일은 컴퓨터가 묵묵히 해낼 수 있는 잡일이 됩니다. "모든 교수는 연구자이다"를 검사하려면, 그냥 개체 목록을 따라 내려가며 하나씩 확인하면 됩니다.

이 장에서 다루는 내용

• 명제논리가 부딪히는 한계 — 참/거짓 원자로 이루어진 논리가 왜 "모든"이나 "어떤"을 표현할 수 없는지, 왜 대상이라는 개념 자체가 전혀 없는지, 그리고 우리의 작은 세계에 있는 근거 사실(ground fact)들의 이름만 붙이는 데도 왜 천 개가 넘는 별도의 원자가 필요한지.
• 1차 논리를 이루는 조각들 — 항(term, 상수와 변수), 술어(predicate)와 그 항수(arity), 익숙한 연결사들, 그리고 두 개의 한정사 ∀("모든 것에 대해")와 ∃("존재한다") — 각 기호는 사용되기 전에 먼저 풀어서 설명합니다.
• 구조와 충족, 정확하게 정의하기 — 개체들의 정의역(domain)과 각 술어의 외연(extension), 그리고 충족 관계 ⊨("…에서 성립한다")의 완전한 재귀적 정의를 holds()가 모든 개체를 하나씩 시도해 한정된 문장을 판정하는 방식과 한 줄 한 줄 대응시킵니다.
• 손으로 훑어보는 세 문장 — 참인 전칭 문장 하나, 거짓인 전칭 문장 하나, 참인 존재 문장 하나를 진행 중인 예제의 모든 개체에 대해 하나씩 추적하고, ∀와 ∃를 한 아이디어의 두 얼굴로 만들어 주는 한정사 쌍대성(duality)도 함께 다룹니다.
• 결합 질의(conjunctive query) — 존재-논리곱(∃∧) 단편(fragment), "alice가 누구를 그랜드-지도하는가?"를 열세 명의 후보 전원에 대해 추적하는 과정, 그리고 이것이 왜 정확히 4권이 답하는 법을 배우는 과제인지.
• 아직 풀리지 않은 부분 — 하나의 유한한 세계에서의 모델 검사(model checking)는 결정 가능하지만, 모든 세계에 걸친 1차 논리의 타당성(validity)은 그렇지 않습니다. 이것이 2권이 온순하고 결정 가능한 단편으로 물러나는 이유입니다.

명제논리가 부딪히는 한계

이전 장인 명제논리는 각 진술을 accepted, novel처럼 더는 쪼갤 수 없는 진리 담지 원자로 취급했고, 유한하게 많은 참/거짓 배정을 모두 나열함으로써 모든 것(충족가능성, 타당성, 함의)을 결정했습니다. 이는 강력하지만 눈이 멀어 있습니다. "alice가 bob을 지도한다"는 하나의 불투명한 원자일 뿐이며, "bob이 carol을 지도한다"와는 논리적으로 아무 관련이 없습니다. 지도 관계의 연쇄(chain)를 말할 수 없습니다. "모든 교수는 연구자이다"라는 말도, alice에 대한 함의 하나, bob에 대한 함의 하나, 그렇게 이름 붙인 교수마다 함의를 하나씩 손으로 써 주지 않고서는 말할 수 없습니다. 그리고 "어떤 학생은 지도받는다"는 아예 말할 수조차 없습니다. "어떤"에는 변수(variable) — 세계 속 사물들 위를 훑는 자리 — 가 필요한데, 명제논리에는 사물도 변수도 없기 때문입니다 [1]. 명제논리는 사실에 대해 말하지만, 그 사실이 무엇에 관한 것인지 그 대상에 대해서는 말할 수 없습니다 [2].

이 한계를 정량적으로 따져 볼 만한 가치가 있습니다. 왜냐하면 바로 그 폭발적 증가야말로 한정사가 존재하는 이유 전부이기 때문입니다. 우리의 학계 세계는 완전히 도출되고 나면 13개의 개체와 12개의 술어를 가집니다. 그중 4개는 인자를 하나 받고(person, professor, researcher, student), 8개는 인자를 둘 받습니다(about, advises, affiliated, authored, cites, citesTransitively, colleague, grandAdvisor). 이 세계에 대해 순수하게 명제적으로 말하려면, 가능한 근거 사실마다 별개의 원자가 하나씩 필요할 것입니다. 그 수를 세어 보면 다음과 같습니다.

$$\underbrace{4 \times 13}_{\text{unary}} \;+\; \underbrace{8 \times 13 \times 13}_{\text{binary}} \;=\; 52 \;+\; 1352 \;=\; 1404 .$$

13개짜리 개체 세계 하나의 원자에 이름만 붙이는 데도 1404개의 별도 명제 문자가 필요하며, 그것들에 대해 일반적인 무언가를 말할 방법은 전혀 없습니다. 더 나쁜 것은, "모든 교수는 연구자이다"가 개체마다 하나씩인 13개 함의의 유한한 논리곱이 되어 버린다는 점입니다(professor-of-alice → researcher-of-alice, professor-of-bob → researcher-of-bob, 그리고 나머지 열한 개의 공허한 함의들). 그리고 열네 번째 개체가 등장하는 순간, 열네 번째 함의를 손으로 써 주어야 합니다. 1차 논리는 1404개의 이름 붙은 원자 전부를 변수에 적용된 몇 개의 술어 기호로 대체하고, 계속 불어나는 그 논리곱을 하나의 문장 ∀X (professor(X) → researcher(X))로 대체합니다. 이 문장은 개체가 몇 개나 나타나든 상관없이 계속 같은 의미를 유지합니다.

항, 술어, 그리고 두 한정사

1차 논리는 부족했던 장치를 여러 층으로 덧붙입니다. 먼저 항(term) — 개체를 가리키는 이름입니다. 상수(constant)는 하나의 고정된 개체를 가리키고(alice, bob, p1, mit), 변수(variable)는 개체들 위를 훑는 자리표시자입니다(X, Y). 진행 중인 예제에서 어느 쪽인지를 결정하는 유일한 기준은 대소문자이며, kb.py의 함수 하나(25–28행)가 이를 그대로 말해 줍니다.

def is_var(term: str) -> bool:
    """A term is a logic variable iff it is a non-empty string that starts with
    an uppercase letter. Constants (``alice``, ``p1``, ``mit``) start lowercase."""
    return isinstance(term, str) and len(term) > 0 and term[0].isupper()

다음은 술어(predicate)입니다. 술어는 한 사물의 속성(professor(x) — 여기서 항수(arity), 즉 인자 자리의 개수가 1이므로 단항(unary) 술어)이나, 여러 사물 사이의 관계(advises(x, y), 항수 2이므로 이항(binary) 술어)를 가리킵니다. 술어를 항들에 적용하면 원자(atom) — 가장 작은 완결된 주장 — 가 만들어집니다. 연결사들은 명제논리에서 그대로 넘어오며, 사용하기 전에 여기서 한 번씩 풀어 두겠습니다. ¬("아님", 부정)은 진릿값을 뒤집습니다. ∧("그리고", 논리곱)은 양쪽이 모두 참일 때만 참입니다. ∨("또는", 논리합)은 적어도 한쪽이 참이면 참입니다. →("함의한다", 실질 함의)은 참인 왼쪽이 거짓인 오른쪽을 만날 때만 거짓입니다. 곧 기대게 될 기호 ∈는 "…의 원소이다"로 읽고, ⊆는 "…의 부분집합이다"로 읽습니다.

진정으로 새로운 힘은 한정사(quantifier) 한 쌍이며, 이 두 기호는 천천히 읽을 가치가 있습니다. ∀(A를 뒤집은 모양, "모든 것에 대해"로 읽음)는 변수 하나에 대한 논리식을 정의역 전체에 대한 주장으로 바꿉니다. ∀X (professor(X) → researcher(X))는 그 함의가 모든 개체에 대해 성립한다고 주장합니다. ∃(E를 좌우 반전한 모양, "존재한다"로 읽음)는 논리식이 적어도 하나의 개체에 대해 성립한다고 주장합니다. ∃X advises(X, bob)는 누군가에 대해 bob을-지도한다가 참이라고 말합니다. 변수는 한정사 아래 놓일 때 한정(bound)되고, 그렇지 않으면 자유(free)입니다. 문장(sentence)이란 자유 변수가 없는 논리식으로, 세계가 고정되면 확정된 진릿값을 갖는 그런 것입니다. 기호들이 실제로 일하기 전에, fol.py가 논리식을 중첩된 파이썬 튜플로 어떻게 적는지에 대한 평이한 해독표를 소개합니다. ("all", "X", F)는 ∀X F를, ("exists", "X", F)는 ∃X F를, ("imp", F, G)는 F → G를 뜻하며, 원자는 술어 이름 뒤에 그 인자들이 이어진 형태입니다.

("atom", "professor", "X")
("not", F) / ("and", F, G) / ("or", F, G) / ("imp", F, G)
("all", "X", F) / ("exists", "X", F)

구조와 충족: 모든 개체를 시도해 보기

문장은 진공 속에서 진릿값을 갖지 않습니다. 그것을 검증할 세계가 필요합니다. 1차 논리에서 그 세계는 구조(structure, 모델(model)이라고도 부릅니다)이며, 여기서는 다음과 같은 쌍으로 씁니다.

$$\mathcal{S} \;=\; (D,\, I),$$

필기체 $\mathcal{S}$는 구조 전체를 가리키는 이름입니다. 첫 번째 부분 $D$는 정의역(domain), 즉 존재하는 개체들의 공집합이 아닌 집합입니다. 두 번째 부분 $I$는 해석(interpretation)으로, 모든 술어 기호에 그 외연(extension) — 그 술어가 성립하는 튜플들의 정확한 집합 — 을 건네주는 함수입니다. $n$항 술어 $P$($n$개의 인자를 받는 술어)에 대해 외연은 $D^n$, 즉 개체들의 길이-$n$ 튜플 전체의 집합의 부분집합입니다.

$$I(P) \;\subseteq\; D^n .$$

$D^n$은 "$D$를 그 자신과 $n$번 곱한 것"으로 읽으면 되며, 따라서 $D^2$는 개체들의 모든 순서쌍입니다. $\lvert D\rvert = 13$일 때(세로 막대는 "그 집합의 크기"를 뜻합니다), 이항 술어는 원리상 $13^2 = 169$개의 쌍에 대해 성립할 수 있습니다. advises의 외연은 그중 딱 4개만을 골라내는데, 이것이 바로 외연을 가능성으로 이루어진 큰 격자 안의 성긴 표로 그려 보는 것이 가장 좋은 이유입니다 [1]. Structure 클래스(fol.py, 27–34행)는 정확히 이 쌍입니다. self.domain이 $D$이고 self.relations가 $I$이며, 이는 각 술어 이름을 그것이 참이 되는 튜플들의 집합으로 대응시키는 딕셔너리입니다.

class Structure:
    def __init__(self, domain, relations: dict):
        self.domain = list(domain)
        # relations: predicate name -> set of tuples of constants
        self.relations = {k: set(v) for k, v in relations.items()}

    def rel(self, pred: str) -> set:
        return self.relations.get(pred, set())

동반 코드는 학계 세계로부터 구조를 곧바로 만들어 냅니다(fol.py, 62–73행). 순방향 연쇄(forward-chaining) 엔진을 모델(도출 가능한 모든 사실의 집합)에 이를 때까지 실행한 다음, 언급된 모든 개체를 정의역으로 읽어 내고 각 술어의 외연을 참인 인자 튜플들의 집합으로 읽어 냅니다.

def structure_from_kb() -> Structure:
    facts, rules = program()
    model = least_fixpoint(facts, rules)
    domain, relations = set(), {}
    for atom in model:
        pred, args = atom[0], atom[1:]
        relations.setdefault(pred, set()).add(tuple(args))
        domain.update(args)
    return Structure(sorted(domain), relations)

저 least_fixpoint 호출은 다음 장의 주제이므로, 지금은 그 출력을 주어진 것으로 받아들이겠습니다. 그것은 누적 크기가 $[23, 41, 47, 47]$인 세 번의 순방향 연쇄 물결을 거쳐 안정됩니다. 기초 사실 23개, 첫 번째 규칙 발화 물결 이후 41개, 그다음 47개, 그리고 더 추가할 것이 없어 다시 47개 — 완성된 모델은 47개의 원자이며 그중 24개가 도출된 것입니다. 그 모델을 구조로 읽어 들이면 13개의 개체(다섯 명의 사람, 세 편의 논문, 두 개의 기관, 세 개의 주제)로 이루어진 정의역과, 고정점에 이르는 과정에서 혼 규칙(Horn rule)들이 만들어 낸 다섯 개(researcher, person, grandAdvisor, colleague, citesTransitively)를 포함한 12개의 술어가 나옵니다. 마지막 지점이 중요합니다. 이 구조는 완성된 세계이므로, researcher는 이미 다섯 명의 사람 전원에 대해 성립하며, 단언된 두 명의 교수에 대해서만 성립하는 것이 아닙니다. 다음은 앞으로 이어질 추적들이 다루게 될 술어들의 외연으로, structure_from_kb가 구성하는 그대로입니다.

술어	항수	외연(참인 튜플)
professor	1	alice, bob
student	1	carol, dave, erin
researcher	1	alice, bob, carol, dave, erin
advises	2	(alice, bob), (bob, carol), (bob, dave), (carol, erin)
grandAdvisor	2	(alice, carol), (alice, dave), (bob, erin)

이제 충족(satisfaction) — "문장 $F$가 구조 $\mathcal{S}$에서 성립한다"는 관계이며, $\mathcal{S} \models F$로 쓰고, 튜른스타일(turnstile) $\models$는 "충족한다" 또는 "모델이 된다"로 읽습니다. 이는 $F$의 형태(shape)에 대한 재귀로 정의되며, 현재 한정되어 있는 각 변수를 그것이 나타내는 개체로 대응시키는 부분함수인 배정(assignment) $g$를 함께 가지고 다닙니다. 항 $t$가 $g$ 아래에서 가리키는 개체를 $\llbracket t\rrbracket_g$로 적으면 — 즉 $t$가 변수이면 $g(t)$이고, $t$가 상수이면 상수는 스스로를 가리키므로 $t$ 자신입니다 — 정의는 다음과 같습니다.

$$\begin{aligned} \mathcal{S},\,g \models P(t_1,\dots,t_n) \;&\text{iff}\; (\llbracket t_1\rrbracket_g,\dots,\llbracket t_n\rrbracket_g) \in I(P), \\ \mathcal{S},\,g \models \neg F \;&\text{iff}\; \text{not } \mathcal{S},\,g \models F, \\ \mathcal{S},\,g \models F \wedge G \;&\text{iff}\; \mathcal{S},\,g \models F \text{ and } \mathcal{S},\,g \models G, \\ \mathcal{S},\,g \models F \vee G \;&\text{iff}\; \mathcal{S},\,g \models F \text{ or } \mathcal{S},\,g \models G, \\ \mathcal{S},\,g \models F \to G \;&\text{iff}\; (\text{not } \mathcal{S},\,g \models F) \text{ or } \mathcal{S},\,g \models G, \\ \mathcal{S},\,g \models \forall X\, F \;&\text{iff}\; \text{for every } d \in D,\; \mathcal{S},\,g[X\!\mapsto\! d] \models F, \\ \mathcal{S},\,g \models \exists X\, F \;&\text{iff}\; \text{for some } d \in D,\; \mathcal{S},\,g[X\!\mapsto\! d] \models F, \end{aligned}$$

여기서 $g[X\!\mapsto\! d]$는 "배정 $g$를 갱신하여 이제 $X$가 $d$를 가리키도록 만든 것"을 뜻합니다. 이는 코드를 다른 말로 바꾼 것이 아닙니다. 그것이 바로 코드입니다. 함수 holds(fol.py, 37–59행)는 같은 순서로 똑같은 일곱 가지 경우를 훑습니다. 원자 절(41–44행)은 각 인자를 g.get(a, a)로 계산합니다 — 배정에서 그 항을 찾아보고, 찾지 못하면 그 항 자체를 상수로 사용하는데, 이것이 바로 $\llbracket t\rrbracket_g$입니다 — 그런 다음 외연에 속하는지를 검사합니다.

if op == "atom":
    pred, args = f[1], f[2:]
    tup = tuple(g.get(a, a) for a in args)
    return tup in struct.rel(pred)

연결사 절(45–52행)은 재귀의 불(Boolean) 행들입니다. 함의 행은 잠시 멈추어 볼 가치가 있습니다. 왜냐하면 그것이 작은 정리 하나를 조용히 담고 있기 때문입니다. imp는 (52행에서) (not holds(f[1], ...)) or holds(f[2], ...)로 구현되어 있으며, 이는 다음 항등식입니다.

$$F \to G \;\equiv\; \neg F \vee G$$

이를 실질 함의(material implication)라고 부릅니다. 네 연결사는 하나의 진리표를 공유하며, 그 표의 모든 행이 우리 세계 어딘가에 등장합니다.

$F$	$G$	$\neg F$	$F\wedge G$	$F\vee G$	$F\to G$	$F\to G$ 열에 대한 실제 증거
T	T	F	T	T	T	professor(alice) → researcher(alice)
T	F	F	F	T	F	student(carol) → professor(carol)
F	T	T	F	T	T	professor(carol) → researcher(carol) (공허)
F	F	T	F	F	T	professor(cmu) → researcher(cmu) (공허)

두 번째 행만이 함의를 거짓으로 만듭니다: 참인 전제와 거짓인 결론입니다. 전제가 거짓인 두 행을 포함해 나머지 모든 행은 함의를 참으로 만듭니다 — 이것이 바로 규칙이 실제로는 별 말도 하지 않는 개체들에 대해서 전칭 함의가 그토록 쉽게 통과하는 이유입니다.

두 한정사 절(53–58행)이야말로 완전히 새로운 아이디어 전부이며, 정의역이 유한하기 때문에 이들은 두 개의 파이썬 내장 함수가 됩니다. "모든 것에 대해"는 모든 개체가 통과해야 한다고 요구하는 말 그대로의 all(...)이고, "존재한다"는 적어도 하나는 통과해야 한다고 요구하는 말 그대로의 any(...)입니다.

if op == "all":
    var, body = f[1], f[2]
    return all(holds(body, struct, {**g, var: d}) for d in struct.domain)
if op == "exists":
    var, body = f[1], f[2]
    return any(holds(body, struct, {**g, var: d}) for d in struct.domain)

표현식 {**g, var: d}는 $g[X\!\mapsto\! d]$를 구체화한 것입니다. 현재 배정을 복사한 다음 var를 d에 고정합니다. struct.domain이 유한하기 때문에 all(...)과 any(...) 둘 다 유한한 목록을 훑으며 항상 종료합니다 — 교과서적인 충족의 정의가 실행 가능해진 것입니다 [1]. 이 모듈을 실행하면 두 개의 대표적인 검사 결과가 출력됩니다.

all professors are researchers: True
somebody advises bob: True

1차 구조로서의 학계 세계: 열세 개체로 이루어진 정의역과 그 위의 술어 외연들, 모든 개체를 훑어 검사하는 전칭 문장, 단 하나의 증인으로 충족되는 존재 문장, 그리고 2홉 관계 연쇄를 따라가며 답해지는 결합 질의. 저자가 AI의 도움을 받아 직접 제작한 원본 도해.

학계 세계에 관한 세 문장

구조를 손에 넣었으니, 세 문장으로 이 장치 전체를 보여 줄 수 있습니다. 각 문장은 동반 코드가 제공하는 생성자들(All, Exists, Imp, Atom — fol.py의 77–82행)로 만들어지고, holds에 의해 판정됩니다.

from fol import structure_from_kb, holds, All, Exists, Imp, Atom
s = structure_from_kb()

# ∀x (professor(x) → researcher(x))
print(holds(All("X", Imp(Atom("professor", "X"), Atom("researcher", "X"))), s))
# ∀x (student(x) → professor(x))
print(holds(All("X", Imp(Atom("student", "X"), Atom("professor", "X"))), s))
# ∃x advises(x, bob)
print(holds(Exists("X", Atom("advises", "X", "bob")), s))

True
False
True

holds가 실제로 정의역을 방문하는 정렬된 순서 그대로 훑으면서, 이들을 하나씩 읽어 보겠습니다.

∀X (professor(X) → researcher(X))는 참입니다. all(...)은 13개 개체 전부에서 그 함의를 확인해야 합니다. 다음은 그 완전한 훑기이며, 각 행은 X를 그 개체에 고정한 채로 이루어지는 holds에 대한 한 번의 호출입니다.

개체 $d$	professor(d)	researcher(d)	professor(d) → researcher(d)
alice	T	T	T
bob	T	T	T
carol	F	T	T
cmu	F	F	T
dave	F	T	T
erin	F	T	T
logic	F	F	T
mit	F	F	T
ml	F	F	T
nesy	F	F	T
p1	F	F	T
p2	F	F	T
p3	F	F	T

alice와 bob에서는 전제가 참이고, researcher ← professor 규칙(kb.py, 75행)이 순방향 연쇄 도중에 발화했기 때문에 결론도 참이므로 함의가 성립합니다. 그 밖의 모든 개체에서는 전제 professor가 거짓이어서 진리표의 세 번째와 네 번째 행에 해당하며, 따라서 함의는 공허하게 참입니다. 13개 전부가 통과하므로 all(...)은 True를 반환합니다.

∀X (student(X) → professor(X))는 거짓입니다. 여기서 이 장치는 지름길 하나를 드러냅니다. all(...)은 실패하는 첫 번째 개체에서 멈춥니다.

개체 $d$	student(d)	professor(d)	student(d) → professor(d)	지금까지의 all 판정
alice	F	T	T	계속 진행
bob	F	T	T	계속 진행
carol	T	F	F	중단, False 반환

carol은 학생이지만 교수는 아닙니다 — 함의표에서 거짓인 유일한 행입니다 — 그래서 holds는 carol에서 False를 반환하고, all(...)은 그 즉시 멈추며(short-circuit), 나머지 열 개체는 결코 검사되지 않습니다. 반례 하나가 전칭 문장을 가라앉힙니다.

∃X advises(X, bob)는 참입니다. 그리고 여기서는 쌍대적인 지름길이 즉시 발동합니다. any(...)는 성공하는 첫 번째 개체에서 멈추며, 정렬된 순서에서 첫 번째 개체는 alice입니다.

개체 $d$	advises(d, bob)	지금까지의 any 판정
alice	T	중단, True 반환

(alice, bob)이 advises의 외연에 들어 있으므로 holds는 alice에서 True를 반환하고, any(...)는 그 즉시 멈추며, 나머지 열두 개체는 결코 시도되지 않습니다. 증인 하나가 존재 문장을 들어 올립니다.

쌍대성: 반례 하나, 증인 하나

위의 두 지름길은 하나의 법칙이 지닌 두 얼굴입니다. 전칭 문장은 첫 번째 반례에서 무너지고, 존재 문장은 첫 번째 증인에서 일어섭니다. 형식적으로, "모든 것에 대해"를 부정하면 그 부정의 "존재한다"로 바뀝니다.

$$\neg\,\forall X\, F \;\equiv\; \exists X\, \neg F .$$

이 도출은 정의를 한 줄 풀어내는 것으로 끝납니다. $\forall X\,F$는 $F$가 모든 $d \in D$에서 성립한다는 뜻이며, 이것이 거짓인 것은 정확히 $F$가 어떤 $d$에서 실패할 때입니다. 그리고 "$F$가 어떤 $d$에서 실패한다"는 것은 정확히 "$\neg F$가 어떤 $d$에서 성립한다"는 것이며, 이는 $\exists X\,\neg F$입니다. 우리의 거짓인 전칭 문장이 바로 이 쌍대성이 작동하는 모습입니다. "모든 학생이 교수인 것은 아니다"라고 말하는 것은 "어떤 학생은 교수가 아니다"라고 말하는 것과 같으며, 함의를 풀어 보면($\text{student} \to \text{professor} \equiv \neg\,\text{student} \vee \text{professor}$이고 그 부정은 $\text{student} \wedge \neg\,\text{professor}$) 증인이 곧바로 드러납니다. carol은 학생이면서 교수가 아닙니다. ∀를 가라앉힌 반례가 곧 쌍대인 ∃를 충족시키는 증인입니다. 이것이 바로 holds가 all과 any 두 절만 있으면 되는 이유입니다. 부정은 어느 한 한정사를 다른 한정사로 바꾸어 놓으므로, 둘 다 구현하는 것은 필수가 아니라 편의를 위한 것입니다.

결합 질의: ∃∧ 단편

실제 질문은 예/아니오로 답해지는 경우가 드뭅니다. 우리는 무언가를 참으로 만드는 개체들을 원합니다. 그런 질문들은 1차 논리 안의 작지만 핵심적인 한 구석 — 존재-논리곱 단편(∃∧, existential-conjunctive fragment) — 에 살고 있습니다. 질의(query)란 원자들의 존재 한정된 논리곱이며, 그중 일부 변수는 답이 될 수 있도록 자유롭게 남겨 둡니다. "alice가 누구를 그랜드-지도하는가?"는 다음을 만족하는 모든 개체 $Z$를 묻습니다.

$$\exists Y\;\big(\mathrm{advises}(\text{alice}, Y) \;\wedge\; \mathrm{advises}(Y, Z)\big),$$

이는 grandAdvisor 규칙(kb.py, 79행)이 포착하는 것과 똑같은, 지도-지도 합성 연쇄입니다. 우리는 각 개체를 $Z$로 시도해 보고, 그때 내부의 존재 문장이 충족되는지를 holds에게 물음으로써 이 질의에 답합니다.

from fol import structure_from_kb, holds, Exists, And, Atom
s = structure_from_kb()

# Who does alice grand-advise?  every Z with  ∃Y advises(alice,Y) ∧ advises(Y,Z)
answers = [z for z in s.domain
           if holds(Exists("Y", And(Atom("advises", "alice", "Y"),
                                     Atom("advises", "Y", z))), s)]
print(answers)

['carol', 'dave']

이 루프는 이중 훑기이며, 그것을 추적해 보면 답이 왜 그렇게 되는지가 정확히 드러납니다. 바깥 루프는 후보 $Z$를 고정하고, 안쪽의 ∃Y는 중간 사람 $Y$를 찾아 모든 개체를 훑습니다. 왼쪽 논리곱 항 advises(alice, Y)는 $Y$의 값이 단 하나, 즉 bob일 때만 참입니다. 왜냐하면 (alice, bob)이 첫 번째 자리가 alice인 advises 외연의 유일한 쌍이기 때문입니다. 그러므로 전체 논리곱은 $Y = \text{bob}$일 때만 성공할 수 있으며, 그러면 문제는 advises(bob, Z)가 성립하는지를 묻는 것으로 줄어듭니다. bob은 carol과 dave를 지도합니다. 다음은 바깥 훑기이며, 의미 있는 후보들만 자세히 적고 나머지는 뭉뚱그렸습니다.

후보 $Z$	advises(bob, Z)가 참인가?	안쪽 ∃Y의 결과	답 집합에 속하는가?
alice	아니요	False	—
bob	아니요	False	—
carol	예	True ($Y=$ bob)	✓
cmu	아니요	False	—
dave	예	True ($Y=$ bob)	✓
erin	아니요	False	—
logic, mit, ml, nesy, p1, p2, p3	아니요	False	—

답 집합은 carol과 dave이며, 이는 grandAdvisor의 외연인 (alice, carol)과 (alice, dave)와 정확히 일치합니다. erin은 이 집합에 속하지 않으며, 추적 과정이 정확히 그 이유를 말해 줍니다. erin에 이르는 유일한 지도 연쇄는 bob → carol → erin이므로, erin은 bob으로부터 두 홉(그것이 도출된 사실 grandAdvisor(bob, erin)입니다) 떨어져 있지만, alice로부터는 세 홉 떨어져 있습니다. 그랜드-지도란 정확히 두 홉을 뜻하며, alice는 erin으로부터 지도-두-홉만큼 떨어져 있지 않습니다.

바로 이 형태 — 존재 한정된 논리곱이 바인딩들의 집합을 반환하는 것 — 이 데이터베이스 질의의 주역이며, SQL의 SELECT ... WHERE 밑바탕에 깔린 ∃∧의 핵심입니다 [3]. 이것은 또한 정확히 4권이 존재-양의 1차(EPFO, existential positive first-order) 질의에 대한 복합 질의 응답(complex query answering)이라는 이름 아래 배우게 될 과제이기도 합니다. 지식 그래프가 불완전해서 정직한 holds 루프가 아무도 적어 두지 않은 답을 놓치게 될 때, 신경망 모델은 그럼에도 답 집합을 예측합니다. 그러므로 정의역에 대한 이 소박한 이중 루프는, 그러한 신경망 질의 응답기들이 우리가 가진 사실들 위에서 흉내 내려 하고, 우리가 갖지 못한 사실들 위에서 뛰어넘으려 하는 상징적 정답(ground truth)입니다.

아직 풀리지 않은 부분

비슷하게 들리는 두 질문이 정반대의 운명을 맞습니다. 첫 번째는 모델 검사(model checking)입니다. 하나의 고정된 유한 구조 $\mathcal{S}$와 문장 $F$가 주어졌을 때, $\mathcal{S} \models F$인가? 이것이 바로 holds가 계산하는 것이며, 이는 완전히 결정 가능합니다 — 재귀는 유한하게 많은 소속 검사로 바닥에 닿고, 각 한정사는 유한한 all(...) 또는 any(...)이므로, 이 절차는 항상 확정된 예/아니오와 함께 멈춥니다. (그 비용은 정직하지만 유계입니다. 크기 $\lvert D\rvert$인 정의역 위에서 $k$개의 한정사가 중첩된 문장은 $\lvert D\rvert^{k}$ 자릿수 정도의 개체 검사를 강제할 수 있습니다. 각 한정사 층이 그 앞 층 안에서 정의역 전체를 훑기 때문입니다.)

두 번째 질문은 "이 세계"를 "모든 세계"로 바꿔 놓습니다. 문장이 타당(valid)하다는 것은, $\models F$로 쓰며, 무한한 것까지 포함한 모든 크기의 모든 구조에서 참이라는 뜻입니다 — 명제논리적 항진명제(tautology)의 1차 논리판 대응물입니다. 여기서 벽이 솟아오릅니다. 1차 논리의 타당성은 결정 불가능(undecidable)합니다. 1936년에 증명되었듯이, 임의의 1차 논리 문장이 타당한지를 반드시 정지하면서 항상 답할 수 있는 알고리즘은 존재할 수 없습니다 [1][2]. 어떤 절차든 할 수 있는 최선은 그것을 반결정(semi-decide)하는 것뿐입니다. 괴델(Gödel)의 완전성 정리에 의해, 어떤 문장이 타당한 것은 정확히 그것이 증명 가능할 때이며, 즉 $\models F$ iff $\vdash F$입니다(단일 튜른스타일 $\vdash$는 "증명 가능하다"로 읽습니다). 따라서 증명 탐색은 타당한 문장을 모두 나열할 수 있고, 진짜로 타당한 어떤 $F$에 대해서든 결국 그것을 확인해 낼 것입니다. 하지만 타당하지 않은 $F$에 대해서는 바로 그 탐색이 영원히 실행되어 결코 사건을 종결짓지 못할 수도 있습니다. 그렇다면-확인, 아니라면-어쩌면-무한루프. 이 비대칭성이 바로 결정 불가능성의 정확한 질감입니다.

두 질문 사이의 간극은 하나의 유한한 세계를 검사하는 것과 상상 가능한 모든 세계에 대해 한정하는 것 사이의 간극이며, 이는 우리 코드의 결함이 아니라 논리 자체에 내장된 벽입니다. 이는 또한 이 시리즈가 완전한 1차 논리에 머무르지 않는 이유이기도 합니다. 2권은 의도적으로 더 온순하고 결정 가능한 단편인 EL 계열의 기술논리(description logic)로 물러나며, 추론이 항상 종료된다는 보장을 얻기 위해 얼마간의 표현력을 내어 줍니다. 벽이 어디에 서 있는지를 아는 것이야말로 그 후퇴를 항복이 아니라 설계상의 선택으로 바꾸어 놓습니다.

왜 중요한가

신경기호 AI(neuro-symbolic AI)는 대체로, 오직 한정된 논리만이 진술할 수 있는 종류의 일반적인 지식 — "모든 교수는 연구자이다", "지도 관계가 합성되어 그랜드-지도가 된다" — 을 신경망이 존중하도록 가르치면서도, 순수한 기호적 매칭이 잘 다루지 못하는 누락된 사실이나 잡음 섞인 입력에 견고하게 대처하도록 만드는 프로젝트입니다. 1차 논리는 이 프로젝트에 정확한 목표를 부여합니다. 이름 붙은 대상들 위의 관계, 한정된 규칙, 그리고 실제 답 집합을 갖는 결합 질의입니다. 그리고 그 목표는 모호하지 않습니다. 그것은 구체적이고 실행 가능한 절차입니다. 유한한 정의역을 all과 any로 훑는 충족 재귀 ⊨입니다. 이후의 모든 권은 이 장의 정확한 절차 중 하나를 미분 가능한 무언가로 근사합니다 — 4권의 학습된 질의 응답은 우리가 carol과 dave에 대해 추적했던 결합 질의 루프를 근사합니다. all(...)이 어느 개체에서 멈추는지, any(...)이 어느 증인을 붙잡는지까지 세세하게 또렷한 기호적 버전을 먼저 알아 두면, 신경망 근사가 무엇을 반환해야 하는지를 언제나 말할 수 있습니다.

핵심 용어

• 항(term) — 개체를 가리키는 이름: 상수이거나 변수이다.
• 상수(constant) — 하나의 고정된 개체를 가리킨다(alice, p1, mit). is_var 관례에 따라 소문자로 시작한다.
• 변수(variable) — 개체들 위를 훑는 자리표시자이다(X, Y). 대문자로 시작한다. 한정사 아래에 있으면 한정(bound)되고, 그렇지 않으면 자유(free)이다.
• 술어/항수(predicate/arity) — 속성을 나타내는 기호(professor, 단항)이거나 관계를 나타내는 기호(advises, 이항)이다. 항수는 인자 자리의 개수이다. 항들에 적용하면 가장 작은 완결된 주장인 원자(atom)가 만들어진다.
• 한정사(quantifier) — ∀("모든 것에 대해")는 술어부가 모든 개체에 대해 성립한다고 주장하고, ∃("존재한다")는 적어도 하나의 개체에 대해 성립한다고 주장한다. 쌍대성 ¬∀X F ≡ ∃X ¬F로 서로 연결된다.
• 문장(sentence) — 자유 변수가 없는 논리식으로, 구조가 고정되면 확정된 진릿값을 갖는다.
• 구조/모델(structure/model) — 쌍 $(D, I)$: 개체들의 정의역 $D$와 각 술어에 외연을 부여하는 해석 $I$. 문장이 그에 비추어 검증되는 세계이다.
• 외연(extension) — $n$항 술어 $P$가 성립하는 튜플들의 정확한 집합 $I(P) \subseteq D^n$.
• 배정(assignment) — 한정된 각 변수를 그것이 현재 나타내는 개체로 대응시키는 함수 $g$이며, 한정사 아래에서 $g[X\!\mapsto\! d]$로 확장된다.
• 충족(satisfaction, ⊨, holds) — 문장이 어떤 구조에서 참인지의 여부. 논리식의 형태에 대한 재귀로 정의되며, 한정사는 유한한 정의역 안의 모든 개체를 시도해 판정한다(∀에는 all, ∃에는 any).
• 실질 함의(material implication) — $F \to G \equiv \neg F \vee G$. 참인 전제가 거짓인 결론을 만날 때만 거짓이며, 이것이 holds가 imp를 구현하는 방식이다.
• 모델 검사 대 타당성(model checking vs. validity) — 하나의 유한한 세계에서의 $\mathcal{S}\models F$는 결정 가능하지만, 모든 세계에서의 $\models F$는 결정 불가능하다(오직 $\vdash$를 통한 반결정만 가능하다). 이것이 2권이 결정 가능한 기술논리로 물러나는 이유이다.
• 결합 질의(∃∧)/EPFO(conjunctive query/EPFO) — 자유로운 답 변수를 가진, 원자들의 존재 한정된 논리곱이다. 데이터베이스 질의의 핵심이며, 불완전한 지식 그래프에 대한 4권의 복합 질의 응답 목표이다.

이 장이 이끄는 곳

우리는 어떤 문장이 어떤 세계에서 참이라는 것이 무엇을 의미하는지를 말했고, 충족 관계를 정확하게 정의했으며, 유한한 정의역에 대한 무차별 나열(brute enumeration)로 그것을 검사했습니다. 하지만 나열은 추론기(reasoner)가 실제로 무언가를 증명하는 방식이 아니며, 끝에서 끝까지 걸어갈 수 없을 만큼 큰 세계에 대해서는 아무것도 말해 주지 않습니다. 또한 이 장은 완성된 모델을 은근슬쩍 선물처럼 받아들였습니다 — 저 $[23, 41, 47, 47]$이라는 물결들은 무대 밖에서 일어난 일이었습니다. 다음 장인 추론과 증명: 사실을 연쇄시켜 결론에 이르기는 의미에서 메커니즘으로 넘어갑니다. 기계가 학계 세계의 혼 규칙들을 한 단계씩 적용하여, 더는 새로운 것이 나타나지 않을 때까지 새로운 사실을 어떻게 도출하는지를 다룹니다 — 검사를 통한 진리가 도출을 통한 진리에 자리를 내어 줍니다.

---

동반 코드: examples/logic/fol.py는 순수 표준 라이브러리 파이썬으로 Structure 클래스와 충족 관계 holds를 구현하며, 위에서 도출한 그대로 일곱 개의 재귀 절을 그대로 써 두었습니다. examples/logic/kb.py는 공유되는 학계 세계입니다. python3 examples/logic/fol.py를 실행해 두 개의 대표적인 검사를 재현하고, structure_from_kb()로 구조를 만들어 이 장에서 추적한 모든 훑기와 질의를 다시 실행해 보십시오.