형식 논리 기호 읽는 법 — ∀, ⇒, ×를 테스트 코드로 옮겨 읽기

정의

형식 논리(formal logic) 는 문장을 기호로 적어서, 그 문장이 참인지 거짓인지를 뜻이 아니라 모양만 보고 기계적으로 따질 수 있게 만든 표기법이에요.

"로그인 안 한 사람한테는 버튼이 꺼져 있어야 해요"라는 문장은 사람마다 조금씩 다르게 읽혀요. 버튼이 안 보이면 되는지, 보이되 눌리지만 않으면 되는지요. 같은 내용을 기호로 적으면 읽는 방법이 하나로 정해져요.

\forall x \in \Omega,\quad \neg Auth(x) \Rightarrow \neg Enabled(x)

이 문서는 명세와 증명에 자주 나오는 기호를 세 묶음으로 나눠 설명해요. 값을 모아두는 집합 기호, 참·거짓을 잇는 논리 연결자, "모든"과 "어떤"을 말하는 한정자예요. 기호마다 TypeScript로 옮긴 코드를 같이 붙였어요. 코드로 읽을 수 있으면 기호는 어렵지 않아요.

왜 필요한가

테스트는 결국 "이 입력들에서 이 성질이 지켜지는가"를 묻는 일이에요. 그런데 "이 입력들"과 "이 성질"을 말로 적어두면 두 군데서 구멍이 생겨요.

범위가 흐려져요. "다양한 화면 크기"는 몇 개인지, 경계가 어디인지 말해주지 않아요. Width = {320, ..., 3840}은 3,521개라고 말해줘요.
방향이 흐려져요. "편집자면 쓸 수 있다"가 "편집자만 쓸 수 있다"까지 뜻하는지 문장만으로는 알 수 없어요. 기호로는 ⇒와 ⇔로 갈려서 섞일 수가 없어요.

AI에게 명세를 넘길 때 특히 중요해요. 말로 된 명세는 구현하기 쉬운 쪽으로 읽히기 쉬운데, 기호로 된 명세는 그렇게 읽을 여지가 거의 없어요. Bend 같은 증명 언어가 받는 입력도 결국 이 기호들을 코드로 옮긴 거예요.

동작 원리

집합: 값을 모아둔 주머니

집합은 값들을 중복 없이 모아둔 거예요. 테스트에서는 "가능한 입력 전부"를 적을 때 써요.

기호	읽는 법	예시	TypeScript로 옮기면
`{a, b, c}`	a, b, c로 이뤄진 집합	`Auth = {false, true}`	`const auth = [false, true]`
`x ∈ A`	x는 A에 속해요	`768 ∈ Width`	`A.includes(x)`
`A ⊆ B`	A는 B에 다 들어가요	`S ⊆ Ω`	`A.every((x) => B.includes(x))`
`A × B`	A와 B에서 하나씩 고른 모든 쌍	`Width × Auth`	이중 `for` 또는 `flatMap`
`{x ∈ A ∣ C(x)}`	A 중에서 C를 만족하는 것만	불가능한 조합 빼기	`A.filter(C)`
`A ∪ B`	합집합: 둘 중 하나에라도 있는 것	구역 합치기	`new Set([...A, ...B])`
`A ∩ B`	교집합: 둘 다에 있는 것	구역 겹침 확인	`A.filter((x) => B.includes(x))`
`∅`	원소가 하나도 없는 집합	겹침이 없음	`[]`
`∣A∣`	A의 원소 개수	`∣Auth∣ = 2`	`A.length`

×(곱집합, Cartesian product)는 테스트 공간을 만들 때 가장 많이 써요.

Auth \times Permission = \{(false, viewer), (false, editor), \dots, (true, admin)\}

개수는 곱으로 늘어나요. ∣A × B∣ = ∣A∣ × ∣B∣라서 2 × 3 = 6쌍이에요. 축을 하나 추가할 때마다 테스트 공간이 곱으로 커지는 이유가 이거예요.

const omega = widths.flatMap((width) =>
  auths.flatMap((auth) => roles.map((role) => ({ width, auth, role }))),
);

{x ∈ A ∣ C(x)} 같은 표기를 조건 제시법(set-builder notation)이라고 해요. 세로 막대 ∣ 왼쪽이 "어디서 고르는지", 오른쪽이 "어떤 조건으로 고르는지"예요. filter와 모양이 똑같아요.

Ω(오메가)나 P₁ 같은 이름은 특별한 기호가 아니고, 집합에 붙인 이름이에요. 아래 첨자는 번호예요. Ω₀, Ω₁은 첫 번째 공간과 그다음 버전의 공간이라는 뜻이고요.

논리 연결자: 참·거짓을 잇는 접착제

명제(proposition)는 참이나 거짓 중 하나로 정해지는 문장이에요. "768은 767보다 크다"는 명제이고, "버튼을 예쁘게 만들자"는 명제가 아니에요. 연결자는 명제 여러 개를 이어 새 명제를 만들어요.

기호	이름	읽는 법	TypeScript
`¬P`	부정	P가 아니다	`!p`
`P ∧ Q`	논리곱	P 그리고 Q	`p && q`
`P ∨ Q`	논리합	P 또는 Q (둘 다여도 됨)	`p \|\| q`
`P ⇒ Q`	함의	P이면 Q	`!p \|\| q`
`P ⇔ Q`	동치	P와 Q는 같이 참이고 같이 거짓	`p === q`

참(T)과 거짓(F)을 모든 조합으로 넣어보면 이래요. 이런 표를 진리표(truth table)라고 해요.

P	Q	`P ∧ Q`	`P ∨ Q`	`P ⇒ Q`	`P ⇔ Q`
T	T	T	T	T	T
T	F	F	T	F	F
F	T	F	T	T	F
F	F	F	F	T	T

다른 건 직관대로인데 ⇒가 낯설어요. P ⇒ Q가 거짓인 경우는 딱 하나, P가 참인데 Q가 거짓일 때뿐이에요. P가 거짓이면 Q가 뭐든 참이에요.

약속으로 생각하면 쉬워요. "비가 오면 우산을 가져갈게"라고 했는데 비가 안 왔어요. 우산을 가져갔든 안 가져갔든 약속을 어긴 건 아니죠. 약속을 어길 기회 자체가 없었으니까요. 그래서 TypeScript로는 !p || q가 돼요.

이 성질이 테스트에서 공허한 참(vacuous truth)을 만들어요. "로그인했으면 편집 가능"을 검사하는데 로그인한 입력이 하나도 없으면 테스트는 전부 통과해요. 조건이 한 번도 참이 된 적이 없으니까요.

함의를 뒤집을 때 조심할 것

P ⇒ Q에서 파생되는 명제가 세 개 있는데, 원래 명제와 같은 뜻인 건 하나뿐이에요.

이름	모양	원래 명제와 같은 뜻인가요?
원래 명제	`P ⇒ Q`	기준
대우(contrapositive)	`¬Q ⇒ ¬P`	같아요
역(converse)	`Q ⇒ P`	달라요
이(inverse)	`¬P ⇒ ¬Q`	달라요

"로그인 안 했으면 비활성"(¬Auth ⇒ ¬Enabled)의 대우는 "활성이면 로그인한 상태"(Enabled ⇒ Auth)예요. 둘은 완전히 같은 법칙이라, 테스트하기 편한 쪽을 골라 쓰면 돼요.

이도 달라요. "로그인 안 했으면 비활성"에서 "로그인했으면 활성"은 나오지 않아요. viewer는 로그인해도 비활성이니까요. 금지 법칙만 적어두고 역방향까지 보장된 것처럼 착각하면, 아무것도 안 하는 구현이 테스트를 통과해요.

`⇔`는 양방향 두 개를 묶은 것

(P \iff Q) \equiv (P \Rightarrow Q) \land (Q \Rightarrow P)

≡는 "두 식이 항상 같은 참·거짓을 가진다"는 뜻이에요. 그러니까 ⇔ 하나에는 법칙이 두 개 들어 있어요.

Enabled \iff Auth \land CanEdit \land Wide

이 한 줄을 풀면 이렇게 나눠져요.

⇒ 방향: 활성이면 세 조건이 다 참이에요. 대우를 취하면 "셋 중 하나라도 거짓이면 비활성"이고, 금지 법칙 L1~L3이 여기서 나와요.
⇐ 방향: 세 조건이 다 참이면 활성이에요. 의무 법칙 L4가 이거예요.

명세를 ⇔로 적어두면 금지와 의무를 한꺼번에 못 박을 수 있어요. ⇒만 적으면 절반이 빠져요.

우선순위

괄호가 없으면 ¬, ∧, ∨, ⇒, ⇔ 순서로 먼저 묶어요. 곱셈이 덧셈보다 먼저인 것과 같아요.

\neg P \land Q \Rightarrow R \quad\equiv\quad ((\neg P) \land Q) \Rightarrow R

헷갈리면 괄호를 치는 게 제일 안전해요. 괄호가 많아서 틀리는 명세는 없어요.

한정자: "모든"과 "어떤"

연결자만으로는 입력 하나에 대한 말밖에 못 해요. "모든 입력에 대해"라고 말하려면 한정자(quantifier)가 필요해요.

