พีชคณิตเฮย์ติง (Heyting algebra) คือแลตทิซที่มีขอบเขต ซึ่งประกอบด้วยวัตถุเลขชี้กำลัง ทั้งหมด${\displaystyle H}$

แลตทิซถือเป็นหมวดหมู่ที่การพบกันเป็นผลคูณเงื่อนไขเลขชี้กำลังหมายความว่าสำหรับวัตถุใดๆและในเลขชี้กำลังจะมีวัตถุเพียงหนึ่งเดียวใน${\displaystyle H}$${\displaystyle \wedge }$${\displaystyle Y}$${\displaystyle Z}$${\displaystyle H}$${\displaystyle Z^{Y}}$${\displaystyle H}$

การบ่งชี้แบบ Heyting (มักเขียนโดยใช้หรือเพื่อหลีกเลี่ยงความสับสนกับการใช้ เพื่อระบุมอร์ฟิซึม ) ก็คือเลขชี้กำลัง: เป็นสัญลักษณ์ทางเลือกสำหรับจากนิยามของเลขชี้กำลัง เรามีว่าการบ่งชี้( )เป็นตัวผกผันทางขวาของ meet ( )การเชื่อมโยงนี้สามารถเขียนได้เป็นหรือเขียนให้สมบูรณ์ยิ่งขึ้นได้ดังนี้: ${\displaystyle \Rightarrow }$${\displaystyle \multimap }$${\displaystyle \to }$${\displaystyle Y\ลูกศรขวา Z}$${\displaystyle Z^{Y}}$${\displaystyle {\Rightarrow }:H\times H\to H}$${\displaystyle \wedge :H\times H\to H}$${\displaystyle (-\wedge Y)\dashv (Y\Rightarrow -)}$$${\displaystyle (-\wedge Y):H{\stackrel {\longrightarrow }{\underset {\longleftarrow }{\top }}}H:(Y\Rightarrow -)}$$

สามารถให้นิยามที่เทียบเท่ากันของพีชคณิตเฮย์ติงได้โดยพิจารณาจากแผนที่ดังต่อไปนี้:

$${\displaystyle {\begin{cases}f_{a}\colon H\to H\\f_{a}(x)=a\wedge x\end{cases}}}$$

สำหรับค่าคงที่a บางค่า ในHแลตทิซที่มีขอบเขตHเป็นพีชคณิตเฮย์ติงก็ต่อเมื่อ การแมป f ทุกตัวเป็นตัวผกผันล่างของการเชื่อมต่อกาโลอิส แบบโมโนโทน ในกรณีนี้ ตัวผกผันบนg ที่เกี่ยวข้อง จะกำหนดโดยg ( x ) = a → xโดยที่ → ถูกกำหนดไว้ดังข้างต้น

นิยามอีกประการหนึ่งคือ แลตทิซตกค้าง ที่มีการ ดำเนินการโมโนอิดเป็น ∧ หน่วยโมโนอิดจะต้องเป็นองค์ประกอบสูงสุด 1 คุณสมบัติการสลับที่ของโมโนอิดนี้หมายความว่าค่าตกค้างทั้งสองจะตรงกันเมื่อa → b

กำหนดให้แลตทิซA ที่มีขอบเขต โดยที่สมาชิกที่ใหญ่ที่สุดและเล็กที่สุดคือ 1 และ 0 และการดำเนินการทวิภาค → สิ่งเหล่านี้รวมกันเป็นพีชคณิตเฮย์ติงก็ต่อเมื่อเงื่อนไขต่อไปนี้เป็นจริง:

1. ${\displaystyle a\to a=1}$
2. ${\displaystyle a\wedge (a\to b)=a\wedge b}$
3. ${\displaystyle b\wedge (a\to b)=b}$
4. ${\displaystyle a\to (b\wedge c)=(a\to b)\wedge (a\to c)}$

โดยสมการที่ 4 คือกฎการกระจายสำหรับ →

ลักษณะเฉพาะของพีชคณิตเฮย์ติงนี้ทำให้การพิสูจน์ข้อเท็จจริงพื้นฐานเกี่ยวกับความสัมพันธ์ระหว่างแคลคูลัสเชิงประพจน์แบบสัญชาตญาณนิยมและพีชคณิตเฮย์ติงเป็นไปได้ทันที (สำหรับข้อเท็จจริงเหล่านี้ โปรดดูส่วน " เอกลักษณ์ที่พิสูจน์ได้ " และ " โครงสร้างสากล ") เราควรคิดว่าองค์ประกอบนี้มีความหมายโดยสัญชาตญาณว่า "พิสูจน์ได้ว่าเป็นจริง" เปรียบเทียบกับสัจพจน์ในตรรกศาสตร์แบบสัญชาตญาณนิยม${\displaystyle \top }$

