Tolong jelaskan mengenai Identitas pembuktian dari Aljabar Heyting

Diberikan rumus  dari kalkulus proposisional (menggunakan, variabel, penghubung , 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  untuk setiap aljabar Heyting H dan elemen .

Metaimplikasi  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  jika dan hanya jika a→b = 1, mengikuti dari  bahwa setiap kali rumus F→G pembuktian dengan benar, kita memiliki  untuk setiap aljabar Heyting H, dan elemen . 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 , 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 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 dalam logika klasik, tidak bisa dibuktikan dalam logika proposisional intuisionis. Untuk membuktikan bahwa beberapa rumus  tidak dapat dibuktikan, cukup dengan menunjukkan aljabar Heyting H dan elemen  sedemikian rupa sehingga .

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 .

Untuk lebih lanjut tentang metaimplication 2 ⇒ 1, lihat bagian "konstruksi universal" dibawah.