직관 논리

"오늘의AI위키"는 AI 기술로 일관성 있고 체계적인 최신 지식을 제공하는 혁신 플랫폼입니다.
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.

1. 개요

직관 논리는 힐베르트 스타일 계산법으로 서술되는 논리 체계로, 아런트 헤이팅에 의해 도입되었다. 명제 논리, 술어 논리 등 다양한 형태를 가지며, 고전 논리와는 달리 배중률을 부정하여 비구성적인 귀류법의 사용을 무효화한다. 직관 논리는 고전 논리의 부분 집합이며, 위상수학적 의미론, 크립키 모형 등 다양한 의미론을 갖는다. 수학의 구성주의, 토포스 이론, 전산학 분야 등 다양한 분야에 응용되며, 최소 논리, 중간 논리, 다치 논리, 양상 논리 등과 관련이 있다.

더 읽어볼만한 페이지

직관 논리 - 에밀 보렐
프랑스의 수학자이자 정치인인 에밀 보렐은 측도론과 확률론에 기여하고 보렐 집합 개념으로 알려져 있으며, 무한 원숭이 정리와 같은 사고 실험과 게임 이론 연구, 프랑스 하원 의원 및 해군부 장관 역임, 레지스탕스 운동 참여, 파리 통계 연구소 및 앙리 푸앵카레 연구소 설립 기여 등으로 다양한 업적을 남겼다.
직관 논리 - 쌍조건문 도입
쌍조건문 도입은 두 논리식 간의 함의 관계를 통해 동치를 추론하는 추론 규칙으로, 직관 논리 및 모든 초직관 논리에서 성립한다.

직관 논리
개요
유형	수리 논리학, 철학, 형식주의
분야	논리학, 구성주의, 수학, 컴퓨터 과학
발달	1907-1908년, 라우베르트 브라우어르
논리 연산
논리곱 (∧)	p ∧ q 는 p와 q가 모두 참일 때만 참이다.
논리합 (∨)	p ∨ q 는 p 또는 q, 또는 둘 다 참일 때 참이다.
함의 (→)	p → q 는 p가 참이면 q도 참이다.
부정 (¬)	¬p 는 p가 참이 아님을 의미한다.
특징
법칙	배중률 거부 이중 부정 제거 거부
관계	고전 논리의 제한된 형태
의미론	BHK 해석
기타
관련 항목	직관주의 구성주의 수학 헤이팅 대수 크리스프케 의미론 선형 논리 양자 논리

2. 정의

'''직관 논리'''는 힐베르트식 계산으로 서술되는 논리 체계이다.

직관주의 논리의 논리식 구문은 고전 명제 논리나 고전 술어 논리와 유사하다. 그러나 직관주의적인 논리 결합자는 고전 논리에서처럼 다른 논리 결합자를 사용하여 정의할 수 없다. 직관주의 명제 논리에서는 $\to,\wedge,\vee,\bot$ 를 기본적인 결합자로 사용하며, $\neg A$ 는 $A \to \bot$ 의 생략형으로 취급한다. 직관주의 술어 논리에서는 여기에 양화 기호 $\exists,\forall$ 를 더한다.

배중률 $p\vee \neg p$ , 퍼스의 법칙 $((p\to q)\to p)\to p$ , 이중 부정 제거 $\neg\neg p \to p$ 등 많은 고전 논리의 항진식은 직관주의적으로 증명할 수 없다. 고전 논리에서는 이중 부정 도입 $p \to \neg\neg p$ 와 이중 부정 제거가 모두 정리이지만, 직관주의 논리에서는 이중 부정 도입만이 유일한 정리이다. 삼중 부정 제거 $\neg\neg\neg p \to \neg p$ 는 직관주의 논리에서 정리이다.

직관주의 논리는 힐베르트식 계산을 사용하여 정의할 수 있으며, 이는 고전 명제 논리의 공리화와 유사하다. 명제 논리에서는 모드스 포넨스를 추론 규칙으로 사용하고, 다음 공리 도식을 사용한다.

공리
$\phi \to (\chi \to \phi )$ (THEN-1)
$(\phi \to (\chi \to \psi )) \to ((\phi \to \chi ) \to (\phi \to \psi ))$ (THEN-2)
$\phi \land \chi \to \phi$ (AND-1)
$\phi \land \chi \to \chi$ (AND-2)
$\phi \to (\chi \to (\phi \land \chi ))$ (AND-3)
$\phi \to \phi \lor \chi$ (OR-1)
$\chi \to \phi \lor \chi$ (OR-2)
$(\phi \to \psi ) \to ((\chi \to \psi ) \to (\phi \lor \chi \to \psi ))$ (OR-3)
$\bot \to \phi$ (FALSE)

1차 술어 논리의 체계를 만들기 위해서는 일반화 규칙을 추가한다.

$\forall$ -GEN: $\psi \to \phi$ 로부터 $\psi \to (\forall x \ \phi )$ 를 유도한다. (단, $x$ 는 $\psi$ 에 자유롭게 나타나지 않는다.)
$\exists$ -GEN: $\phi \to \psi$ 로부터 $(\exists x \ \phi ) \to \psi$ 를 유도한다. (단, $x$ 는 $\psi$ 에 자유롭게 나타나지 않는다.)

또한 다음 공리 도식을 추가한다.

PRED-1: $(\forall x \ \phi (x)) \to \phi (t)$ (단, 항 ''t''는 $\phi$ 안에서 ''x''로의 대입에 대해 자유롭다.)
PRED-2: $\phi (t) \to (\exists x \ \phi (x))$ (단, PRED-1과 유사한 조건을 만족한다.)

