헤이팅 대수

3. 성질

헤이팅 대수는 직관 논리를 설명하는 데 중요한 역할을 하는, 특정 조건을 만족하는 유계 격자이다.

헤이팅 대수 ''H''는 다음 조건을 만족하는 가장 큰 원소 ''x''가 존재한다.

:$a\; \backslash wedge\; x\; \backslash le\; b$

이 원소 ''x''는 ''b''에 대한 ''a''의 상대적 유사 여집합이라고 하며, ''a''→''b''로 표기한다.

헤이팅 대수는 곱이 만남 연산($\backslash wedge$)인 범주로 볼 수 있다. 이때, 지수 조건은 임의의 대상 ''Y''와 ''Z''에 대해 지수 $Z^Y$가 유일하게 존재함을 의미한다. 헤이팅 함축($\backslash Rightarrow$ 또는 $\backslash multimap$로 표기)은 지수와 같으며, 만남의 오른쪽 수반이다. 즉, $(-\; \backslash wedge\; Y)\; \backslash dashv\; (Y\; \backslash Rightarrow\; -)$ 관계가 성립한다.

헤이팅 대수는 모노이드 연산이 ∧이고 모노이드 단위가 상위 원소 1인 잔여 격자로 정의할 수도 있다.

최대 원소 1과 최소 원소 0을 갖는 유계 격자 ''A''와 이항 연산 →가 주어졌을 때, 다음 조건들을 모두 만족하면 헤이팅 대수를 이룬다.

# $a\backslash to\; a\; =\; 1$

# $a\backslash wedge(a\backslash to\; b)=a\backslash wedge\; b$

# $b\backslash wedge(a\backslash to\; b)=\; b$

# $a\backslash to\; (b\backslash wedge\; c)=\; (a\backslash to\; b)\backslash wedge\; (a\backslash to\; c)$

헤이팅 대수는 분배적이며, 다음의 무한 분배 법칙도 만족한다.

:$x\backslash wedge\backslash bigvee\; Y\; =\; \backslash bigvee\; \backslash \{x\backslash wedge\; y\; \backslash mid\; y\; \backslash in\; Y\backslash \}$

헤이팅 대수는 다음 조건 중 하나를 만족하는 경우 부울 대수가 된다.

• 모든 원소가 정칙 원소이다. (''x'' = ¬¬''x'')
• 모든 원소가 상보적 원소이다. (''x''∧''y'' = 0 이고 ''x''∨''y'' = 1 인 ''y''가 존재)

3. 1. 함의 관계

3. 2. 불 대수가 될 조건

• 이중 부정의 삭제: $\backslash lnot\backslash lnot\backslash colon\; H\backslash to\; H$는 항등 함수이다. 즉, 모든 원소에 대해 이중 부정이 원래 원소와 같다.
• 배중률: 모든 원소 $a\backslash in\; H$에 대하여, $a\backslash lor\backslash lnot\; a=\backslash top$이다. 즉, 어떤 명제와 그 명제의 부정의 논리합은 항상 참이다.

3. 3. 분배 법칙

3. 4. 정칙 원소와 보충 원소

3. 5. 드 모르간 법칙

4. 예

• 모든 부울 대수는 헤이팅 대수이며, 이 경우 ''p''→''q''는 ¬''p''∨''q''로 정의된다.
• 최소 원소 0과 최대 원소 1을 갖는 모든 전순서 집합은 헤이팅 대수이다(격자로 간주될 경우). 이 경우 ''p''→''q''는 ''p≤q''일 때 1과 같고, 그렇지 않으면 ''q''와 같다.
• 부울 대수가 아닌 가장 간단한 헤이팅 대수는 {0, 1/2, 1}의 전순서 집합이다(격자로 간주). 이 경우 연산은 다음과 같다:

이 예에서 1/2∨¬1/2 = 1/2∨(1/2 → 0) = 1/2∨0 = 1/2는 배중률을 위반한다.

