추론 규칙

3. 연역적 추론 규칙

연역적 추론 규칙은 전제가 참일 때 결론이 반드시 참이 되는 추론 규칙이다. 이는 하나 또는 여러 개의 주장들로부터 논리적으로 동등하거나 보다 특수한 주장을 결론짓는 추론 형식의 성립 여부의 타당성을 확인할 수 있다는 것을 내포한다.

수리 논리학에서 추론 규칙은 일반적으로 다음과 같은 표준 형식으로 제시된다.

  전제#1


  전제#2


        '''...'''


  전제#n   


  결론

이 표현은 논리적 도출 과정에서 주어진 전제들이 얻어졌을 때, 지정된 결론 또한 당연하게 받아들일 수 있음을 나타낸다. 간단한 경우, 명제 논리의 ''조건증명''(modus ponens) 규칙은 다음과 같이 표현될 수 있다.

: $A\; \backslash to\; B$

: $\backslash underline\{A\; \backslash quad\; \backslash quad\; \backslash quad\}\backslash ,\backslash !$

: $B\backslash !$

추론 규칙은 종종 메타변수를 사용하는 스키마로 공식화된다.^[2]

증명 체계는 증명을 형성하기 위해 연결된 규칙 집합으로 구성되며, 증명은 ''도출''이라고도 한다. 모든 도출에는 증명되거나 도출된 명제인 하나의 최종 결론만 있다. 도출에서 전제가 충족되지 않으면 도출은 ''가정적'' 명제, 즉 "전제가 참이라면 결론도 참이다"의 증명이 된다.

힐베르트 시스템에서 추론 규칙의 전제와 결론은 단순히 어떤 언어의 공식이며, 보통 메타변수를 사용한다. 표현의 그래픽적인 간결성과 공리와 추론 규칙 간의 구분을 강조하기 위해, 규칙의 수직적 표현 대신 항절 표기법($\backslash vdash$)을 사용한다.

이 표기법에서,

$\backslash begin\{array\}\{c\}$

\text{전제 1} \\

\text{전제 2} \\ \hline

\text{결론}

\end{array}

는 $(\backslash text\{전제\; 1\}),\; (\backslash text\{전제\; 2\})\; \backslash vdash\; (\backslash text\{결론\})$으로 표기된다.

고전적 명제 논리를 위한 형식 언어는 부정(¬), 함의(→), 그리고 명제 기호만을 사용하여 표현될 수 있다. 세 개의 공리 도식과 하나의 추론 규칙 (''모두스 포넨스'')로 구성된 잘 알려진 공리화는 다음과 같다.

(CA1) ⊢ ''A'' → (''B'' → ''A'')


(CA2) ⊢ (''A'' → (''B'' → ''C'')) → ((''A'' → ''B'') → (''A'' → ''C''))


(CA3) ⊢ (¬''A'' → ¬''B'') → (''B'' → ''A'')


(MP) ''A'', ''A'' → ''B'' ⊢ ''B''

고전적 명제 논리에서 연역 정리는 ''A'' ⊢ ''B''이면 그리고 그럴 경우에만 ⊢ ''A'' → ''B''임을 명시한다. 그러나 첫 번째 표기법은 연역을 설명하는데, 이는 문장에서 문장으로 넘어가는 활동인 반면, ''A'' → ''B''는 단순히 논리적 연결사(이 경우 함의)를 사용하여 만들어진 공식이다. (이 경우 ''모두스 포넨스''와 같은) 추론 규칙이 없다면, 연역이나 추론이 없다. 이 점은 루이스 캐롤의 대화 "아킬레스에게 거북이가 한 말"^[3]에서 설명된다.

일부 비고전 논리의 경우, 연역 정리가 성립하지 않는다. 예를 들어, 우카셰비치의 삼값 논리는 다음과 같이 공리화될 수 있다.^[4]

(CA1) ⊢ ''A'' → (''B'' → ''A'')


(LA2) ⊢ (''A'' → ''B'') → ((''B'' → ''C'') → (''A'' → ''C''))


(CA3) ⊢ (¬''A'' → ¬''B'') → (''B'' → ''A'')


(LA4) ⊢ ((''A'' → ¬''A'') → ''A'') → ''A''


(MP) ''A'', ''A'' → ''B'' ⊢ ''B''

이 순서는 공리 2의 변경과 공리 4의 추가를 통해 고전 논리와 다르다. 고전적 연역 정리는 이 논리에 대해 성립하지 않지만, 수정된 형태는 성립한다. 즉, ''A'' ⊢ ''B''이면 그리고 그럴 경우에만 ⊢ ''A'' → (''A'' → ''B'')이다.^[5]

3. 1. 대표적인 연역적 추론 규칙

고전 논리에서 대표적인 추론 규칙은 다음과 같다. (⊢는 추론을 나타내는 메타언어 기호이며, A₀, …, Aₙ₋₁ ⊢ B는 A₀, …, Aₙ₋₁에서 B가 도출됨을 나타낸다.)^[2]

3. 2. 타당한 추론 형식

명제의 형식, 명제의 양과 질, 명사의 위치 및 개수, 이들의 출현 순서는 추론 형식이 타당성을 확보하기 위해 필요한 명제들의 주요한 성분이다.

4. 힐베르트 시스템의 예시

명제 논리를 위한 힐베르트 시스템은 세 개의 공리 도식과 하나의 추론 규칙(조건증명)으로 구성된다.^[2]

(CA1) ⊢ ''A'' → (''B'' → ''A'')

(CA2) ⊢ (''A'' → (''B'' → ''C'')) → ((''A'' → ''B'') → (''A'' → ''C''))

(CA3) ⊢ (¬''A'' → ¬''B'') → (''B'' → ''A'')