2. 1. 통사론

직관 명제 논리에서, 명제

\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)$ 가 성립한다"라고 읽는다.

직관 논리 공식의 구문론은 명제 논리 또는 일차 논리와 유사하다. 그러나 직관적 논리 연산자는 고전 논리에서처럼 서로를 통해 정의될 수 없으므로 선택이 중요하다. 직관적 명제 논리(IPL)에서는 →, ∧, ∨, ⊥를 기본 연산자로 사용하는 것이 일반적이며, ¬''A''는 (''A'' → ⊥)의 약어로 취급된다. 직관적 일차 논리에서는 양화사 ∃, ∀ 둘 다 필요하다.

만약

\phi \to \bot

의 약어로 간주하기보다는 부정에 대한 연결사

\neg

를 포함시키고 싶다면 다음과 같이 하면 된다.

NOT-1': $(\phi \to \bot) \to \neg \phi$
NOT-2': $\neg \phi \to (\phi \to \bot)$

연결사

\bot

(거짓)을 생략하고 싶다면 여러 대안이 있다. 예를 들어, 세 개의 공리 FALSE, NOT-1', NOT-2'를 두 개의 공리로 대체할 수 있다.

NOT-1: $(\phi \to \chi) \to \big((\phi \to \neg \chi) \to \neg \phi \big)$
NOT-2: $\chi \to (\neg \chi \to \psi)$

공리에서와 같다. NOT-1의 대안으로는

(\phi \to \neg \chi) \to (\chi \to \neg \phi)

또는

(\phi \to \neg \phi) \to \neg \phi

가 있다.

동치에 대한 연결사

\leftrightarrow

는

\phi \leftrightarrow \chi

가

(\phi \to \chi) \land (\chi \to \phi)

를 의미하는 약어로 취급될 수 있다. 또는 다음과 같은 공리를 추가할 수도 있다.

IFF-1: $(\phi \leftrightarrow \chi) \to (\phi \to \chi)$
IFF-2: $(\phi \leftrightarrow \chi) \to (\chi \to \phi)$
IFF-3: $(\phi \to \chi) \to ((\chi \to \phi) \to (\phi \leftrightarrow \chi))$

필요하다면, IFF-1과 IFF-2를 결합하여 단일 공리

(\phi \leftrightarrow \chi) \to ((\phi \to \chi) \land (\chi \to \phi))

로 만들 수 있다.

이미 최소 논리는 다음과 같은 정리를 쉽게 증명하며, 결합과 분리를 조건문과 부정과 관련시킨다.

:

(\phi \lor \psi) \to \neg (\neg \phi \land \neg \psi)

:

(\phi \lor \psi) \to (\neg \phi \to \neg \neg \psi)

, 분리 삼단 논법의 약화된 변형

또는

:

(\phi \land \psi) \to \neg (\neg \phi \lor \neg \psi)

:

(\phi \land \psi) \to \neg (\phi \to \neg \psi)

그리고 유사하게

(\phi \to \psi) \to \neg (\phi \land \neg \psi)

실제로, 이들의 더 강력한 변형도 여전히 유효하다. 그러나 이 다섯 개의 함축 중 어느 것도 배제된 중간 (중간자)를 즉시 함축하지 않고서는 반전될 수 없다. 따라서, 좌변은 우변의 가능한 정의를 구성하지 않는다.

반대로, 고전 명제 논리에서는 이 세 개의 연결사 중 하나와 부정을 기본으로 취하여 다른 두 개를 그에 따라 정의할 수 있다. 예를 들어, 우카시에비츠의 명제 논리의 세 가지 공리에서 이와 같이 수행된다.

심지어 단독 충분 연산자인 피어스 화살표 (NOR) 또는 셰퍼 획 (NAND)의 관점에서 모두 정의하는 것도 가능합니다. 마찬가지로, 고전 일차 논리에서는 한정자를 다른 한정자와 부정의 관점에서 정의할 수 있다.

이들은 기본적으로 양가 원리의 결과이며, 이는 이러한 모든 연결사를 단순히 불 대수 함수로 만든다. 직관 논리에서는 양가 원리가 적용될 필요가 없다. 결과적으로 기본 연결사 중 어느 것도 생략할 수 없으며, 위의 공리는 모두 필요하다. 따라서 연결사와 한정자 사이의 대부분의 고전적 동일성은 한 방향으로만 직관 논리의 정리이다.

명제

\varphi

에서

x

가 자유롭지 않다면,

:

\big(\exists x\, (\phi(x) \to \varphi) \big) \,\, \to \,\, \Big(\big(\forall x \ \phi(x) \big) \to \varphi \Big)

담론 영역이 비어 있다면, 모순율에 의해, 존재 명제는 무엇이든 함축한다. 영역에 최소한 하나의 항이 포함되어 있다면,

\forall x \, \phi(x)

에 대해 배중률을 가정할 때, 위의 함축의 역도 증명 가능하게 되며, 이는 두 변이 동일하게 된다는 의미이다. 이 역방향은 술꾼의 역설 (DP)과 동일하다. 더욱이, 그 존재적이고 이중적인 변형은 전제 독립성 원리(IP)에 의해 주어집니다.

원래의 함축에 대한 거짓 명제

\varphi

를 고려하면 중요한 결과가 발생한다.

$(\exists x \ \neg \phi(x)) \to \neg (\forall x \ \phi(x))$

말: "속성

\phi

를 '가지지 않는' 개체

x

가 존재한다면, 다음은 '반박'됩니다: 각 개체는 속성

\phi

를 갖는다."