• 모든 위상은 열린 집합 격자의 형태로 완비 헤이팅 대수를 제공한다. 이 경우, 요소 ''A''→''B''는 ''A^c''와 ''B''의 합집합의 내부이다. 여기서 ''A^c''는 여집합을 나타낸다. 모든 완비 헤이팅 대수가 이런 형태를 갖는 것은 아니다. 이러한 문제는 무점 위상수학에서 연구되며, 여기서 완비 헤이팅 대수는 '''프레임''' 또는 '''로컬'''이라고도 한다.
• 모든 내부 대수는 열린 원소의 격자 형태로 헤이팅 대수를 제공한다. 모든 헤이팅 대수는 이 형태를 갖는데, 헤이팅 대수는 자유 부울 확장을 유계 분배 격자로 취하고 이를 이 부울 대수에서 일반화된 위상으로 취급함으로써 부울 대수로 완성될 수 있기 때문이다.
• 린덴바움 대수는 명제적 직관 논리의 헤이팅 대수이다.
• 기초 토포스의 부분 대상 분류자 Ω의 전역 원소는 헤이팅 대수를 형성한다. 이는 토포스에 의해 유도된 직관 고차 논리의 진리값의 헤이팅 대수이다. 더 일반적으로, 토포스 내의 임의의 객체 ''X''의 부분 대상의 집합은 헤이팅 대수를 형성한다.
• 우카시에비치-모이실 대수 (LM_''n'')는 모든 ''n''에 대해 헤이팅 대수이다.^[7] (하지만, 이는 ''n'' ≥ 5에 대해 MV-대수는 아니다^[8]).

5. 역사

아런트 헤이팅이 직관 논리를 형식화하기 위하여 도입하였다.^[16][17][18]

6. 직관 논리와의 관계

직관 명제 논리에서, 명제들의 격자는 헤이팅 대수를 이룬다.^[7] 마찬가지로, 모든 헤이팅 대수는 어떤 초직관 논리의 명제 격자와 동형이다.

(작은) 토포스에서, 모든 대상의 부분 대상의 부분 순서 집합은 헤이팅 대수를 이룬다. 즉, 토포스의 내부 논리는 직관 논리이다.

헤이팅 대수의 이러한 특성은 직관주의 명제 미적분과 헤이팅 대수 사이의 관계에 관한 기본적인 사실들의 증명을 즉시 가능하게 한다. (이러한 사실에 대해서는 "증명 가능한 항등식" 및 "보편적 구성" 섹션을 참조하십시오.) 원소 $\backslash top$을 직관적으로 "증명 가능하게 참"을 의미하는 것으로 생각해야 한다. 직관주의 논리의 공리와 비교해 보십시오.

세 개의 이항 연산 →, ∧ 및 ∨와 두 개의 특수한 원소 $\backslash bot$ 및 $\backslash top$을 가진 집합 ''A''가 주어지면, ''A''는 (조건 $a\; \backslash le\; b$가 ''a''→''b'' = $\backslash top$일 때 정의되는 관계 ≤와 함께) 임의의 ''A''의 원소 ''x'', ''y'' 및 ''z''에 대해 다음 조건이 충족되는 경우 이러한 연산에 대한 헤이팅 대수이다.

# $\backslash mbox\{만약\; \}\; x\; \backslash le\; y\; \backslash mbox\{\; 이고\; \}\; y\; \backslash le\; x\; \backslash mbox\{\; 이면\; \}\; x\; =\; y\; ,$

# $\backslash mbox\{만약\; \}\; \backslash top\; \backslash le\; y\; ,\; \backslash mbox\{\; 이면\; \}\; y\; =\; \backslash top\; ,$

# $x\; \backslash le\; y\; \backslash to\; x\; ,$

# $x\; \backslash to\; (y\; \backslash to\; z)\; \backslash le\; (x\; \backslash to\; y)\; \backslash to\; (x\; \backslash to\; z)\; ,$

# $x\; \backslash land\; y\; \backslash le\; x\; ,$

# $x\; \backslash land\; y\; \backslash le\; y\; ,$

# $x\; \backslash le\; y\; \backslash to\; (x\; \backslash land\; y)\; ,$

# $x\; \backslash le\; x\; \backslash lor\; y\; ,$

# $y\; \backslash le\; x\; \backslash lor\; y\; ,$

# $x\; \backslash to\; z\; \backslash le\; (y\; \backslash to\; z)\; \backslash to\; (x\; \backslash lor\; y\; \backslash to\; z)\; ,$

# $\backslash bot\; \backslash le\; x\; .$

마지막으로 ¬''x''를 ''x''→ $\backslash bot$로 정의한다.

