논리적이 되는 두 가지 방법 - 논리와 저수준(Low-level) 자료 표현(Data representation) (2 편 중 1 편)
논리적인 말?
언제 어떤 문장이 "논리적이다"고 할 수 있을까? 일상적으로는우리는 이를 남용해 의미가 있어 보이는 것을 "논리적이다"라고수식하고는 한다. 그러나 필자는 이 남용이 "논리적"이라는 표현을 너무가볍게 보고 있는 것이라 말하겠다. 어떤 것이 진정 논리적이기 위해서는의미가 있는 것은 물론이거니와 최소한 다음의 두 조건을 더 만족해야한다.몇몇 가정으로부터 그것을 증명해야 한다.증명에 쓰인 체계가 모순을 보일 수 없어야 한다.<이 글에서는 이 중 1 번을 중점으로 설명하여 "좋은 가정 아래"어떤 것이 논리적임을 증명하는 두 방법에 대해 다루어 볼 것이다.두 방법 중 하나는 함수형 언어로 쓰인 프로그램과 유사한 구조를가지며 나머지 하나는 일반적인 함수형 언어와는 상이한 구조를 가진다.이 중 두번째 방법에 대해서는 (약간의 부정행위를 하면…\ldots)2 번을 간단하게 보일 수 있기 때문에 이 또한 다룰 것이다.논리적 증명의 대상
어떻게 어떤 것이 논리적이라는 걸 증명할 수 있는 지에 설명하기에앞서 짚고 넘어가야 할 매우 중요한 요소가 하나 있다. 바로
질문
무엇이 논리적이냐?<는 것이다. 이 글에서는 철학적인 복잡도를덜기 위해 이 대상을 다음과 같이 단순히 설명할 것이다.<논리적일 수 있는 대상은 명제(proposition)에 대한판단(judgment)이다.<여기서 명제는 다음과 같이 정의되는 대상이다.단위 명제(Atomic Proposition) AA는 명제이다.참 명제(True Proposition) ⊤\top은 명제이다.거짓 명제(False Proposition) ⊥\bot은 명제이다.명제 PP와 QQ가 있을 때, P∧QP \land Q(PP 그리고 QQ)는 명제이다.명제 PP와 QQ가 있을 때, P∨QP \lor Q(PP 또는 QQ)는 명제이다.명제 PP와 QQ가 있을 때, P→QP \to Q(PP라면 QQ)는 명제이다.<여기서 단위 명제란 우리가 선택한, 더이상 세밀하게분석하지 않을 논리적인 최소 단위이다. 예를 들어 1+1=21 + 1 = 2와0+2=30 + 2 = 3을 단위 명제로 두었을 때[1] 다음과 같은 것들이 명제이다.⊤\top1+1=21 + 1 = 2(1+1=2)∧(0+2=3)(1 + 1 = 2) \land (0 + 2 = 3)(0+2=3)→⊥(0 + 2 = 3) \to \bot⊤→⊥\top \to \bot<그렇다면 판단이란 무엇인가? 우리가 명제에 가지는 논리적태도이다. 이 글에서는 다음과 같은 판단만을 이야기 할 것이다.<P trueP\ \texttt{true}, 즉 명제 PP가 참이다.<이를 "진리 판단"("truth judgment")라고 한다. 좀 더엄밀히는 다음과 같이 가정을 포함한 명제에 대해 다룰것이다.Γ⊢Ptrue\Gamma \vdash P \texttt{true}<이 판단은 어떤 진리 판단의 나열 Γ\Gamma을 가정했을 때 명제 PP가참이라고 말하는 판단이다. 이를 "가정적 판단"("hypotheticaljudgement")이라고 한다. 또한 여기서 Γ\Gamma를 "가정"("hypothesis") 혹은"전건"("前件", "antecedent")이라고 하고, PtrueP \texttt{true}를"귀결("consequent") 혹은 "후건"("後件", "succedent")이라고한다. 요약하자면 이 절의 핵심 질문
질문
무엇이 논리적일 수 있는 대상이냐?<에 대한 답은
답
명제의 진리에 대한 가정적 판단이 논리적일 수 있는 대상이다.<진짜 논리적이 되는 방법 1 - 자연 연역(Natural Deduction)
이제 어떤 가정적 판단이 논리적인지 증명하는 한 방법에 대해서알아보자. 우선 PP가 참이라는 판단이 가정 중 하나라면 당연히그 가정 아래에서는 PP가 참이라고 판단할 수 있을 것이다.이를 간략하게 표현한 규칙(rule)이P true∈ΓΓ⊢P truehyp\global\def\tJ#1{#1\ \texttt{true}}\begin{equation}\cfrac{\tJ P \in \Gamma}{\Gamma \vdash \tJ P}\text{hyp}\end{equation}<이다. 이 규칙 표현은 줄 위의 것들을전제(premise)로 줄 밑의 결론(conclusion)을추론(infer)해 낼 수 있음을 말한다. 전제에 쓰여있는 P true∈ΓP\ \texttt{true} \in \Gamma는 P trueP\ \texttt{true}가 가정의 나열 Γ\Gamma에 포함되어 있음을 말한다. 또한 줄 옆에 써져있는"hyp"는 이 추론 규칙(inference rule)의 이름으로서가정(hypothesis)을 사용한다는 것을 나타낸다.
이런 추론 규칙을 명제를 만드는 각각의 방법에 대해 정의할 수 있다.참 명제 ⊤\top에 대해서는 Γ⊢⊤ trueI⊤\global\def\tJ#1{#1\ \texttt{true}}\begin{equation}\cfrac{\ }{\Gamma \vdash \tJ \top}\text{I}\top\end{equation}<라는 규칙을 줄 수 있다. 이 규칙 I⊤\text{I}\top은 어떤Γ\Gamma를 가정하든 참 명제는 참이라고 판단할 수 있다는 규칙이다.여기서 이름의 I\text{I}는 참 명제를 결론에소개(introduce)하는 규칙이라는 뜻이다.대칭적으로 거짓 명제에 대해서는Γ⊢⊥ trueΓ⊢P trueE⊥\global\def\tJ#1{#1\ \texttt{true}}\begin{equation}\cfrac{\Gamma \vdash \tJ \bot}{\Gamma \vdash \tJ P}\text{E}\bot\end{equation}<라는 규칙을 줄 수 있다. 이 규칙 E⊥\text{E}\bot은어떤 가정들 Γ\Gamma로 부터 거짓 명제가 참이라고판단했다면 그 가정들 아래에서는 아무 명제나 참이라고판단할 수 있다는 규칙이다[2]. 여기서 이름의 E\text{E}는우리가 거짓 명제가 참임을 결론으로 가지는 전제에 도달했을 때그 결론을 제거(eliminate)하여 다른 결론에 도달할수 있도록 하는 규칙이라는 뜻이다.
⊤\top과 ⊥\bot을 제외한 명제를 만드는 방법들은 이두 종류의 규칙(I\text{I} 규칙과 E\text{E} 규칙)을모두 가진다. P∧QP \land Q의 경우는 다음과 같다.Γ⊢P trueΓ⊢Q trueΓ⊢P∧Q trueI∧Γ⊢P∧Q trueΓ,P true,Q true⊢R trueΓ⊢R trueE∧\global\def\tJ#1{#1\ \texttt{true}}\begin{equation}\cfrac{\Gamma \vdash \tJ P\qquad\Gamma \vdash \tJ Q}{\Gamma \vdash \tJ{P \land Q}}\text{I}\land\qquad\cfrac{\Gamma \vdash \tJ{P \land Q}\qquad\Gamma, \tJ P, \tJ Q \vdash \tJ R}{\Gamma \vdash \tJ R}\text{E}\land\end{equation}<I∧\text{I}\land는 Γ\Gamma를 가정하여 PP와 QQ 각각이 참이라판단했다면 같은 가정에서 P∧QP \land Q도 참이라고 판단할 수 있다는규칙이다. 반대로 E∧\text{E}\land는 Γ\Gamma를 가정하여P∧QP \land Q이 참이라 판단했고 Γ\Gamma에 더해 P trueP\ \text{true}와Q trueQ\ \text{true}를 가정했을 때 RR이라는 명제가 참이라고 판단할 수 있다면Γ\Gamma만 가정하고도 RR이 참이라고 판단할 수 있다는 뜻이다.P∨QP \lor Q와 P→QP \to Q를 위한 규칙도 나열하면 다음과 같다.Γ⊢P trueΓ⊢P∨Q trueI∨1Γ⊢Q trueΓ⊢P∨Q trueI∨2Γ⊢P∨Q trueΓ,P true⊢R trueΓ,Q true⊢R trueΓ⊢R trueE∨Γ,P true⊢Q trueΓ⊢P→Q trueI→Γ⊢P→Q trueΓ⊢P trueΓ⊢Q trueE→\global\def\tJ#1{#1\ \texttt{true}}\begin{equation}\begin{array}{c}\cfrac{\Gamma \vdash \tJ P}{\Gamma \vdash \tJ{P \lor Q}}\text{I}\lor_1\qquad\cfrac{\Gamma \vdash \tJ Q}{\Gamma \vdash \tJ{P \lor Q}}\text{I}\lor_2\newline\newline\cfrac{\Gamma \vdash \tJ{P \lor Q}\qquad\Gamma, \tJ P \vdash \tJ R\qquad\Gamma, \tJ Q \vdash \tJ R}{\Gamma \vdash \tJ R}\text{E}\lor\newline\newline\newline\cfrac{\Gamma, \tJ P \vdash \tJ Q}{\Gamma \vdash \tJ{P \to Q}}\text{I}\to\qquad\cfrac{\Gamma \vdash \tJ{P \to Q}\qquad\Gamma \vdash \tJ P}{\Gamma \vdash \tJ Q}\text{E}\to\end{array}\end{equation}<여기서 I∨1\text{I}\lor_1과 I∨2\text{I}\lor_2는 PP나 QQ중 하나가 참이라고 판단했다면 P∨QP \lor Q가 참이라고 판단할수 있다는 규칙이며 E∨\text{E}\lor는 P∨QP \lor Q가 참이라고판단할 수 있고 PP가 참이라고 가정하든 QQ가 참이라고가정하든 RR이 참이라고 판단할 수 있다면 그 가정 없이RR이 참이라고 판단할 수 있다는 규칙이다. I→\text{I}\to는PP가 참임을 가정해서 QQ가 참이라고 판단할 수 있다면P→QP \to Q 또한 참이라고 판단할 수 있다는 규칙이며E→\text{E}\to는 P→QP \to Q가 참이라고 판단할 수 있고PP가 참이라고 판단할 수 있다면 QQ가 참이라고 판단할 수있다는 규칙이다. 이렇게 소개 규칙과 제거 규칙의 쌍으로논리적 증명을 하는 방식을 "자연 연역"("naturaldeduction")이라고 한다.
자연 연역으로 단순한 논리적 증명을 하는 방법의 예시를들어보겠다. 어떤 단위 명제 AA, BB, CC에 대해서A→BA \to B와 B→CB \to C가 참이라고 판단했다면A→CA \to C 또한 참이라 판단할 수 있다. 이 증명은 다음과같다. 우선 A→BA \to B 그리고 B→CB \to C와 AA가 참이라고판단했을 때 BB가 참이라고 다음과 같이 판단할 수 있다.A→B true∈(A→B true,B→C true,A true)A→B true,B→C true,A true⊢A→B truehypA true∈(A→B true,B→C true,A true)A→B true,B→C true,A true⊢A truehypA→B true,B→C true,A true⊢B trueE→\global\def\tJ#1{#1\ \texttt{true}}\global\def\MyGamma{\tJ{A \to B}, \tJ{B \to C}, \tJ A}\begin{equation}\begin{array}{c}\cfrac{\cfrac{\tJ{A \to B} \in (\MyGamma)}{\MyGamma \vdash \tJ{A \to B}}\text{hyp}\qquad\cfrac{\tJ A \in (\MyGamma)}{\MyGamma \vdash \tJ A}\text{hyp}}{\MyGamma \vdash \tJ B}\text{E}\to\end{array}\end{equation}<이를 써서 다음과 같이 증명을 끝낼 수 있다.B→C true∈(A→B true,B→C true,A true)A→B true,B→C true,A true⊢B→C truehypA→B true,B→C true,A true⊢B true⏞위의증명A→B true,B→C true,A true⊢C trueE→A→B true,B→C true⊢A→C trueI→\global\def\tJ#1{#1\ \texttt{true}}\global\def\MyGamma{\tJ{A \to B}, \tJ{B \to C}, \tJ A}\begin{equation}\begin{array}{c}\cfrac{\cfrac{\cfrac{\tJ{B \to C} \in (\MyGamma)}{\MyGamma \vdash \tJ{B \to C}}\text{hyp}\qquad\raisebox{-0.65em}{\(\overbrace{\MyGamma \vdash \tJ B}^{위의 증명}\)}}{\MyGamma \vdash \tJ C}\text{E}\to}{\tJ{A \to B}, \tJ{B \to C} \vdash \tJ{A \to C}}\text{I}\to\end{array}\end{equation}<따라서 논리적으로 A→BA \to B 그리고 B→CB \to C가 참임을가정했을 때 A→CA \to C가 참이라고 판단할 수 있다.자연 연역과 함수형 언어
혹자는 위 규칙들에서 미묘한 친숙함을 발견했을지도모른다. 이를 좀 더 구체적으로 살펴보기 위해 →\to의규칙들을 다시 살펴보자.Γ,P true⊢Q trueΓ⊢P→Q trueI→Γ⊢P→Q trueΓ⊢P trueΓ⊢Q trueE→\global\def\tJ#1{#1\ \texttt{true}}\begin{equation}\cfrac{\Gamma, \tJ P \vdash \tJ Q}{\Gamma \vdash \tJ{P \to Q}}\text{I}\to\qquad\cfrac{\Gamma \vdash \tJ{P \to Q}\qquad\Gamma \vdash \tJ P}{\Gamma \vdash \tJ Q}\text{E}\to\end{equation}<여기에 약간의 조작을 가해보자. 우선 Γ\Gamma를단순한 판단의 나열로 취급하는 대신 이름 붙은판단들로 취급하자. 예를 들어 위의 P trueP\ \texttt{true}라는 판단에 xx라는 이름을 붙이면 다음과 같은규칙을 얻는다.Γ,x:P true⊢Q trueΓ⊢P→Q trueI→Γ⊢P→Q trueΓ⊢P trueΓ⊢Q trueE→\global\def\tJ#1{#1\ \texttt{true}}\begin{equation}\cfrac{\Gamma, x {:} \tJ P \vdash \tJ Q}{\Gamma \vdash \tJ{P \to Q}}\text{I}\to\qquad\cfrac{\Gamma \vdash \tJ{P \to Q}\qquad\Gamma \vdash \tJ P}{\Gamma \vdash \tJ Q}\text{E}\to\end{equation}<더욱이 각각의 규칙들에 지금까지의 증명을 나타내는 항들을더해보도록 하겠다. 예를 들어 I→\text{I}\to 규칙에서Γ,x:P true⊢Q true\Gamma, x {:} P\ \texttt{true} \vdash Q\ \texttt{true}가어떤 항 MM으로 나타내지는 증명이라면Γ⊢P→Q true\Gamma \vdash P \to Q\ \texttt{true}의증명은 fun (x:P)⇒M\mathtt{fun}\ (x \mathbin{:} P) \Rightarrow M이라는 항으로 나타내도록 하자.마찬가지로 E→\text{E}\to 규칙에서Γ⊢P→Q true\Gamma \vdash P \to Q\ \texttt{true}가MM, Γ⊢P true\Gamma \vdash P\ \texttt{true}가 NN이라는 항으로나타내진다면 Γ⊢Q true\Gamma \vdash Q\ \texttt{true}의 증명은M NM\ N으로 나타내도록 하자. 이 항들을 판단에 끼워넣으면다음과 같이 규칙을 바꿔 쓸 수 있다.Γ,x:P true⊢M:Q trueΓ⊢fun (x:P)⇒M:P→Q trueI→Γ⊢M:P→Q trueΓ⊢N:P trueΓ⊢M N:Q trueE→\global\def\tJ#1{#1\ \texttt{true}}\begin{equation}\cfrac{\Gamma, x {:} \tJ P \vdash M \mathbin{:} \tJ Q}{\Gamma \vdash \mathtt{fun}\ (x \mathbin{:} P) \Rightarrow M \mathbin{:} \tJ{P \to Q}}\text{I}\to\qquad\cfrac{\Gamma \vdash M \mathbin{:} \tJ{P \to Q}\qquad\Gamma \vdash N \mathbin{:} \tJ P}{\Gamma \vdash M\ N \mathbin{:} \tJ Q}\text{E}\to\end{equation}<이는 (단순한) 함수형 언어의 형 검사 규칙과 동일하다!함수 fun (x : P) => M이 형 P -> Q를 가지는지검사하고 싶을 때는 x : P를 가정한 뒤 M이 형 Q를가지는지 검사하면 된다. 또한 함수 M을 인자 N에적용하는 것이 형 Q를 가지는지 알고 싶다면 함수M이 형 P -> Q를 가질 때 인자 N이 형 P를 가지는지검사하면 된다. 마찬가지 변화를 다음과 같이 모든 추론규칙들에 적용할 수 있다.x:P true∈ΓΓ⊢x:P truehyp Γ⊢unit:⊤ trueI⊤Γ⊢M:⊥ trueΓ⊢case M of {}:P trueE⊥Γ⊢M:P trueΓ⊢N:Q trueΓ⊢(M,N):P∧Q trueI∧Γ⊢M:P∧Q trueΓ,x:P true,y:Q true⊢N:R trueΓ⊢case M of (x,y)⇒N:R trueE∧Γ⊢M:P trueΓ⊢Left M:P∨Q trueI∨1Γ⊢M:Q trueΓ⊢Right M:P∨Q trueI∨2Γ⊢M:P∨Q trueΓ,x1:P true⊢N1:R trueΓ,x2:Q true⊢N2:R trueΓ⊢case M of Left x1⇒N1 ∣ Right x2⇒N2:R trueE∨\global\def\tJ#1{#1\ \texttt{true}}\begin{equation}\begin{array}{c}\cfrac{x{:}\tJ P \in \Gamma}{\Gamma \vdash x \mathbin{:} \tJ P}\text{hyp}\newline\newline\newline\cfrac{\ }{\Gamma \vdash \mathtt{unit} \mathbin{:} \tJ \top}\text{I}\top\qquad\cfrac{\Gamma \vdash M \mathbin{:} \tJ \bot}{\Gamma \vdash \mathtt{case}\ M\ \mathtt{of}\ \{\} \mathbin{:} \tJ P}\text{E}\bot\newline\newline\newline\newline\cfrac{\Gamma \vdash M \mathbin{:} \tJ P\qquad\Gamma \vdash N \mathbin{:} \tJ Q}{\Gamma \vdash (M, N) \mathbin{:} \tJ{P \land Q}}\text{I}\land\newline\newline\cfrac{\Gamma \vdash M \mathbin{:} \tJ{P \land Q}\qquad\Gamma, x {:} \tJ P, y {:} \tJ Q \vdash N {:} \tJ R}{\Gamma \vdash \mathtt{case}\ M\ \mathtt{of}\ (x, y) \Rightarrow N \mathbin{:} \tJ R}\text{E}\land\newline\newline\newline\newline\cfrac{\Gamma \vdash M \mathbin{:} \tJ P}{\Gamma \vdash \mathtt{Left}\ M \mathbin{:} \tJ{P \lor Q}}\text{I}\lor_1\qquad\cfrac{\Gamma \vdash M \mathbin{:} \tJ Q}{\Gamma \vdash \mathtt{Right}\ M \mathbin{:} \tJ{P \lor Q}}\text{I}\lor_2\newline\newline\cfrac{\Gamma \vdash M \mathbin{:} \tJ{P \lor Q}\qquad\Gamma, x_1{:}\tJ P \vdash N_1 \mathbin{:} \tJ R\qquad\Gamma, x_2{:}\tJ Q \vdash N_2 \mathbin{:} \tJ R}{\Gamma \vdash \mathtt{case}\ M\ \mathtt{of}\ \mathtt{Left}\ x_1 \Rightarrow N_1\ |\ \mathtt{Right}\ x_2 \Rightarrow N_2 \mathbin{:} \tJ R}\text{E}\lor\end{array}\end{equation}<⊤\top은 단위(Unit) 자료형에 대응되며 ⊥\bot은 빈자료형에 대응되고 P∧QP \land Q는 P 형과 Q 형의쌍(Pair) 자료형에 대응된다. 같은 방식으로 P∨QP \lor Q는P 형과 Q 형의 합(Sum) 자료형[3]에 대응된다.항에서부터 각각의 추론 규칙이 (I\texttt{I} 규칙의 경우)각 자료형의 생성자(Constructor)나 (E\texttt{E} 규칙의경우) 패턴 맞추기(Pattern Matching)의 형 검사 규칙에대응된다는 것을 볼 수 있을 것이다. 이를 처음 구체화시킨두 사람의 이름을 따 이 대응을 "커리-하워드대응"("Curry-Howard correspondence")이라고부른다. 이 대응이 발견됨으로써 논리적인 사고와프로그래밍 언어의 이해 간에 중요한 연결고리가 생겼고이는 현재에도 프로그래밍 언어의 발전과 논리학의 발전양측에 모두 지대한 영향을 끼치고 있다.
이 대응을 따랐을 때 어떤 판단을 증명한다는 것은그 판단의 형을 가지는 프로그램(Program)을 짜는 것과동일하다. 이를 보다 구체적으로 이해하기 위해 앞서의예시 증명을 다시 반복해보자. 증명의 너비를 줄이기위해 Γ\Gamma를x:A→B true,y:B→C true,z:A truex{:}A \to B\ \texttt{true}, y{:}B \to C\ \texttt{true}, z{:}A\ \texttt{true}대신 사용하겠다.x:A→B true∈ΓΓ⊢x:A→B truehypz:A true∈ΓΓ⊢z:A truehypΓ⊢x z:B trueE→\global\def\tJ#1{#1\ \texttt{true}}\begin{equation}\begin{array}{c}\cfrac{\cfrac{x{:}\tJ{A \to B} \in \Gamma}{\Gamma \vdash x \mathbin{:} \tJ{A \to B}}\text{hyp}\qquad\cfrac{z{:}\tJ A \in \Gamma}{\Gamma \vdash z \mathbin{:} \tJ A}\text{hyp}}{\Gamma \vdash x\ z \mathbin{:} \tJ B}\text{E}\to\end{array}\end{equation}<즉 함수 x : A -> B와 인자 z : A가 있을 때 함수 적용 x z이 B trueB\ \texttt{true}의 증명이다.이어서,y:B→C true∈ΓΓ⊢y:B→C truehypΓ⊢x z:B true⏞위의증명Γ⊢y (x z):C trueE→x:A→B true,y:B→C true⊢fun (z:A)⇒y (x z):A→C trueI→\global\def\tJ#1{#1\ \texttt{true}}\begin{equation}\begin{array}{c}\cfrac{\cfrac{\cfrac{y{:} \tJ{B \to C} \in \Gamma}{\Gamma \vdash y \mathbin{:} \tJ{B \to C}}\text{hyp}\qquad\raisebox{-0.65em}{\(\overbrace{\Gamma \vdash x\ z \mathbin{:} \tJ B}^{위의 증명}\)}}{\Gamma \vdash y\ (x\ z) \mathbin{:} \tJ C}\text{E}\to}{x{:}\tJ{A \to B}, y{:}\tJ{B \to C} \vdash \mathtt{fun}\ (z \mathbin{:} A) \Rightarrow y\ (x\ z) \mathbin{:} \tJ{A \to C}}\text{I}\to\end{array}\end{equation}<따라서 fun (z : A) => y (x z)가 x : A -> B와 y : B -> C가주어졌을 때 A→C trueA \to C\ \texttt{true}의 증명이다.
지금까지 자연 연역에 대해서 알아보았다. 자연 연역은함수형 언어를 쓰는 사람들에게는 어찌보면 매우 친숙할수 있는 증명 방식이다. 그러나 자연 연역을 사용했을 때거짓을 증명할 수 없다는 것을 보이는 것은 쉽지 않다.자연 연역을 처음 도입한 게르하르트 겐첸(Gerhard Gentzen)은같은 논문에서 거짓을 증명할 수 없다는 것을 보다 쉽게보일 수 있는 다른 방식 또한 소개하였는데, 그것이 바로논건 대수(Sequent Calculus)이다.진짜 논리적이 되는 방법 2 - 논건 대수(Sequent Calculus)
논건 대수 또한 명제의 진리에 대한 가정적 판단을 추론 규칙을통해 이끌어낸다는 점은 자연 연역과 동일하다. 자연 연역과논건 대수의 가장 큰 차이점은 명제를 만드는 각 방법에게어떤 식으로 추론 규칙을 부여하는지에 있다. 자연 연역에서는소개 규칙(I\text{I} 규칙)과 제거 규칙(E\text{E} 규칙)이라는분류를 통해 ∧\land, ∨\lor, …\ldots에 추론 규칙을부여했다. 논건 대수의 접근법은 이와는 살짝 다르다.예를 들어 논건 대수에서의 P∧QP \land Q의 규칙에 대해 살펴보자.Γ⊢P trueΓ⊢Q trueΓ⊢P∧Q trueR∧Γ,P true,Q true⊢R trueΓ,P∧Q true⊢R trueL∧\global\def\tJ#1{#1\ \texttt{true}}\begin{equation}\begin{array}{c}\cfrac{\Gamma \vdash \tJ P\qquad\Gamma \vdash \tJ Q}{\Gamma \vdash \tJ{P \land Q}}\text{R}\land\qquad\cfrac{\Gamma, \tJ P, \tJ Q \vdash \tJ R}{\Gamma, \tJ{P \land Q} \vdash \tJ R}\text{L}\land\end{array}\end{equation}<차이점을 눈치챘는가? 크게 두 차이점이 있다.규칙의 이름이 다르다. 😅E∧\text{E}\land을 대체하는 L∧\text{L}\land의 꼴이 다르다.<먼저 이름의 차이를 설명하고 넘어가자. 자연 연역의경우 I∧\text{I}\land 규칙은 ∧\land를 소개(introduce)하는규칙, E∧\text{E}\land 규칙은 ∧\land를 제거(eliminate)하는규칙이었다. 반면에 논건 대수의 R∧\text{R}\land 규칙은∧\land를 오른쪽(Right side)에 소개하는규칙이고 L∧\text{L}\land 규칙은 ∧\land를 왼쪽(Leftside)에 소개하는 규칙이다. E∧\text{E}\land와 L∧\text{L}\land의꼴의 차이는 이 접근법의 차이에서부터 자연스럽게 따라나온 것이다.
명제를 만드는 다른 방법들에 있어서도 논건 대수의 방식을따라서 추론 규칙을 마련해 줄 수 있다. Γ⊢⊤ trueR⊤ Γ,⊥ true⊢P trueL⊥Γ⊢P trueΓ⊢P∨Q trueR∨1Γ⊢Q trueΓ⊢P∨Q trueR∨2Γ,P true⊢R trueΓ,Q true⊢R trueΓ,P∨Q true⊢R trueL∨Γ,P true⊢Q trueΓ⊢P→Q trueR→Γ⊢P trueΓ,Q true⊢R trueΓ,P→Q true⊢R trueL→\global\def\tJ#1{#1\ \texttt{true}}\begin{equation}\begin{array}{c}\cfrac{\ }{\Gamma \vdash \tJ \top}\text{R}\top\qquad\cfrac{\ }{\Gamma, \tJ \bot \vdash \tJ P}\text{L}\bot\newline\newline\newline\cfrac{\Gamma \vdash \tJ P}{\Gamma \vdash \tJ{P \lor Q}}\text{R}\lor_1\qquad\cfrac{\Gamma \vdash \tJ Q}{\Gamma \vdash \tJ{P \lor Q}}\text{R}\lor_2\newline\newline\cfrac{\Gamma, \tJ P \vdash \tJ R\qquad\Gamma, \tJ Q \vdash \tJ R}{\Gamma, \tJ{P \lor Q} \vdash \tJ R}\text{L}\lor\newline\newline\newline\cfrac{\Gamma, \tJ P \vdash \tJ Q}{\Gamma \vdash \tJ{P \to Q}}\text{R}\to\qquad\cfrac{\Gamma \vdash \tJ P\qquad\Gamma, \tJ Q \vdash \tJ R}{\Gamma, \tJ{P \to Q} \vdash \tJ R}\text{L}\to\end{array}\end{equation}<논건 대수가 자연 연역과 동등함을 (비교적) 쉽게보이기 위해서는 명제를 만드는 각 방식의 R\text{R}과L\text{L} 규칙에 더해 다음의 두 규칙을 추가해야한다.P true∈ΓΓ⊢P trueinitΓ⊢P trueΓ,P true⊢Q trueΓ⊢Q truecut\global\def\tJ#1{#1\ \texttt{true}}\begin{equation}\begin{array}{c}\cfrac{\tJ P \in \Gamma}{\Gamma \vdash \tJ P}\text{init}\qquad\cfrac{\Gamma \vdash \tJ P\qquad\Gamma, \tJ P \vdash \tJ Q}{\Gamma \vdash \tJ Q}\text{cut}\end{array}\end{equation}<여기서 init\text{init} 규칙은 자연 연역에서의hyp\text{hyp} 규칙과 같은 꼴이다. 반면에 cut\text{cut}규칙은 직접적으로 비교할만한 자연 연역에서의 규칙이존재하지 않는데, 이는 논건 대수가 자연 연역과 전혀 다른방식으로 증명을 전개하기 때문이다. 자연 연역에서는예를 들어 I∧\text{I}\land 규칙으로 만들어진P∧QP \land Q가 참이라는 판단을 바로 E∧\text{E}\land에사용할 수 있었다. 함수형 언어로 말하자면case (M, N) of (x, y) => L<같은 꼴의 사용이 가능했다. 그러나 논건 대수에서는R∧\text{R}\land 규칙은 가정적 판단의 (오른쪽) 후건에,L∧\text{L}\land 규칙은 가정적 판단의 (왼쪽) 전건에∧\land를 새로 만들어낼 뿐이고 두 규칙이 상호작용할수 있는 방법이 없다. 이를 해결해주는 것이 바로이 cut\text{cut} 규칙이다. 그런데, 과연 이 상호작용은필요한 것인가? 함수형 언어의 예시에서 보다 분명히보이는 것은 저런 식의 I∧\text{I}\land와E∧\text{E}\land 규칙의 연달은 사용이 불필요하다는 것이다.저런 식의 증명 대신 L에서 x가 등장하는 자리에M을 치환해넣고, y가 등장하는 자리에 N을 치환해넣은증명 또한 가능하기 때문이다. 이 직관을 구체화한 것이바로 다음의 cut\text{cut} 제거 정리이다.
정리
cut\text{cut} 제거 정리cut\text{cut}을 사용해 증명 가능한 모든 판단은cut\text{cut}을 사용하지 않고서도 증명할 수 있다.<cut\text{cut} 제거 정리의 의의는 단순히 필요없는 규칙을제거하는 정도에 멈추지 않는다. cut\text{cut}을 제거하고나면 논건 대수에서 가정 없이는 거짓을 증명하지 못한다는 것이자명해지기 때문이다.
정리
cut\text{cut}을 제거한 논건 대수의 일관성cut\text{cut}을 제거한 논건 대수는 판단 ⊢⊥ true\vdash \bot\ \texttt{true}를 증명하지 못한다.<증명은 다음의 네 문장이면 충분하다.귀결이 ⊥\bot인 R\text{R} 규칙이 존재하지 않기 때문에 어떤 R\text{R} 규칙도 쓸 수 없다.가정이 없기 때문에 어떤 L\text{L} 규칙도 쓸 수 없다.마찬가지로 가정이 없기 때문에 init\text{init} 규칙을 쓸 수 없다.따라서 어떤 규칙도 판단 ⊢⊥ true\vdash \bot\ \texttt{true}을 결론으로 주지 않는다.<앞서 이 글의 서두에서 논건 대수의 일관성을 보이기 위해"약간의 부정행위"를 저지를 것이라고 말했다. 오해가 없도록명시하자면 위의 증명은 cut\text{cut}을 제거한논건 대수에 있어서는 문제가 없다. 부정행위라고 부를 만한 부분은바로 cut\text{cut} 제거 정리의 증명이더 어렵다는 점에 있다. 다만 이 어려운 증명도 수학적귀납법(Induction) 이상의 지식은 필요로 하지 않기 때문에,시도해보고자 하는 독자가 있다면 직접 시도해 볼 수 있을 것이다[4].
논건 대수의 소개를 앞서의 예시 증명을 논건 대수에서 반복하는것으로 마치도록 하자. 우선 A→BA \to B와 AA가참이라고 판단했을 때 BB가 참이라고 다음과 같이 판단할 수 있다.A true∈(A true)A true⊢A trueinitB true∈(A true,B true)A true,B true⊢B trueinitA→B true,A true⊢B trueL→\global\def\tJ#1{#1\ \texttt{true}}\begin{equation}\begin{array}{c}\cfrac{\cfrac{\tJ A \in (\tJ A)}{\tJ A \vdash \tJ A}\text{init}\qquad\cfrac{\tJ B \in (\tJ A, \tJ B)}{\tJ A, \tJ B \vdash \tJ B}\text{init}}{\tJ{A \to B}, \tJ A \vdash \tJ B}\text{L}\to\end{array}\end{equation}<이를 써서 다음과 같이 증명을 끝낼 수 있다.A→B true,A true⊢B true⏞위의증명C true∈(A→B true,A true,C true)A→B true,A true,C true⊢C trueinitA→B true,B→C true,A true⊢C trueL→A→B true,B→C true⊢A→C trueR→\global\def\tJ#1{#1\ \texttt{true}}\begin{equation}\begin{array}{c}\cfrac{\cfrac{\raisebox{-0.65em}{\(\overbrace{\tJ{A \to B}, \tJ A \vdash \tJ B}^{위의 증명}\)}\qquad\cfrac{\tJ C \in (\tJ{A \to B}, \tJ A, \tJ C)}{\tJ{A \to B}, \tJ A, \tJ C \vdash \tJ C}\text{init}}{\tJ{A \to B}, \tJ{B \to C}, \tJ A \vdash \tJ C}\text{L}\to}{\tJ{A \to B}, \tJ{B \to C} \vdash \tJ{A \to C}}\text{R}\to\end{array}\end{equation}<앞서의 자연 연역 증명의 구조가 크게 다름에 주의해서논건 대수 증명의 구조를 이해해보도록 하자. 앞서의 자연연역 증명은hyp규칙E규칙↓E규칙↑I규칙결론\begin{array}{c}\texttt{hyp} 규칙 \qquad \phantom{\texttt{E} 규칙}\\\downarrow \qquad \texttt{E} 규칙\\\uparrow \qquad \texttt{I} 규칙\\결론\end{array}<의 구조를 가지고 있다. 즉 결론에 \texttt{I} 규칙을 적용하고어떤 가정에 \texttt{E} 규칙을 적용해서 이 둘이 만나는 지점을찾는 것이 증명의 구조이다. 이와는 다르게 논건 대수의 증명은L규칙init규칙R규칙L규칙↓init규칙↓R규칙결론\begin{array}{c}\phantom{\texttt{L} 규칙} \qquad \texttt{init} 규칙 \qquad \phantom{\texttt{R} 규칙}\\\texttt{L} 규칙 \qquad \downarrow \phantom{\texttt{init} 규칙} \downarrow \qquad \texttt{R} 규칙\\결론\end{array}<와 같이 (여러 개의) init\texttt{init} 규칙에서 시작해서L\texttt{L} 규칙으로 가정, R\texttt{R} 규칙으로귀결을 변경해 결론에 도달할 때까지 차례로 내려오는구조를 가진다. 이런 구조의 차이가 바로 (자연 연역의)hyp\texttt{hyp} 규칙과 (논건 대수의) init\texttt{init}규칙이 (같은 꼴임에도 불구하고) 다른 이름을 가지게 된이유이자 논건 대수의 init\texttt{init} 규칙이 시작점(initial point)에해당하는 이름을 가지게 된 이유이다.논건 대수의 항
논건 대수를 좀 더 컴퓨터 공학적으로 이해할 수 있을까?이를 위해 자연 연역의 경우와 마찬가지로 논건 대수에도 증명에 커리-하워드대응을 통해 항을 주려고 시도할 수 있다. 그러나 앞서 언급한 것처럼 논건 대수증명은 자연 연역의 증명, 그러니까 함수형 언어와 구조가 크게 다르다.따라서 원본 그대로의 논건 대수에 주는 항은 상대적으로 복잡하고다양한 개념들(생산자, 소비자, 소비자를 생산자로 바꾸기, 생산자와소비자가 거래하게 하기, …\ldots)을 요구하고, 결과적으로 이는 컴퓨터공학적으로 직관성 또한 떨어지는 복잡한 항을 만들어 내게 된다. 이어질2 편에서는 논건 대수에 약간의 변형을 가하면 직관적이고 쉽게 이해가가능한 항을 줄 수 있으며, 항이 뜻하는 바가 저수준(low-level) 자료표현(data representation)과 자연스럽게 연결될 수 있음을 설명할 것이다.마치며
2 편의 "논리와 저수준 자료표현" 연작 중 1 편인 이 글에서는 논리적증명을 하는 두 방법과 커리-하워드 대응에 대해서 설명했다. 1 편의내용은 말하자면 2 편의 바탕 및 서두 역할을 하고 있다. 이 내용들이2 편에서 다룰 본격적인 논리와 자료 표현의 관계에 대해 흥미를불러일으켰기를 바라며 이만 마치도록 하겠다.
이 중 두번째 단위 명제는 일반적인 자연수 체계에서거짓이나, 명제의 정의 자체는 명제가 참인지 거짓인지에대해 논하지 않는다는 것을 강조하기 위해 단위 명제에포함하였다. ↩︎
거짓도 참이라면 대체 무엇이 참이 아니겠는가? ↩︎
이는 Rust나 OCaml의 Result 형 혹은 Haskell의Either형과 같은 형이다. ↩︎
증명에 대한 구체적인 질문이 있다면 답글을 남겨주기를바란다. ↩︎
Ailrun (UTC-5/-4)
nope