概述
在數學中，Heyting 代數是構成對布爾代數的推廣的特殊的偏序集。Heyting 代數為直覺邏輯而提出，它是在其中排中律一般不成立的邏輯。完全Heyting代數是無點拓撲學研究的中心對象。
形式定義
Heyting 代數 H 是滿足如下條件的有界格，對於在 H 中的所有 a 和 b 有最大的 H 元素 x 使得
<math> a \wedge x \le b</math>。
這個元素 x 是 a 關於 b 的相對偽補元(pseudo-complement)，並指示為 <math>a \Rightarrow b</math> (或 <math> a \rightarrow b</math>)。
可以通過如下映射給出等價定義：對於 H 中某個固定的 a，
<math>f_a: H \to H</math> 定義為 <math>f_a(x)=a\wedge x</math>。
有界格 H 是 Heyting 代數，若且唯若所有映射 <math>f_a</math> 都是單調的伽羅瓦連線的下共軛(adjoint)。在這種情況下各自的上共軛 <math>g_a</math> 通過 <math>g_a(x)= (a \Rightarrow x)</math> 給出，這裡的 <math>\Rightarrow</math> 定義同上。
完全Heyting代數是是完全格的 Heyting 代數。
在任何 Heyting 代數中，你可以通過設立 <math>\lnot x = (x \Rightarrow 0)</math> 定義某個元素 x 的偽補元 <math>\lnot x</math>，這裡的 0 是 Heyting 代數的最小元素。
Heyting 代數的一個元素 x 叫做正規的，如果 <math>x=\lnot\lnot x</math>。元素 x 是正規的，若且唯若對於 Heyting 代數的某個元素 y 有 <math>x=\lnot y</math>。
性質
Heyting 代數總是符合分配律。這有時被陳述為公理，但實際上可以從相對偽補元的存在性得到。道理是作為伽羅瓦連線的下共軛，<math>\wedge</math> 保持所有現存的上確界。所以分配律就是 <math>\wedge</math> 對二元最小上界的保持。
進一步的，通過類似的論證，下列無限分配律在任何完全 Heyting 代數中都成立:
<math>x\wedge\bigvee Y = \bigvee \{x\wedge y : y \in Y\}</math>
對於 H 中的任何元素 x 和H 的子集 Y。
不是所有 Heyting 代數都滿足兩個De Morgan 定律。但是，對於所有 Heyting 代數 H 下列陳述都是等價的:
H 滿足兩個 De Morgan 定律。
對於 H 中的所有 x y 有 <math>\lnot(x \wedge y)=\lnot x \vee \lnot y</math>。
對於 H 中的所有 x 有 <math>\lnot x \vee \lnot\lnot x = 1</math>。
對於 H 中的所有 x y 有 <math>\lnot\lnot (x \vee y) = \lnot\lnot x \vee \lnot\lnot y</math>。
H 的一個元素 x 的偽補元是集合 <math>\{ y : y \wedge x = 0\}</math> 的上確界，並且屬於這個集合(就是說，<math>x \wedge \lnot x = 0</math> 成立)。
布爾代數準確的是如下成立的 Heyting 代數：對於所有 x 有 <math> x = \lnot\lnot x</math>，或等價的說，布爾代數準確的是如下成立的 Heyting 代數：對於所有 x 有 <math>x\vee\lnot x=1</math>。在這種情況下，元素 <math>a \Rightarrow b</math> 等價於 <math>\lnot a \vee b</math>。
在任何 Heyting 代數中，最小 0 和最大元素 1 都是正規的。
任何 Heyting 代數的正規元素都構成一個布爾代數。除非 Heyting 代數的所有元素都是正規的，這個布爾代數都不會是這個 Heyting 代數的子格，因為交運算將是不同的。
例子
所有是有界格的全序集合也是 Heyting 代數，在這裡對於不是 0 的所有 a 有 <math>\lnot 0 = 1</math> 和 <math>\lnot a = 0</math>。所有的拓撲都以它的開集格的形式提供完全 Heyting 代數。在這種情況下，元素 <math>A \Rightarrow B</math> 是 <math>A_c</math> 和 B 的並的內部，這裡的 <math>A_c</math> 指示開集 A 的補。不是所有完全 Heyting 代數都有這種形式。這些問題在無點拓撲學中研究，這裡完全 Heyting 代數也叫做 frame 或 locale。
命題直覺邏輯的Lindenbaum 代數是 Heyting 代數。它被定義為所有命題邏輯公式的集合，並通過邏輯蘊涵來排序: 對於任何兩個公式 F 和 G 我們有 <math>F \le G</math> ，若且唯若 <math>F \models G</math>。在這個階段 <math>\le</math> 只是誘發 Heyting 代數所需要的偏序的預序。
套用於直覺邏輯的 Heyting 代數
Arend Heyting (1898年-1980年)自己感興趣於以這種類型的結構來澄清直覺邏輯的基礎地位。Peirce 定律的案例說明了 Heyting 代數的語義角色。沒有簡單的證明能證明 Peirce 定律不能從直覺邏輯的基本定律中推導出來。
Heyting 代數，從邏輯的立場來說，本質上是普通真值系統的一般化。同其他性質一起，最大元素，在邏輯中叫做 <math>\top</math>，是'真'的同義詞，普通二值邏輯系統是 Heyting 代數的最簡單的例子，在這個代數中兩個元素是<math>\top</math>(真)和<math>\bot</math>(假)。用抽象的術語說，兩元素布爾代數也是 Heyting 代數。
經典有效的公式是在這種布爾代數中在對公式的變數的任意可能的真假指派下有 <math>\top</math> 值的公式 — 就是說，它們是在普通真值表意義上的重言式。直覺有效的公式是在任何 Heyting 代數中在對公式變數的值的任何指派下有<math>\top</math>值的公式。
你可以構造在其中 Peirce 定律不總是<math>\top</math>的 Heyting 代數。考慮 Sierpinski 空間的開集(不是布爾代數的 Heyting 代數的最簡單的例子)，並觀察如果我們釋義 P 為 、Q 為 <math>\varnothing</math>，則 Peirce 定律 ((P → Q) → P) → P 的釋義是 <math>\{1\}\ne \{0,1\} = \top</math>。從我們剛才所說的，這不能是直覺推導出來的。詳情參見Curry-Howard同構和類型論。
