No.63 Referenced from ~ Part2 - Chapter 2 - Hard study 5-5-4

The Type II proof tables for the Kripke system

When I saw the sentence, "There is no Heyting algebraic model that can express all theorems/non-theorems in intuitionistic logic", "plank in my own eye" was removed. If that is the case, the situation changes dramatically.

It is natural that the Type I proof tables for the Kripke system that I have created do not all correctly represent 12 logical formulas, and it is possible that the Type II proof tables function as a proof table that complements the Type I proof tables.

The number of rows and proof values ​​of a Type I proof tables are exactly the same as the truth tables for the simplest (but still difficult) 3-valued Heyting algebra {0, 1/2, 1}, and the 5-valued Heyting algebra {0, 1/3, 1/3', 2/3, 1} is similar in some respects to a Type II proof tables.

The 5-valued Heyting algebra model is used to show the non-theorem of De Morgan law (2)a, just like my Type II proof tables. Moreover, this 5-valued Heyting algebra defines three types of false, just like my Type II proof tables.