Definition. Semantic Entailment \(\models \) (FOL) [0015]

We evaluate formulas in first order logic under a structure which consists of a domain and an interpretation function. In addition, we need a variable assignment to evaluate formulas with free variables. To denote truth under a structure \(S\) and variable assignment \(\sigma \) we write:

  • True: If a formula \(F\) evaluates to true under \(U, I, \sigma \) we write \[U, I, \sigma \models F\]
  • False: If a formula \(F\) evaluates to false under \(U, I, \sigma \) we write \[U, I, \sigma \nvDash F\]

We can define semantic entailment inductively as follows: