힐베르트 시스템 목록

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

이 글에는 제안적 논리를 위한 힐버트식 연역 시스템 샘플 목록이 포함되어 있다.

고전 명제 미적분학 시스템

고전 명제 미적분은 표준 명제 논리학이다.그것의 의도된 의미론은 이분법적이고 그것의 주된 특성은 그것이 강하게 완전하다는 것이다. 그렇지 않으면 공식은 의미론적으로 일련의 전제로부터 의미론적으로 따를 때마다, 그것은 또한 정해진 구문론에서도 따른다고 말한다.많은 동등한 완전한 공리 시스템이 공식화되었다.사용되는 기본 연결 장치의 선택에는 차이가 있으며, 모든 경우 기능적으로 완전해야 하며(즉, 모든 n-ari 진리 표를 구성으로 표현할 수 있어야 함), 선택한 연결 장치에 대한 공리의 정확한 전체 선택에서 차이가 있다.

시사 및 부정

여기서의 공식은 기능적으로 완전한 기본 커넥티브 집합으로$$ 시사 및 부정${\displaystyle }${${\displaystyle }$→ ,${\displaystyle \mathrm{\neg }}$ ${\displaystyle \}}$ ${\displaystyle \{\to ,\neg \}}$을(를) 사용한다.모든 논리 체계는 적어도 하나의 비영원적인 추론 규칙을 요구한다.고전 명제 미적분학에서는 일반적으로 다음과 같은 모더스 폰의 법칙을 사용한다.

$B\vdash B.}$

달리 명시되지 않은 한 이 규칙이 아래의 모든 시스템에 포함되어 있다고 가정한다.

프레지의 ^[1]공리 체계:

$A\to(B\to A)}$

$(A\to(B\to C)\to(A\to C)\to(A\to C))\to(A\to C)}$

$[\displaystyle (A\to B)\to (\neg B\to(\neg B\to (\neg B\to \neg A)}$

$\displaystyle \neg \neg A\to A}$

$\displaystyle A\to \neg \neg A}$

힐버트의 공리 체계:^[1]

$A\to(B\to A)}$

$(A\to(B\to C)\to(A\to C))\to(A\to C)}$

$[\displaystyle (B\to C)\to (A\to B)\to (A\to C)}}$

$A\to(\neg A\to B)}$

$(\displaystyle (A\to B)\to (\neg A\to B)\to B)}$

우카시오비치의 공리 체계:^[1]

• 첫 번째:

  $(A\displaystyle (A\to B)\to (B\to C)\to (A\to C)}}$

  $(\displaystyle(\neg A\to A)\to A}$

  $A\to(\neg A\to B)}$

• 두 번째:

  $[\displaystyle ((A\to B)\to C)\to(\neg A\to C)}$

  $(A\to B)\to C)\to(B\to C)}$

  $(\displaystyle (\neg A\to C)\to ((B\to C)\to (A\to B)\to C)}}$

• 세 번째:

  $A\to(B\to A)}$

  $(A\to(B\to C)\to(A\to C)\to(A\to C))\to(A\to C)}$

  $(\displaystyle (\neg A\to \neg B)\to (B\to A)}$

• 넷째:^{[citation needed]}

  $(A\displaystyle (A\to B)\to (B\to C)\to (A\to C)}}$

  $A\to(\neg A\to B)}$

  $(\displaystyle (\neg A\to B)\to ((B\to A)\to A)}$

우카시오비츠와 타르스키의 공리 체계:^[2]

$[\displaystyle [(A\to (B\to A))]\to[(\neg C\to (D\to \e)\to (D\to F)]\to (E\to F)]to (H\to G)]to]to (H\to G)]to.$

메러디스의 공리 체계:

$#\displaystyle ((A\to B)\to (\neg C\to \neg D)\to (E\to A)\to (D\to A)}}}$

멘델슨의 공리 체계:^[3]

$A\to(B\to A)}$

$(A\to(B\to C)\to(A\to C)\to(A\to C))\to(A\to C)}$

$(\displaystyle(\neg A\to \neg B)\to(\neg A\to B)\to A)}$

러셀의 공리 체계:^[1]

$A\to(B\to A)}$

$(A\displaystyle (A\to B)\to (B\to C)\to (A\to C)}}$

$(A\to(B\to C)\to(A\to C))\to(A\to C)}$

$\displaystyle \neg \neg A\to A}$

$(A\to \neg A)\to \neg A}$

$(A\to \neg B)\to (B\to \neg A)}$

