시스템 L

이 글은 검증을 위해 인용구가 추가로 필요하다. 신뢰할 수 있는 출처에 인용문을 추가하여 이 기사를 개선할 수 있도록 도와주십시오. 공급되지 않은 재료는 도전하여 제거할 수 있다. 출처 찾기: "시스템 L" – 뉴스 · 신문 · 책 · 학자 · JSTOR (2010년 4월) (이 템플릿 메시지를 제거하는 방법과 시기 알아보기)

시스템 L은 E.J. 렘몬이 개발한 자연 연역 논리학이다.^[1]Suppes의 방법에서 파생된 ^[2]이 방법은 자연적 공제 증빙을 정당화된 단계의 순서로 나타낸다.두 가지 방법 모두 겐첸의 1934/1935년 자연공제 시스템에서 파생된 것으로,^[3] 증명서는 Suppes와 Lemmon의 표 형식이 아닌 나무 다이어그램 형태로 제시되었다.트리 다이어그램 레이아웃은 철학적, 교육적 목적을 위한 장점이 있지만, 표 레이아웃은 실제 적용에 훨씬 더 편리하다.

비슷한 표의 레이아웃은 Kleene에 의해 제시된다.^[4]주된 차이점은 클레네는 선 번호에 대한 주장들의 왼쪽 측면을 줄여서 표현하지 않고, 선례 명제의 전체 목록을 제공하는 대신 의존성을 나타내기 위해 테이블의 왼쪽을 달려가는 막대로 왼쪽을 표시하는 것을 선호한다는 것이다.그러나, 클레네의 버전은 매우 미묘하지만, 변성 이론의 엄격한 틀 안에서 제시된다는 장점이 있는 반면, Suppes와^[2] Lemmon의^[1] 책들은 입문 논리를 가르치기 위한 표의 레이아웃을 응용한 것이다.

연역제도 설명

시스템 L은 평등이 있는 술어 미적분학이므로 그 설명은 일반적인 증명 구문과 맥락별 규칙의 두 부분으로 분리될 수 있다.

일반 증명 구문

증표는 4열과 무제한의 순서가 있는 테이블이다.왼쪽에서 오른쪽으로 열 유지:

1. 양의 정수 집합, 비어 있을 수 있음
2. 양의 정수
3. 올바른 형식의 공식(또는 wff)
4. 숫자 집합(비어 있을 수 있음), 규칙, 그리고 다른 증거에 대한 참조

예를 들면 다음과 같다.

p → q, ¬q ⊢ ¬p [MTT(Modus Tollendo Tollenso Tollens)]
가정수	라인 번호	공식(wff)	사용 중인 라인 및 정당성
1	(1)	p → q	A
2	(2)	¬q	A
3	(3)	p	A (RAA의 경우)
1, 3	(4)	q	1, 3, MPP
1, 2, 3	(5)	Q ∧ qq	2, 4, 4I
1, 2	(6)	¬p	3, 5, RAA
Q.E.D.

두 번째 열에는 줄 번호가 있다.세 번째는 wff를 들고 있는데, 다른 wff에 대한 보조 정보와 함께 네 번째에 있는 규칙에 의해 정당화된다.첫 번째 열은 인용된 규칙을 문맥에 적용하여 결정되는 wff가 가지고 있는 가정들의 선 번호를 나타낸다.모든 유효한 증빙 라인은 인용된 라인의 wff를 전제로, 라인에서의 wff를 결론으로 나열함으로써 시퀀스로 변환할 수 있다.유사하게, 그것들은 선행조건이 접속사인 조건부로 전환될 수 있다.모더스 톨렌스가 위에 있기 때문에 이러한 속편은 종종 증거 위에 나열된다.

동일성이 있는 술어의 미적분법칙

위의 증명은 유효한 증명이지만 증명이 증명의 일반적인 구문에 부합할 필요는 없다.그러나, 속편의 타당성을 보장하기 위해서, 우리는 세심하게 명시된 규칙에 따라야 한다.이 규칙은 발의 규칙(1-10), 술어 규칙(11-14), 평등 규칙(15-16), 대체 규칙(17)의 4개 그룹으로 나눌 수 있다.이들 집단을 순서대로 추가하면 명제 미적분, 술어 미적분, 술어 미적분, 그리고 평등을 가진 술어 미적분, 그리고 평등을 가진 술어 미적분학을 새로운 규칙의 파생을 가능하게 할 수 있다.MTT와 같은 명제 미적분법 규칙 중 일부는 불필요하며 다른 규칙에서 규칙으로 파생될 수 있다.