부정을 사용한 양화사 공식은 또한 위에서 파생된 무모순 원리에서 즉시 파생되며, 각 인스턴스는 이미 더 특별한

\neg (\neg \neg \phi \land \neg \phi)

에서 파생된다. 마찬가지로, 원래의 양화사 공식은 사실

\forall x \big((\phi(x) \to \varphi) \to \varphi \big)

로 약화된

\forall x \ \phi(x)

로 여전히 유지됩니다. 따라서 실제로 더 강력한 정리가 유지됩니다.

:

(\exists x \ \neg \phi(x)) \to \neg (\forall x \, \neg \neg \phi(x))

말: "속성

\phi

를 '가지지 않는' 개체

x

가 존재한다면, 다음은 '반박'됩니다: 각 개체에 대해, 개체가 속성

\phi

를 '가지지 않는다'는 것을 증명할 수 '없다'."

두 번째로,

:

\big(\forall x \, (\phi(x) \to \varphi) \big) \,\, \leftrightarrow \,\, \big((\exists x \ \phi(x)) \to \varphi \big)

여기에도 유사한 고려 사항이 적용됩니다. 여기서 존재적 부분은 항상 가설이며, 이는 동치입니다. 특별한 경우를 다시 고려하면,

$(\forall x \ \neg \phi(x)) \leftrightarrow \neg (\exists x \ \phi(x))$

증명된 변환

(\chi \to \neg \phi) \leftrightarrow (\phi \to \neg \chi)

는 두 개의 추가 함축을 얻는 데 사용할 수 있다.

:

(\forall x \ \phi(x)) \to \neg (\exists x \ \neg \phi(x))

:

(\exists x \ \phi(x)) \to \neg (\forall x \ \neg \phi(x))

물론, 이러한 공식의 변형은 전항에 이중 부정을 삽입하여 파생될 수도 있다.

더 일반적인 변형이 유효합니다. 술어

\psi

를 통합하고 커리화하면, 아래에서 논의되는 술어 계산에서 함축과 결합 사이의 관계를 함축하는 다음 일반화도 유효합니다.

:

\big(\forall x \ \phi(x) \to (\psi(x) \to \varphi) \big) \,\, \leftrightarrow \,\, \Big(\big(\exists x \ \phi(x) \land \psi(x) \big) \to \varphi \Big)

술어

\psi

가 모든

x

에 대해 명백히 거짓이면, 이 동치는 사소합니다.

\psi

가 모든

x

에 대해 명백히 참이면, 스키마는 단순히 이전에 언급된 동치로 감소합니다. 클래스의 언어에서,

A=\{x \mid \phi(x)\}

및

B=\{x \mid \psi(x)\}

를 사용하면, 거짓

\varphi

를 사용한 이 동치의 특별한 경우는 상호소 집합

A \cap B = \emptyset

의 두 가지 특성화를 동일하게 만듭니다.

:

\forall (x \in A).x \notin B \,\, \leftrightarrow \,\, \neg \exists (x \in A).x \in B

유한한 변형의 양화사 공식이 존재하며, 두 개의 명제만 사용한다.

$(\neg \phi \lor \neg \psi) \to \neg (\phi \land \psi)$
$(\neg \phi \land \neg \psi) \leftrightarrow \neg (\phi \lor \psi)$

첫 번째 원리는 반대로 적용될 수 없다. 따라서 특히,

\neg (\phi \land \psi)

에서

\neg \phi \lor \neg \psi

를 도출하는 부정을 위한 분배 법칙은 없다. 구성적 해석의 비공식적인 예로, 다음을 고려해 보자. 앨리스와 밥 ''둘 다'' 데이트에 나타나지 않았다는 확실한 증거로부터, 이 두 사람 ''중 한 사람''에게만 관련된 확실한 증거, 즉 이 사람이 나타나지 않았다는 증거를 도출할 수 없다. 부정된 명제는 비교적 약하며, 단일 부정 가설로부터 분리를 허용하는 드 모르간의 법칙은 구성적으로 자동으로 성립하지 않는다. 직관적 명제 계산법과 그 확장 중 일부는 대신 분리 속성을 나타내며, 이는 분리의 임의의 분리자 중 하나가 개별적으로 도출될 수도 있음을 암시한다.

이 두 가지의 역변형과 이중 부정 전건이 있는 동등한 변형은 이미 위에서 언급되었다. 결합의 부정으로의 함축은 모순율로부터 직접 증명될 수 있는 경우가 많다. 이런 방식으로, 예를 들어

(\neg \phi \lor \psi) \to \neg (\phi \land \neg \psi)

와 같은 함축의 혼합 형태도 얻을 수 있다. 정리를 연결하면, 다음도 찾을 수 있다.

$(\neg \neg \phi \lor \neg \neg \psi) \to \neg \neg (\phi \lor \psi)$

약한 배제 중간의 법칙을 증명하므로 그 반대는 증명할 수 없다.

술어 논리에서, 상수 영역 원리는 유효하지 않다.

\forall x \big(\varphi \lor \psi(x) \big)

는 더 강력한

\varphi \lor \forall x \, \psi(x)

를 함축하지 않는다. 분배 법칙은 그러나 유한한 수의 명제에 대해 성립한다. 두 개의 존재적으로 닫힌 결정 가능한 술어와 관련된 드 모르간 법칙의 변형은 LLPO를 참조하라.

일반적인 동치로부터 두 개의 다른 논리 연산자를 사용하여 두 개의 술어의 비호환성을 표현하는 수출입도 도출됩니다.

$(\phi \to \neg \psi) \leftrightarrow \neg (\phi \land \psi)$

결합 연산자의 대칭성으로 인해, 이것은 이미 확립된

(\phi \to \neg \psi) \leftrightarrow (\psi \to \neg \phi)

를 다시 의미합니다.

부정된 결합에 대한 동치 공식은 커링과 언커링의 특별한 경우로 이해될 수 있습니다. 이중 부정과 관련된 더 많은 고려 사항이 다시 적용됩니다. 그리고 서론에서 언급된 결합과 함의를 연결하는 두 개의 비가역적 정리가 이 동치로부터 도출됩니다. 하나는 역이며,

\phi \to \psi

가

\phi \to \neg \neg \psi

보다 강하기 때문에

(\phi \to \psi) \to \neg (\phi \land \neg \psi)

가 성립합니다.

이제 다음 절에서 이 원리를 사용할 때, 좌측에 더 많은 부정을 가진 후자의 변형도 성립합니다.

$\neg (\phi \to \psi) \leftrightarrow (\neg \neg \phi \land \neg \psi)$

그 결과는 다음과 같습니다.

$\neg \neg (\phi \land \psi) \leftrightarrow (\neg \neg \phi \land \neg \neg \psi)$

이미 최소 논리는 배제된 중간값과 consequentia mirabilis, 즉 피어스 법칙의 한 예를 증명한다.

이제 직설법과 유사하게, 분명히

(\phi \lor \psi) \to ((\phi \to \psi) \to \psi)

는 이미 최소 논리 내에 존재하며, 이는 부정을 포함하지 않는 정리이다. 고전 논리에서 이 함축은 실제로 동치 관계이다.

\phi

를

\psi \to \varphi

의 형태로 취하면, 배제된 중간값은 폭발과 함께 피어스 법칙을 수반하는 것으로 나타난다.

직관주의 논리에서,

\bot

를 포함하는 진술된 정리의 변형을 얻는다. 먼저, 위에 언급된

\neg (\phi \land \psi)

에 대한 두 가지 다른 공식은

(\neg \phi \vee \neg \psi) \to (\phi \to \neg \psi)

를 암시하는 데 사용될 수 있다. 후자는 부정된 명제

\neg \psi

에 대한 선언적 삼단 논법의 형태이다. 강화된 형태는 직관주의 논리에서도 여전히 유효하다.

$(\neg \phi \lor \psi) \to (\phi \to \psi)$

이전 절과 마찬가지로,

\neg \phi

와

\phi

의 위치를 바꾸면, 도입부에서 언급된 것보다 더 강력한 원리를 얻을 수 있다. 예를 들어, 직관주의적으로 "P 또는 Q"는 "P가 아니면, Q"보다 더 강력한 명제 공식이며, 이들은 고전적으로 상호 교환 가능하다. 그 함축은 일반적으로 반전될 수 없는데, 이는 즉시 배제된 중간값을 암시하기 때문이다.

모순 불가능성과 폭발은 또한 더 강력한 변형

(\neg \phi \lor \psi) \to (\neg \neg \phi \to \psi)

를 증명한다. 그리고 이것은

\psi

에 대한 배제된 중간값이 어떻게 그것에 대한 이중 부정 제거를 암시하는지 보여준다. 고정된

\psi

에 대해, 이 함축은 일반적으로 반전될 수 없다.

물론 여기서 확립된 공식은 조합되어 더욱 다양한 변형을 얻을 수 있다. 예를 들어, 제시된 선언적 삼단 논법은 다음과 같이 일반화된다.

:

\Big(\big(\exists x \ \neg \phi(x) \big) \lor \varphi \Big) \,\, \to \,\, \Big(\big(\forall x \ \phi(x) \big) \to \varphi \Big)

어떤 항이든 존재한다면, 여기의 선행사는

\exists x \big(\phi(x) \to \varphi \big)

를 암시하며, 이는 다시 여기의 결론을 암시한다(이는 이 절에서 언급된 바로 첫 번째 공식이다).

이 절의 논의 대부분은 최소 논리에도 동일하게 적용된다. 그러나 일반적인

\psi

를 갖는 선언적 삼단 논법의 경우, 최소 논리는

(\neg \phi \lor \psi) \to (\neg \neg \phi \to \psi')

를 최대한 증명할 수 있으며, 여기서

\psi'

는

\neg \neg \psi \land (\psi \lor \neg \psi)

를 나타낸다. 여기서의 결론은 폭발을 사용하여

\psi

로 단순화될 수 있다.

위 목록에는 동치 관계도 포함되어 있다.

결합과 분리를 포함하는 동치는

(P \lor Q) \to R

이 실제로

P \to R

보다 더 강력하기 때문에 발생합니다. 동치의 양쪽은 독립적인 함의의 결합으로 이해될 수 있습니다. 위에서 모순

\bot

은

R

에 사용됩니다. 함수적 해석에서 이는 if-절 구조에 해당합니다.

예를 들어 "Not (

P

or

Q

)"는 "Not

P

이고, 또한 Not

Q

"와 동치입니다.

동치 자체는 일반적으로 다음과 같이 함의(

\to

)의 결합(

\land

)으로 정의되며, 동치입니다.

$(\phi \leftrightarrow \psi) \leftrightarrow \big((\phi \to \psi) \land (\psi \to \phi) \big)$

이것으로 그러한 연결 연산자는 차례로 다음에서 정의될 수 있다.

$(\phi \to \psi) \leftrightarrow ((\phi \lor \psi) \leftrightarrow \psi)$
$(\phi \to \psi) \leftrightarrow ((\phi \land \psi) \leftrightarrow \phi)$
$(\phi \land \psi) \leftrightarrow ((\phi \to \psi) \leftrightarrow \phi)$
$(\phi \land \psi) \leftrightarrow (((\phi \lor \psi) \leftrightarrow \psi) \leftrightarrow \phi)$