소보키스키의 공리 체계:^[1]

• 첫 번째:

  $\displaystyle \neg A\to (A\to B)}$

  $(\displaystyle A\to(B\to(C\to A))}$

  $(\displaystyle (\neg A\to C)\to ((B\to C)\to (A\to B)\to C)}}$

• 두 번째:

  $(A\to B)\to(\neg B\to(A\to C))}$

  $(\displaystyle A\to(B\to(C\to A))}$

  $(\displaystyle(\neg A\to B)\to(A\to B)\to B)}$

함축성 및 거짓성

부정 대신 고전적 논리도 connectives의 기능적으로$$ 완전한 집합${\displaystyle }${${\displaystyle }$→ ,${\displaystyle \mathrm{\perp }}$ ${\displaystyle \}}$ ${\displaystyle \{\to ,\bot \}}$을 사용하여 공식화할 수 있다.

타르스키-베르나이-Wajsberg 공리 시스템:

$(A\displaystyle (A\to B)\to (B\to C)\to (A\to C)}}$

$A\to(B\to A)}$

$[\displaystyle ((A\to B)\to A)\to A}$

$\displaystyle \bot \to A}$

Church의 공리 체계:

$A\to(B\to A)}$

$(A\to(B\to C)\to(A\to C)\to(A\to C))\to(A\to C)}$

$[\displaystyle(A\to \bot )\to \bot )\to A}$

메러디스의 공리 체계:

• 첫 번째:^[4][5][6]

  $((A\to B)\to (C\to \bot )\to D)\to (E\to A)\to (C\to A)}}$

• 두 번째:^[4]

  $(A\to B)\to(\bot \to C)\to D)\to(D\to A)\to(E\to (F\to A))}}$

부정과 분리

함축성 대신에 고전적 논리도 connectives의 기능적으로$$ 완전한 집합${\displaystyle }${ ${\displaystyle \mathrm{\neg }}$ ,${\displaystyle \vee }$ ${\displaystyle \}}$ ${\displaystyle \{\neg ,\lor \}}$을 사용하여 공식화할 수 있다.이러한 공식은 다음과 같은 추론 규칙을 사용한다.

$A, A, B, Vdash B.$

러셀-버네이즈 공리 시스템:

$\displaystyle \neg (\neg B\lor C)\lor (\neg (A\lor B)\lor (A\lor C))}$

$\displaystyle \neg (A\lor B)\lor (B\lor A)}$

$\displaystyle \neg A\lor (B\lor A)}$

$\displaystyle \neg (A\lor A)\lor A}$

메러디스의 공리 체계:^[7]

• 첫 번째:

  $\displaystyle \neg (\neg (\neg A\lor B)\lor (D\lor E))\lor (\neg D\lor A)\lor (E\lor A))}}$

• 두 번째:

  $\displaystyle \neg (\neg (\neg A\lor B)\lor (D\lor E))\lor (\neg E\lor D)\lor (A\lor D))}}$

• 세 번째:

  $\displaystyle \neg (\neg (\neg A\lor B)\lor (D\lor E))\lor (\neg C\lor A)\lor (D\lor A))}}$

일반적으로 고전적인 명제적 논리는 접속사와 부정만을 사용하여 정의할 수 있다.

셰퍼의 뇌졸중

셰퍼의 뇌졸중(NAND 연산자라고도 함)은 기능적으로 완전하기 때문에 명제 미적분학의 전체 제형을 만드는 데 사용할 수 있다.NAND 공식은 Nicod's modus ponens라고 불리는 추론 규칙을 사용한다.

$A,A,mid (B\mid C)\vdash C.}$

Nicod의 공리 시스템:^[4]

$[\displaystyle (A\mid (B\mid C)]\mid [(E\mid (E\mid E)]\mid ((D\mid B)\mid [(A\mid D)]]]]}$

우카시오비치의 공리 체계:^[4]

• 첫 번째:

  $[\displaystyle (A\mid (B\mid C)]\mid [(D\mid (D)]\mid (D\mid D)\mid [(A\mid D)]]]]}$

• 두 번째:

  $[\displaystyle (A\mid (B\mid C)]\mid [(A\mid (C\mid A)]\mid (D\mid B)\mid [(A\mid D)]]]]}$

Wajsberg의 공리 체계:^[4]

$(A\mid (B\mid C)\mid [(D\mid C)]\mid [(A\mid D)\mid (A\mid D)])\mid (A\mid (A\mid B))]]}$

