추론 규칙

논리학에서, 추론 규칙() 또는 추론 규칙()은 전제를 취하고, 구문을 분석하고, 결론(또는 결론)을 반환하는 함수로 구성된 논리 형식입니다.예를 들어, 모더스 포넨스라고 불리는 추론 규칙은 "If p then q" 형태와 "p" 형태의 두 전제를 취하고, 결론 "q"를 반환합니다.규칙은 (해석 하에서) 전제가 참이라면 결론도 마찬가지라는 점에서 고전 논리의 의미론(및 다른 많은 비고전 논리의 의미론)과 관련하여 유효합니다.

일반적으로 추론 규칙은 의미론적 속성인 진실을 보존합니다.다값 논리에서는 일반적인 명칭을 유지합니다.그러나 추론 규칙의 행동은 순전히 통사적이며 의미론적 특성을 보존할 필요가 없습니다. 공식 집합에서 공식에 이르는 모든 함수는 추론 규칙으로 간주됩니다.일반적으로 재귀적인 규칙만 중요합니다. 즉, 주어진 공식이 규칙에 따라 주어진 공식 집합의 결론인지 여부를 결정하는 효과적인 절차가 있는 규칙입니다.이러한 의미에서 효과적이지 않은 규칙의 예로는 무한 ^[1]ω-rule이 있습니다.

명제 논리에서 일반적인 추론 규칙에는 모드 포넨, 모드 톨렌 및 대위법이 포함됩니다.1차 술어 논리는 논리적 정량자를 다루기 위해 추론 규칙을 사용합니다.

표준형

형식 논리(및 많은 관련 영역)에서 추론 규칙은 일반적으로 다음과 같은 표준 형태로 제공됩니다.

전제#1
전제 #2
...
전제#n
결론

이 표현은 어떤 논리적 파생 과정에서 주어진 전제가 얻어질 때마다 지정된 결론도 당연하게 받아들일 수 있다고 말합니다.전제와 결론을 모두 설명하는 데 사용되는 정확한 공식 언어는 파생어의 실제 맥락에 따라 달라집니다.간단한 경우 다음과 같은 논리식을 사용할 수 있습니다.

스타일 A를 B에 표시

{\style{A\quad \quad \quad }},\!}표시

스타일 B 표시!

이것은 명제 논리의 모더스포넨스 규칙입니다.추론 규칙은 종종 메타 ^[2]변수를 사용하는 스키마로 공식화됩니다.위의 규칙(스키마)에서 메타변수 A와 B는 무한한 추론 규칙 집합을 형성하기 위해 우주의 어떤 요소(또는 때때로, 관례에 의해, 명제와 같은 제한된 부분 집합)로 인스턴스화될 수 있습니다.

증명 시스템은 파생이라고도 하는 증명을 형성하기 위해 체인으로 연결된 일련의 규칙으로 구성됩니다.모든 파생은 오직 하나의 최종 결론, 즉 증명되거나 파생된 진술만 가지고 있습니다.만약 전제가 파생에서 불만족스러운 상태로 남아 있다면, 파생은 가설적인 진술의 증거입니다: "만약 전제가 유지된다면, 결론은 유지됩니다."

예:두 명제 논리에 대한 힐베르트 체계

힐베르트 시스템에서 추론 규칙의 전제와 결론은 일반적으로 메타 변수를 사용하는 일부 언어의 공식입니다.프레젠테이션의 그래픽 간결성과 공리와 추론 규칙의 구별을 강조하기 위해 이 섹션에서는 규칙의 수직적인 표현 대신 순차 표기법 $displaystyle \vdash$ 을 사용합니다.이 표기법에서,