기호	이름	읽는 법	TypeScript
`∀x ∈ A, P(x)`	전칭 한정자	A의 모든 x에 대해 P(x)가 참	`A.every(P)`
`∃x ∈ A, P(x)`	존재 한정자	A에 P(x)를 만족하는 x가 적어도 하나 있음	`A.some(P)`

∀는 All의 A를, ∃는 Exists의 E를 뒤집은 모양이에요.

P(x)처럼 입력을 받아 참·거짓을 돌려주는 걸 술어(predicate)라고 해요. TypeScript로는 (x) => boolean 함수예요.

반례는 `∀`의 부정이에요

\neg\, \forall x,\ P(x) \iff \exists x,\ \neg P(x)

"모두가 P다"가 거짓이라는 건 "P가 아닌 게 적어도 하나 있다"는 뜻이에요. 그 하나가 바로 반례(counterexample)예요.

그래서 테스트와 증명이 할 수 있는 일이 갈려요.

∀를 참이라고 보이려면 모든 경우를 확인해야 해요. 공간이 유한하고 작으면 전부 돌려볼 수 있고, 무한하거나 크면 증명이 필요해요.
∀를 거짓이라고 보이려면 반례 하나면 돼요. 속성 기반 테스트(property-based testing) 도구가 하는 일이 이 반례 찾기예요.

테스트 1,000번이 통과했다는 건 이렇게 적을 수 있어요.

\forall x \in S,\ P(x) \qquad S \subseteq \Omega,\ \ \lvert S \rvert = 1000

S가 Ω 전체가 아니면 ∀x ∈ Ω, P(x)는 여전히 모르는 상태예요. 통과한 테스트와 증명이 다른 이유가 기호로는 이렇게 한 줄에 보여요.

빈 집합 위의 `∀`는 항상 참이에요

\forall x \in \varnothing,\ P(x)

이 명제는 P가 무엇이든 참이에요. 확인할 원소가 없으니 어긴 원소도 없어요. JavaScript에서도 [].every(() => false)는 true예요. 필터 조건이 서로 모순이어서 입력이 하나도 안 남았는데 "전부 통과"라고 보고되는 사고가 여기서 나와요. 그래서 ∀를 검사할 때는 짝으로 ∃도 확인해요. 조건을 만족하는 입력이 실제로 있는지요.

한정자 순서를 바꾸면 뜻이 바뀌어요

\forall x\, \exists y,\ Mother(y, x) \qquad\text{vs}\qquad \exists y\, \forall x,\ Mother(y, x)

왼쪽은 "모든 사람에게는 엄마가 있다"예요. 오른쪽은 "모든 사람의 엄마인 한 사람이 있다"고요. 기호 두 개의 순서만 바꿨는데 전혀 다른 주장이 돼요.

테스트에서도 같아요. "모든 사용자에게 쓸 수 있는 역할이 있다"와 "모든 사용자가 쓸 수 있는 역할이 하나 있다"는 다른 요구사항이에요.

함수 표기

표기	뜻	예시
`f(x)`	f에 x를 넣은 결과	`I(x)`: 구현에 입력 x를 넣은 결과
`f: A → B`	A의 값을 받아 B의 값을 돌려주는 함수	`π: Result → Bool`
`f(g(x))`	g를 먼저, 그 결과에 f	`U(U(s, p), p)`: 같은 업데이트를 두 번
`π`	투영: 필요한 부분만 골라냄	`π(result) = result.enabled`

π는 원주율이 아니라 투영(projection)의 머리글자로 쓴 이름이에요. 여기서는 "무엇을 보고 같다고 판단할지"를 정하는 함수예요.

실무 적용

긴 수식은 바깥에서 안쪽으로 읽어요

defining-done-for-ai-code에서 "완벽한 구현"을 이렇게 적었어요.

Perfect(I) \iff \forall x \in \Omega,\quad P\big(x,\ \pi(I(x))\big)

바깥부터 한 겹씩 벗기면 돼요.

Perfect(I) ⇔ …: 구현 I가 완벽하다는 건 오른쪽과 같은 뜻이에요.
∀x ∈ Ω: 공간 Ω의 모든 입력 x에 대해
I(x): 구현에 x를 넣고
π(…): 그 결과에서 볼 부분만 골라서
P(x, …): 입력과 함께 법칙 P에 넣었을 때 참이에요.

코드로 옮기면 한 줄이에요.

const perfect = omega.every((x) => P(x, pi(I(x))));

Bend 문법과 기호 대응

증명 언어 Bend 2는 이 기호들을 코드로 적어요. Bend 가이드는 "명제는 타입이고, 증명은 그 타입의 def"라고 설명하는데, 이 대응을 커리-하워드 대응(Curry–Howard correspondence)이라고 불러요.

