Sequent Soundness, Completeness, and More

We are about to prove several principal facts about GS4: semantical complete­ness, finite model property, equivalency of sequent GS4 and Hilbert-style S4 axiomatizations, and cut-elimination in GS4, in one theorem.

Theorem 5.9 The following are equivalent

Proof Items “(1) yields (2)” and “(4) yields (5)” hold vacuously. Item “(3) yields (4)” is the well-known fact of soundness of axiomatic S4 with respect to S4-models.

Item “(2) yields (3)” states the soundness of sequent rules with respect to S4 and its proof consists of checking that axioms and rules of GS4 are S4 com­pliant. The cases of axioms, propositional, and structural rules are straightfor­ward, and we only check the modal rules.

By necessitation,

by normality,

hence

It remains to establish that (5) yields (1), which we show Contrapositively as “not (1)” yields “not (5).” Specifically, we show that from a sequent that is not derivable inwe can build a finite S4-modeland a

world„ such that all formulas from Γ are true and all formulas from A are false at Γ.

For the rest of this argument for Theorem 5.9, we assumeis not

provable in, the negation of item (1) of the Theorem.

Proof We eliminate all violations of the saturation property one by one with­out repetitions, in the following way.

Corollary 5.13 All the following hold.

(1) Equivalence of axiomatic S4 and GS4:

In particular,

(2) S4 is complete with respect to the class of transitive reflexive models.

5.5