在数学中，heyting代数是构成对布尔代数的推广的特殊的偏序集。heyting代数为直觉逻辑而提出，它是在其中排中律一般不成立的逻辑。完全heyting代数是无点拓扑学研究的中心对象。

形式定义
heyting代数h是满足如下条件的有界格，对于在h中的所有a和b有最大的h元素x使得

<math>a\wedgex\leb</math>。
这个元素x是a关于b的相对伪补元(pseudo-complement)，并指示为<math>a\rightarrowb</math>(或<math>a\rightarrowb</math>)。

可以通过如下映射给出等价定义：对于h中某个固定的a，

<math>f_a:h\toh</math>定义为<math>f_a(x)=a\wedgex</math>。
有界格h是heyting代数，当且仅当所有映射<math>f_a</math>都是单调的伽罗瓦连接的下共轭(adjoint)。在这种情况下各自的上共轭<math>g_a</math>通过<math>g_a(x)=(a\rightarrowx)</math>给出，这里的<math>\rightarrow</math>定义同上。

完全heyting代数是是完全格的heyting代数。

在任何heyting代数中，你可以通过设立<math>\lnotx=(x\rightarrow0)</math>定义某个元素x的伪补元<math>\lnotx</math>，这里的0是heyting代数的最小元素。

heyting代数的一个元素x叫做正规的，如果<math>x=\lnot\lnotx</math>。元素x是正规的，当且仅当对于heyting代数的某个元素y有<math>x=\lnoty</math>。

性质
heyting代数总是符合分配律。这有时被陈述为公理，但实际上可以从相对伪补元的存在性得到。道理是作为伽罗瓦连接的下共轭，<math>\wedge</math>保持所有现存的上确界。所以分配律就是<math>\wedge</math>对二元最小上界的保持。

进一步的，通过类似的论证，下列无限分配律在任何完全heyting代数中都成立:

<math>x\wedge\bigveey=\bigvee\{x\wedgey:y\iny\}</math>

对于h中的任何元素x和h的子集y。

不是所有heyting代数都满足两个demorgan定律。但是，对于所有heyting代数h下列陈述都是等价的:

h满足两个demorgan定律。
对于h中的所有xy有<math>\lnot(x\wedgey)=\lnotx\vee\lnoty</math>。
对于h中的所有x有<math>\lnotx\vee\lnot\lnotx=1</math>。
对于h中的所有xy有<math>\lnot\lnot(x\veey)=\lnot\lnotx\vee\lnot\lnoty</math>。
h的一个元素x的伪补元是集合<math>\{y:y\wedgex=0\}</math>的上确界，并且属于这个集合(就是说，<math>x\wedge\lnotx=0</math>成立)。

布尔代数准确的是如下成立的heyting代数：对于所有x有<math>x=\lnot\lnotx</math>，或等价的说，布尔代数准确的是如下成立的heyting代数：对于所有x有<math>x\vee\lnotx=1</math>。在这种情况下，元素<math>a\rightarrowb</math>等价于<math>\lnota\veeb</math>。

在任何heyting代数中，最小0和最大元素1都是正规的。

任何heyting代数的正规元素都构成一个布尔代数。除非heyting代数的所有元素都是正规的，这个布尔代数都不会是这个heyting代数的子格，因为交运算将是不同的。

例子
所有是有界格的全序集合也是heyting代数，在这里对于不是0的所有a有<math>\lnot0=1</math>和<math>\lnota=0</math>。
所有的拓扑都以它的开集格的形式提供完全heyting代数。在这种情况下，元素<math>a\rightarrowb</math>是<math>a_c</math>和b的并的内部，这里的<math>a_c</math>指示开集a的补。不是所有完全heyting代数都有这种形式。这些问题在无点拓扑学中研究，这里完全heyting代数也叫做frame或locale。
命题直觉逻辑的lindenbaum代数是heyting代数。它被定义为所有命题逻辑公式的集合，并通过逻辑蕴涵来排序:对于任何两个公式f和g我们有<math>f\leg</math>，当且仅当<math>f\modelsg</math>。在这个阶段<math>\le</math>只是诱发heyting代数所需要的偏序的预序。
应用于直觉逻辑的heyting代数
arendheyting(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同构和类型论。