(MP) ''A'', ''A'' → ''B'' ⊢ ''B''

이때 ⊢와 →는 각각 연역과 함의를 나타내는 기호로, 고전 명제 논리에서는 서로 일치한다. 연역 정리에 따르면, ''A'' ⊢ ''B''이면 그리고 그럴 경우에만 ⊢ ''A'' → ''B''이다. 그러나 루이스 캐럴의 "아킬레스에게 거북이가 한 말"에서 지적되었듯이,^[3] 추론 규칙이 없다면 연역은 불가능하다.

일부 비고전 논리에서는 연역 정리가 성립하지 않는다. 얀 우카셰비치의 삼값 논리는 다음과 같이 공리화될 수 있다.^[4]

(CA1) ⊢ ''A'' → (''B'' → ''A'')

(LA2) ⊢ (''A'' → ''B'') → ((''B'' → ''C'') → (''A'' → ''C''))

(CA3) ⊢ (¬''A'' → ¬''B'') → (''B'' → ''A'')

(LA4) ⊢ ((''A'' → ¬''A'') → ''A'') → ''A''

(MP) ''A'', ''A'' → ''B'' ⊢ ''B''

이 논리 체계는 고전 논리와 달리 공리 2가 변경되고 공리 4가 추가되었다. 이 경우 고전적 연역 정리는 성립하지 않지만, 수정된 형태(''A'' ⊢ ''B''이면 그리고 그럴 경우에만 ⊢ ''A'' → (''A'' → ''B''))는 성립한다.^[5]

5. 허용 규칙과 도출 가능 규칙

규칙 집합에서 추론 규칙은 ''허용 가능''하거나 ''도출 가능''하다는 의미에서 중복될 수 있다. 도출 가능한 규칙이란 다른 규칙들을 사용하여 그 전제로부터 결론을 도출할 수 있는 규칙이다. 허용 가능한 규칙이란 전제가 참일 때마다 결론이 참인 규칙이다. 모든 도출 가능한 규칙은 허용 가능하다. 그 차이를 이해하기 위해 자연수를 정의하는 다음 규칙 집합을 고려해 보자 (판단 n nat|n은 자연수^영어)

:$\backslash begin\{matrix\}$

\begin{array}{c}\\ \hline{\mathbf{0} \,\,\mathsf{nat}}\end{array} &

\begin{array}{c}{n \,\,\mathsf{nat}} \\ \hline {\mathbf{s(}n\mathbf{)} \,\,\mathsf{nat}} \end{array}

\end{matrix}

첫 번째 규칙은 '''0'''이 자연수임을 나타내고, 두 번째 규칙은 ''n''이 자연수이면 '''s('''''n''''')'''도 자연수임을 나타낸다. 이 증명 시스템에서 자연수의 두 번째 후속자가 자연수임을 보여주는 다음 규칙은 도출 가능하다.

:$\backslash begin\{array\}\{c\}$

{n \,\,\mathsf{nat}} \\ \hline

{\mathbf{s(s(}n\mathbf{))} \,\,\mathsf{nat}}

\end{array}

그 도출은 위의 후속 규칙을 두 번 사용한 합성이다. 0이 아닌 모든 수에 대한 전임자의 존재를 주장하는 다음 규칙은 단순히 허용 가능하다.

:$\backslash begin\{array\}\{c\}$

{\mathbf{s(}n\mathbf{)} \,\,\mathsf{nat}} \\ \hline

{n \,\,\mathsf{nat}}

\end{array}

이는 귀납법으로 증명할 수 있듯이 자연수의 참된 사실이다. (이 규칙이 허용 가능함을 증명하려면 전제의 도출을 가정하고 그것에 대해 귀납하여 n nat|n은 자연수^영어의 도출을 생성한다.) 그러나 그것은 전제의 도출 구조에 의존하기 때문에 도출 가능하지 않다. 이 때문에 도출 가능성은 증명 시스템에 대한 추가에 대해 안정적이지만 허용 가능성은 그렇지 않다. 그 차이를 보기 위해 다음과 같은 무의미한 규칙이 증명 시스템에 추가되었다고 가정해 보자.

:$\backslash begin\{array\}\{c\}\backslash \backslash \backslash hline\; \{\backslash mathbf\{s(-3)\}\; \backslash ,\backslash ,\backslash mathsf\{nat\}\}\; \backslash end\{array\}$

이 새로운 시스템에서 이중 후속 규칙은 여전히 도출 가능하다. 그러나 전임자를 찾는 규칙은 더 이상 허용 가능하지 않다. -3 nat|-3은 자연수^영어를 도출할 방법이 없기 때문이다. 허용 가능성의 취약성은 그것이 증명되는 방식에서 비롯된다. 증명이 전제의 도출 구조에 대해 귀납할 수 있기 때문에 시스템에 대한 확장은 이 증명에 새로운 경우를 추가하며, 더 이상 유지되지 않을 수 있다.

허용 가능한 규칙은 증명 시스템의 정리로 생각할 수 있다.

6. 비연역적 추론 규칙

비연역적 추론에는 귀납 등이 있다.

6. 1. 가추법 (Abduction)

참조

_[1] 서적 Computability and logic https://archive.org/[...] Cambridge University Press
_[2] 서적 Theories of Programming Languages https://books.google[...] Cambridge University Press
_[3] 서적 Logic and Scientific Methods: Volume One of the Tenth International Congress of Logic, Methodology and Philosophy of Science, Florence, August 1995 http://www.mi.sanu.a[...] Springer
_[4] 서적 An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems https://archive.org/[...] Cambridge University Press
_[5] 서적 An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems https://archive.org/[...] Cambridge University Press