1. 가정법칙(A): "A"는 어떤 wff도 정당화한다.유일한 가정은 그 자신의 라인 번호뿐이다.
2. Modus Ponendo Ponenso (MPP): 이전에 P→Q와 P를 각각 포함하는 증명에 a와 b가 있었다면, "a,b MPP"는 Q를 정당화한다.가정은 a선과 b선의 집합적인 풀이다.
3. 조건부 증명 규칙(CP) : 제안 P가 있는 라인에 제안 Q가 있는 가정선 b가 있다면, "b,a CP"는 Q→P를 정당화한다.a의 모든 가정은 b를 제외하고 유지된다.
4. 이중 부정의 법칙(DN): "DN"은 증명에서 앞줄에 있는 wff에서 두 개의 부정 기호를 더하거나 빼는 것을 정당화하여 이 규칙을 이중으로 만든다.가정 풀은 인용된 선 중 하나이다.
5. ∧소개서 규칙 (∧I): 제안 P와 Q가 a와 b 라인에 있다면, "a,b iI"는 PqQ를 정당화한다.그 가정들은 결합된 명제들의 집합적인 풀이다.
6. ∧-제거의 규칙(∧E): a라인이 접속사 P∧Q인 경우, 「a ∧E」를 이용하여 P나 Q 중 어느 하나를 결론을 내릴 수 있다.가정은 A의 선이다.∧I와 ∧E는 제안 P가 ∧I와 Q로 결합되고 ∧E와 분리될 때 Q의 가정을 유지하는 것처럼 관여의 단조로움을 허용한다.
7. ∨소개 규칙 (∨I): 제안서 P를 가진 행은 "a ∨I"를 인용하여 P∨Q를 도입할 수 있다.가정은 a의 것이다.
8. ∨-제거의 법칙 (∨E): 분리 P∨Q의 경우, P와 Q를 가정하고 각각에서 결론 R을 분리하면 R을 체결할 수 있다.규칙은 "a,b,c,d,e ∨E"로 인용된다. 여기서 a 라인은 초기 분리 P∨Q를 가지며, b 라인과 d 라인은 각각 P와 Q를 가정하며, c 라인과 e는 각각의 가정 풀에 P와 Q를 갖는 R이다.가정은 R로 끝나는 두 선의 집합 풀에서 P와 Q, b, d의 선을 뺀 것이다.
9. Reducationctio Ad Unlubum(RAA):선상 PpP의 경우, 선상 B의 가정 Q를 인용하여 "b,a RA"를 인용할 수 있으며, 선상 A의 가정으로부터 ¬Q를 도출할 수 있다.
10. 모더스 톨렌스(MTT): a와 b 라인의 제안 P→Q와 ¬Q에 대해서는 ¬P를 도출하기 위해 "a,b MTT"를 인용할 수 있다.가정은 a선과 b선의 가정이다.이것은 위의 다른 규칙에서 증명되었다.
11. 범용 소개(UI$):$ a라인에 있는$$ $R{\displaystyle }$ ${\displaystyle a}$${\displaystyle \mathrm{\{\backslash }}$$displaystyle$ $Ra$$}$의 경우, ${\displaystyle \mathrm{a라인}}$에 있는 가정 중 $어느{\displaystyle }$ 하나에도 ${\displaystyle a}$이라는 용어가 없는$$ 경우, 보편적 정량화를 정당화하기 위한 "UI$"$를 인용할 수 있다$.$가정은 a행의 가정이다.
12. 범용 제거(UE): A 라인에서 ${\displaystyle \mathrm{보편적}}$으로 정량화된 술어${\displaystyle \mathrm{(\forall }}$ x${\displaystyle }$) ${\displaystyle R}$ ${\displaystyle x}$ ${\displaystyle (\forall x)Rx}$에 대해, R $a{\displaystyle }$ ${\displaystyle Ra}$을(를) 정당화하기 위한 "UE"를 인용할 수 있다$.$가정은 a행의 가정이다.UE는 이러한 규칙을 사용하여 정량화된 변수와 자유 변수 사이를 전환할 수 있다는 점에서 UI를 가진 이중성이다.
13. 실존론적 소개(EI): $R$의 ${\displaystyle \mathrm{경우}}$, 온라인상의$$ 술어 R a ${\displaystyle Ra}$에 대해 실존론적 정량화를 정당화하기 위한 "EI"를 인용할 수 있다$.$ (${\displaystyle \mathrm{}x}$ x${\displaystyle }$) ${\displaystyle R}$ ${\displaystyle x}$ ${\displaystystyle$ (\$exist x$)Rx$}.$ 가정은 라인의 그것들이다.
14. 실존적 소거(${\displaystyle \mathrm{EE}}$): a라인에서$$ 실존적으로 정량화된 술어(${\displaystyle }$(${\displaystyle \mathrm{}}$x${\displaystyle }$) R ${\displaystyle x}$ ${\$$displaystyle$ $(\exist$ x$)$$Rx}$에 대해, 우리가 R ${\displaystyle \mathrm{a라인}}$ b라인에서 진실이라고$$ 가정하고 그것을 가지고 p를 c라인에서 도출한다면, P를 정당화하기 위해 "a$,$b,c EE"를 인용할 수 있다.${\displaystyle a}$라는 용어는 결론 P에, b행 또는 a행에서 제외되는 가정에는 표시할 수 없다$$.이러한 이유로 EE와 EI는 이중성에 있으며, R $a{\displaystyle }$ ${\displaystyle Ra}$을(를) 가정할 수 있고$$ EI가 {\$displaystyle a}$라는 용어의 결론을 없앨 것이기 때문에 ($$${\displaystyle x}$ x${\displaystyle }$) ${\displaystyle R}$ ${\displaystyle x}${\$displaystyle$(\$exist$ x$)Rx}$에서 결론을 도출할 수 있다$.$가정은 b를 제외하고 a 라인과 c 라인에서의 가정이다.
15. 평등소개(=I): 어느 시점에서나 $a{\displaystyle }$= ${\displaystyle a=a}$을(를) 도입할 수 있으며, 가정은 전혀 없다.
16. 동등성 제거(=E): $제안{\displaystyle }$a = ${\displaystyle b}$ ${\displaystyle$ a$=b}$ 및 p$$ 라인 a와 b의 경우, P에서 ${\$$displaystyle$ $a$$}$ $용어$를$$b로 $변경$하는 것을 정당화하기 위해 "a,b =E"를 인용할 수 있다$.$가정은 a와 b의 풀이다.
17. Substitution Instance (SI(S)): For a sequent ${\displaystyle P,Q\vdash R}$ proved in proof X and substitution instances of ${\displaystyle P}$ and ${\displaystyle Q}$ on lines a and b, one can cite "a,b SI(S) X" to justify introducing a substitution instance of ${\displaystyle R}$. The assumptions are those of 선 a와 b가정이 없는 파생된 규칙은 정리로서, 가정 없이 언제든지 도입할 수 있다.일부에서는 '시퀀트' 대신 '테오렘'을 위한 'TI(S)'로 언급하고 있다.또한 일부에서는 대체 인스턴스가 필요하지 않은 경우 두 경우 모두 "SI" 또는 "TI"만 인용하는데, 이는 그들의 제안이 참조된 증명의 제안과 정확히 일치하기 때문이다.

예

시퀀스 증명의 예(이 경우 정리):

⊢p ∨ ∨ p
가정수	라인 번호	공식(wff)	사용 중인 라인 및 정당성
1	(1)	¬(p ∨ ¬ ¬ )	A (RAA의 경우)
2	(2)	p	A (RAA의 경우)
2	(3)	(p ∨ ¬ ¬p)	2, ∨I
1, 2	(4)	(p ∨ ¬p) ¬(p ∨ ¬p)	3, 1, ∧I
1	(5)	¬p	2, 4, RAA
1	(6)	(p ∨ ¬ ¬p)	5, ∨I
1	(7)	(p ∨ ¬p) ¬(p ∨ ¬p)	1, 6, ∧I
	(8)	¬¬(p ∨ ¬ ¬ )	1, 7, RAA
	(9)	(p ∨ ¬ ¬p)	8, DN
Q.E.D.

수반의 단조로움을 이용한 폭발 원리의 증명.어떤 사람들은 (마인드)의 법칙 3-6행에서 증명된 다음과 같은 기법을 불렀다.구내 증축:^[5]

p, ¬p q q.
가정수	라인 번호	공식(wff)	사용 중인 라인 및 정당성
1	(1)	p	A (RAA의 경우)
2	(2)	¬p	A (RAA의 경우)
1, 2	(3)	p ∧ ¬ p	1, 2, ∧I
4	(4)	¬q	A(DN의 경우)
1, 2, 4	(5)	(p ∧ ¬p) q qq	3, 4, ∧I
1, 2, 4	(6)	p ∧ ¬ p	5, ∨E
1, 2	(7)	¬¬q	4, 6, RAA
1, 2	(8)	q	7, DN
Q.E.D.

대체 및 andE의 예:

(p ∧ pp) ∨ (q ∧ ∧ )q) r r
가정수	라인 번호	공식(wff)	사용 중인 라인 및 정당성
1	(1)	(p ∧ ¬p) ∨ (q ∧ ¬q)	A
2	(2)	p ∧ ¬ p	A (∨E의 경우)
2	(3)	p	2 ∧E
2	(4)	¬p	2 ∧E
2	(5)	r	3, 4 SI 위 증거 참조
6	(6)	Q ∧ qq	A (∨E의 경우)
6	(7)	q	6 ∧E
6	(8)	¬q	2 ∧E
6	(9)	r	7, 8 SI 위 증거 참조
1	(10)	r	1, 2, 5, 6, 9 ∨E
Q.E.D.

