직관 논리

논리학에서 **직관 논리**(直觀論理, intuitionistic logic)는 수학적 직관주의에 근거하여 귀류법을 배척하는 논리 체계이다. 직관 논리에서 참인 모든 명제는 고전적으로도 참이지만 그 역은 일반적으로 성립하지 않는 특징이있다. 이처럼 직관주의 논리학은 이중부정의 일부법칙이 성립하지 않는다.
# 정의
**직관 논리**는 힐베르트 식으로 다음과 같이 서술되는 논리 체계이다.
## 통사론
직관 명제 논리에서, 명제 \phi,\chi,\dots로부터 다음과 같은 새 명제들을 구성할 수 있다. * 논리곱 \phi\land\chi. 이는 "\phi이며 또한 \chi"라고 읽는다. * 논리합 \phi\lor\chi. 이는 "\phi이거나 또는 \chi"라고 읽는다. * 함의 \phi\implies\chi. 이는 "만약 \phi이라면 \chi 또한 성립한다"라고 읽는다. * 거짓 \bot. 이는 거짓 명제로 읽는다. 이들로부터 다음과 같은 기호들을 정의한다. * 부정 \lnot\phi는 \phi\implies\bot을 줄인 것이며, "\phi가 아니다"라고 읽는다. * 동치 \phi\iff\chi는 (\phi\implies\chi)\land(\chi\implies\phi)를 줄인 것이며, "\phi와 \chi는 서로 동치이다"라고 읽는다. 직관 술어 논리에서는 명제 논리 연산자 밖에도, 자유 변수 x를 가지는 명제 \phi(x)로부터 다음과 같은 새 명제들을 구성할 수 있다. * (존재 술어) \exists x\colon\phi(x). 이는 "\phi(x)를 성립시키는 x가 존재한다"라고 읽는다. * (보편 술어) \forall x\colon\phi(x). 이는 "모든 x에 대하여, \phi(x)가 성립한다"라고 읽는다.
## 추론
직관 명제 논리의 유일한 추론법은 전건 긍정의 형식이며, 이는 다음과 같다. :\phi,\phi\implies\chi\vdash\chi 직관 술어 논리에서는 다음과 같은 두 변수 일반화 규칙이 추가된다. 여기서, x는 \phi에서 자유 변수가 아닌 변수(한정 변수이거나, 아니면 \phi에 등장하지 않는 변수)이다. * \phi\implies\psi\vdash\phi\implies\forall x\colon\psi * \phi\implies\psi\vdash\phi\implies\exists x\colon\psi
## 공리
직관 명제 논리의 공리들은 다음과 같다. 임의의 명제 \phi,\chi,\psi에 대하여, * (함의 조건의 추가) \vdash\phi \implies (\chi\implies\phi ) * (함의의 분배) \vdash(\phi \implies (\chi \implies \psi )) \implies ((\phi \implies \chi ) \implies (\phi \implies \psi )) * (논리곱의 좌측 제거) \vdash\phi \land \chi \implies \chi * (논리곱의 우측 제거) \vdash\phi \land \chi \implies \phi * (논리곱과 함의 조건의 추가) \vdash\phi \implies (\chi \implies(\phi \land \chi )) * (논리합의 좌측 추가) \vdash\chi \implies \phi \lor \chi * (논리합의 우측 추가) \vdash\phi \implies \phi \lor \chi * (함의 조건들의 논리합) \vdash(\phi \implies \psi ) \implies ((\chi \implies \psi ) \implies (\phi \lor \chi \implies \psi )) * (거짓은 모든 명제를 함의) \vdash\bot \implies \phi 직관 술어 논리에서는 다음 두 공리들이 추가로 성립한다. 여기서 t는 \phi(t)에서 한정 변수가 아닌 변수이다. * (보편 기호의 특수화) \vdash(\forall x\colon\phi(x))\implies\phi(t) * (존재 기호의 추가) \vdash\phi(t)\implies(\exists x\colon\phi(x))
# 성질

## 명제의 격자
주어진 명제 \phi로부터, 고전 명제 논리에서는 \bot,\phi,\lnot\phi,\top 네 개의 명제밖에 정의할 수 없지만, 직관 명제 논리에서는 이로부터 무한한 수의, 서로 동치이지 않는 명제들이 존재한다. 이를 **리에게르-니시무라 사다리**(Rieger–Nishimura ladder)라고 하며, 라디슬라프 스반테 리에게르(Ladislav Svante Rieger)언어=en와 니시무라 이와오언어=en가 정의하였다.
## 고전 논리와의 관계
직관 논리는 고전 논리의 일부분이다. 직관 논리에서 참인 모든 명제는 고전적으로도 참이지만, 고전적으로 참이지만 직관 논리에서는 증명할 수 없는 명제들이 존재한다. 이러한 명제들은 다음을 들 수 있다. * (배중률) \phi\lor\lnot\phi * (이중 부정 삭제) \lnot\lnot\phi\implies\phi * (퍼스의 법칙) \left(\phi\implies\chi)\implies\phi\right)\implies\phi
## 의미론
직관 논리의 경우, 다양한 의미론이 존재한다. 이 가운데 하나로는 다음과 같은 위상수학적 의미론을 생각할 수 있다. 어떤 위상 공간 X에 대하여, 직관 논리를 다음과 같이 해석하자. * 명제는 X의 열린 집합에 대응한다. * 논리합 \phi\lor\chi는 합집합 \phi\cup\chi에 대응한다. * 논리곱 \phi\land\chi는 교집합 \phi\cap\chi에 대응한다. * 함의 \phi\implies\chi는 교집합 \operatorname{int}\left((X\setminus\phi)\cup\chi\right)에 대응한다. 여기서 \operatorname{int}는 집합의 내부이다. * 거짓 \bot은 공집합 \varnothing이다. 이로부터 정의되는 부정과 동치는 다음과 같다. * 부정 \lnot\phi는 여집합의 내부 \operatorname{int}(X\setminus\phi)에 대응한다. * 동치 \phi\iff\chi는 \operatorname{int}\left((\phi\cap\chi)\cup\left(X\setminus(\phi\cup\chi)\right)\right)에 대응한다. 일반적인 위상 공간에 대하여 증명할 수 있는 모든 명제들은 직관 논리에서 참임을 보일 수 있다. 이 밖에도, 양상 논리의 크립키 모형(Kripke model)을 직관 논리에서도 사용할 수 있다.
# 역사
라위트전 브라우어르의 직관주의 수학을 형식화하기 위하여, 아런트 헤이팅이 도입하였다.
# 응용
직관 논리는 일반적인 토포스의 내부 논리(internal logic)로 등장한다.언어=en (표준적인) 집합의 토포스나, 이산 공간 위의 층의 토포스 등에서는 고전 논리가 성립하지만, 예를 들어 이산 공간이 아닌 위상 공간 위의 층의 토포스에서는 고전 논리가 성립하지 않고, 직관 논리를 사용해야만 한다.