결과적으로,

\{\lor, \leftrightarrow, \bot\}

와

\{\land, \leftrightarrow, \neg\}

는 예를 들어 직관주의적 연결 연산자의 완전한 기저입니다.

2. 2. 추론

직관 명제 논리의 유일한 추론법은 전건 긍정의 형식(Modus Ponens)이다.

:

\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$

일차 술어 논리 시스템을 만들기 위해, 일반화 규칙^[2]이 추가된다.

$\forall$ -GEN: $\psi \to \phi$ 에서 $\psi \to (\forall x \ \phi )$ 를 추론한다. 단, $x$ 는 $\psi$ 에서 자유롭게 나타나지 않는다.
$\exists$ -GEN: $\phi \to \psi$ 에서 $(\exists x \ \phi ) \to \psi$ 를 추론한다. 단, $x$ 는 $\psi$ 에서 자유롭게 나타나지 않는다.

다음 공리도 추가된다.^[2]

PRED-1: $(\forall x \ \phi (x)) \to \phi (t)$ . 단, 항 $t$ 는 $\phi$ 에서 변수 $x$ 에 대한 대체를 위해 자유롭게 존재한다(즉, $t$ 에서 어떤 변수의 발생도 $\phi (t)$ 에서 묶이지 않는다).
PRED-2: $\phi (t) \to (\exists x \ \phi (x))$ . PRED-1과 동일한 제한이 적용된다.

2. 3. 공리

직관 명제 논리의 공리는 다음과 같다. 임의의 명제

\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))$

직관 논리는 힐베르트 스타일 계산법을 사용하여 정의할 수 있다. 이는 고전 명제 논리를 공리화하는 한 가지 방법과 유사하다.

명제 논리에서 추론 규칙은 Modus Ponens이다.

MP: $\phi \to \psi$ 와 $\phi$ 에서 $\psi$ 를 추론한다.

그리고 공리는 다음과 같다.

THEN-1	$\psi \to (\phi \to \psi )$
THEN-2	$\big(\chi \to (\phi \to \psi )\big) \to \big((\chi \to \phi) \to (\chi \to \psi )\big)$
AND-1	$\phi \land \chi \to \phi$
AND-2	$\phi \land \chi \to \chi$
AND-3	$\phi \to \big(\chi \to (\phi \land \chi )\big)$
OR-1	$\phi \to \phi \lor \chi$
OR-2	$\chi \to \phi \lor \chi$
OR-3	$(\phi \to \psi ) \to \Big((\chi \to \psi ) \to \big((\phi \lor \chi) \to \psi )\Big)$
FALSE	$\bot \to \phi$

이것을 일차 술어 논리 시스템으로 만들기 위해, 일반화 규칙

$\forall$ -GEN: $\psi \to \phi$ 에서 $\psi \to (\forall x \ \phi )$ 를 추론한다. 단, $x$ 는 $\psi$ 에서 자유롭게 나타나지 않는다.
$\exists$ -GEN: $\phi \to \psi$ 에서 $(\exists x \ \phi ) \to \psi$ 를 추론한다. 단, $x$ 는 $\psi$ 에서 자유롭게 나타나지 않는다.

가 추가되고, 다음 공리도 추가된다.

PRED-1: $(\forall x \ \phi (x)) \to \phi (t)$ . 단, 항 $t$ 는 $\phi$ 에서 변수 $x$ 에 대한 대체를 위해 자유롭게 존재한다(즉, $t$ 에서 어떤 변수의 발생도 $\phi (t)$ 에서 묶이지 않는다).
PRED-2: $\phi (t) \to (\exists x \ \phi (x))$ . PRED-1과 동일한 제한이 적용된다.

만약

\phi \to \bot

의 약어로 간주하기보다는 부정에 대한 연결사

\neg

를 포함시키고 싶다면 다음과 같이 하면 된다.

NOT-1': $(\phi \to \bot ) \to \neg \phi$
NOT-2': $\neg \phi \to (\phi \to \bot )$

연결사

\bot

(거짓)을 생략하고 싶다면 여러 대안이 있다. 예를 들어, 세 개의 공리 FALSE, NOT-1', NOT-2'를 두 개의 공리로 대체할 수 있다.

NOT-1: $(\phi \to \chi ) \to \big((\phi \to \neg \chi ) \to \neg \phi \big)$
NOT-2: $\chi \to (\neg \chi \to \psi)$

NOT-1의 대안으로는

(\phi \to \neg \chi ) \to (\chi \to \neg \phi )

또는

(\phi \to \neg \phi ) \to \neg \phi

가 있다.

동치에 대한 연결사

\leftrightarrow

는

\phi \leftrightarrow \chi

가

(\phi \to \chi ) \land (\chi \to \phi )

를 의미하는 약어로 취급될 수 있다. 또는 다음과 같은 공리를 추가할 수도 있다.

IFF-1: $(\phi \leftrightarrow \chi ) \to (\phi \to \chi )$
IFF-2: $(\phi \leftrightarrow \chi ) \to (\chi \to \phi )$
IFF-3: $(\phi \to \chi ) \to ((\chi \to \phi ) \to (\phi \leftrightarrow \chi ))$

필요하다면, IFF-1과 IFF-2를 결합하여 단일 공리

(\phi \leftrightarrow \chi ) \to ((\phi \to \chi ) \land (\chi \to \phi ))

로 만들 수 있다.