กำหนดให้เซตAมีการดำเนินการทวิภาคสามอย่างคือ →, ∧ และ ∨ และมีสมาชิกที่โดดเด่นสองตัวคือ และแล้วAเป็นพีชคณิตเฮย์ติงสำหรับการดำเนินการเหล่านี้ (และความสัมพันธ์ ≤ ที่กำหนดโดยเงื่อนไขที่ว่าเมื่อa → b = ) ก็ต่อเมื่อเงื่อนไขต่อไปนี้เป็นจริงสำหรับสมาชิกx , yและz ใดๆ ของA :${\displaystyle \bot }$${\displaystyle \top }$${\displaystyle a\leq b}$${\displaystyle \top }$

1. $ถ้า x ≤ y และ y ≤ x แล้ว x = y$
2. $ถ้า ≤ y แล้ว y = √$
3. ${\displaystyle x\leq y\to x,}$
4. ${\displaystyle x\to (y\to z)\leq (x\to y)\to (x\to z),}$
5. ${\displaystyle x\land y\leq x,}$
6. ${\displaystyle x\ที่ดิน y\leq y,}$
7. ${\displaystyle x\leq y\to (x\land y),}$
8. ${\displaystyle x\leq x\lor y,}$
9. ${\displaystyle y\leq x\lor y,}$
10. ${\displaystyle x\to z\leq (y\to z)\to (x\lor y\to z),}$
11. ${\displaystyle \bot \leq x.}$

สุดท้ายนี้ เรากำหนดให้ ¬ xเป็นx → .${\displaystyle \bot }$

เงื่อนไขที่ 1 กล่าวว่าต้องระบุสูตรที่เทียบเท่ากัน เงื่อนไขที่ 2 กล่าวว่าสูตรที่พิสูจน์ได้ว่าเป็นจริงนั้นปิดภายใต้modus ponensเงื่อนไขที่ 3 และ 4 จึง เป็น เงื่อนไข เงื่อนไขที่ 5, 6 และ 7 เป็นเงื่อนไขแบบ " และ  " เงื่อนไขที่ 8, 9 และ 10 เป็นเงื่อนไขแบบ " หรือ  " เงื่อนไข ที่ 11 เป็นเงื่อนไขเท็จ

แน่นอน หากมีการเลือกชุดสัจพจน์ที่แตกต่างออกไปสำหรับตรรกศาสตร์ เราก็สามารถปรับเปลี่ยนสัจพจน์ของเราให้สอดคล้องกันได้

ลำดับบนพีชคณิตเฮย์ติงHสามารถกู้คืนได้จากการดำเนินการ → ดังนี้: สำหรับองค์ประกอบใดๆa , bของHก็ต่อเมื่อa → b = 1 เท่านั้น${\displaystyle \leq }$${\displaystyle a\leq b}$

ตรงกันข้ามกับตรรกศาสตร์หลายค่าบางประเภทพีชคณิตเฮย์ติงมีคุณสมบัติร่วมกับพีชคณิตบูลีนดังต่อไปนี้: ถ้าการปฏิเสธมีจุดตรึง (กล่าวคือ ¬ a = aสำหรับบางค่าa ) แล้วพีชคณิตเฮย์ติงจะเป็นพีชคณิตเฮย์ติงแบบหนึ่งองค์ประกอบที่ไม่มีความสำคัญ

เมื่อกำหนดสูตรของแคลคูลัสเชิงประพจน์ (โดยใช้ตัวเชื่อมและค่าคงที่ 0 และ 1 นอกเหนือจากตัวแปร) เป็นที่พิสูจน์ได้ตั้งแต่แรกเริ่มในการศึกษาพีชคณิตของเฮย์ติงว่า เงื่อนไขสองข้อต่อไปนี้เทียบเท่ากัน:${\displaystyle F(A_{1},A_{2},\ldots ,A_{n})}$${\displaystyle \land ,\lor ,\lnot ,\to }$

1. สูตรFพิสูจน์ได้ว่าเป็นจริงในแคลคูลัสเชิงประพจน์แบบสัญชาตญาณนิยม
2. เอกลักษณ์นี้เป็นจริงสำหรับพีชคณิตเฮย์ติงH ใดๆ และสำหรับองค์ประกอบใดๆ${\displaystyle F(a_{1},a_{2},\ldots ,a_{n})=1}$${\displaystyle a_{1},a_{2},\ldots ,a_{n}\in H}$

