 Each of the above logics turns out decidable (i.e. has a decidable set of validities), which is typically shown by proving the so-called finite model property (“Every satisfiable formula is satisfiable in a finite model”), in most cases, with respect to non-standard finite models. For detailed proofs of completeness of variations of these axiomatic systems as well as proofs of decidability, see Segerberg (1970); Rescher and Urquhart (1971); Burgess (1979); Burgess and Gurevich (1985); Goldblatt (1992); and Gabbay et al. (1994).