조건 1은 동등한 공식이 식별되어야 함을 나타낸다. 조건 2는 증명 가능하게 참인 공식이 modus ponens에 대해 닫혀 있음을 나타낸다. 조건 3과 4는 ''then'' 조건이다. 조건 5, 6 및 7은 ''and'' 조건이다. 조건 8, 9 및 10은 ''or'' 조건이다. 조건 11은 ''false'' 조건이다.

물론, 논리에 대해 다른 공리 집합을 선택했다면, 이에 따라 우리 공리를 수정할 수 있다.

린덴바움 대수는 명제적 직관 논리의 헤이팅 대수이다.

기초 토포스의 부분 대상 분류자 Ω의 전역 원소는 헤이팅 대수를 형성한다. 이는 토포스에 의해 유도된 직관 고차 논리의 진리값의 헤이팅 대수이다. 더 일반적으로, 토포스 내의 임의의 객체 ''X''의 부분 대상의 집합은 헤이팅 대수를 형성한다.

직관 논리의 공리를 헤이팅 대수의 용어로 해석하면, 어떤 헤이팅 대수에서든, 수식 변수에 값을 할당하면 해당 공리는 최대 원소인 1로 평가된다. 예를 들어, (''P''∧''Q'')→''P''는 유사 여집합의 정의에 따라, $P\; \backslash land\; Q\; \backslash land\; x\; \backslash le\; P$를 만족하는 가장 큰 원소 ''x''이다. 이 부등식은 모든 ''x''에 대해 성립하므로, 가장 큰 ''x''는 1이다.

또한, 전건 긍정의 규칙을 사용하면 수식 ''Q''를 수식 ''P''와 ''P''→''Q''로부터 도출할 수 있다. 그러나 모든 헤이팅 대수에서 ''P''의 값이 1이고, ''P''→''Q''의 값이 1이면 $P\; \backslash land\; 1\; \backslash le\; Q$를 의미하며, 따라서 $1\; \backslash land\; 1\; \backslash le\; Q$가 된다. 이는 ''Q''의 값이 1일 수밖에 없음을 의미한다.

이는 수식이 직관 논리의 법칙으로부터 추론 가능하며, 전건 긍정의 규칙을 통해 공리에서 파생된 경우, 수식 변수에 대한 값 할당에 관계없이 모든 헤이팅 대수에서 항상 값 1을 갖는다는 것을 의미한다. 그러나 피어스의 법칙의 값이 항상 1이 아닌 헤이팅 대수를 구성할 수 있다. 위에서 주어진 3-원소 대수 {0,1/2,1}를 고려해 보자. 만약 ''P''에 1/2를 할당하고, ''Q''에 0을 할당하면, 피어스의 법칙 ((''P''→''Q'')→''P'')→''P''의 값은 1/2이다. 따라서 피어스의 법칙은 직관적으로 도출될 수 없다. 이에 대한 일반적인 맥락은 커리-하워드 동형사상에서 타입 이론과 관련하여 확인할 수 있다.

역도 증명할 수 있다. 즉, 수식이 항상 값 1을 가지면, 직관 논리의 법칙으로부터 도출 가능하므로, "직관적으로 유효한" 수식은 정확히 항상 값 1을 갖는 수식이다. 이는 "고전적으로 유효한" 수식이 수식 변수에 대해 참과 거짓을 할당하는 모든 가능한 경우에 2-원소 부울 대수에서 값 1을 갖는 수식, 즉, 일반적인 진리표 의미에서 항진명제라는 개념과 유사하다. 논리적 관점에서 헤이팅 대수는 일반적인 진리값 시스템의 일반화이며, 그 최대 원소인 1은 '참'과 유사하다. 일반적인 2-값 논리 시스템은 헤이팅 대수의 특수한 경우이며, 대수의 유일한 원소가 1 (참)과 0 (거짓)인 가장 작은 비자명한 경우이다.

명제 미적분학의 공식 $F(A\_1,\; A\_2,\backslash ldots,\; A\_n)$ (변수 외에 연결사 $\backslash land,\; \backslash lor,\; \backslash lnot,\; \backslash to$와 상수 0과 1을 사용)이 주어졌을 때, 헤이팅 대수 연구 초기에 증명된 사실은 다음 두 조건이 동치라는 것이다.