การอนุมานเชิงอภิมานที่ว่าข้อแรกบ่งชี้ถึงข้อที่สอง ซึ่งเราจะเขียนว่า1 ⇒ 2นั้น มีประโยชน์อย่างยิ่งและเป็นวิธีปฏิบัติหลักในการพิสูจน์เอกลักษณ์ในพีชคณิตเฮย์ติง ในทางปฏิบัติ เรามักใช้ทฤษฎีบทการหักล้างในการพิสูจน์ดังกล่าว

เนื่องจากสำหรับaและb ใดๆ ในพีชคณิตเฮย์ติงHเราจะได้ก็ต่อเมื่อa → b = 1 เท่านั้น ดังนั้นจึงสรุปได้จาก1 ⇒ 2ว่าเมื่อใดก็ตามที่สูตรF → Gพิสูจน์ได้ว่าเป็นจริง เราจะได้สำหรับพีชคณิตเฮย์ติงH ใดๆ และสมาชิกใดๆ(สรุปได้จากทฤษฎีบทการหักล้างว่าF → Gพิสูจน์ได้ (โดยไม่มีเงื่อนไข) ก็ต่อเมื่อGพิสูจน์ได้จากFนั่นคือ ถ้าGเป็นผลลัพธ์ที่พิสูจน์ได้จากF ) โดยเฉพาะอย่างยิ่ง ถ้าFและGสมมูลกันที่พิสูจน์ได้แล้วเนื่องจาก ≤ เป็นความสัมพันธ์เชิงลำดับ${\displaystyle a\leq b}$${\displaystyle F(a_{1},a_{2},\ldots ,a_{n})\leq G(a_{1},a_{2},\ldots ,a_{n})}$${\displaystyle a_{1},a_{2},\ldots ,a_{n}\in H}$${\displaystyle F(a_{1},a_{2},\ldots ,a_{n})=G(a_{1},a_{2},\ldots ,a_{n})}$

1 ⇒ 2 สามารถพิสูจน์ได้โดยการตรวจสอบสัจพจน์เชิงตรรกะของระบบการพิสูจน์และตรวจสอบว่าค่าของสัจพจน์เหล่านั้นเป็น 1 ในพีชคณิตเฮย์ติงใดๆ จากนั้นตรวจสอบว่าการประยุกต์ใช้กฎการอนุมานกับนิพจน์ที่มีค่าเป็น 1 ในพีชคณิตเฮย์ติงส่งผลให้ได้นิพจน์ที่มีค่าเป็น 1 ตัวอย่างเช่น ให้เราเลือกใช้ระบบการพิสูจน์ที่มีmodus ponensเป็นกฎการอนุมานเพียงอย่างเดียว และมีสัจพจน์แบบฮิลเบิร์ตตามที่ระบุไว้ในIntuitionistic logic#Axiomatizationข้อเท็จจริงที่จะต้องตรวจสอบจะตามมาโดยตรงจากนิยามของพีชคณิตเฮย์ติงที่คล้ายกับสัจพจน์ที่กล่าวไว้ข้างต้น

1 ⇒ 2 ยังเสนอวิธีการพิสูจน์ว่าสูตรประพจน์บางอย่าง แม้จะเป็นสัจนิรันดร์ในตรรกศาสตร์คลาสสิก แต่ก็ไม่สามารถพิสูจน์ได้ในตรรกศาสตร์ประพจน์แบบสัญชาตญาณนิยม ในการพิสูจน์ว่าสูตรบางสูตรไม่สามารถพิสูจน์ได้นั้น เพียงพอที่จะแสดงให้เห็นพีชคณิตเฮย์ติงHและองค์ประกอบต่างๆ ที่ทำให้${\displaystyle F(A_{1},A_{2},\ldots ,A_{n})}$${\displaystyle a_{1},a_{2},\ldots ,a_{n}\in H}$${\displaystyle F(a_{1},a_{2},\ldots ,a_{n})\neq 1}$

หากต้องการหลีกเลี่ยงการกล่าวถึงตรรกศาสตร์ ในทางปฏิบัติจึงจำเป็นต้องพิสูจน์เป็นบทพิสูจน์ย่อยของทฤษฎีบทการหักล้างที่ใช้ได้กับพีชคณิตเฮย์ติง: สำหรับองค์ประกอบใดๆa , bและcของพีชคณิตเฮย์ติงHเราจะได้ว่า${\displaystyle (a\land b)\to c=a\to (b\to c)}$

สำหรับข้อมูลเพิ่มเติมเกี่ยวกับนัยยะแฝง 2 ⇒ 1 โปรดดูส่วน " โครงสร้างสากล " ด้านล่าง

