 Kripke’s completeness proof makes use of Beth’s method of semantic tableaux. A semantic tableau is used to test whether a formula \(B\) is a semantic consequence of some formulas \(A_1, \ldots, A_n\). The tableau assumes that the formulas \(A_1, \ldots, A_n\) are true and \(B\) is false and is built according to rules that follow the definitions of the logical connectives. For example, if a formula \(\neg A\) is on the left column of the tableau (where true formulas are listed), \(A\) will be put on the right column (where false formulas are listed). To deal with modal formulas, sets of tableaux must be considered, since if \(\Box A\) is on the right column of a tableau, a new auxiliary tableau must be introduced with \(A\) on its right column. A main tableau and its auxiliary tableaux form a set of tableaux. If a formula \(A\wedge B\) is on the right column of the main tableau, the set of tableaux splits into two new sets of tableaux: one whose main tableau lists \(A\) on its right column and one whose main tableau lists \(B\) on the right column. So we have to consider alternative sets of tableaux. A semantic tableau is closed if and only if all its alternative sets are closed. A set of tableaux is closed if it contains a tableau (main or auxiliary) that reaches a contradiction in the form of (i) one and the same formula \(A\) appearing in both its columns or (ii) an identity formula of the form \(a = a\) in its right side (this is an oversimplification of the definition of a closed tableau, but not harmful for our purposes). Oversimplifying once more, the structure of Kripke’s completeness proof consists of proving that a semantic tableau used to test whether a formula \(B\) is a semantic consequence of formulas \(A_1, \ldots, A_n\) is closed if and only (i) in S5*\(^=\) \(A_1, \ldots, A_n\vdash B\) and (ii) \(A_1, \ldots, A_n\vDash B\). This last result is achieved by showing how to build models from semantic tableaux. As a consequence of (i) and (ii) we have soundness and completeness for S5*\(^=\), that is: \(A_1, \ldots, A_n\vdash B\) if and only if \(A_1, \ldots, A_n\vDash B\).