3. 성질

직관 논리의 정리는 고전 논리의 관점에서 약화된 형태로 이해될 수 있다. 즉, 고전 논리에서 가능했던 추론을 제한하지만, 새로운 추론을 허용하지는 않는다.^[9]^[10] 고전 논리의 많은 항진명제는 직관 논리에서 정리가 아닌데, 특히 배중률을 긍정하지 않아 비구성적인 귀류법 사용을 무효화하기 때문이다.

이중 부정은 배중률을 긍정하지 않는다. 배중률이 어떤 맥락에서도 지켜지지 않는 것은 아니지만, 반례도 제시될 수 없다. 그러한 반례는 고전 논리에서 허용되지 않는 추론(특정 명제에 대한 배중률의 부정을 추론)이 될 것이므로 직관 논리에서는 허용되지 않는다.

몇몇 양화 표현이 부정될 때 술어 논리 공식의 상황은 더 복잡하다.

3. 1. 명제의 격자

주어진 명제 $\phi$로부터, 고전 명제 논리에서는 $\bot,\phi,\lnot\phi,\top$ 네 개의 명제밖에 정의할 수 없지만, 직관 명제 논리에서는 이로부터 무한한 수의, 서로 동치이지 않는 명제들이 존재한다. 이를 '''리에게르-니시무라 사다리'''(Rieger–Nishimura ladder^영어)라고 하며, 라디슬라프 스반테 리에게르(cs: Ladislav Svante Rieger^cs)^[9]와 니시무라 이와오^[10]가 정의하였다.

:

3. 2. 고전 논리와의 관계

직관 논리는 고전 논리의 일부분으로, 직관 논리에서 참인 모든 명제는 고전 논리에서도 참이다. 하지만 고전 논리에서는 참이지만 직관 논리에서는 증명할 수 없는 명제들이 존재한다. 이러한 명제들의 예시는 다음과 같다.

(배중률) $\phi\lor\lnot\phi$
(이중 부정 삭제) $\lnot\lnot\phi\implies\phi$
(퍼스의 법칙) $\left(\phi\implies\chi)\implies\phi\right)\implies\phi$

직관 논리의 정리는 고전 논리의 관점에서 약화된 형태로 이해될 수 있다. 즉, 고전 논리에서 가능했던 추론을 제한하지만, 새로운 추론을 허용하지는 않는다. 고전 논리의 많은 항진명제는 직관 논리에서 정리가 아닌데, 특히 배중률을 긍정하지 않아 비구성적인 귀류법 사용을 무효화하기 때문이다.

이중 부정 번역은 고전 일차 논리를 직관 논리에 내장하는 방법을 제공한다. 이 번역에 따르면, 일차 논리 공식이 고전 논리에서 증명 가능하면, 그 공식의 괴델-겐첸 번역은 직관 논리에서 증명 가능하다. 예를 들어,

\psi\to\phi

형태의 고전 명제 논리 정리는

\psi\to\neg\neg\phi

에 대한 직관적 증명과 이중 부정 제거를 한 번 적용하여 증명할 수 있다. 따라서 직관 논리는 고전 논리를 구성적 의미론으로 확장하는 것으로 볼 수 있다.

3. 3. 의미론

직관 논리는 다양한 의미론을 갖는다. 그 중 하나는 위상수학적 의미론이다. 위상 공간

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^영어)도 직관 논리에서 사용 가능하다.

직관 논리의 의미론은 고전 논리보다 복잡하다. 모형 이론은 헤이팅 대수나 크립키 의미론으로 주어진다. 2014년 밥 콘스터블은 타르스키와 유사한 모형 이론의 완전성을 증명했지만, 고전적인 것과는 다른 완전성 개념을 사용했다.

직관 논리에서 증명되지 않은 명제는 중간 진리값을 갖지 않는다. 이러한 명제는 제3의 진리값을 갖지 않는다는 것이 1928년 글리벤코에 의해 증명되었다. 명제는 증명되거나 반증될 때까지 알 수 없는 진리값을 갖는다. 명제는 그 명제로부터 모순을 추론함으로써 반증된다.

직관 논리는 이진 논리나 유한 다치 논리로 해석될 수 없다. 직관 논리는 고전 논리의 명제

\{\top, \bot\}

를 유지하지만, 명제 공식의 각 "증명"은 유효한 명제 값으로 간주되므로, 헤이팅의 명제-집합 개념에 따라 명제 공식은 (잠재적으로 비-유한) 증명의 집합이다.

고전 논리에서는 공식의 진리값을 부울 대수의 원소로 선택한다. 부울 대수에서의 결합과 교집합 연산은 ∧ 및 ∨ 논리 연결자와 동일시되어, ''A'' ∧ ''B'' 형식의 공식의 값은 부울 대수에서 ''A''의 값과 ''B''의 값의 교집합이 된다. 공식이 고전 논리의 유효한 명제이기 위한 필요충분 조건은 해당 값이 모든 평가에 대해 1인 경우이다.

직관 논리에서도 유사한 정리가 성립하지만, 헤이팅 대수에서 값을 사용한다. 공식은 헤이팅 대수에서 모든 평가에 대해 최고 요소의 값을 받으면 직관 논리에서 유효하다.

유효한 공식을 확인하기 위해, 실수 '''R'''의 열린 부분 집합인 단일 헤이팅 대수를 고려하는 것으로 충분하다. 이 대수에서 다음이 성립한다.

:

\begin{align}\text{값}[\bot] &=∅ \\\text{값}[\top] &= \mathbf{R} \\\text{값}[A \land B] &= \text{값}[A] \cap \text{값}[B] \\\text{값}[A \lor B]  &= \text{값}[A] \cup \text{값}[B] \\\text{값}[A \to B] &= \text{int} \left ( \text{값}[A]^\complement \cup \text{값}[B] \right )\end{align}

여기서 int(''X'')는 ''X''의 내부이고, ''X''^∁은 여집합이다.

''A'' → ''B''에 관한 항등식으로 ¬''A''의 값을 계산할 수 있다.

:

\begin{align}\text{값}[\neg A] &= \text{값}[A \to \bot] \\&=  \text{int} \left ( \text{값}[A]^\complement \cup \text{값}[\bot] \right ) \\&= \text{int} \left ( \text{값}[A]^\complement \cup ∅ \right ) \\&=  \text{int} \left ( \text{값}[A]^\complement \right )\end{align}

이러한 할당을 통해 직관적으로 유효한 공식은 정확히 전체 선의 값을 할당받은 공식이다. 예를 들어 ¬(''A'' ∧ ¬''A'')는 유효하다. 어떤 집합 ''X''가 공식 ''A''의 값으로 선택되더라도 ¬(''A'' ∧ ¬''A'')의 값은 다음과 같이 직선 전체가 되기 때문이다.

:

\begin{align}\text{값}[\neg(A \land \neg A)] &= \text{int} \left ( \text{값} [A \land \neg A]^\complement   \right )  && \text{값}[\neg B] = \text{int}\left ( \text{값}[B]^\complement \right) \\&= \text{int} \left ( \left (\text{값}[A] \cap \text{값}[\neg A] \right )^\complement \right )\\&= \text{int} \left ( \left (\text{값}[A]  \cap \text{int} \left (\text{값}[A]^\complement \right ) \right )^\complement \right )  \\&= \text{int} \left ( \left (X  \cap \text{int} \left (X^\complement \right ) \right )^\complement \right ) \\&= \text{int} \left (\emptyset^\complement \right ) && \text{int} \left (X^\complement \right ) \subseteq X^\complement \\&= \text{int} (\mathbf{R}) \\&= \mathbf{R}\end{align}

그러나 배중률 ''A'' ∨ ¬''A''는 ''A''에 대해 양의 실수 집합의 특정 값을 사용하여 "무효"인 것으로 나타낼 수 있다.

:

\begin{align}\text{값}[A \lor \neg A] &=  \text{값}[A] \cup \text{값}[\neg A] \\&=  \text{값}[A] \cup \text{int} \left (  \text{값}[A]^\complement \right) && \text{값}[\neg B] = \text{int}\left ( \text{값}[B]^\complement \right) \\&=  \{ x > 0\} \cup \text{int} \left (  \{x > 0\}^\complement \right ) \\&= \{ x > 0\} \cup \text{int} \left (  \{x \leqslant 0 \} \right) \\&= \{ x > 0\} \cup  \{x < 0 \} \\&=\{ x \neq 0 \} \\&\neq \mathbf{R}\end{align}

위에 설명된 무한 헤이팅 대수에서 직관적으로 유효한 모든 공식의 해석은 최고 요소가 평가로 나타난다. 유효하지 않은 모든 공식에 대해 최고 요소와 다른 평가를 생성하는 변수에 값 할당이 있다. 유한 헤이팅 대수는 이 속성을 갖지 않는다.

솔 크립키는 모달 논리 의미론 연구를 바탕으로 직관 논리를 위한 크립키 의미론(관계적 의미론)을 만들었다.^[3]

직관 논리에 대한 타르스키식 의미론은 완전성 증명이 불가능하다. 로버트 콘스터블은 타르스키식 모델에서 직관 논리에 대해 약한 완전성 개념이 성립함을 보였다. 모든 모델에서 "동일한 방식"으로 참인 명제에 관심을 두며, 모델이 어떤 공식을 참으로 판단하는 단일 증명은 모든 모델에 대해 유효해야 한다.

4. 역사

아런트 헤이팅은 라위트전 브라우어르의 직관주의 수학을 형식화하기 위해 직관 논리를 도입하였다.^[1]

5. 응용

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

5. 1. 토포스 이론

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

5. 2. 전산학 분야

직관 논리는 존재성 성질을 갖는 증명을 생성하여 다른 형태의 수학적 구성주의에도 적합하다는 특징이 있다. 객체가 존재한다는 구성적 증명이 있다면, 그 증명은 해당 객체의 예시를 생성하는 알고리즘으로 사용될 수 있는데, 이는 증명과 알고리즘 사이의 Curry–Howard 대응으로 알려진 원리이다.^[1]

이러한 특징 덕분에 증명 도우미라는 컴퓨터 도구를 활용할 수 있다. Agda나 Coq와 같은 증명 도우미는 사용자가 대규모 증명을 생성하고 검증하는 데 도움을 준다. 이를 통해 수학자와 논리학자들은 매우 복잡한 시스템을 개발하고 증명할 수 있게 되었다.

형식적 검증 없이는 검증이 불가능했던 증명의 예로 사색 정리의 증명이 있다. 이 정리는 100년 이상 수학자들을 곤경에 빠뜨렸지만, 컴퓨터 프로그램으로 증명을 완료하고 Coq를 사용하여 검증하였다.^[1]

6. 관련 문서

