고차 논리

틀:위키데이터 속성 추적 고차 논리(高次論理, 틀:Llang)는 관계 또는 관계의 관계 등을 지칭하는 변수에 전칭·존재 기호를 가할 수 있는 일련의 논리 체계들이다. 모든 고차 논리는 ω차 논리(ω次論理, 틀:Llang)의 부분 논리 체계로 생각할 수 있다.틀:Rp

정의

문법

$d\in \{2,3,\dots ,\omega \}$가 2 이상의 자연수 또는 가장 작은 무한 극한 순서수 $\omega$라고 하자.

d차 논리(d次論理, 틀:Llang)의 종류(種類, 틀:Llang)와 이들의 차수(次數, 틀:Llang)는 다음과 같다. (편의상 연산의 종류를 다루는 것을 생략하자.)

• $ı$는 0차 종류이다.
• 차수가 각각 $d_1,\dots ,d_n$인 종류 ${\sigma }_1,\dots ,{\sigma }_n$에 대하여, 만약 $\max \{d_1,\dots ,d_n\}+1<d$라면, $({\sigma }_1\cdots {\sigma }_n)$은 $\max \{d_1,\dots ,d_n\}+1$차 종류이다.

d차 논리의 언어는 각 종류의 변수와 상수들로 구성된다. 종류가 $ı$인 변수를 개체 변수(個體變數, 틀:Llang)라고 하며, 종류가 $()$인 변수를 명제 변수(命題變數, 틀:Llang)라고 한다.

d차 논리의 논리식(論理式, 틀:Llang)은 다음과 같다.

• 종류 $({\sigma }_1\cdots {\sigma }_n)$의 변수 또는 상수 $t^{({\sigma }_1\cdots {\sigma }_n)}$ 및 종류가 각각 ${\sigma }_1,\dots ,{\sigma }_n$인 변수 또는 상수 $u_1^{{\sigma }_1},\dots ,u_n^{{\sigma }_n}$에 대하여, $t^{({\sigma }_1\cdots {\sigma }_n)}(u_1^{{\sigma }_1},\dots ,u_n^{{\sigma }_n})$은 논리식이다.
• $d-1$차 미만의 같은 종류 $\sigma$의 두 변수 또는 상수 $t^{\sigma },u^{\sigma }$에 대하여, $t^{\sigma }=u^{\sigma }$는 논리식이다.
• 논리식 $\varphi ,\psi$ 및 변수 $x^{\sigma }$에 대하여,
  • $\mathrm{\neg }\varphi$는 논리식이다.
  • 만약 $\varphi$의 속박 변수가 $\psi$에 등장하지 않으며, $\psi$의 속박 변수가 $\varphi$에 등장하지 않는다면, $\varphi ⟹\psi$는 논리식이다.
  • 만약 $x^{\sigma }$가 $\varphi$의 자유 변수라면, $\mathrm{\forall }{x}^{\sigma }\varphi$는 논리식이다.

여기서 논리식 $\varphi$와 그 속에 등장하는 변수 $x^{\sigma }$에 대하여, 만약 $\varphi$가 $\mathrm{\forall }{x}^{\sigma }$를 포함하지 않는다면, $x^{\sigma }$를 $\varphi$의 자유 변수(自由變數, 틀:Llang)라고 하며, 그렇지 않다면 $x^{\sigma }$를 $\varphi$의 속박 변수(束縛變數, 틀:Llang)라고 한다.

증명 이론

다음과 같은 기호들을 사용하자.

• $\varphi$, $\psi$, $\chi$는 임의의 논리식이다.
• 각 종류 $\sigma$에 대하여, $x^{\sigma }$, $y^{\sigma }$, $z^{\sigma }$, $y_i^{\sigma }$, $z_i^{\sigma }$는 종류 $\sigma$의 변수이다.
• 각 종류 $\sigma$에 대하여, $t^{\sigma }$는 종류 $\sigma$의 변수 또는 상수이다.

d차 논리의 추론 규칙들은 다음과 같다.

• (전건 긍정) $\begin{array}{c}\varphi \varphi ⟹\psi \\ \psi \end{array}$
• (일반화) $\begin{array}{c}\varphi \\ \mathrm{\forall }x\varphi \end{array}$
  • 여기서 $x$는 $\varphi$의 자유 변수이어야 한다.

d차 논리의 공리 기본꼴들은 다음과 같다.

• $\varphi ⟹(\psi ⟹\varphi )$
• $(\varphi ⟹(\psi ⟹\chi ))⟹((\varphi ⟹\psi )⟹(\varphi ⟹\chi ))$
• $(\mathrm{\neg }\varphi ⟹\mathrm{\neg }\psi )⟹(\psi ⟹\varphi )$
• $\mathrm{\forall }{x}^{\sigma }\varphi ⟹\varphi [t^{\sigma }/x^{\sigma }]$
  • 여기서 $x^{\sigma }$는 $\varphi$의 자유 변수이며, $\varphi [t^{\sigma }/x^{\sigma }]$는 $\varphi$에 등장하는 자유 변수 $x^{\sigma }$를 모두 $t^{\sigma }$로 대체하여 얻는 논리식이다. 만약 $t^{\sigma }$가 변수일 경우, $x^{\sigma }$는 $\varphi$의 $\mathrm{\forall }{t}^{\sigma }\cdots$ 꼴의 부분 논리식 속에 등장하지 않아야 한다.
• $\mathrm{\forall }{x}^{\sigma }(\varphi ⟹\psi )⟹(\varphi ⟹\mathrm{\forall }{x}^{\sigma }\psi )$
  • 여기서 $x^{\sigma }$는 $\varphi$에 등장하지 않는 변수이며, $\psi$의 자유 변수이어야 한다.
• (분류 공리 기본꼴) $\mathrm{\exists }{x}^{({\sigma }_1\cdots {\sigma }_n)}\mathrm{\forall }{y}_1^{{\sigma }_1}\cdots \mathrm{\forall }{y}_n^{{\sigma }_n}(x^{({\sigma }_1\cdots {\sigma }_n)}(y_1^{{\sigma }_1},\dots ,y_n^{{\sigma }_n})⟺\varphi )$
  • 여기서 $x^{({\sigma }_1\cdots {\sigma }_n)}$은 $\varphi$의 자유 변수일 수 없다.
• $x^{\sigma }=x^{\sigma }$
• $(x^{\sigma }=y^{\sigma })⟹(z^{(\sigma )}(x^{\sigma })⟹z^{(\sigma )}(y^{\sigma }))$
• (확장 공리) $\mathrm{\forall }{z}_1^{{\sigma }_1}\cdots \mathrm{\forall }{z}_n^{{\sigma }_n}(x^{({\sigma }_1\cdots {\sigma }_n)}(z_1^{{\sigma }_1},\dots ,z_n^{{\sigma }_n})⟺y^{({\sigma }_1\cdots {\sigma }_n)}(z_1^{{\sigma }_1},\dots ,z_n^{{\sigma }_n}))⟹(x^{({\sigma }_1\cdots {\sigma }_n)}=y^{({\sigma }_1\cdots {\sigma }_n)})$

물론 모든 공리는 d차 논리의 유효한 논리식이어야 한다. 예를 들어, 확장 공리는 3차 논리에서부터 사용된다. (다른 공리들은 2차 논리에도 존재한다.)

같이 보기

• 1차 논리