직관 논리

논리학에서 **직관 논리**(直觀論理, )는 수학적 직관주의에 근거하여 귀류법을 배척하는 논리 체계이다. 직관 논리에서 참인 모든 명제는 고전적으로도 참이지만 그 역은 일반적으로 성립하지 않는 특징이있다.
이처럼 직관주의 논리학은 이중부정의 일부법칙이 성립하지 않는다.
## 정의
**직관 논리**는 힐베르트 식으로 다음과 같이 서술되는 논리 체계이다.

### [[통사론]]
직관 명제 논리에서, 명제 \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.svg

### 고전 논리와의 관계
직관 논리는 고전 논리의 일부분이다. 직관 논리에서 참인 모든 명제는 고전적으로도 참이지만, 고전적으로 참이지만 직관 논리에서는 증명할 수 없는 명제들이 존재한다. 이러한 명제들은 다음을 들 수 있다.
* (배중률) \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)에 대응한다.
일반적인 위상 공간에 대하여 증명할 수 있는 모든 명제들은 직관 논리에서 참임을 보일 수 있다.

이 밖에도, 양상 논리의 크립키 모형()을 직관 논리에서도 사용할 수 있다.

## 역사
라위트전 브라우어르의 직관주의 수학을 형식화하기 위하여, 아런트 헤이팅이 도입하였다.

## 응용
직관 논리는 일반적인 토포스의 내부 논리()로 등장한다. (표준적인) 집합의 토포스나, 이산 공간 위의 층의 토포스 등에서는 고전 논리가 성립하지만, 예를 들어 이산 공간이 아닌 위상 공간 위의 층의 토포스에서는 고전 논리가 성립하지 않고, 직관 논리를 사용해야만 한다.

## 각주

* 
* 
*(직관주의 논리,한국수학사학회지 = The Korean journal for history of mathematics v.12 no.1 , 1999년, pp.32 - 44 이승온,  김혁수,, 박진원 ,  이병식  )https://scienceon.kisti.re.kr/commons/util/originalView.do?cn=JAKO199911921897668&oCn=JAKO199911921897668&dbt=JAKO&journal=NJOU00294661
*(논리연구14-2(2011)pp.39～75 - 직관주의적 유형론에서의 명제와 판단, 정인교-KRF-2007-327-A00159)http://logicalkorea.com/attach/paper/14-2-ChungIK.pdf

## 외부 링크
* 
* 
* 
* 
* 
* 

## 같이 보기
* 직관주의
* 초직관 논리