Lihat sumber Aljabar Heyting

Dalam [[matematika]], sebuah '''Aljabar Heyting''' (juga dikenal sebagai '''aljabar pseudo-Boolean'''<ref>https://www.encyclopediaofmath.org/index.php/Pseudo-Boolean_algebra</ref>) adalah [[Kekisi (urutan)#Kisi berbatas|kekisi berbatas]], dengan operasi sambungan dan pertemuan yang tertulis ∨ dan ∧ dan dengan elemen terkecil 0 dan elemen terbesar 1, dilengkapi dengan operasi biner ''a'' → ''b'' dari ''implikasi'' sedemikian rupa maka (''c'' ∧ ''a'') ≤ ''b'' adalah ekuivalen ''c'' ≤ (''a'' → ''b''). Dari sudut pandang logika, ''A'' → ''B'' adalah definisi dengan proposisi terlemah yang [[modus ponens]], pada kaidah inferensi ''A'' → ''B'', ''A'' ⊢ ''B'' yang merupakan kesan. Seperti [[Aljabar Boolean (struktur)|Aljabar Boolean]], aljabar Heyting sebagai bentuk [[varietas (aljabar universal)|varietas]] dapat diaksiomatis dengan persamaan hingga. Aljabar Heyting diperkenalkan oleh {{harvs|txt|authorlink= Arend Heyting|first=Arend|last= Heyting|year=1930}} untuk memformalkan [[logika intuisi]].

Sebagai kekisi, aljabar Heyting merupakan [[kekisi distributif|distributif]]. Setiap aljabar Boolean adalah aljabar Heyting ketika ''a'' → ''b'' didefinisikan sebagai ¬''a'' ∨ ''b'', seperti halnya setiap [[Kelengkapan (teori orde)|kelengkapan]] [[kekisi distributif]] yang memenuhi satu sisi [[Distributif (teori tatanan)#Hukum distributif untuk kisi lengkap|hukum distributif tak hingga]] ''a'' → ''b'' diambil sebagai [[supremum]] dari himpunan semua ''c'' yang sebagai ''c'' ∧ ''a'' ≤ ''b''. Dalam kasus hingga, setiap kekisi distributif tak kosong, khususnya setiap tak kosong hingga [[urutan total#Kaidah|kaidah]], secara otomatis kelengkapan dan sepenuhnya adalah distributif, dan karenanya dinamakan sebagai aljabar Heyting.

Ini mengikuti dari definisi bahwa 1 ≤ 0 → ''a'', sesuai dengan intuisi bahwa setiap proposisi ''a'' tersirat oleh kontradiksi 0.  Meskipun operasi negasi ¬''a'' bukan bagian dari definisi, maka hal itu didefinisikan sebagai ''a'' → 0. Konten intuitif dari ¬''a'' adalah proposisi yang mengasumsikan ''a'' yang disebabkan terjadinya kontradiksi. Definisi tersebut menyiratkan bahwa ''a'' ∧ ¬''a'' = 0. Selanjutnya dapat ditunjukkan bahwa ''a'' ≤ ¬¬''a'', sebaliknya ¬¬''a'' ≤ ''a'' tidak semua benar secara umum, yaitu [[eliminasi negasi ganda]] yang tidak berlaku secara umum dalam aljabar Heyting.

Aljabar Heyting menggeneralisasi aljabar Boolean dalam arti bahwa aljabar Heyting memenuhi ''a'' ∨ ¬''a'' = 1 ([[pengecualian tengah]]), ekuivalen ¬¬''a'' = ''a'' ([[eliminasi negasi ganda]]), adalah aljabar Boolean. Elemen-elemen dari aljabar Heyting ''H'' dari bentuk ¬''a'' terdiri dari kisi Boolean, tetapi secara umum ini bukan [[subaljabar]] dari ''H'' (lihat [[#Elemen Reguler dan kelengkapan|di bawah]]).

Aljabar Heyting berfungsi sebagai model aljabar proposisional [[logika intuisi]] dengan cara yang sama dengan model aljabar Boolean proposisional [[logika klasik]]. Logika internal dari [[topos elementer]] didasarkan pada aljabar Heyting dari [[subobjek]] dari [[objek terminal]] 1 yang diurutkan dengan penyertaan, ekuivalen morfisme dari 1 ke [[pengklasifikasi subobbjek]].

[[Himpunan terbuka]]sdari [[ruang topologi]] sebagai bentuk [[kelengkapan aljabar Heyting]]. Kelengkapan aljabar Heyting dengan demikian menjadi objek utama studi dalam [[topologi tanpa titik]].

Setiap aljabar Heyting yang himpunan elemen non-terbesarnya memiliki elemen terbesar (dan sebagai bentuk aljabar Heyting lainnya) adalah [[Aljabar irreduksi tak langsung|irreduksi tak langsung]], dimana setiap aljabar Heyting dibuat secara irreduksi secara sublangsung dengan menggabungkan elemen terbesar yang baru. Oleh karena itu, bahkan di antara aljabar Heyting hingga, yang terdiri dari tak hingga yang tidak direduksi secara sublangsung, tidak ada dua di antaranya memiliki teori persamaan yang sama. Oleh karena itu, tidak ada himpunan hingga aljabar Heyting yang dapat menyediakan semua contoh tandingan untuk non-hukum aljabar Heyting. Ini sangat kontras dengan aljabar Boolean, yang satu-satunya yang tidak direduksi secara sublangsung adalah dua elemen dengan cukup untuk semua contoh tandingan untuk non-hukum aljabar Boolean, dasar untuk metode keputusan [[tabel kebenaran]] sederhana. Namun demikian, dapat ditentukan apakah persamaan berlaku untuk semua aljabar Heyting.<ref name="Kripke63">Kripke, S. A.: 1965, 'Analisis semantik logika intuisionistik I'. Dalam: J. N. Crossley dan M. A. E. Dummett (eds.): Sistem Formal dan Fungsi Rekursif. Amsterdam: Belanda Utara, hlm. 92–130.</ref>

Aljabar Heyting terkadang menggunakan '''aljabar semu-Boolean''',<ref name="Rasiowa-Sikorski">{{cite book|author1=Helena Rasiowa|author2=Roman Sikorski|title=The Mathematics of Metamathematics|year=1963 |publisher=Państwowe Wydawnictwo Naukowe (PWN)|pages=54–62, 93–95, 123–130}}</ref> atau bahkan '''kekisi Brouwer''',<ref name="KusraevKutateladze1999">{{cite book|author1=A. G. Kusraev|author2=Samson Semenovich Kutateladze|title=Boolean valued analysis|url=https://books.google.com/books?id=MzVXq3LRHOYC&pg=PA12 |year=1999 |publisher=Springer|isbn=978-0-7923-5921-0|page=12}}</ref> meskipun istilah yang terakhir mungkin menunjukkan definisi ganda,<ref>{{springer | title=Brouwer lattice  | id= b/b017660  | last= Yankov  | first= V.A.}}</ref> atau memiliki arti yang sedikit lebih umum.<ref name="Blyth2005">{{cite book|author=Thomas Scott Blyth|title=Lattices and ordered algebraic structures|url=https://books.google.com/books?id=WgROkcmTxG4C&pg=PA151 |year=2005 |publisher=Springer |isbn=978-1-85233-905-0|page=151}}</ref>

== Definisi formal ==
Aljabar Heyting ''H'' adalah [[kekisi (tatanan)#Kekisi sebagai pohimpunan|kisi hingga]], maka untuk semua ''a'' dan ''b'' dalam ''H'' terdapat nilai terbesar elemen ''x'' dari ''H'' sedemikian rupa sehingga

:<math> a \wedge x \le b.</math>

Elemen ini adalah '''pseudo-kelengkapan relatif''' dari ''a'' dihubungkan dengan ''b'', dan dilambangkan sebagai ''a''→''b''. Kita menulis 1 dan 0 untuk elemen terbesar dan terkecil dari ''H''.

Dalam aljabar Heyting, kita mendefinisikan '''[[pseudo-kelengkapan]]''' ¬''a'' dari elemen ''a'' dengan menyetel  ¬''a'' = (''a''→0). Menurut definisi, <math>a\wedge \lnot a = 0</math>, dan ¬''a'' adalah elemen terbesar yang memiliki sifat ini. Namun, secara umum tidak benar bahwa <math>a\vee\lnot a=1</math>, demikian ¬ hanya sebagai pseudo-kelengkapan, bukan [[kelengkapan (teori himpunan)|kelengkapan]] yang sebenarnya, seperti yang terjadi pada aljabar Boolean.

Sebuah '''[[kelengkapan aljabar Heyting]]''' adalah aljabar Heyting yang merupakan [[kekisi lengkap]].

Sebuah '''subaljabar''' dari aljabar Heyting ''H'' adalah himpunan bagian ''H''<sub>1</sub> dari ''H'' yang merupakan 0 dan 1 dan sebagai penutupan bawah operasi ∧, ∨ dan →. Oleh karena itu, ¬ juga sebagai penutupan bawah. Sebuah subaljabar sebagai aljabar Heyting dengan operasi induksi.

== Definisi alternatif ==
=== Definisi teori-kategori ===
Aljabar Heyting <math>H</math> adalah kekisi batas yang memiliki semua [[objek eksponensial]].

Kekisi <math>H</math> sebagai salah satu [[kategori (matematika)|kategori]] dimana
pertemuan <math>\wedge</math>, adalah [[produk (teori kategori)|produk]]. Kondisi eksponensial berarti bahwa untuk setiap objek <math>Y</math> dan <math>Z</math> dalam <math>H</math> sebuah <math>Z^Y</math> eksponensial unik sebagai objek dalam <math>H</math>.

Implikasi Heyting (ditulis juga <math>\Rightarrow</math> atau <math>\multimap</math> untuk menghindari kebingungan seperti penggunaan <math>\to</math> untuk menunjukkan [[fungtor]]) sebagai eksponensial: <math>Y \Rightarrow Z</math> adalah notasi alternatif untuk <math>Z^Y</math>. Dari definisi eksponensial kita memiliki implikasi (<math>\Rightarrow : H \times H \to H</math>) adalah [[kanan adjoin]] untuk pertemuan (<math>\wedge : H \times H \to H</math>). Adjungsi ini dapat ditulis sebagai <math>(- \wedge Y) \dashv (Y \Rightarrow -)</math> atau lebih lengkapnya sebagai:
<math display="block">(- \wedge Y): H \stackrel {\longrightarrow} {\underset {\longleftarrow}{\top}} H: (Y \Rightarrow -)</math>

===Definisi teori kisi===
Definisi ekuivalen dari aljabar Heyting dapat diberikan dengan mempertimbangkan pemetaan:

:<math>\begin{cases} f_a \colon H \to H \\ f_a(x)=a\wedge x \end{cases}</math>

untuk beberapa ''a'' dalam ''H''. Kekisi berbatas ''H'' adalah aljabar Heyting [[jika dan hanya jika]] setiap pemetaan ''f<sub>a</sub>'' adalah adjoint bawah monoton [[hubungan Galois]]. Dalam hal ini adjoin atas ''g<sub>a</sub>'' diberikan oleh ''g<sub>a</sub>''(''x'') = ''a''→''x'', dimana → sebagai definisi atas.

Namun definisi lain adalah sebagai [[kekisi residu]] dimana operasi monoidnya adalah ∧. Unit monoid kemudian menjadi sebagai elemen teratas 1. Komutatifitas monoid ini menyiratkan bahwa kedua residu bertepatan sebagai ''a''→''b''.

=== Kekisi terikat dengan operasi implikasi ===
Diberikan kisi terbatas ''A'' dengan elemen terbesar dan terkecil 1 dan 0, dan [[operasi biner]] →, ini sebagai bentuk aljabar Heyting jika dan hanya jika yang berikut ini berlaku:
#<math>a\to a = 1</math>
#<math>a\wedge(a\to b)=a\wedge b</math>
#<math>b\wedge(a\to b)= b</math>
#<math>a\to (b\wedge c)= (a\to b)\wedge (a\to c)</math>
dimana 4 adalah hukum distributif untuk →.

=== Karakterisasi menggunakan aksioma logika intuisi ===
Karakterisasi aljabar Heyting ini membuat bukti fakta dasar mengenai hubungan antara kalkulus proposisional, intuisionis, dan aljabar Heyting dekat (untuk fakta ini, lihat bagian "[[#Identitas yang dapat dibuktikan|identitas pembuktian]]" dan "[[#Konstruksi universal|konstruksi universal]]"). Orang harus menganggap elemen <math>\top</math> sebagai makna, secara intuitif, "terbukti benar." Bandingkan dengan aksioma di [[Logika intuisi#Aksiomatisasi]].

Diberikan satu himpunan ''A'' dengan tiga operasi biner →, ∧ dan ∨, dan dua elemen berbeda <math>\bot</math> dan <math>\top</math>, maka ''A'' adalah aljabar Heyting untuk operasi ini (dan relasinya ≤ didefinisikan oleh kondisi bahwa <math>a \le b</math> maka ''a''→''b'' = <math>\top</math>) jika dan hanya jika kondisi berikut berlaku untuk setiap elemen ''x'', ''y'' dan ''z'' dari ''A'':

#<math>\mbox{Jika } x \le y  \mbox{ dan } y \le x  \mbox{ maka } x = y ,</math>
#<math>\mbox{Jika } \top \le y , \mbox{ maka } y = \top ,</math>
#<math>x \le y \to x  ,</math>
#<math> x \to (y \to z) \le (x \to y) \to (x \to z)  ,</math>
#<math> x \land y \le x  ,</math>
#<math> x \land y \le y ,</math>
#<math> x \le y \to (x \land y)  ,</math>
#<math> x \le x \lor y ,</math>
#<math> y \le x \lor y  ,</math>
#<math> x \to z \le (y \to z) \to (x \lor y \to z)  ,</math>
#<math> \bot \le x  .</math>
Akhirnya, kita dapat mendefinisikan ¬''x'' sebagai ''x''→ <math>\bot</math>.

Kondisi 1 mengatakan bahwa formula yang setara harus diidentifikasi. Ketentuan 2 menyatakan bahwa rumus yang terbukti benar ditutup di bawah [[modus ponens]]. Ketentuan 3 dan 4 adalah ketentuan ''lalu''. Ketentuan 5, 6, dan 7 adalah ketentuan ''dan''. Ketentuan 8, 9, dan 10 adalah ketentuan ''atau''. Kondisi 11 adalah kondisi ''salah''.

Tentu saja, jika serangkaian aksioma yang berbeda dipilih untuk logika, kita dapat memodifikasi aksioma.

== Contoh ==
[[Berkas:Rieger-Nishimura.svg|thumb|right|280px|Aljabar Heyting [[objek bebas|bebas]] melalui satu generator (alias kekisi Rieger–Nishimura)]]

<ul>
<li> Setiap [[Aljabar Boolean (struktur)|aljabar Boolean]] adalah aljabar Heyting, dengan ''p''→''q'' diberikan oleh ¬''p''∨''q''.
<li> Setiap [[tatanan total|himpunan terurut total]] yang memiliki elemen terkecil 0 dan elemen terbesar 1 adalah aljabar Heyting (jika dilihat sebagai kekisi). Dalam hal ini ''p''→''q'' sama dengan 1 ketika ''p≤q'', dan ''q'' sebaliknya.
<li> Aljabar Heyting sederhana yang belum menjadi aljabar Boolean adalah himpunan terurut total {0, {{sfrac|1|2}}, 1} (dilihat sebagai kekisi), menghasilkan sebagai operasi:
{|
|-style="vertical-align:bottom"
|
<div>
{| class="wikitable"
|+ <math>a \land b</math>
|-
! {{diagonal split header|''a''|''b''}}
| bgcolor="white" width="30" align="center" | 0
| bgcolor="white" width="30" align="center" | {{sfrac|1|2}}
| bgcolor="white" width="30" align="center" | 1
|-
| bgcolor="white" align="center" | 0
| align="center" | 0
| align="center" | 0
| align="center" | 0
|-
| bgcolor="white" align="center" | {{sfrac|1|2}}
| align="center" | 0
| align="center" | {{sfrac|1|2}}
| align="center" | {{sfrac|1|2}}
|-
| bgcolor="white" align="center" | 1
| align="center" | 0
| align="center" | {{sfrac|1|2}}
| align="center" | 1
|}
</div>
| width="30" | &nbsp;
|
<div>
{| class="wikitable"
|+ <math>a \lor b</math>
|-
! {{diagonal split header|''a''|''b''}}
| bgcolor="white" width="30" align="center" | 0
| bgcolor="white" width="30" align="center" | {{sfrac|1|2}}
| bgcolor="white" width="30" align="center" | 1
|-
| bgcolor="white" align="center" | 0
| align="center" | 0
| align="center" | {{sfrac|1|2}}
| align="center" | 1
|-
| bgcolor="white" align="center" | {{sfrac|1|2}}
| align="center" | {{sfrac|1|2}}
| align="center" | {{sfrac|1|2}}
| align="center" | 1
|-
| bgcolor="white" align="center" | 1
| align="center" | 1
| align="center" | 1
| align="center" | 1
|}
</div>
| width="30" | &nbsp;
|
<div>
{| class="wikitable"
|+ {{nobold|{{math|''a''→''b''}}}}
|-
! {{diagonal split header|''a''|''b''}}
| bgcolor="white" width="30" align="center" | 0
| bgcolor="white" width="30" align="center" | {{sfrac|1|2}}
| bgcolor="white" width="30" align="center" | 1
|-
| bgcolor="white" align="center" | 0
| align="center" | 1
| align="center" | 1
| align="center" | 1
|-
| bgcolor="white" align="center" | {{sfrac|1|2}}
| align="center" | 0
| align="center" | 1
| align="center" | 1
|-
| bgcolor="white" align="center" | 1
| align="center" | 0
| align="center" | {{sfrac|1|2}}
| align="center" | 1
|}
</div>
| width="30" | &nbsp;
|
<div>
{| class="wikitable"
| width="50" align="center" | ''a''
| width="50" align="center" | ¬''a''
|-
| bgcolor="white" align="center" | 0
| align="center" | 1
|-
| bgcolor="white" align="center" | {{sfrac|1|2}}
| align="center" | 0
|-
| bgcolor="white" align="center" | 1
| align="center" | 0
|}
</div>
|}
Dalam contoh ini, {{math|size=100%|1= {{sfrac|1|2}}&or;¬{{sfrac|1|2}} = {{sfrac|1|2}}&or;({{sfrac|1|2}} → 0) = {{sfrac|1|2}}&or;0 = {{sfrac|1|2}}}} melancungkan hukum tengah yang dikecualikan.

<li> Setiap [[topologi]] sebagai kelengkapan aljabar Heyting dalam bentuk kisi [[himpunan terbuka]]-nya. Dalam hal ini, elemen ''A''→''B'' adalah [[interior (topologi)|interior]] dari gabungan ''A<sup>c</sup>'' dan ''B'', di mana ''A<sup>c</sup>'' menunjukkan [[kelengkapan (teori himpunan)|kelengkapan]] dari [[himpunan terbuka]] ''A''. Tidak semua kelengkapan aljabar Heyting sebagai bentuk seperti ini. Isu-isu ini dipelajari dalam [[topologi tak berarti]], dimana kelengkapan aljabar Heyting juga disebut '''bingkai''' atau '''lokal'''.
<li> Setiap [[aljabar interior]] sebagai aljabar Heyting dalam bentuk kekisi elemen terbukanya. Setiap aljabar Heyting sebagai bentuk ini karena aljabar Heyting diselesaikan menjadi aljabar Boolean dengan mengambil ekstensi Boolean bebas sebagai kekisi distributif hingga dan maka sebagai [[topologi umum]] dalam aljabar Boolean ini.
<li> [[Aljabar Lindenbaum]] dari [[logika intuisi]] proposisional adalah aljabar Heyting.
<li> [[Elemen global]] dari [[pengklasifikasi subobjek]] Ω dari [[topos dasar]] sebagai bentuk aljabar Heyting; itu adalah aljabar Heyting dari [[nilai kebenaran]] dari logika tingkat tinggi intuitif induksi oleh topos.
<li> [[Aljabar Łukasiewicz—Moisil]] (LM<sub>''n''</sub>) merupakan aljabar Heyting untuk semua ''n''<ref>{{Cite journal | doi = 10.1007/s10516-005-4145-6| title = N-Valued Logics and Łukasiewicz–Moisil Algebras| journal = Axiomathes| volume = 16| pages = 123| year = 2006| last1 = Georgescu | first1 = G. }}, Theorem 3.6</ref> (namun bukan [[aljabar-MV]] untuk ''n'' ≥ 5<ref>Iorgulescu, A.: Hubungan antara aljabar-MV<sub>''n''</sub> dan ''n''-nilai aljabar Łukasiewicz–Moisil—I. Matematika Diskrit. 181, 155–177 (1998) {{doi|10.1016/S0012-365X(97)00052-6}}</ref>).
</ul>

== Sifat ==

=== Sifat umum ===
Urutan <math>\le</math> pada aljabar Heyting ''H'' dapat diperoleh dari operasi → sebagai berikut: untuk setiap elemen ''a'', ''b'' dari ''H'', <math>a \le b</math> jika dan hanya jika ''a''→''b'' = 1.

Berbeda dengan beberapa [[logika nilai banyak]], aljabar Heyting terbagi sifat berikut dengan aljabar Boolean: jika negasi memiliki [[titik tetap (matematika)|titik tetap]] (misal ¬''a'' = ''a'' untuk beberapa ''a''), maka aljabar Heyting adalah aljabar Heyting satu-elemen trivial.

=== Identitas pembuktian ===
Diberikan rumus <math>F(A_1, A_2,\ldots, A_n)</math> dari kalkulus proposisional (menggunakan, variabel, penghubung <math>\land, \lor, \lnot, \to</math>, dan konstanta 0 dan 1), yang terbukti sejak awal studi aljabar Heyting, bahwa dua kondisi berikut adalah ekuivalen:
# Rumus ''F'' terbukti benar dalam kalkulus proposisional intuisionis.
# Identitas <math>F(a_1, a_2,\ldots, a_n) = 1</math> untuk setiap aljabar Heyting ''H'' dan elemen <math>a_1, a_2,\ldots, a_n \in H</math>.
Metaimplikasi {{nowrap|1 ⇒ 2}} merupakan metode praktis utama untuk membuktikan identitas dalam aljabar Heyting. Dalam praktiknya, dengan menggunakan [[teorema deduksi]] dalam pembuktian semacam itu.

Karena untuk setiap ''a'' dan ''b'' dalam aljabar Heyting ''H'' kita memiliki <math>a \le b</math> jika dan hanya jika ''a''→''b'' = 1, mengikuti dari {{nowrap|1 ⇒ 2}} bahwa setiap kali rumus ''F''→''G'' pembuktian dengan benar, kita memiliki <math>F(a_1, a_2,\ldots, a_n) \le G(a_1, a_2,\ldots, a_n)</math> untuk setiap aljabar Heyting ''H'', dan elemen <math>a_1, a_2,\ldots, a_n \in H</math>. Ini mengikuti dari teorema deduksi bahwa ''F''→''G'' dapat dibuktikan [dari ketiadaan] jika dan hanya jika ''G'' dibuktikan dari ''F'', yaitu jika ''G'' adalah konsekuensi pembuktian dari ''F''. Khususnya, jika ''F'' dan ''G'' membuktikan ekuivalen, maka <math>F(a_1, a_2,\ldots, a_n) = G(a_1, a_2,\ldots, a_n)</math>, karena ≤ adalah relasi orde.

1 ⇒ 2 dibuktikan dengan aksioma logika dari sistem pembuktian dan memverifikasi bahwa nilainya adalah 1 dalam setiap aljabar Heyting, dan kemudian memverifikasi bahwa penerapan aturan inferensi ke ekspresi dengan nilai 1 dalam aljabar Heyting menghasilkan ekspresi dengan nilai 1. Sebagai contoh, memilih sistem pembuktian yang memiliki [[modus ponens]] sebagai satu-satunya aturan inferensi, dan aksiomanya adalah gaya Hilbert yang diberikan dalam [[Logika intuitif#Aksiomatisasi|aksiomatisasi]]. Maka memverifikasikan dengan mengikuti dari definisi aljabar Heyting seperti aksioma yang diberikan di atas.

1 ⇒ 2 sebagai metode untuk membuktikan bahwa rumus proposisi tertentu, meskipun [[tautologi (logika)|tautologi]] dalam logika klasik, ''tidak bisa'' dibuktikan dalam logika proposisional intuisionis. Untuk membuktikan bahwa beberapa rumus <math>F(A_1, A_2,\ldots, A_n)</math> tidak dapat dibuktikan, cukup dengan menunjukkan aljabar Heyting ''H'' dan elemen <math>a_1, a_2,\ldots, a_n \in H</math> sedemikian rupa sehingga <math>F(a_1, a_2,\ldots, a_n) \ne 1</math>.

Jika ingin penyebutan logika tidak digunakan, maka dalam praktiknya menjadi perlu untuk membuktikan sebagai lema versi teorema deduksi yang valid untuk aljabar Heyting: untuk setiap elemen ''a'', ''b'' dan ''c'' dari aljabar Heyting ''H'', dengan memiliki <math>(a \land b) \to c = a \to (b \to c)</math>.

Untuk lebih lanjut tentang metaimplication 2 ⇒ 1, lihat bagian "[[#Konstruksi universal|konstruksi universal]]" dibawah.

=== Distributivitas ===
Aljabar Heyting digunakan sebagai [[distributivitas (teori orde)|distributif]]. Secara khusus, maka kita memiliki identitas
#<math>a \wedge (b \vee c) = (a \wedge b) \vee (a \wedge c)</math>
#<math>a \vee (b \wedge c) = (a \vee b) \wedge (a \vee c)</math>

Hukum distributif terkadang dinyatakan sebagai aksioma, namun kenyataannya mengikuti dari keberadaan pseudo-kelengkapan relatif. Alasannya adalah, sebagai adjoin bawah dari [[hubungan Galois]], [[limit fungsi kekal (teori urutan)|kekal]] <math>\wedge</math> untuk semua [[suprema]]. Distribusi pada gilirannya hanyalah kekal suprema biner oleh <math>\wedge</math>.

Dengan argumen serupa, [[hukum distributif tak hingga]] berikut berlaku dalam kelengkapan aljabar Heyting:

:<math>x\wedge\bigvee Y = \bigvee \{x\wedge y \mid y \in Y\}</math>

untuk setiap elemen ''x'' dalam ''H'' dan setiap himpunan bagian ''Y'' dari ''H''. Sebaliknya, setiap kisi kelengkapan yang memenuhi hukum distributif tak hingga atas adalah kelengkapan aljabar Heyting, dengan
:<math>a\to b=\bigvee\{c\mid a\land c\le b\}</math>
sebagai operasi pseudo-kelengkapan relatif.

=== Elemen reguler dan kelengkapan ===
Sebuah elemen ''x'' dari aljabar Heyting ''H'' disebut '''reguler''' jika salah satu dari kondisi ekuivalen berikut berlaku:
#''x'' =  ¬¬''x''.
#''x'' =  ¬''y'' untuk beberapa ''y'' dalam ''H''.
Kondisi ekuivalen ini dapat dinyatakan kembali hanya sebagai identitas ¬¬¬''x'' = ¬''x'', berlaku untuk semua ''x'' dalan ''H''.

Elemen ''x'' dan ''y'' dari aljabar Heyting ''H'' disebut '''kelengkapan''' satu sama lain jika ''x''∧''y'' = 0 dan ''x''∨''y'' = 1. Jika, "y" adalah unik dan sebenarnya harus sama dengan ¬''x''. Yang disebut juga dengan elemen '''kelengkapan''' ''x'' jika ia adalah komplemen. Bahwa ''jika'' kelengkapan ''x'', maka demikian pula ¬''x'', kemudian ''x'' dan ¬''x'' adalah kelengkapan sama lain. Namun, bahkan jika ''x'' kelengkapan sama lain, ¬''x'' mungkin tetap memiliki komplemen (tidak sama dengan ''x''). Dalam setiap aljabar Heyting, elemen 0 dan 1 saling melengkapi. Misalnya, mungkin saja ¬''x'' adalah 0 untuk setiap ''x'' berbeda dari 0, dan 1 jika ''x'' = 0, dalam hal ini 0 dan 1 adalah satu-satunya elemen reguler.

Setiap elemen kelengkapan dari aljabar Heyting adalah reguler, meskipun sebaliknya tidak berlaku secara umum. Secara khusus, 0 dan 1 adalah reguler.

Untuk setiap aljabar Heyting ''H'', kondisi ekuivalen berikut ini:
# ''H'' adalah [[Aljabar Boolean (struktur)|aljabar Boolean]];
# setiap ''x'' dalam ''H'' adalah reguler;<ref>Rutherford (1965), Th.26.2 p.78.</ref>
# setiap ''x'' dalam ''H'' adalah kelengkapan.<ref>Rutherford (1965), Th.26.1 p.78.</ref>
Dalam hal ini, elemen {{nowrap|1=''a''→''b''}} adalah sama dengan {{nowrap|1=¬''a'' ∨ ''b''.}}

Elemen reguler (resp. kelengkapan) dari setiap aljabar Heyting ''H'' membentuk aljabar Boolean ''H''<sub>reg</sub> (resp. ''H''<sub>komp</sub> ), dimana operasi ∧, ¬ dan →, serta konstanta 0 dan 1, bertepatan dengan "H". Dalam kasus ''H''<sub>comp</sub> dengan operasi ∨, maka ''H''<sub>comp</sub> adalah subaljabar dari ''H''. Namun secara umum, ''H''<sub>reg</sub> bukan sebagai subaljabar dari ''H'', karena operasi gabungan ∨<sub>reg</sub> mungkin berbeda dari ∨. Untuk {{nowrap|1=''x'', ''y'' ∈ ''H''<sub>reg</sub>,}} maka kita menggunakan sebagai {{nowrap|1=''x'' ∨<sub>reg</sub> ''y'' = ¬(¬''x'' ∧ ¬''y'').}} Lihat di bawah untuk kondisi perlu dan cukup agar ∨<sub>reg</sub> bertepatan dengan ∨.

=== Hukum De Morgan dalam aljabar Heyting ===
Salah satu dari dua [[hukum De Morgan]] terpenuhi dalam setiap aljabar Heyting, yaitu

:<math>\forall x,y \in H: \qquad \lnot(x \vee y)=\lnot x \wedge \lnot y.</math>

Namun, hukum De Morgan lainnya tidak berlaku. Sebagai gantinya, kita memiliki hukum de Morgan lemah:

:<math>\forall x,y \in H: \qquad \lnot(x \wedge y)= \lnot \lnot (\lnot x \vee \lnot y).</math>

Pernyataan berikut ekuivalen untuk semua aljabar Heyting ''H'':
# ''H'' memenuhi kedua hukum De Morgan,
#<math>\lnot(x \wedge y)=\lnot x \vee \lnot y \mbox{ untuk semua } x, y \in H,</math>
#<math>\lnot(x \wedge y)=\lnot x \vee \lnot y \mbox{ untuk semua reguler } x, y \in H,</math>
#<math>\lnot\lnot (x \vee y) = \lnot\lnot x \vee \lnot\lnot y \mbox{ untuk semua } x, y \in H,</math>
#<math>\lnot\lnot (x \vee y) = x \vee y \mbox{ untuk semua reguler } x, y \in H,</math>
#<math>\lnot(\lnot x \wedge \lnot y) = x \vee y \mbox{ untuk semua reguler } x, y \in H,</math>
#<math>\lnot x \vee \lnot\lnot x = 1 \mbox{ untuk semua } x \in H.</math>
Kondisi 2 adalah hukum De Morgan lainnya. Kondisi 6 menyatakan bahwa operasi gabungan ∨<sub>reg</sub> pada aljabar Boolean ''H''<sub>reg</sub> elemen reguler ''H'' bertepatan dengan operasi ∨ dari ''H''. Kondisi 7 menyatakan bahwa setiap elemen kelengkapan reguler, yaitu ''H''<sub>reg</sub> = ''H''<sub>komp</sub>.

Dengan membuktikan ekuivalen, jelas metaimplikasi {{nowrap|1 ⇒ 2,}} {{nowrap|2 ⇒ 3}} dan {{nowrap|4 ⇒ 5}} adalah trivial. Selanjutnya, {{nowrap|3 ⇔ 4}} dan {{nowrap|5 ⇔ 6}} hasil sederhana dari hukum De Morgan pertama dan definisi elemen reguler. Dengan menunjukkan bahwa {{nowrap|6 ⇒ 7}} dengan mengambil ¬''x'' dan ¬¬''x'' menggantikan ''x'' dan ''y'' di 6 dan menggunakan identitas {{nowrap|''a'' &and; ¬''a'' {{=}} 0.}} Perhatikan bahwa {{nowrap|2 ⇒ 1}} mengikuti dari hukum De Morgan pertama, dan {{nowrap|7 ⇒ 6}} hasil dari fakta bahwa operasi gabungan ∨ pada subaljabar ''H''<sub>comp</sub> hanyalah pembatas ∨ ke ''H''<sub>komp</sub>, dengan mempertimbangkan karakterisasi yang telah kami berikan untuk kondisi 6 dan 7. Metaimplikasi {{nowrap|5 ⇒ 2}} adalah konsekuensi trivial dari hukum De Morgan lemah, dengan ¬''x'' dan ¬''y'' menggantikan ''x'' dan ''y'' di 5.

Aljabar Heyting yang memenuhi sifat- di atas terkait dengan [[Logika menengah|logika De Morgan]] dengan cara yang sama seperti aljabar Heyting pada umumnya terkait dengan logika intuisionis.

== Morfisme aljabar Heyting ==

=== Definisi ===
Diberikan dua aljabar Heyting ''H''<sub>1</sub> dan ''H''<sub>2</sub> dengan pemetaan {{nowrap|1=''f'' : ''H''<sub>1</sub> → ''H''<sub>2</sub>,}} maka bahwa ''ƒ'' adalah '''[[morfisme]]''' dari aljabar Heyting apabila untuk setiap elemen ''x'' dan ''y'' dalam ''H''<sub>1 </sub>, maka dari itu:
#<math>f(0) = 0,</math>
#<math>f(x \land y) = f(x) \land f(y),</math>
#<math>f(x \lor y) = f(x) \lor f(y),</math>
#<math>f(x \to y) = f(x) \to f(y),</math>

Ini mengikuti dari salah satu dari tiga kondisi terakhir (2, 3, atau 4) bahwa ''f'' adalah fungsi tingkatan, yaitu {{nowrap|1=''f''(''x'') ≤ ''f''(''y'')}} dengan {{nowrap|1=''x'' ≤ ''y''}}.

Asumsi ''H''<sub>1</sub> dan ''H''<sub>2</sub> adalah struktur dengan operasi →, ∧, ∨ (kemungkinan ¬) dan konstanta 0 dan 1, dan ''f'' adalah pemetaan surjektif dari ''H''<sub>1</sub> ke ''H''<sub>2</sub> dengan sifat 1 sampai 4 atas. Maka jika ''H''<sub>1</sub> adalah aljabar Heyting, demikian pula ''H''<sub>2</sub>. Ini mengikuti dari karakterisasi aljabar Heyting sebagai kekisi batas (sebagai [[struktur aljabar]] dari himpunan terurut sebagian) dengan operasi → yang memenuhi identitas tertentu.

=== Sifat ===
Peta identitas {{nowrap|1=''f''(''x'') = ''x''}} dari aljabar Heyting ke sendiri adalah morfisme, dan gabungan {{nowrap|1=''g'' ∘ ''f''}} dari setiap dua morfisme ''f'' dan ''g'' adalah morfisme. Oleh karena itu aljabar Heyting sebagai bentuk [[Kategori (matematika)|kategori]].

=== Contoh ===
Diberikan aljabar Heyting ''H'' dan setiap subaljabar ''H''<sub>1</sub>, pemetaan inklusi {{nowrap|1=''i'' : ''H''<sub>1</sub> → ''H''}} adalah morfisme.

Untuk setiap aljabar Heyting ''H'', peta {{nowrap|1=''x'' ↦ ¬¬''x''}} didefinisikan morfisme dari ''H'' ke aljabar Boolean dari elemen reguler ''H''<sub>reg</sub>. Ini adalah secara umum ''bukan'' sebuah morfisme dari ''H'' ke sendiri, karena operasi gabungan dari ''H''<sub>reg</sub> mungkin berbeda dari ''H''.

== Hasil bagi ==
Maka ''H'' sebagai aljabar Heyting, dan {{nowrap|1=''F'' ⊆ ''H''.}} Dengan menyebutnya ''F'' sebagai '''filter''' pada ''H'' jika memenuhi sifat berikut:
#<math>1 \in F,</math>
#<math> \mbox{Jika } x,y \in F \mbox{ maka } x \land y \in F,</math>
#<math> \mbox{Jika } x \in F, \ y \in H, \ \mbox{dan } x \le y \mbox{ maka } y \in F.</math>

Perpotongan himpunan filter pada ''H'' adalah filter. Oleh karena itu, jika diberikan himpunan bagian ''S'' dari ''H'', maka filter terkecil-nya adalah ''S''. Dengan menyebutnya filter yang '''dihasilkan''' oleh ''S''. Jika ''S'' kosong, {{nowrap|1=''F'' = {1}.}} Jika tidak, ''F'' sama dengan himpunan ''x'' dalam ''H'' sehingga terdapat {{nowrap|1=''y''<sub>1</sub>, ''y''<sub>2</sub>, ..., ''y''<sub>''n''</sub> ∈ ''S''}} dengan {{nowrap|1=''y''<sub>1</sub> ∧ ''y''<sub>2</sub> ∧ ... ∧ ''y''<sub>''n''</sub> ≤ ''x''.}}

Jika ''H'' adalah aljabar Heyting dan ''F'' adalah filter pada ''H'', dengan mendefinisikan relasi ∼ pada ''H'' sebagai berikut: maka ditulis sebagai {{nowrap|1=''x'' ∼ ''y''}} dengan {{nowrap|1=''x'' → ''y''}} dan {{nowrap|1=''y'' → ''x''}} keduanya milik ''F''. Maka ∼ adalah [[relasi ekuivalen]]; apabila ditulis {{nowrap|1=''H''/''F''}} untuk [[himpunan hasil bagi]]. Terdapat struktur aljabar Heyting unik pada {{nowrap|1=''H''/''F''}} sehingga surjeksi kanonik-nya adalah {{nowrap|1=''p''<sub>''F''</sub> : ''H'' → ''H''/''F''}} yang sebagai morfisme aljabar Heyting. Dengan menyebutnya aljabar Heyting {{nowrap|1=''H''/''F''}} sebagai '''hasil bagi''' dari ''H'' dengan ''F''.

Maka ''S'' sebagai himpunan bagian dari aljabar Heyting ''H'' dan maka ''F'' sebagai filter yang dihasilkan oleh ''S''. Maka ''H''/''F'' memenuhi sifat universal berikut:
:Mengingat morfisme dari aljabar Heyting {{nowrap|1=''f'' : ''H'' → ''H′''}} suatu {{nowrap|1=''f''(''y'') = 1}} untuk setiap {{nowrap|1=''y'' ∈ ''S'',}} faktor ''f'' unik melalui surjeksi kanonik {{nowrap|1=''p''<sub>''F''</sub> : ''H'' → ''H''/''F''.}} Artinya, morfisme unik {{nowrap|1=''f′'' : ''H''/''F'' → ''H′''}} sebagai {{nowrap|1=''f′p''<sub>''F''</sub> = ''f''.}} Morfisme ''f′'' dikatakan sebagai ''induksi'' oleh ''f''.

Maka {{nowrap|1=''f'' : ''H''<sub>1</sub> → ''H''<sub>2</sub>}} adalah morfisme aljabar Heyting. '''Kernel''' dari ''f'', yang ditulis sebagai "ker" ''f'' yang merupakan himpunan {{nowrap|1=''f''<sup>−1</sup>[{1}].}} Ini adalah filter pada ''H''<sub>1</sub>. (Catatan: Harus diperhatikan karena definisi ini, jika diterapkan pada morfisme aljabar Boolean, adalah ganda dengan apa yang disebut inti morfisme yang dipandang sebagai morfisme gelanggang.) Dengan hal diatas, induksi ''f'' adalah morfisme {{nowrap|1=''f′'' : ''H''<sub>1</sub>/(ker ''f'') → ''H''<sub>2</sub>.}} Ini adalah isomorfisme {{nowrap|1=''H''<sub>1</sub>/(ker ''f'')}} ke subaljabar ''f''[''H''<sub>1</sub>] dari ''H''<sub>2</sub>.

== Konstruksi universal ==

=== Aljabar Heyting rumus proposisional dalam variabel ''n'' hingga dengan ekuivalen intuisi ===
Metaimplikasi {{nowrap|2 ⇒ 1}} pada bagian "[[#Indetitas pembuktian|identitas pembuktian]]" dibuktikan dengan menunjukkan bahwa hasil konstruksi berikut yang merupakan aljabar Heyting:
#Pertimbangkan himpunan ''L'' dari rumus proposisi dalam variabel ''A''<sub>1</sub>, ''A''<sub>2</sub>,..., ''A''<sub>''n''</sub>.
# Diberikan ''L'' dengan preorder ≼ dengan mendefinisikan ''F''≼''G'' jika ''G'' adalah (intuisionis) [[konsekuensi logika]] dari ''F'', yaitu jika ''G'' membuktikan dari ''F''. Bahwa ≼ adalah preorder.
# Pertimbangkan relasi ekuivalensi ''F''∼''G'' induksi dari preorder F≼G. Didefinisikan oleh ''F''∼''G'' jika dan hanya jika ''F''≼''G'' dan ''G''≼''F''. Sebenarnya adalah hubungan ekuivalen logika (intuisionis).
# Misalkan ''H''<sub>0</sub> sebagai himpunan hasil bagi ''L''/∼. Ini akan menjadi aljabar Heyting yang diinginkan.
# Dengan menulis [''F''] untuk kelas ekuivalensi dari rumus ''F''. Operasi →, ∧, ∨ dan ¬ yang didefinisikan oleh ''L''. Verifikasi bahwa rumus yang diberikan ''F'' dan ''G'', kelas ekuivalensi [''F''→''G''], [''F''∧''G''], [''F''∨''G''] dan [¬''F''] hanya bergantung pada [''F''] dan [''G'']. Ini mendefinisikan operasi →, ∧, ∨ dan ¬ pada himpunan hasil bagi ''H''<sub>0</sub>=''L''/∼. Lebih lanjut definisikan 1 sebagai kelas pernyataan yang terbukti benar, dan himpunan 0=[⊥].
# Verifikasi bahwa ''H''<sub>0</sub>, bersama dengan operasi ini, adalah aljabar Heyting. Dengan menggunakan definisi seperti aksioma dari aljabar Heyting. ''H''<sub>0</sub> memenuhi kondisi MAKA-1 sampai SALAH karena semua rumus dari bentuk yang diberikan adalah aksioma logika intuisionis. MODUS-PONENS mengikuti dari fakta bahwa jika rumus ⊤→''F'', dimana pembuktian benar, maka ''F'' adalah pembuktian benar (dengan penerapan kaidah modus ponens inferensi). Akhirnya, hasil EKUIV dari fakta bahwa jika ''F''→''G'' dan ''G''→''F'' keduanya terbukti benar, maka ''F'' dan ''G'' dapat dibuktikan satu sama lain (dengan penerapan kaidah modus ponens inferensi) dengan [''F'']=[''G''].

Seperti biasa di bawah definisi aljabar Heyting seperti aksioma, kita mendefinisikan ≤ pada ''H''<sub>0</sub> dengan syarat bahwa ''x''≤''y'' jika dan hanya jika '' x''→''y''=1. Karena, dengan [[teorema deduksi]], rumus ''F''→''G'' dengan pembuktian benar jika dan hanya jika ''G'' dapat dibuktikan dari ''F'', maka [''F'']≤[''G''] jika dan hanya jika F≼G. Dengan kata lain, adalah relasi order pada ''L''/∼ yang diinduksi oleh preorder ≼ pada ''L''.

=== Aljabar Heyting bebas pada himpunan generator sebarang ===
Bahkan, konstruksi sebelumnya dapat dilakukan untuk setiap Himpunan variabel {''A''<sub>''i''</sub> : ''i''∈''I''} (secara khusus tak hingga). Dengan cara ini diperoleh aljabar Heyting ''bebas'' pada variabel {''A''<sub>''i''</sub>}, yang akan dinyatakan kembali dengan ''H''<sub>0</sub>. Dalam arti "bebas" bahwa aljabar Heyting "H" yang diberikan bersama dengan keluarga elemen〈''a''<sub>''i''</sub>: ''i''∈''I''〉, apabila terdapat morfisme unik ''f'':''H''<sub>0</sub>→''H'' dari suatu ''f''([''A''<sub>''i''</sub>])=''a''<sub>''i''</sub>. Keunikan ''f'' tidak sulit untuk dilihat, dan keberadaannya pada dasarnya berasal dari metaimplikasi {{nowrap|1 ⇒ 2}} dari bagian "[[#Identitas pembuktian|Identitas pembuktian]]" di atas, dalam bentuk akibat wajarnya bahwa setiap kali ''F'' dan ''G'' adalah rumus pembuktian ekuivalen, ''F''(〈''a''<sub>''i''</sub>〉)=''G''(〈''a''<sub>''i''</sub>〉) untuk setiap keluarga elemen 〈''a''<sub>''i''</sub>〉dalam ''H''.

=== Aljabar Heyting rumus ekuivalen yang berhubungan dengan teori ''T'' ===
Diberikan satu himpunan rumus ''T'' dalam variabel {''A''<sub>''i''</sub>}, dilihat sebagai aksioma, konstruksi yang sama dapat dilakukan terhadap suatu relasi ''F''≼''G'' mendefinisikan pada ''L'' berarti bahwa ''G'' adalah konsekuensi pembuktian dari ''F'' dan himpunan aksioma ''T''. Maka dengan menunjukkan ''H''<sub>''T''</sub> sebagai aljabar Heyting yang diperoleh. Maka ''H''<sub>''T''</sub> memenuhi sifat universal yang sama dengan ''H''<sub>0</sub> di atas, namun apabila aljabar Heyting ''H'' dan keluarga elemen 〈''a''<sub>''i''</sub>〉 memenuhi sifat ''J''(〈''a''<sub>''i''</sub>〉)=1 untuk setiap aksioma ''J''(〈''A''<sub>''i''</sub>〉) dalam ''T''. Maka dengan memperhatikan bahwa ''H''<sub>''T''</sub>, diambil dengan keluarga elemen 〈[''A''<sub>''i''</sub>]〉sendiri yang memenuhi sifat ini. Keberadaan dan keunikan morfisme pembuktian dengan cara yang sama untuk ''H''<sub>0</sub>, kecuali bahwa apabila memodifikasi metaimplikasi {{nowrap|1 ⇒ 2}} di "[[#Identitas pembuktian|Identitas pembuktian]]" sehingga 1 terbaca "pembuktian benar" ''dari T''," dan 2 terbaca "setiap elemen ''a''<sub>1</sub>, ''a''<sub>2</sub>,..., ''a''<sub>''n''</sub> dalam ''H'' ''pernyataan rumus T''."

Aljabar Heyting ''H''<sub>''T''</sub> yang baru saja didefinisikan apabila dilihat sebagai hasil bagi dari aljabar Heyting bebas ''H''<sub>0</sub> pada himpunan variabel yang sama, dengan sifat universal ''H''<sub>0</sub> sehubungan dengan ''H''<sub>''T''</sub>, dan keluarga elemen 〈[''A''<sub>''i''</sub>]〉.

Setiap aljabar Heyting isomorfik ke salah satu bentuk ''H''<sub>''T''</sub>. Untuk melihat ini, misalkan ''H'' berupa aljabar Heyting, dan maka 〈''a''<sub>''i''</sub>: ''i''∈I〉 sebagai keluarga elemen dengan hasil ''H'' (misalnya, keluarga surjektif). Dengan memperhatikan himpunan ''T'' dari rumus ''J''(〈''A''<sub>''i''</sub>〉) dalam variabel 〈''A''<sub>''i''</sub>: ''i''∈I〉 seperti ''J''(〈''a''<sub>''i''</sub>〉)=1. Maka, memperoleh morfisme ''f'':''H''<sub>''T''</sub>→''H'' dengan sifat universal ''H''<sub>''T ''</sub>, yang jelas-jelas surjektif. Tidak sulit untuk menunjukkan bahwa ''f'' adalah injektif.

=== Perbandingan dengan aljabar Lindenbaum ===
Konstruksi yang diberikan memainkan peran memenuhi analog sehubungan dengan aljabar Heyting dengan [[aljabar Lindenbaum]] berhubungan dengan [[Aljabar Boolean (struktur)|Aljabar Boolean]]. Faktanya, aljabar Lindenbaum ''B''<sub>''T''</sub> dalam variabel {''A''<sub>''i''</sub>} sehubungan dengan aksioma ''T'' bersama ''H''<sub>''T''∪''T''<sub>1</sub></sub>, dimana ''T''<sub>1</sub> adalah himpunan semua rumus dari formulir ¬¬''F''→''F'', karena aksioma tambahan ''T''<sub>1</sub> adalah satu-satunya aksioma yang perlu ditambahkan agar semua tautologi klasik pembuktian.

== Aljabar Heyting seperti yang diterapkan pada logika intuisi ==
Jika menafsirkan aksioma logika proposisional intuisionistik sebagai istilah dari aljabar Heyting, apabila mengevaluasi ke elemen terbesar 1, dalam aljabar Heyting ''hanya'' di bawah penetapan nilai ke variabel rumus. Misalnya, (''P''∧''Q'')→''P'' adalah apabila definisi kelengkapan semu dengan elemen terbesar ''x'' sehingga <math>P \land Q \land x \le P</math>. Pertidaksamaan ini dipenuhi untuk setiap ''x'', sebagai ''x'' yang terbesar adalah 1.

Selanjutnya, kaidah [[modus ponens]] memungkinkan kita untuk menurunkan rumus ''Q'' dari rumus ''P'' dan ''P''→''Q''. Namun dalam aljabar Heyting, jika ''P'' bernilai 1, dan ''P''→''Q'' bernilai 1, maka itu berarti <math>P \land 1 \le Q</math>, dan maka <math>1 \land 1 \le Q</math>; hanya mungkin ''Q'' memiliki nilai 1.

Ini berarti bahwa jika suatu rumus dapat diturunkan dari hukum logika intuisionistik, yang diturunkan dari aksiomanya melalui kaidah modus ponens, maka apabila nilai 1 di semua aljabar Heyting di bawah penetapan nilai hanya ke variabel rumus. Namun apabila membangun aljabar Heyting di mana nilai hukum Peirce tidak selalu 1. Pertimbangkan aljabar 3-elemen {0,{{sfrac|1|2}},1} seperti yang diberikan di atas. Jika menetapkan {{sfrac|1|2}} ke ''P'' dan 0 ke ''Q'', maka nilai hukum Peirce ((''P''→''Q'')→'' P'')→''P'' adalah {{sfrac|1|2}}. Oleh karena itu, hukum Peirce tidak dapat diturunkan secara intuitif. Lihat [[isomorfisme Curry–Howard]] untuk konteks umum tentang apa yang menjelaskan dalam [[teori tipe]].

Kebalikannya juga dapat dibuktikan: jika suatu rumus selalu bernilai 1, maka rumus tersebut dapat dikurangkan dari hukum logika intuisionistik, jadi rumus "valid secara intuitif" adalah rumus yang selalu memiliki nilai 1. Ini mirip dengan gagasan bahwa rumus yang "valid secara klasik" adalah rumus yang memiliki nilai 1 di [[aljabar Boolean dua elemen]] di bawah kemungkinan penetapan nilai benar dan salah ke variabel rumus—yaitu, yaitu rumus yang merupakan tautologi dalam pengertian tabel kebenaran yang biasa. Aljabar Heyting, dari sudut pandang logika, merupakan generalisasi dari sistem nilai kebenaran yang biasa, dan elemen terbesarnya 1 dianalogikan dengan 'benar'. Sistem logika dua nilai yang biasa adalah kasus khusus dari aljabar Heyting, dan yang terkecil non-trivial, dimana satu-satunya elemen aljabar adalah 1 (benar) dan 0 (salah).

== Masalah keputusan ==
Masalah apakah persamaan yang diberikan berlaku di setiap aljabar Heyting pembuktian apabila ditentukan oleh S. Kripke pada tahun 1965.<ref name="Kripke63" /> [[Teori kompleksitas komputasional|Kompleksitas komputasi]] yang tepat dari masalah ini dibuat oleh R. Statman pada tahun 1979, yang menunjukkan [[kelengkapan-RUANGP]]<ref>{{cite journal | last1 = Statman | first1 = R. | year = 1979 | title = Intuitionistic propositional logic is polynomial-space complete | journal = Theoretical Comput. Sci. | volume = 9 | pages = 67–72 | doi=10.1016/0304-3975(79)90006-9| hdl = 2027.42/23534 | hdl-access = free }}</ref> dan karenanya setidaknya [[Masalah kepuasan Boolean|memutuskan persamaan aljabar Boolean]] (ditunjukkan oleh ''coNP-complete'' pada tahun 1971 oleh S. Cook)<ref name="Cook71">{{Cite news|last = Cook  | first = S.A. | author-link = Stephen A. Cook  | title = The complexity of theorem proving procedures
 | book-title = Proceedings, Third Annual ACM Symposium on the Theory of Computing, ACM, New York | year = 1971 | pages = 151–158 | doi = 10.1145/800157.805047}}</ref> dan diperkirakan akan jauh lebih sulit. Teori dasar atau urutan pertama dari aljabar Heyting tidak dapat diputuskan.<ref>{{cite journal | last1 = Grzegorczyk | first1 = Andrzej | author-link = Andrzej Grzegorczyk | year = 1951 | title = Undecidability of some topological theories | url =https://www.impan.pl/shop/publication/transaction/download/product/93826?download.pdf | journal = Fundamenta Mathematicae | volume = 38 | pages = 137–52 }}</ref> Masih terbuka apakah [[teori universal Horn]] dari aljabar Heyting, atau [[masalah kata (matematika)|masalah kata]], apabila ditentukan.<ref>Peter T. Johnstone, ''Stone Spaces'', (1982) Cambridge University Press, Cambridge, {{ISBN|0-521-23893-5}}. ''(See paragraph 4.11)''</ref> Sebuah propos dari masalah kata diketahui bahwa aljabar Heyting tak hingga secara lokal (tidak ada aljabar Heyting yang dihasilkan oleh himpunan tak kosong hingga), berbeda dengan aljabar Boolean hingga secara lokal dan masalah kata yang dapat ditentukan. Tidak diketahui apakah aljabar Heyting lengkap gratis ada kecuali dalam kasus generator tunggal dimana aljabar Heyting bebas pada satu generator yang diselesaikan secara sederhana dengan menghubungkan puncak baru.

== Catatan ==
{{Reflist}}

== Lihat pula ==
* [[topologi Alexander]]
* [[Logika menengah|Logika superintuitif (alias menengah)]]
* [[Daftar topik aljabar Boolean]]
* [[Aljabar Ockham]]

== Referensi ==
* {{cite book | first = Daniel Edwin | last = Rutherford | year = 1965 | title = Introduction to Lattice Theory | publisher = Oliver and Boyd | oclc = 224572 }}
* F. Borceux, ''Handbook of Categorical Algebra 3'', In ''Encyclopedia of Mathematics and its Applications'', Vol. 53, [[Cambridge University Press]], 1994. {{ISBN|0-521-44180-3}} {{OCLC|52238554}}
* G. Gierz, K.H. Hoffmann, K. Keimel, J. D. Lawson, M. Mislove and D. S. Scott, ''Continuous Lattices and Domains'', In ''Encyclopedia of Mathematics and its Applications'', Vol. 93, Cambridge University Press, 2003.
* S. Ghilardi. ''Free Heyting algebras as bi-Heyting algebras'', Math. Rep. Acad. Sci. Canada XVI., 6:240–244, 1992.
*{{citation|last=Heyting|first= A.
|title=Die formalen Regeln der intuitionistischen Logik. I, II, III|jfm= 56.0823.01
|journal=Sitzungsberichte Akad. Berlin |year=1930|pages= 42–56, 57–71, 158–169 }}

== Pranala luar ==
* {{PlanetMath|urlname=heytingalgebra|title=Aljabar Heyting}}

{{DEFAULTSORT:Heyting Algebra}}
[[Kategori:Teori kekisi]]
[[Kategori:Konstruktivisme (matematika)]]
[[Kategori:Logika aljabar]]