논리 기호	Bend 문법	설명
`∀x ∈ T`	`for x: T`	law의 바인더. 증명 def에서는 매개변수가 돼요
`∃z ∈ C`	`exs z: C`	증인(witness)을 `(z, proof)` 쌍으로 돌려줘야 해요
`a = b`	`{a == b : T}`	등식 명제
`a ≠ b`	`{a != b : T}`	`{a == b : T} -> Empty`의 줄임말
`P ⇒ Q`	`P -> Q` 또는 추가 `for h: P`	P의 증명을 받아 Q의 증명을 돌려주는 함수
거짓	`Empty`	값이 하나도 없는 타입

P ⇒ Q의 증명이 함수라는 게 핵심이에요. "P의 증거를 주면 Q의 증거를 만들어줄게"라는 약속이니까요. 그래서 가정이 곧 매개변수가 되고, 목표가 가정과 같은 모양으로 줄어들면 그 매개변수를 그대로 돌려주는 것만으로 증명이 끝나요.

law wide_editor_is_enabled:
  for width: Nat
  for wide: {Nat.is_ge(width, 768n) == True{} : Bool}
  {E.enabled(True{}, E.Editor{}, width) == True{} : Bool}

def Laws.wide_editor_is_enabled(width, wide):
  wide

{==}는 반사율(reflexivity), 즉 "양쪽을 계산해보니 똑같다"로 등식을 증명해요. ≠가 -> Empty인 것도 같은 원리예요. "같다는 증거를 주면 불가능한 것을 만들어낼 수 있다"는 뜻이니 "같지 않다"가 되는 거죠.

명세를 기호로 옮기는 순서

입력의 축마다 집합을 적어요. Width = {320, …, 3840}처럼 범위와 단위까지요.
축을 ×로 묶어 공간 Ω를 만들어요. 뺄 조합이 있으면 {x ∈ Ω ∣ C(x)}로 빼고 C의 근거를 적어요.
법칙을 ⇔로 먼저 적어봐요. ⇒로 충분한 법칙인지, 역방향도 필요한지 여기서 드러나요.
맨 앞에 ∀x ∈ Ω를 붙이고, 짝으로 ∃x ∈ Ω(법칙의 조건을 만족하는 입력이 있는지)를 확인해요.
기호마다 TypeScript의 every, some, filter로 옮겨서 작은 공간에서 돌려봐요.

트레이드오프

기호는 짧고 모호하지 않지만, 처음 보는 사람에게는 진입 장벽이에요. 명세 문서에는 기호 바로 아래에 한국어 풀이를 붙이는 게 좋아요.
기호로 정확하게 적어도 틀린 명세는 틀린 채로 정확해요. 경계를 1000으로 잘못 적으면 그 잘못도 정확하게 전달돼요. 형식화는 모호함을 없애줄 뿐, 요구사항이 맞는지는 따로 확인해야 해요.
무한 집합 위의 ∀는 돌려서 확인할 수 없어요. 증명을 써야 하는데, 증명은 테스트보다 훨씬 비싸요.

사용하면 안 되는 경우

정답이 원래 여러 개인 영역이에요. 레이아웃 미세 조정, 문구, 추천 순서 같은 걸 ⇔ 한 줄로 못 박으면 정상 변경마다 명세가 깨져요.
뭘 만들지 자체가 미정인 프로토타입이에요. 공간과 법칙을 적는 비용이 만드는 비용보다 커요.
팀원 대부분이 기호를 못 읽는 상황에서, 풀이 없이 기호만 남기는 경우예요. 아무도 검토하지 못하는 명세는 명세가 아니에요.

흔한 실수

⇒를 인과관계로 읽어요. P ⇒ Q는 "P가 Q를 일으킨다"가 아니라 "P가 참인데 Q가 거짓인 경우는 없다"예요.
이를 원래 명제로 착각해요. "로그인 안 했으면 비활성"에서 "로그인했으면 활성"은 나오지 않아요.
빈 공간에서 ∀를 확인해요. 조건이 모순이면 입력이 0개인데 테스트는 전부 통과해요. ∃로 짝을 확인해요.
∈와 ⊆를 섞어요. ∈는 원소 하나가 집합에 속한다는 뜻이고, ⊆는 집합 전체가 다른 집합에 들어간다는 뜻이에요. 768 ∈ Width, {767, 768} ⊆ Width예요.
한정자 순서를 무심코 바꿔요. ∀∃와 ∃∀는 다른 주장이에요.
∀x ∈ S를 ∀x ∈ Ω로 보고해요. 테스트로 확인한 건 넣어본 입력 S에서뿐이에요.