표 자연공제제도의 역사

규칙 기반이며 선 번호별 선행 명제(및 세로 막대 또는 별표 등 관련 방법)를 나타내는 표-레이아웃 자연 공제 시스템의 역사적 발전은 다음과 같은 간행물을 포함한다.

• 1940: 교과서에서 Quine은^[6] Suppes의 1957 라인 번호 표기법을 예상하면서 대괄호 안의 라인 번호에 의한 선행 종속성을 나타냈다.
• 1950: 교과서에서, Quine(1982년, 페이지 241–255)은 각 증명서의 왼쪽에 하나 이상의 별표를 사용하여 의존성을 나타내는 방법을 보여주었다.이것은 클린의 세로 막대에 해당한다. (Quine의 별표 표기법이 1950년 원본에 등장했는지, 이후 판에 추가되었는지는 완전히 확실하지 않다.)
• 1957: Suppes(1999, 페이지 25–150)의 교과서에서 입증된 실제 논리 정리에 대한 소개.이것은 각 선의 왼쪽에 있는 라인 번호에 의한 의존성(즉 선행 제안)을 나타냈다.
• 1963: 스톨(1979, 페이지 183–190, 215–2199)은 자연적 공제 추론 규칙에 기초한 순차적 논리적 원칙 라인의 선행 종속성을 나타내기 위해 일련의 라인 번호를 사용한다.
• 1965: 렘몬(1965)의 교과서 전체는 서피스(Suppes)에 근거한 방법을 이용한 논리증거의 도입이다.
• 1967: 교과서에서 클레네(2002, 페이지 50–58, 128–130)는 두 종류의 실용적인 논리 증거를 간략히 보여주었는데, 하나는 각 행의 왼쪽에 있는 선행 명제의 명시적 인용구를 사용한 것이고, 다른 하나는 의존성을 나타내기 위해 왼쪽의 수직 막대를 사용한 것이다.^[7]