พีชคณิตเฮย์ติงมีคุณสมบัติการแจกแจง เสมอ โดยเฉพาะอย่างยิ่ง เราจะมีเอกลักษณ์เหล่านี้เสมอ

1. ${\displaystyle a\wedge (b\vee c)=(a\wedge b)\vee (a\wedge c)}$
2. ${\displaystyle a\vee (b\wedge c)=(a\vee b)\wedge (a\vee c)}$

กฎการกระจายบางครั้งถูกระบุว่าเป็นสัจพจน์ แต่ในความเป็นจริงแล้วมันเป็นผลมาจากการมีอยู่ของส่วนเติมเต็มเทียมเชิงสัมพัทธ์ เหตุผลก็คือ เนื่องจากเป็นตัวผกผันล่างของการเชื่อมต่อกาโลอิสจึง รักษา ค่าสูงสุดที่มีอยู่ทั้งหมดไว้ได้การกระจายตัวนั้นก็คือการรักษาค่าสูงสุดทวิภาคโดยนั่นเอง${\displaystyle \wedge }$${\displaystyle \wedge }$

ด้วยเหตุผลที่คล้ายกันกฎการกระจายอนันต์ต่อ ไปนี้ จึงใช้ได้กับพีชคณิต Heyting ที่สมบูรณ์ใดๆ:

$${\displaystyle x\wedge \bigvee Y=\bigvee \{x\wedge y\mid y\in Y\}}$$

สำหรับองค์ประกอบx ใดๆ ในHและเซตย่อยY ใดๆ ของHในทางกลับกัน แลตทิซสมบูรณ์ใดๆ ที่สอดคล้องกับกฎการกระจายอนันต์ข้างต้น จะเป็นพีชคณิตเฮย์ติงสมบูรณ์ โดย มีการดำเนินการส่วนเติมเต็มเทียมสัมพัทธ์$${\displaystyle a\to b=\bigvee \{c\mid a\land c\leq b\}}$$

สมาชิกxของพีชคณิตเฮย์ติงHเรียกว่าสมาชิกปกติถ้าเงื่อนไขสมมูลอย่างใดอย่างหนึ่งต่อไปนี้เป็นจริง:

1. x = ¬¬ x .
2. x = ¬ yสำหรับyบาง ค่า ในH

ความเท่าเทียมกันของ เงื่อนไขเหล่านี้สามารถกล่าวใหม่ได้ง่ายๆ ว่าเป็นเอกลักษณ์ ¬¬¬ x = ¬ xซึ่งใช้ได้กับx ทุกตัว ในH

สมาชิกxและyในพีชคณิตเฮย์ติงHเรียกว่าส่วนเติมเต็มซึ่งกันและกัน ถ้าx ∧ y = 0 และx ∨ y = 1 ถ้ามีอยู่จริงy ใดๆ ก็ตาม จะมีค่าเพียงหนึ่งเดียวและต้องเท่ากับ ¬ xเราเรียกสมาชิกx ว่ามีส่วน เติมเต็มถ้ามันยอมรับส่วนเติมเต็มได้ เป็นความจริงที่ว่าถ้าxมีส่วนเติมเต็มแล้ว ¬ x ก็มีส่วนเติมเต็มเช่นกัน และดังนั้นxและ ¬ xจึงเป็นส่วนเติมเต็มซึ่งกันและกัน อย่างไรก็ตาม ที่น่าสับสนคือ แม้ว่าxจะไม่มีส่วนเติมเต็ม แต่ ¬ xก็อาจมีส่วนเติมเต็มได้ (ไม่เท่ากับx ) ในพีชคณิตเฮย์ติงใดๆ สมาชิก 0 และ 1 เป็นส่วนเติมเต็มซึ่งกันและกัน ตัวอย่างเช่น เป็นไปได้ที่ ¬ xจะเป็น 0 สำหรับทุกxที่แตกต่างจาก 0 และเป็น 1 ถ้าx = 0 ซึ่งในกรณีนี้ 0 และ 1 เป็นสมาชิกปกติเพียงสองตัวเท่านั้น

องค์ประกอบเสริมใดๆ ของพีชคณิตเฮย์ติงถือเป็นจำนวนปกติ แม้ว่าในทางกลับกันจะไม่เป็นจริงโดยทั่วไปก็ตาม โดยเฉพาะอย่างยิ่ง 0 และ 1 เป็นจำนวนปกติเสมอ

สำหรับพีชคณิตเฮย์ติงH ใดๆ เงื่อนไขต่อไปนี้ถือว่าเทียบเท่ากัน:

1. Hคือพีชคณิตบูลีน ;
2. xทุกตัวในHเป็นแบบปกติ^{[ 11 ]}
3. xทุกตัวในHจะถูกเติมเต็ม^{[ 12 ]}

ในกรณีนี้ องค์ประกอบa → bจะเท่ากับ¬ a ∨ b

องค์ประกอบปกติ (หรือองค์ประกอบเสริม) ของพีชคณิตเฮย์ติงH ใดๆ จะประกอบกันเป็นพีชคณิตบูลีนH (หรือH ) ซึ่งการดำเนินการ ∧, ¬ และ → รวมถึงค่าคงที่ 0 และ 1 จะตรงกับของHในกรณีของH การดำเนินการ ∨ ก็เหมือนกันด้วย ดังนั้นH จึงเป็นพีชคณิตย่อยของHอย่างไรก็ตาม โดยทั่วไปแล้วH จะไม่เป็นพีชคณิตย่อยของHเพราะการดำเนินการเชื่อม ∨ อาจแตกต่างจาก ∨ สำหรับx , y ∈ H เราจะได้x ∨ y = ¬(¬ x ∧ ¬ y )ดูเงื่อนไขที่จำเป็นและเพียงพอด้านล่างเพื่อให้ ∨ ตรงกับ ∨

กฎของเดอ มอร์แกนข้อใดข้อหนึ่งจากสองข้อนี้จะเป็นจริงในพีชคณิตของเฮย์ติงทุกชุด กล่าวคือ

$${\displaystyle \forall x,y\in H:\qquad \lnot (x\vee y)=\lnot x\wedge \lnot y.}$$

อย่างไรก็ตาม กฎของเดอ มอร์แกนอีกข้อหนึ่งนั้นไม่ได้ใช้ได้เสมอไป เราจึงมีกฎของเดอ มอร์แกนที่อ่อนกว่าแทน:

$${\displaystyle \forall x,y\in H:\qquad \lnot (x\wedge y)=\lnot \lnot (\lnot x\vee \lnot y).}$$

ข้อความต่อไปนี้เทียบเท่ากันสำหรับพีชคณิต Heyting H ทั้งหมด :

1. Hเป็นไปตามกฎของเดอ มอร์แกนทั้งสองข้อ
2. ${\displaystyle \lnot (x\wedge y)=\lnot x\vee \lnot y{\mbox{ for all }}x,y\in H,}$
3. ${\displaystyle \lnot (x\wedge y)=\lnot x\vee \lnot y{\mbox{ for all regular }}x,y\in H,}$
4. ${\displaystyle \lnot \lnot (x\vee y)=\lnot \lnot x\vee \lnot \lnot y{\mbox{ for all }}x,y\in H,}$
5. ${\displaystyle \lnot \lnot (x\vee y)=x\vee y{\mbox{ for all regular }}x,y\in H,}$
6. ${\displaystyle \lnot (\lnot x\wedge \lnot y)=x\vee y{\mbox{ for all regular }}x,y\in H,}$
7. ${\displaystyle \lnot x\vee \lnot \lnot x=1{\mbox{ for all }}x\in H.}$

เงื่อนไขที่ 2 คือกฎของเดอ มอร์แกนอีกข้อหนึ่ง เงื่อนไขที่ 6 กล่าวว่า การดำเนินการร่วม ∨ บนพีชคณิตบูลีนH ขององค์ประกอบปกติของHตรงกับการดำเนินการ ∨ ของH เงื่อนไขที่ 7 ระบุว่า องค์ประกอบปกติทุกตัวได้รับการเติมเต็ม กล่าวคือH = H

เราพิสูจน์ความสมมูล เห็นได้ชัดว่าการบ่งชี้เชิงอภิมาน1 ⇒ 2, 2 ⇒ 3และ4 ⇒ 5นั้นเป็นไปอย่างชัดเจน ยิ่งไปกว่านั้น3 ⇔ 4และ5 ⇔ 6เป็นผลมาจากการใช้กฎของเดอ มอร์แกนข้อแรกและนิยามขององค์ประกอบปกติ เราแสดงให้เห็นว่า6 ⇒ 7โดยการใช้ ¬ xและ ¬¬ xแทนxและyใน 6 และใช้เอกลักษณ์a ∧ ¬ a = 0สังเกตว่า2 ⇒ 1เป็นผลมาจากกฎของเดอ มอร์แกนข้อแรก และ7 ⇒ 6เป็นผลมาจากข้อเท็จจริงที่ว่าการดำเนินการรวม ∨ บนพีชคณิตย่อยH เป็นเพียงการจำกัดของ ∨ ไปยังH โดยคำนึงถึงลักษณะเฉพาะที่เราได้ให้ไว้ของเงื่อนไข 6 และ 7 การบ่งชี้เชิงเมตา5 ⇒ 2เป็นผลลัพธ์ที่ชัดเจนของกฎของเดอ มอร์แกนแบบอ่อน โดยใช้ ¬ xและ ¬ yแทนxและyใน 5