Argonne 공리 시스템:^[4]

• 첫 번째:

$[\displaystyle (A\mid (B\mid C)]\mid [(A\mid (B\mid C)]\mid ((D\mid C)]\mid [(C\mid D)]]]}$

• 두 번째:

$[\displaystyle (B\mid C)]\mid [[(B\mid D)\mid (A\mid D)]\mid (D\mid B)\mid (C\mid B)\mid (A)]]]]}$^[8]

아르곤느의 컴퓨터 분석 결과 > 60개의 단일 공리계통이 추가로 밝혀져 낸드 명제 미적분학 공식화에 활용할 수 있다.^[6]

내연적 명제 미적분학

내연적 명제 미적분은 함축적 결합만을 인정하는 고전 명제 미적분학의 단편이다.기능적으로는 완전하지 않지만(왜곡과 부정의 표현 능력이 부족하기 때문에) 구문적으로는 완전하다.아래의 관계식 계산은 추론 규칙으로 모드스 폰(modus ponens)을 사용한다.

버네이스-타르스키 공리 체계:^[9]

$A\to(B\to A)}$

$(A\displaystyle (A\to B)\to (B\to C)\to (A\to C)}}$

$[\displaystyle ((A\to B)\to A)\to A}$

우카시오비츠와 타르스키의 공리 체계:

• 첫 번째:^[9]

  $[\displaystyle [(A\to(B\to A))]\to[[(C\to D)\to E]\to[D\to F)]\to G]\to G}$

• 두 번째:^[9]

  $[\displaystyle [(A\to B)\to ((C\to D)\to E)]to[F\to(C\to D)\to (D\to E)]]to [A\to (D\to E)]}}}$

• 세 번째:

  $(A\to B)\to (C\to D)\to (D\to A)\to (C\to A)}$

• 넷째:

  $(A\to B)\to (C\to D)\to (D\to A)\to (E\to (C\to A))}$

우카시오비치의 공리 체계:^[10][9]

$(A\to B)\to C)\to(C\to A)\to(D\to A)}$

직관적 및 중간 논리학

직감적 논리는 고전적 논리의 하위 체계다.일반적으로 (기능적으로 완전한) 기본 커넥티브 집합으로${\displaystyle }${ → ,${\displaystyle ,}$ ,${\displaystyle ,}$ , ${\displaystyle \mathrm{\perp }}$} ${\displaystyle$\{\$to$,\$land$,\$lor$,\$bot$\}}}로 공식화된다.배제된 중간 A∨¬A나 Peirce의 법칙((A→B)→A)이 없기 때문에 구문론적으로 완전하지 않다.→논리 불일치 없이 추가할 수 있는 A.추론 규칙으로서 모드 폰이 있으며, 다음과 같은 공리가 있다.

$A\to(B\to A)}$

$(A\to(B\to C)\to(A\to C)\to(A\to C))\to(A\to C)}$

$(A\displaystyle (A\land B)\to A}$

$(A\playstyle (A\land B)\to B}$

$A\to(B\to(A\land B))}$

$A\to(A\lor B)}$

$B\to (A\lor B)}$

$(A\displaystyle (A\to C)\to ((B\to C)\to (A\lor B)\to C)}}$

$\displaystyle \bot \to A}$

또는 직감적 논리는 {${\displaystyle }$→ ,${\displaystyle \wedge }$ ,${\displaystyle \vee }$ ,${\displaystyle }$¬ }$}$ {\$displaystyle \{\to ,\land$ ,\lor $,\neg \}}$을(를) 기본 연결부 집합으로$$ 사용하여 공리화하여 마지막 공리를 다음으로 대체할 수 있다.

$(A\to \neg A)\to \neg A}$

$\displaystyle \neg A\to (A\to B)}$

중간 로직은 직관적 논리와 고전적 논리 사이에 있다.다음은 몇 가지 중간 로직:

• 얀코프 논리(KC)는 직감적 논리의 연장선상으로, 직감적 공리 체계와 공리(公理^[11])에 의해 공리(公理)가 될 수 있다.

$\displaystyle \neg A\lor \neg A.}$

• 괴델-덤메트 논리(LC)는 공리를^[11] 추가하여 직관적 논리보다 공리화할 수 있다.

$(A\to B)\lor(B\to A)}$

양연성 미적분학

긍정적인 관계적 미적분학은 직관적 논리의 관계적 단편이다.아래의 캘커리는 추론 규칙으로 모드스 폰스를 사용한다.ponens)을 사용한다.