참고 항목

• 자연공제
• 시퀀스 미적분학
• 연역계

메모들

참조

• Gentzen, Gerhard Karl Erich (1934). "Untersuchungen über das logische Schließen. I". Mathematische Zeitschrift. 39 (2): 176–210. doi:10.1007/BF01201353. (영어 번역: Szabo의 논리적 추론에 대한 조사)
• Gentzen, Gerhard Karl Erich (1935). "Untersuchungen über das logische Schließen. II". Mathematische Zeitschrift. 39 (3): 405–431. doi:10.1007/bf01201363.
• Kleene, Stephen Cole (2002) [1967]. Mathematical logic. Mineola, New York: Dover Publications. ISBN 978-0-486-42533-7.
• Lemmon, Edward John (1965). Beginning logic. Thomas Nelson. ISBN 0-17-712040-1.
• Quine, Willard Van Orman (1981) [1940]. Mathematical logic (Revised ed.). Cambridge, Massachusetts: Harvard University Press. ISBN 978-0-674-55451-1.
• Quine, Willard Van Orman (1982) [1950]. Methods of logic (Fourth ed.). Cambridge, Massachusetts: Harvard University Press. ISBN 978-0-674-57176-1.
• Stoll, Robert Roth (1979) [1963]. Set Theory and Logic. Mineola, New York: Dover Publications. ISBN 978-0-486-63829-4.
• Suppes, Patrick Colonel (1999) [1957]. Introduction to logic. Mineola, New York: Dover Publications. ISBN 978-0-486-40687-9.
• Szabo, M.E. (1969). The collected papers of Gerhard Gentzen. Amsterdam: North-Holland.

외부 링크

• 펠레티어, 제프 "자연공제와 초등논리교과서 역사"