พีชคณิตเฮย์ติงที่ตรงตามคุณสมบัติข้างต้นมีความสัมพันธ์กับตรรกศาสตร์เดอ มอร์แกนในลักษณะเดียวกับที่พีชคณิตเฮย์ติงโดยทั่วไปมีความสัมพันธ์กับตรรกศาสตร์แบบสัญชาตญาณนิยม

กำหนดให้พีชคณิตเฮย์ติงสองตัวH และH และฟังก์ชันf  : H → H เรากล่าวว่าƒเป็นมอร์ฟิซึมของพีชคณิตเฮย์ติง ถ้าสำหรับสมาชิกxและy ใดๆ ในH เรามี:

1. ${\displaystyle f(0)=0,}$
2. ${\displaystyle f(x\land y)=f(x)\land f(y),}$
3. ${\displaystyle f(x\lor y)=f(x)\lor f(y),}$
4. ${\displaystyle f(x\to y)=f(x)\to f(y),}$

จากเงื่อนไขสามข้อสุดท้ายข้อใดข้อหนึ่ง (2, 3 หรือ 4) จะได้ว่าfเป็นฟังก์ชันเพิ่มขึ้น นั่นคือf ( x ) ≤ f ( y )เมื่อใดก็ตามที่x ≤ y

สมมติว่าH และH เป็นโครงสร้างที่มีการดำเนินการ →, ∧, ∨ (และอาจรวมถึง ¬) และค่าคงที่ 0 และ 1 และfเป็นฟังก์ชันทั่วถึงจากH ไปยังH ที่มีคุณสมบัติข้อ 1 ถึง 4 ข้างต้น ถ้าH เป็นพีชคณิตเฮย์ติงแล้วH ก็เป็นพีชคณิตเฮย์ติงด้วยเช่น กัน นี่เป็นผลมาจากการจำแนกลักษณะของพีชคณิตเฮย์ติงว่าเป็นแลตทิซที่มีขอบเขต (ซึ่งคิดว่าเป็นโครงสร้างพีชคณิตมากกว่าเซตที่มีลำดับบางส่วน) โดยมีการดำเนินการ → ที่สอดคล้องกับเอกลักษณ์บางประการ

แผนที่เอกลักษณ์f ( x ) = xจากพีชคณิตเฮย์ติงใดๆ ไปยังตัวมันเองเป็นมอร์ฟิซึม และมอร์ฟิซึมประกอบg ∘ f ของมอร์ฟิซึม fและgสองตัวใดๆ ก็เป็นมอร์ฟิซึมเช่นกัน ดังนั้น พีชคณิตเฮย์ติงจึงก่อตัวเป็นหมวดหมู่

เมื่อกำหนดพีชคณิตเฮย์ติงHและพีชคณิตย่อยH ใดๆ แล้ว การแมปการรวมi  : H → Hถือเป็นมอร์ฟิซึม

สำหรับพีชคณิตเฮย์ติงH ใดๆ แผนที่x ↦ ¬¬ xกำหนดมอร์ฟิซึมจากHไปยังพีชคณิตบูลีนขององค์ประกอบปกติH โดยทั่วไปแล้วนี่ไม่ใช่ มอร์ฟิซึมจาก H ไปยังตัวมันเอง เนื่องจากโอเป อเรชันการรวมของH อาจแตกต่างจากของH

การบ่งชี้เชิงอภิมาน2 ⇒ 1ในหัวข้อ " เอกลักษณ์ที่พิสูจน์ได้ " ได้รับการพิสูจน์โดยการแสดงให้เห็นว่าผลลัพธ์ของการสร้างต่อไปนี้เป็นพีชคณิตเฮย์ติงเอง:

1. พิจารณาเซตL ของสูตร เชิงประพจน์ในตัวแปรA , A ,..., A
2. กำหนดให้Lมีลำดับก่อนหน้า ≼ โดยนิยามF ≼ Gถ้าG เป็น ผลลัพธ์เชิงตรรกะ (แบบสัญชาตญาณนิยม) ของFกล่าวคือ ถ้าGสามารถพิสูจน์ได้จากFเป็นที่แน่ชัดว่า ≼ เป็นลำดับก่อนหน้า
3. พิจารณาความสัมพันธ์สมมูลF ~ Gที่เกิดจากลำดับก่อนหน้า F≼G (ความสัมพันธ์นี้กำหนดโดยF ~ Gก็ต่อเมื่อF ≼ GและG ≼ F เท่านั้น ในความเป็นจริง ~ คือความสัมพันธ์ของความสมมูลเชิงตรรกะ (แบบสัญชาตญาณนิยม))
4. ให้H เป็นเซตผลหารL /~ นี่จะเป็นพีชคณิต Heyting ที่ต้องการ
5. เราเขียน [ F ] แทนชั้นสมมูลของสูตรFการดำเนินการ →, ∧, ∨ และ ¬ ถูกกำหนดไว้อย่างชัดเจนบนLตรวจสอบว่าสูตรFและG ที่กำหนดให้ ชั้นสมมูล [ F → G ], [ F ∧ G ], [ F ∨ G ] และ [¬ F ] ขึ้นอยู่กับ [ F ] และ [ G ] เท่านั้น สิ่งนี้กำหนดการดำเนินการ →, ∧, ∨ และ ¬ บนเซตผลหารH = L /~ นอกจากนี้ กำหนดให้ 1 เป็นชั้นของข้อความที่พิสูจน์ได้ว่าเป็นจริง และกำหนด 0=[⊥]
6. ตรวจสอบว่าH พร้อมกับการดำเนินการเหล่านี้ เป็นพีชคณิตเฮย์ติงหรือไม่ เราทำเช่นนี้โดยใช้คำจำกัดความแบบสัจพจน์ของพีชคณิตเฮย์ติงH สอดคล้องกับเงื่อนไข THEN-1 ถึง FALSE เพราะสูตรทั้งหมดในรูปแบบที่กำหนดเป็นสัจพจน์ของตรรกะแบบสัญชาตญาณนิยม MODUS-PONENS เป็นผลมาจากข้อเท็จจริงที่ว่า ถ้าสูตร ⊤→ Fพิสูจน์ได้ว่าเป็นจริง โดยที่ ⊤ พิสูจน์ได้ว่าเป็นจริง แล้วFก็พิสูจน์ได้ว่าเป็นจริงเช่นกัน (โดยการประยุกต์ใช้กฎการอนุมานแบบ modus ponens) สุดท้าย EQUIV เป็นผลมาจากข้อเท็จจริงที่ว่า ถ้าF → GและG → Fพิสูจน์ได้ว่าเป็นจริงทั้งคู่ แล้วFและGก็พิสูจน์ได้จากกันและกัน (โดยการประยุกต์ใช้กฎการอนุมานแบบ modus ponens) ดังนั้น [ F ]=[ G ]

ตามนิยามแบบสัจพจน์ของพีชคณิตเฮย์ติง เรากำหนด ≤ บนH โดยเงื่อนไขที่ว่าx ≤ yก็ต่อเมื่อx → y = 1 เท่านั้น เนื่องจากตามทฤษฎีบทการหักล้างสูตรF → Gเป็นจริงที่พิสูจน์ได้ก็ต่อเมื่อGสามารถพิสูจน์ได้จากFดังนั้นจึงสรุปได้ว่า [ F ]≤[ G ] ก็ต่อเมื่อ F≼G กล่าวอีกนัยหนึ่ง ≤ คือความสัมพันธ์ลำดับบนL /~ ที่เกิดจากลำดับก่อนหน้า ≼ บนL

อันที่จริง การสร้างข้างต้นสามารถดำเนินการได้สำหรับชุดตัวแปรใดๆ{ A   : i ∈ I } (อาจเป็นอนันต์) ด้วยวิธีนี้ เราจะได้ พีชคณิตเฮย์ติง อิสระบนตัวแปร { A } ซึ่งเราจะใช้สัญลักษณ์H อีกครั้ง พีชคณิตนี้เป็นอิสระในแง่ที่ว่า เมื่อกำหนดพีชคณิตเฮย์ติงH ใดๆ พร้อมกับตระกูลขององค์ประกอบ⟨ a : i ∈ I ⟩แล้ว จะมีมอร์ฟิซึมf : H → Hที่ไม่ซ้ำ กันเพียงหนึ่งเดียว ที่ สอดคล้องกับ f ([ A ])= a ความเป็นเอกลักษณ์ของfนั้นมองเห็นได้ไม่ยาก และการมีอยู่ของมันเป็นผลมาจากการบ่งชี้เชิงอภิมาน1 ⇒ 2ของส่วน " เอกลักษณ์ที่พิสูจน์ได้ " ข้างต้น ในรูปแบบของบทสรุปที่ว่า เมื่อใดก็ตามที่FและGเป็นสูตรที่เทียบเท่ากันที่พิสูจน์ได้F (⟨ a ⟩)= G (⟨ a ⟩ ) สำหรับตระกูลขององค์ประกอบ ⟨ a ⟩ ใดๆ ในH

