 The other connectives can be defined in the usual way. Validity is expressed as a λ-term, λsι→ο∀wι sw, that when applied to a term sσ we write as [sσ]. For example, under the embedding, proving in HOML the possibility of God’s existence, ◊ο→ο∃(μ→ο)→ο Xμ . gμ→ο X, is tantamount to proving its validity in HOL: [◊•σ→σ∃•(μ→σ)→σ Xμ . gμ→σ X]μ→ο. To prove so, the type-raised HOL expression [◊•∃•Xμ . gμ→σ X] is then encoded in the so-called THF0 syntax (Sutcliffe &amp; Benzmüller 2010) prior to being fed, along with the above set of equality rules, to the provers that were used in completing the proof: 