# 공식 ''F''는 직관주의 명제 미적분학에서 증명 가능하다.

# 항등식 $F(a\_1,\; a\_2,\backslash ldots,\; a\_n)\; =\; 1$은 임의의 헤이팅 대수 ''H''와 임의의 원소 $a\_1,\; a\_2,\backslash ldots,\; a\_n\; \backslash in\; H$에 대해 참이다.

메타 함의 1 ⇒ 2는 매우 유용하며 헤이팅 대수에서 항등식을 증명하는 주요 실용적인 방법이다. 실제로는 이러한 증명에서 추론 정리를 자주 사용한다.

헤이팅 대수 ''H''의 임의의 ''a''와 ''b''에 대해 $a\; \backslash le\; b$는 ''a''→''b'' = 1인 경우에만 해당하므로 1 ⇒ 2에서 공식 ''F''→''G''가 증명 가능한 경우 임의의 헤이팅 대수 ''H''와 임의의 원소 $a\_1,\; a\_2,\backslash ldots,\; a\_n\; \backslash in\; H$에 대해 $F(a\_1,\; a\_2,\backslash ldots,\; a\_n)\; \backslash le\; G(a\_1,\; a\_2,\backslash ldots,\; a\_n)$이 성립한다. (추론 정리에 따르면, ''F''에서 ''G''가 증명 가능하면 즉, ''G''가 ''F''의 증명 가능한 결과인 경우에만 ''F''→''G''가 (무조건) 증명 가능한다.) 특히, ''F''와 ''G''가 증명적으로 동등하면 ≤는 순서 관계이므로 $F(a\_1,\; a\_2,\backslash ldots,\; a\_n)\; =\; G(a\_1,\; a\_2,\backslash ldots,\; a\_n)$이다.

1 ⇒ 2는 증명 시스템의 논리적 공리를 검토하고 헤이팅 대수에서 그 값이 1임을 확인한 다음, 헤이팅 대수에서 값이 1인 식에 추론 규칙을 적용하면 값이 1인 식이 나온다는 것을 확인하여 증명할 수 있다. 예를 들어, 모두스 포넨스를 유일한 추론 규칙으로 하고 공리가 직관주의 논리#공리화에 주어진 힐베르트 스타일의 공리인 증명 시스템을 선택해 보자. 그러면 확인해야 할 사실은 위에 주어진 헤이팅 대수의 공리 같은 정의에서 즉시 따릅니다.

1 ⇒ 2는 또한 어떤 명제 공식이 고전 논리에서는 항진명제이지만, 직관주의 명제 논리에서는 ''증명될 수 없다''는 것을 증명하는 방법을 제공한다. 어떤 공식 $F(A\_1,\; A\_2,\backslash ldots,\; A\_n)$이 증명 불가능함을 증명하기 위해, 헤이팅 대수 ''H''와 $F(a\_1,\; a\_2,\backslash ldots,\; a\_n)\; \backslash ne\; 1$인 원소 $a\_1,\; a\_2,\backslash ldots,\; a\_n\; \backslash in\; H$를 제시하는 것으로 충분하다.

논리 언급을 피하려면 실제로는 헤이팅 대수에 유효한 추론 정리의 버전을 보조 정리로 증명해야 한다. 헤이팅 대수 ''H''의 임의의 원소 ''a'', ''b'', ''c''에 대해 $(a\; \backslash land\; b)\; \backslash to\; c\; =\; a\; \backslash to\; (b\; \backslash to\; c)$이다.

7. 응용

직관 명제 논리에서, 명제들의 격자는 헤이팅 대수를 이룬다. 마찬가지로, 모든 헤이팅 대수는 어떤 초직관 논리의 명제 격자와 동형이다.

(작은) 토포스에서, 모든 대상의 부분 대상의 부분 순서 집합은 헤이팅 대수를 이룬다. 즉, 토포스의 내부 논리는 직관 논리이다.

모든 헤이팅 대수는 위상 공간의 열린 집합의 유계 부분 격자와 자연스럽게 동형이며, 여기서 함의 $U\backslash to\; V$는 $(X\backslash setminus\; U)\backslash cup\; V$의 내부로 주어진다. 더 정확하게는, 유계 격자의 소 아이디얼의 스펙트럼 공간이며, 열린 준콤팩트 부분 집합의 격자이다.