เมื่อกำหนดชุดสูตรTในตัวแปร { A } ซึ่งมองว่าเป็นสัจพจน์ การสร้างแบบเดียวกันนี้สามารถดำเนินการได้โดยสัมพันธ์กับความสัมพันธ์F ≼ Gที่กำหนดบนLซึ่งหมายความว่าGเป็นผลลัพธ์ที่พิสูจน์ได้ของFและชุดสัจพจน์Tให้เราใช้สัญลักษณ์H แทน พีชคณิตเฮย์ติงที่ได้มา จากนั้นH จะมีคุณสมบัติสากลเช่นเดียวกับH ข้างต้น แต่สัมพันธ์กับพีชคณิตเฮย์ติงHและตระกูลขององค์ประกอบ ⟨ a ⟩ ที่มีคุณสมบัติว่าJ (⟨ a ⟩)=1 สำหรับสัจพจน์J (⟨ A ⟩ ) ใดๆ ในT (โปรดทราบว่าH เมื่อพิจารณาร่วมกับตระกูลขององค์ประกอบ ⟨[ A ⟩ ก็มีคุณสมบัตินี้เช่นกัน) การมีอยู่และความเป็นเอกลักษณ์ของมอร์ฟิซึมได้รับการพิสูจน์ในลักษณะเดียวกับH ยกเว้นว่าต้องแก้ไขเมตาอิมพลีเมนต์1 ⇒ 2ใน " เอกลักษณ์ที่พิสูจน์ได้ " โดยที่ 1 อ่านว่า "พิสูจน์ได้ว่าเป็นจริงจาก T " และ 2 อ่านว่า "องค์ประกอบใดๆa , a ,..., a ในH ที่สอดคล้องกับสูตรของ T "

พีชคณิตเฮย์ติงH ที่เราเพิ่งนิยามไปนั้น สามารถมองได้ว่าเป็นผลหารของพีชคณิตเฮย์ติงอิสระH บนเซตตัวแปรเดียวกัน โดยการใช้คุณสมบัติสากลของH ที่เกี่ยวข้องกับH และตระกูลขององค์ประกอบ ⟨[ A ]⟩

พีชคณิตเฮย์ติงทุกตัวสมสัณฐานกับพีชคณิตเฮย์ติงในรูปแบบH เพื่อดูสิ่งนี้ ให้Hเป็นพีชคณิตเฮย์ติงใดๆ และให้⟨ a : i ∈ I ⟩เป็นตระกูลของสมาชิกที่สร้างH (ตัวอย่างเช่น ตระกูลฟังก์ชันทั่วถึงใดๆ) ทีนี้ลองพิจารณาเซตTของสูตรJ (⟨ A ⟩) ในตัวแปร⟨ A : i ∈ I ⟩โดยที่J (⟨ a ⟩)=1 จากนั้นเราจะได้มอร์ฟิซึมf : H → HโดยคุณสมบัติสากลของH ซึ่งเห็นได้ชัดว่าเป็นฟังก์ชันทั่วถึง การแสดงว่า fเป็นฟังก์ชันหนึ่งต่อหนึ่งนั้นไม่ใช่เรื่องยาก

โครงสร้างที่เราเพิ่งกล่าวมานี้มีบทบาทที่คล้ายคลึงกันอย่างยิ่งกับพีชคณิตเฮย์ติง (Heyting algebras) เช่นเดียวกับพีชคณิตลินเดนบอม (Lindenbaum algebras)ที่มีบทบาทกับ พีชคณิตบู ลีน (Boolean algebras ) อันที่จริง พีชคณิตลินเดนบอมB ในตัวแปร { A } ที่เกี่ยวข้องกับสัจพจน์T ก็คือ H ของเรานั่นเองโดยที่T คือเซตของสูตรทั้งหมดในรูปแบบ ¬¬ F → Fเนื่องจากสัจพจน์เพิ่มเติมของT เป็นเพียงสัจพจน์เดียวที่จำเป็นต้องเพิ่มเข้าไปเพื่อให้สามารถพิสูจน์สัจนิรันดร์แบบคลาสสิกทั้งหมดได้