우카시오비치의 공리 체계:

$A\to(B\to A)}$

$(A\to(B\to C)\to(A\to C)\to(A\to C))\to(A\to C)}$

메러디스의 공리 체계:

• 첫 번째:

  $(A\to B)\to ((D\to A)\to (B\to C)\to (A\to C))}$

• 두 번째:

  $A\to(B\to A)}$

  $(A\displaystyle (A\to B)\to (B\to C)\to (A\to C)}$

• 세 번째:

  $[\displaystyle ((A\to B)\to C)\to (D\to (C\to E)\to (B\to E)to)]}$^[12]

힐버트의 공리 체계:

• 첫 번째:

  $(A\to(A\to B)\to(A\to B)\to(A\to B)}$

  $[\displaystyle (B\to C)\to (A\to B)\to (A\to C)}}$

  $(A\to(B\to C)\to(A\to C))\to(A\to C)}$

  $A\to(B\to A)}$

• 두 번째:

  $(A\to(A\to B)\to(A\to B)\to(A\to B)}$

  $(A\displaystyle (A\to B)\to (B\to C)\to (A\to C)}}$

  $A\to(B\to A)}$

• 세 번째:

  $A\to A}$

  $(A\displaystyle (A\to B)\to (B\to C)\to (A\to C)}}$

  $[\displaystyle (B\to C)\to (A\to B)\to (A\to C)}}$

  $(A\to(A\to B)\to(A\to B)\to(A\to B)}$

양의 명제 미적분학

포지티브 명제 미적분학은 (비기능적으로 완전하지 않은) 커넥티비즈$({\displaystyle }$connectives${\displaystyle )\{}$ → ,${\displaystyle \wedge }$, ${\displaystyle \vee }$ ∨ ${\displaystyle \}}$ ${\displaystyle$\{\$to,\land,\lor$\}}}}}만을 사용하는 직관논리의 파편이다$.$ 공리와 함께 포지티브 관계 미적분학에 대해 위에서 언급한 미적분학을 공리학적으로 해석할 수 있다.

$(A\displaystyle (A\land B)\to A}$

$(A\playstyle (A\land B)\to B}$

$A\to(B\to(A\land B))}$

$A\to(A\lor B)}$

$B\to (A\lor B)}$

$(A\displaystyle (A\to C)\to ((B\to C)\to (A\lor B)\to C)}}$

선택적으로, 우리는 또한 결합${\displaystyle }$파운드 $({\displaystyle \leftrightarrow })$와 공리를 포함할 수 있다.

$(A\displaystyle (A\좌우 이동 화살표 B)\to (A\to B)}$

$(A\displaystyle (A\좌우 이동 화살표 B)\to (B\to A)}$

$(A\displaystyle (A\to B)\to (B\to A)\to (A\좌측 화살표 B)}$

Johansson의 최소 논리는 추가적인 공리 스키마 없이 양의 명제 미적분학을 위한 공리 계통들 중 어느 것에 의해서도 공리화될 수 있고, 무효 결합형 $⊥{\displaystyle \bot}$ 로$$언어를 확장시킬 수 있다.또는 공리와 함께 양의 명제 미적분을 확장하여${\displaystyle }${${\displaystyle }$→ ,${\displaystyle \wedge }$, ${\displaystyle \vee }$ ,${\displaystyle }$¬ , ${\displaystyle \mathrm{\neg }}$ ¬ ${\displaystyle \}}$ ${\displaystyle \{\to ,\land ,\lor ,\neg$\}}}의 언어로도 공리화할 수 있다.

$(A\to \neg B)\to (B\to \neg A)}$

또는 공리 쌍

$[\displaystyle (A\to B)\to (\neg B\to(\neg B\to (\neg B\to \neg A)}$

$\displaystyle A\to \neg \neg A}$

부정어가 있는 언어의 직감적 논리는 공리의 쌍에 의해 양의 미적분보다 공리적으로 해석될 수 있다.

$(A\to \neg B)\to (B\to \neg A)}$

$\displaystyle \neg A\to (A\to B)}$

또는 공리^[13] 쌍

$(A\to \neg A)\to \neg A}$

$\displaystyle \neg A\to (A\to B)}$

$\{{\displaystyle }$→ ,${\displaystyle \wedge }$ ,${\displaystyle \vee }$ ,${\displaystyle }$¬ }${\displaystyle \mathrm{}\}}$ ${\displaystyle \{\to ,\land ,\lor ,\neg$\}}라는 언어의 고전적 논리는 공리를 추가하여 양의 명제적 미적분학에서 얻을 수 있다$$.

