고차 논리

고차 논리(高次論理, 영어: higher-order logic)는 관계 또는 관계의 관계 등을 지칭하는 변수에 전칭·존재 기호를 가할 수 있는 일련의 논리 체계들이다. 모든 고차 논리는 ω차 논리(ω次論理, 영어: ω-order logic)의 부분 논리 체계로 생각할 수 있다.^{:Chapter 5, §50}

정의

문법

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

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

• $\imath$는 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차 논리의 언어는 각 종류의 변수와 상수들로 구성된다. 종류가 $\imath$인 변수를 개체 변수(個體變數, 영어: individual variable)라고 하며, 종류가 $()$인 변수를 명제 변수(命題變數, 영어: propositional variable)라고 한다.

d차 논리의 논리식(論理式, 영어: (well-formed) formula)은 다음과 같다.

• 종류 $(\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 }$는 논리식이다.
• 논리식 $\phi ,\psi$ 및 변수 $x^{\sigma }$에 대하여,
  • $\lnot \phi$는 논리식이다.
  • 만약 $\phi$의 속박 변수가 $\psi$에 등장하지 않으며, $\psi$의 속박 변수가 $\phi$에 등장하지 않는다면, $\phi \implies \psi$는 논리식이다.
  • 만약 $x^{\sigma }$가 $\phi$의 자유 변수라면, $\forall x^{\sigma }\phi$는 논리식이다.

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

증명 이론

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

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

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

• (전건 긍정) ${\begin{matrix}\phi \qquad \phi \implies \psi \\\hline \psi \end{matrix}}$
• (일반화) ${\begin{matrix}\phi \\\hline \forall x\phi \end{matrix}}$
  • 여기서 $x$는 $\phi$의 자유 변수이어야 한다.

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

• $\phi \implies (\psi \implies \phi )$
• $(\phi \implies (\psi \implies \chi ))\implies ((\phi \implies \psi )\implies (\phi \implies \chi ))$
• $(\lnot \phi \implies \lnot \psi )\implies (\psi \implies \phi )$
• $\forall x^{\sigma }\phi \implies \phi [t^{\sigma }/x^{\sigma }]$
  • 여기서 $x^{\sigma }$는 $\phi$의 자유 변수이며, $\phi [t^{\sigma }/x^{\sigma }]$는 $\phi$에 등장하는 자유 변수 $x^{\sigma }$를 모두 $t^{\sigma }$로 대체하여 얻는 논리식이다. 만약 $t^{\sigma }$가 변수일 경우, $x^{\sigma }$는 $\phi$의 $\forall t^{\sigma }\cdots$ 꼴의 부분 논리식 속에 등장하지 않아야 한다.
• $\forall x^{\sigma }(\phi \implies \psi )\implies (\phi \implies \forall x^{\sigma }\psi )$
  • 여기서 $x^{\sigma }$는 $\phi$에 등장하지 않는 변수이며, $\psi$의 자유 변수이어야 한다.
• (분류 공리 기본꼴) $\exists x^{(\sigma _{1}\cdots \sigma _{n})}\forall y_{1}^{\sigma _{1}}\cdots \forall y_{n}^{\sigma _{n}}(x^{(\sigma _{1}\cdots \sigma _{n})}(y_{1}^{\sigma _{1}},\dots ,y_{n}^{\sigma _{n}})\iff \phi )$
  • 여기서 $x^{(\sigma _{1}\cdots \sigma _{n})}$은 $\phi$의 자유 변수일 수 없다.
• $x^{\sigma }=x^{\sigma }$
• $(x^{\sigma }=y^{\sigma })\implies (z^{(\sigma )}(x^{\sigma })\implies z^{(\sigma )}(y^{\sigma }))$
• (확장 공리) $\forall z_{1}^{\sigma _{1}}\cdots \forall z_{n}^{\sigma _{n}}(x^{(\sigma _{1}\cdots \sigma _{n})}(z_{1}^{\sigma _{1}},\dots ,z_{n}^{\sigma _{n}})\iff y^{(\sigma _{1}\cdots \sigma _{n})}(z_{1}^{\sigma _{1}},\dots ,z_{n}^{\sigma _{n}}))\implies (x^{(\sigma _{1}\cdots \sigma _{n})}=y^{(\sigma _{1}\cdots \sigma _{n})})$

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

같이 보기

• 1차 논리