$표시({style{begin{array}{c}{\text{Premise}}1\\{\text{Premise}2\\hline{{text{Conclusion}}\end{array}}}$

는 ( $({\text{Premise }}1),({\text{Premise }}2)\vdash ({\text{Conclusion}})$ 1 $({\text{Premise }}1),({\text{Premise }}2)\vdash ({\text{Conclusion}})$ ( $({\text{Premise }}1),({\text{Premise }}2)\vdash ({\text{Conclusion}})$ 2 $({\text{Premise }}1),({\text{Premise }}2)\vdash ({\text{Conclusion}})$ $({\text{Premise }}1),({\text{Premise }}2)\vdash ({\text{Conclusion}})$ ( $({\text{Premise }}1),({\text{Premise }}2)\vdash ({\text{Conclusion}})$ ) \ $displaystyle ({\text{$ Premise $}}1$ ), ({\ $text{$ Premise $}}2)\vdash ({\text{Conclusion}})}$ 로 $({\text{Premise }}1),({\text{Premise }}2)\vdash ({\text{Conclusion}})$ 작성됩니다 $({\text{Premise }}1),({\text{Premise }}2)\vdash ({\text{Conclusion}})$

고전적인 명제 논리의 형식 언어는 부정(부정), 함축(→) 및 명제 기호를 사용하여 표현할 수 있습니다.세 개의 공리 도식과 하나의 추론 규칙(모드 포넨)으로 구성된 잘 알려진 공리화는 다음과 같습니다.

(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]이라는 대화뿐만 아니라, 이후 대화에서 소개된 역설을 해결하기 위한 버트런드 러셀과 피터 윈치의 시도에 잘 나타나 있습니다.

일부 비고전 논리학의 경우, 공제 정리가 성립하지 않습니다.예를 들어, 우카시에비치의 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 → (A → B)^[5]인 경우에만 적용됩니다.

허용성 및 파생성

일련의 규칙에서 추론 규칙은 허용되거나 파생될 수 있다는 점에서 중복될 수 있습니다.파생 규칙은 다른 규칙을 사용하여 전제로부터 결론을 도출할 수 있는 규칙입니다.허용되는 규칙은 전제가 유지될 때마다 결론이 유지되는 규칙입니다.파생 가능한 모든 규칙은 허용됩니다.차이를 이해하려면 자연수를 정의하기 위한 다음 규칙 집합을 고려하십시오({{ $displaystyle$ n $\,\,{\mathsf {nat}}$ 에서 $n\,\,\mathsf{nat}$ $n$ $n\,\,{\mathsf {nat}}$ $n\,\,{\mathsf {nat}}$ 은자연수라는 $n$ 을 주장합니다).

표시({style}{\mathbf{array}{c}\\hline{mathbf{0}\,\,{\mathsf{nat}}}&{\math{array}{c}{n\,\mathbf{nat}}}\\hline{mathbf{nat}}\,\mathsf{nat}\}\end{{{}}}}}{{{{}}}}{{{{{{{}}}}}}}}{{{{}}}}}}{{{

첫 번째 규칙은 0이 자연수이고, 두 번째 규칙은 n이 자연수이면 s(n)가 자연수라고 말합니다.이 증명 시스템에서, 자연수의 두 번째 계승자 역시 자연수임을 증명하는 다음의 규칙은 도출 가능합니다.

{\style{array}{c}{n\,\,{\mathsf{nat}}}\\hline{mathbf{s(s)n\mathbf{nat}}\,\,{\mathsf{nat}}}\end{array}}}를 표시합니다.

그것의 파생은 위의 후속 규칙의 두 가지 용도의 구성입니다.0이 아닌 숫자에 대한 선행자의 존재를 주장하는 다음 규칙은 단지 허용될 뿐입니다.

표시({style{\mathbf{array}{c}{\mathbf{s(} n\mathbf{nat}}) \,\,{\mathsf{nat}}}\\\hline{n\,{\mathsf{nat}}}\end{array}}}}}

이것은 유도에 의해 증명될 수 있듯이 자연수의 사실입니다.(이 규칙이 허용 가능하다는 것을 증명하기 위해, 전제의 유도를 가정하고 $n\,\,{\mathsf {nat}}$ 의 $n\,\,{\mathsf {nat}}$ 를 생성하기 위해 $n\,\,{\mathsf {nat}}$ n을 유도합니다. {{ $displaystyle$ n $\,\,{\mathsf {nat}}}.)$ 그러나 이것은 전제의 유도 구조에 의존하기 때문에 유도할 수 없습니다.이 때문에, 증명 시스템에 추가된 파생성은 안정적인 반면, 허용성은 그렇지 않습니다.차이를 확인하기 위해 다음과 같은 넌센스 규칙이 증명 시스템에 추가되었다고 가정합니다.

{\style{array}{c}\\hline{mathbf{s}} \,\,{\mathsf{nat}}\end{array}} 표시

이 새로운 시스템에서, 이중 승계 규칙은 여전히 도출 가능합니다.그러나 이전을 찾기 위한 규칙은 더 이상 허용되지 않습니다. 왜냐하면 $\displaystyle$ \ $mathbf {-3} \,\,{\mathsf$ {nat $\mathbf {-3} \,\,{\mathsf {nat}}$ 에서 $\mathbf {-3} \,\,{\mathsf {nat}}$ 을 도출할 방법이 없기 때문입니다.허용성의 취약성은 증명된 방식에서 비롯됩니다. 증명이 전제의 파생 구조를 유도할 수 있기 때문에 시스템 확장은 이 증명에 새로운 사례를 추가하며, 이는 더 이상 유지되지 않을 수 있습니다.

허용되는 규칙은 증명 시스템의 정리로 생각할 수 있습니다.예를 들어, 절단 제거가 유지되는 순차 미적분에서는 절단 규칙이 허용됩니다.

참고 항목

레퍼런스

^ Boolos, George; Burgess, John; Jeffrey, Richard C. (2007). Computability and logic. Cambridge: Cambridge University Press. p. 364. ISBN 978-0-521-87752-7.
^ John C. Reynolds (2009) [1998]. Theories of Programming Languages. Cambridge University Press. p. 12. ISBN 978-0-521-10697-9.
^ Kosta Dosen (1996). "Logical consequence: a turn in style". In Maria Luisa Dalla Chiara; Kees Doets; Daniele Mundici; Johan van Benthem (eds.). Logic and Scientific Methods: Volume One of the Tenth International Congress of Logic, Methodology and Philosophy of Science, Florence, August 1995. Springer. p. 290. ISBN 978-0-7923-4383-7. 미리 인쇄(다른 페이지 사용)
^ Bergmann, Merrie (2008). An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems. Cambridge University Press. p. 100. ISBN 978-0-521-88128-9.
^ Bergmann, Merrie (2008). An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems. Cambridge University Press. p. 114. ISBN 978-0-521-88128-9.

[1] Boolos, George; Burgess, John; Jeffrey, Richard C. (2007). Computability and logic. Cambridge: Cambridge University Press. p. 364. ISBN 978-0-521-87752-7.

[Reynolds2009-2] John C. Reynolds (2009) [1998]. Theories of Programming Languages. Cambridge University Press. p. 12. ISBN 978-0-521-10697-9.

[ChiaraDoets1996-3] Kosta Dosen (1996). "Logical consequence: a turn in style". In Maria Luisa Dalla Chiara; Kees Doets; Daniele Mundici; Johan van Benthem (eds.). Logic and Scientific Methods: Volume One of the Tenth International Congress of Logic, Methodology and Philosophy of Science, Florence, August 1995. Springer. p. 290. ISBN 978-0-7923-4383-7. 미리 인쇄(다른 페이지 사용)

[4] Bergmann, Merrie (2008). An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems. Cambridge University Press. p. 100. ISBN 978-0-521-88128-9.

[5] Bergmann, Merrie (2008). An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems. Cambridge University Press. p. 114. ISBN 978-0-521-88128-9.

[1]

[2]

[3]

[4]

[5]

Search

추론 규칙

네임스페이스

더

목차

표준형

예:두 명제 논리에 대한 힐베르트 체계

허용성 및 파생성

참고 항목

레퍼런스