최소 논리: 거짓 공리를 제거한 직관 논리의 하위 시스템이다.^[2]
중간 논리: 쿠르트 괴델이 1932년에 정의한 고전 논리와 직관 논리 사이의 논리 체계이다.^[2]
다치 논리: 쿠르트 괴델은 1932년에 직관 논리가 유한 다치 논리가 아님을 보였다.^[3]
양상 논리: 직관 명제 논리의 모든 공식은 정규 양상 논리 S4의 언어로 변환할 수 있다.
람다 계산: 직관주의적 논리와 단순 유형화된 람다 계산 사이에는 확장된 커리-하워드 동형사상이 존재한다.^[8]

6. 1. 최소 논리

FALSE(거짓) 공리를 제거한 직관 논리의 하위 시스템은 최소 논리로 알려져 있다.^[2] 최소 논리는 직관주의 논리에서 공리를 제거한 것이다.

6. 2. 중간 논리

쿠르트 괴델은 1932년에 고전 논리와 직관 논리 사이의 중간 논리 체계를 정의했다.^[2] 실제로 부울 대수와 동등하지 않은 모든 유한 하이팅 대수는 (의미론적으로) 중간 논리를 정의한다.^[2] 반면에 순수 직관 논리에서 공식의 유효성은 어떤 개별 하이팅 대수와 관련된 것이 아니라 모든 하이팅 대수에 동시에 관련된다.^[2]

예를 들어, 부정을 포함하지 않는 스키마의 경우, 고전적으로 유효한

(A\to B)\lor(B\to A)

를 고려해 보자. 이것을 직관 논리 위에 채택하면 괴델-더밋 논리라고 하는 중간 논리가 된다.^[2]

고전 논리 체계는 다음 공리 중 하나를 추가하여 얻을 수 있다.^[2]

$\phi \lor \neg \phi$ (배중률)
$\neg \neg \phi \to \phi$ (이중 부정 제거)
$(\neg \phi \to \phi) \to \phi$ (Consequentia mirabilis, 피어스 법칙 참조)

다양한 재구성 또는 두 변수(예: 피어스 법칙)의 도식으로의 공식도 존재한다.^[2] 주목할 만한 예는 (역) 대우 법칙이다.^[2]

$(\neg \phi \to \neg \chi ) \to (\chi \to \phi)$

일반적으로 추가 공리로 두 원소 크립키 틀

\circ{\longrightarrow}\circ

에서 유효하지 않은 모든 고전적 항진명제를 사용할 수 있다(즉, 스메타니치의 논리에 포함되지 않음).^[2] 임의의 유한 하이팅 대수에서 부울 대수가 아닌 것은 (의미론적으로) 중간 논리를 정의한다.^[2] 한편, 순수한 직관주의 논리에 있어서의 논리식의 타당성은 특정 하이팅 대수에 결부된 것이 아니라, 모든 하이팅 대수와 관계가 있다.^[2]

6. 3. 다치 논리

쿠르트 괴델은 1932년에 직관 논리가 유한 다치 논리가 아님을 보였다.^[3] 헤이팅 대수를 통해 직관 논리의 무한 다치 논리적 해석을 할 수 있다.^[3]

6. 4. 양상 논리

직관 명제 논리(IPC)의 모든 공식은 정규 양상 논리 S4의 언어로 변환할 수 있다.

직관 명제 논리 (IPC)	양상 명제 논리 S4
$\bot$	$\bot$
$A$ (A는 양의 리터럴)	$\Box A$
$A \wedge B$	$A^* \wedge B^*$
$A \vee B$	$A^* \vee B^*$
$A \to B$	$\Box (A^* \to B^*)$
$\neg A$ ( $A \to \bot$ 의 축약형)	$\Box(\neg (A^*))$

여기서 * 표시는 변환을 나타낸다. 이렇게 번역된 공식이 양상 명제 논리 S4에서 유효할 필요충분조건은 원래 공식이 IPC에서 유효하다는 것이 증명되었다.^[7] 이 변환은 괴델-매킨지-타르스키 변환이라고 불린다.

또한, 양상 논리 S4의 직관주의적 버전인 구성적 양상 논리 CS4도 존재한다.^[8]

6. 5. 람다 계산

직관주의적 논리와 단순 유형화된 람다 계산 사이에는 확장된 커리-하워드 동형사상이 존재한다.^[8]

참조

_[1] 문서 Hilbert (1927), p.476
_[2] 서적 Proof Theory
_[3] 서적 Lectures on the Curry-Howard Isomorphism Elsevier
_[4] 문서 ここでの双対はシークエント計算においての双対である。
_[5] 학술지 Dual-Intuitionistic Logic https://projecteucli[...] 1996-07-01
_[6] 학술지 LK, LJ, Dual Intuitionistic Logic, and Quantum Logic
_[7] 웹사이트 Logique modale propositionnelle S4 et logique intuitioniste propositionnelle http://teachinglogic[...] 2015-05-08
_[8] 웹사이트 Categorical and Kripke Semantics for Constructive S4 Modal Logic http://www.cs.nott.a[...] 2015-05-08
_[9] 저널
_[10] 저널
_[11] 서적

본 사이트는 AI가 위키백과와 뉴스 기사,정부 간행물,학술 논문등을 바탕으로 정보를 가공하여 제공하는 백과사전형 서비스입니다.
모든 문서는 AI에 의해 자동 생성되며, CC BY-SA 4.0 라이선스에 따라 이용할 수 있습니다.
하지만, 위키백과나 뉴스 기사 자체에 오류, 부정확한 정보, 또는 가짜 뉴스가 포함될 수 있으며, AI는 이러한 내용을 완벽하게 걸러내지 못할 수 있습니다.
따라서 제공되는 정보에 일부 오류나 편향이 있을 수 있으므로, 중요한 정보는 반드시 다른 출처를 통해 교차 검증하시기 바랍니다.

문의하기 : help@durumis.com