더 일반적으로, 헤이팅 대수의 범주는 헤이팅 공간의 범주와 쌍대 동치이다.^[15] 이러한 쌍대성은 유계 분배 격자의 고전적인 스톤 쌍대성을 헤이팅 대수의 (비전체) 부분 범주로 제한한 것으로 볼 수 있다.

또는 헤이팅 대수의 범주는 에사키아 공간의 범주와 쌍대 동치이다. 이것을 에사키아 쌍대성이라고 한다.

8. 추가 정보

• 모든 부울 대수는 헤이팅 대수이며, 이 경우 ''p''→''q''는 ¬''p''∨''q''로 정의된다.
• 최소 원소 0과 최대 원소 1을 갖는 모든 전순서 집합은 헤이팅 대수이다(격자로 간주될 경우). 이 경우 ''p''→''q''는 ''p≤q''일 때 1과 같고, 그렇지 않으면 ''q''와 같다.
• 부울 대수가 아닌 가장 간단한 헤이팅 대수는 {0, 1/2, 1}의 전순서 집합이다(격자로 간주). 이 경우 연산은 다음과 같다:

이 예에서 1/2∨¬(1/2) = 1/2∨(1/2→0) = 1/2∨0 = 1/2는 배중률을 위반한다.

• 모든 위상은 열린 집합 격자의 형태로 완비 헤이팅 대수를 제공한다. 이 경우, 요소 ''A''→''B''는 ''A^c''와 ''B''의 합집합의 내부이다. 여기서 ''A^c''는 여집합을 나타낸다. 모든 완비 헤이팅 대수가 이런 형태를 갖는 것은 아니다. 이러한 문제는 무점 위상수학에서 연구되며, 여기서 완비 헤이팅 대수는 '''프레임''' 또는 '''로컬'''이라고도 한다.
• 모든 내부 대수는 열린 원소의 격자 형태로 헤이팅 대수를 제공한다. 모든 헤이팅 대수는 이 형태를 갖는데, 헤이팅 대수는 자유 부울 확장을 유계 분배 격자로 취하고 이를 이 부울 대수에서 일반화된 위상으로 취급함으로써 부울 대수로 완성될 수 있기 때문이다.
• 린덴바움 대수는 명제적 직관 논리의 헤이팅 대수이다.
• 기초 토포스의 부분 대상 분류자 Ω의 전역 원소는 헤이팅 대수를 형성한다. 이는 토포스에 의해 유도된 직관 고차 논리의 진리값의 헤이팅 대수이다. 더 일반적으로, 토포스 내의 임의의 객체 ''X''의 부분 대상의 집합은 헤이팅 대수를 형성한다.
• 우카시에비치-모이실 대수 (LM_''n'')는 모든 ''n''에 대해 헤이팅 대수이다.^[7] (하지만, 이는 ''n'' ≥ 5에 대해 MV-대수는 아니다^[8]).

참조

_[1] 웹사이트 Pseudo-Boolean algebra - Encyclopedia of Mathematics https://www.encyclop[...]
_[2] 논문 Semantical analysis of intuitionistic logic I North-Holland
_[3] 서적 The Mathematics of Metamathematics Państwowe Wydawnictwo Naukowe (PWN)
_[4] 서적 Boolean valued analysis https://books.google[...] Springer
_[5] 간행물 Brouwer lattice springer
_[6] 서적 Lattices and ordered algebraic structures https://books.google[...] Springer
_[7] 학술지 N-Valued Logics and Łukasiewicz–Moisil Algebras
_[8] 논문 Connections between MV_''n''-algebras and ''n''-valued Łukasiewicz–Moisil algebras—I
_[9] 문서
_[10] 문서
_[11] 학술지 Intuitionistic propositional logic is polynomial-space complete
_[12] 학회자료 The complexity of theorem proving procedures
_[13] 학술지 Undecidability of some topological theories https://www.impan.pl[...]
_[14] 서적 Stone Spaces Cambridge University Press
_[15] 서적 Spectral Spaces Cambridge University Press
_[16] 저널 Die formalen Regeln der intuitionistischen Logik I
_[17] 저널 Die formalen Regeln der intuitionistischen Logik II
_[18] 저널 Die formalen Regeln der intuitionistischen Logik III