$(\displaystyle (\neg A\to \neg B)\to (B\to A)}$

또는 공리 쌍

$(A\to \neg B)\to (B\to \neg A)}$

$\displaystyle \neg \neg A\to A}$

피치 미적분은 양의 명제 미적분학을 위한 공리계를 취하고 공리를^[13] 추가한다.

$\displaystyle \neg A\to (A\to B)}$

$\displaystyle A\왼쪽 화살표 \neg \neg A}$

$\displaystyle \neg(A\lor B)\좌우 이동(\neg A\land \neg B)}$

$\displaystyle \neg(A\land B)\좌우타로우(\neg A\lor \neg B)}$

첫 번째와 세 번째 공리는 직관적 논리에서도 유효하다는 점에 유의한다.

등가 미적분학

등가성 미적분은 고전 명제 미적분학의 서브시스템으로 여기서${\displaystyle }$here ${\displaystyle \equiv }$로 표기된 (기능적으로 불완전한) 등가성 결합만 허용한다$.$ 이러한 시스템에 사용되는 추론의 규칙은 다음과 같다.

$A, A, A, Equiv B, Vdash B}$

이세키의 공리 체계:^[14]

$(A\equiv C)\equiv (B\equiv A)\equiv (C\equiv B)}$

$[\displaystyle (A\equiv (B\equiv C))]\equiv ((A\equiv B)\equiv C)}$

Iséki-Arai axiom 시스템:^[15]

$(\displaystyle A\equiv A}$

$[\displaystyle (A\equiv B)\equiv (B\equiv A)}$

$(A\displaystyle (A\equiv B)\equiv ((B\equiv C)\equiv (A\equiv C))}$

아라이의 공리 체계

• 첫 번째:

  $[\displaystyle (A\equiv (B\equiv C))]\equiv ((A\equiv B)\equiv C)}$

  $(A\equiv C)\equiv (B\equiv A)\equiv (C\equiv B)}$

• 두 번째:

  $[\displaystyle (A\equiv B)\equiv (B\equiv A)}$

  $(A\equiv C)\equiv (B\equiv A)\equiv (C\equiv B)}$

우카시오비치의 공리 체계:^[16]

• 첫 번째:

  $(A\displaystyle (A\equiv B)\equiv ((C\equiv B)\equiv (A\equiv C))}$

• 두 번째:

  $(A\displaystyle (A\equiv B)\equiv (A\equiv C)\equiv (C\equiv B)}$

• 세 번째:

  ${\displaystyle (A\equiv B)\equiv ((C\equiv A)\equiv (B\equiv C)}}$

메러디스의 공리 체계:^[16]

• 첫 번째:

  $[\displaystyle ((A\equiv B)\equiv C)\equiv (B\equiv (C\equiv A))}$

• 두 번째:

  $[\displaystyle A\equiv ((B\equiv (A\equiv C))]\equiv (C\equiv B)}}$

• 세 번째:

  $[\displaystyle (A\equiv (B\equiv C))]\equiv (C\equiv (A\equiv B)}$

• 넷째:

  $(A\displaystyle (A\equiv B)\equiv (C\equiv C)\equiv A)}$

• 다섯째:

  $[\displaystyle (A\equiv B)\equiv (C\equiv B)\equiv A)}$

• 여섯 번째:

  $[\displaystyle (A\equiv (B\equiv C))\equiv C)\equiv (B\equiv A)}$

• 일곱 번째:

  $[\displaystyle (A\equiv (B\equiv C))\equiv B)\equiv (C\equiv A)}$

칼만의 ^[16]공리 체계:

$[\displaystyle A\equiv ((B\equiv (C\equiv A))]\equiv (C\equiv B)}}$

Winker의 공리 시스템:^[16]

• 첫 번째:

  $[\displaystyle A\equiv ((B\equiv C)\equiv (A\equiv C)\equiv B)}$

• 두 번째:

  $[\displaystyle A\equiv ((B\equiv C)\equiv ((C\equiv A)\equiv B)]}$

XCB 공리 시스템:^[16]

$[\displaystyle A\equiv ((A\equiv B)\equiv (C\equiv B)\equiv C)}$

참고 항목

• 상존 논리 § 포함 — Hilbert 스타일의 상존 논리에 대한 공리 스키마 목록

참조