What are propositions and sets? Why are they related to us?

  It's been a widely known truth that Sets have some relations with Boolean Algebra and propositions, intuitively, the union of sets resemble the disjunction of propositions, and the intersection of sets resemble the conjunction of propositions, the \tt True and \tt False corresponds to the universal set \mathcal U and the empty set \empty. Consider a group of people where each of them have different age and occupations, we can easily write down some propositons like "A's occupation is postman" or "C is a 20-year-old boy", or, we can take all the people with occupation "doctor" and say "these guys are doctors", this statement itself is undoubtedly a proposition, while it also describes a set perfectly, this fit our intuition because, well, the propositions are mostly used to filtrate objects around us in our daily life.
  But, how exactly can we formalize this intuition, and make it a rigorous definition? People is just one kind of objects, there are countless many different kind of objects and things around us, and since one of the most important thing in mathematics is abstraction, we need to find a way to generalize all of these objects, establish a solid connection between "objects" and "propositions" (or assertions, whatever)

Models come to the rescue

This is really the most foundamental thing, but in order to get a better intuition about what I'm going to say, you may want to read what is inductive definition/recursive definition first.

[Definition] Model (in Propositional Logic)

Let set of all propositions be \mathcal S, A model \mathcal M for propositions consists of a set of objects, called universe of \mathcal M, written in \mathcal{U_M}, and interpretation function \llbracket p\rrbracket_\mathcal{M}:\mathcal{S}\to\mathcal{P(U_M)}, which is a function that given a proposition p, gives you a subset of \mathcal{U_M} that satisfies the proposition p, it is recursively defined by following cases:

\begin{aligned}
\llbracket\top \rrbracket_\mathcal{M} &= \mathcal{U_M}\\
\llbracket\bot\rrbracket_\mathcal{M} &= \empty\\
\llbracket p\land q\rrbracket_\mathcal{M}&= \llbracket p \rrbracket_\mathcal{M}\cap\llbracket q \rrbracket_\mathcal{M}\\
\llbracket p\lor q\rrbracket_\mathcal{M} &= \llbracket p \rrbracket_\mathcal{M}\cup\llbracket q \rrbracket_\mathcal{M}\\
\llbracket \neg p \rrbracket_\mathcal{M} &= \complement_{\mathcal{U_M}}^{\llbracket p\rrbracket_\mathcal{M}}
\end{aligned}

As for the implication(p \implies q) and equivalence(p \iff q), in propositional logic, they can be interpreted (lowered) as \neg p \lor q and p\implies q \land q\implies p, thus makes them just shorthand forms1.
  This defintion can be implemented in programming languages using a syntax-directed way:

enum Proposition:
  case True extends Proposition
  case False extends Proposition
  case Not(val prop: Proposition) extends Proposition
  case And(val left: Proposition, val right: Proposition) extends Proposition
  case Or(val left: Proposition, val right: Proposition) extends Proposition
  case Implication(val left: Proposition, val right: Proposition) extends Proposition
  case Equivalence(val left: Proposition, val right: Proposition) extends Proposition
  case Variable(name: String) extends Proposition
end Proposition

trait Model[T]:
  val universe: Set[T]
  def predicate(variable: Proposition.Variable): Set[T]
  def interpret(p: Proposition): Set[T] =
    import Proposition._
    p match
      case True => universe
      case False => Set.empty
      case Not(prop) => universe -- interpret(prop)
      case And(left, right) => interpret(left) & interpret(right)
      case Or(left, right) => interpret(left) | interpret(right)
      case Implication(left, right) => interpret(Or(Not(left), right))
      case Equivalence(left, right) => interpret(And(Implication(left, right), Implication(right, left)))
      case a @ Variable(_) => predicate(a)
end Model

def interpret[T](i: Proposition)(using model: Model[T]): Set[T] =
  model.interpret(i)

  Notice that the universe \mathcal{U_M} corresponds to the people in the example above, this set now abstracts away the detail of objects, you can think of it as a container of anything, people, cars, phones, or even metaphysical objects that do not exist in real world. The key part is the interpretation function, it basically acts as a filter, with an proposition as input, gives you all items that satisfies that proposition in \mathcal{U_M} as output. For example, one can formulate a model \mathcal{H} to represent the hardware circuit that described in the following paragraph.
  Assume that there is a set of connection points a, b, c, ... on a wiring board, each of which can be of two states: high voltage and low voltage, we can assign a set of mappings \mathcal{V} (called assignments) that specifies the voltage of every point, for example, if the set of points are \lbrace a, b, c, d\rbrace, then both \lbrace a\mapsto\top, b\mapsto\top, c\mapsto\bot, d\mapsto\bot\rbrace and \lbrace a\mapsto\bot, b\mapsto\top, c\mapsto\top, d\mapsto\bot\rbrace are valid assignments (we use \top to denote high voltage and \bot to denote low voltage). Now, let the universe \mathcal{U_H} be the set of all points, and define the interpretation function \llbracket a\rrbracket_\mathcal{H} to be family of sets \mathcal{W} such that \forall w\in \mathcal{W}. a\in w\land w(a)=\top, that is, a family of sets that each element assigns \top to point a, so now under this context, we can consider a proposition a as "a is in high voltage", then the interpretation function will be the function that finds all assignments that assigns a high voltage to point a.
  This example, again, can be implemented using scala combined with the above definition:

given CircuitModel: Model[SortedSet[(Char, Boolean)]] = new Model[SortedSet[(Char, Boolean)]]:
  override val universe: Set[SortedSet[(Char, Boolean)]] = ('a' to 'z').let { range =>
    // all assignments that assigns a true (high voltage) or false (low voltage) to point a to z
    val assignments = Set(
      List(false, true, false, true, true, false, true, true, false, false, false, true, true, false, false, true, false, false, true, true, true, true, true, false, false, false),
      List(true, false, true, true, false, false, true, false, true, false, true, true, false, false, false, true, true, false, true, true, true, false, true, false, true, true),
      List(false, false, false, true, false, true, false, true, false, true, true, true, false, false, false, true, false, false, true, false, true, false, false, true, false, false),
      List(true, true, false, true, true, false, true, true, true, false, true, true, true, true, true, true, true, true, true, true, true, false, true, true, false, false),
      List(false, false, false, true, false, true, false, true, true, true, false, true, true, false, true, false, false, false, false, true, true, true, true, true, false, true),
      List(false, false, false, false, false, false, false, true, false, true, true, true, false, true, false, false, false, false, false, false, false, true, true, true, false, false),
      List(true, false, true, false, true, false, false, false, false, false, false, true, true, false, false, false, false, true, false, false, false, false, false, false, true, false),
      List(true, false, true, false, false, true, false, false, false, true, true, false, false, false, false, false, true, true, false, false, true, true, false, false, true, false),
      List(true, true, false, false, false, true, true, true, false, true, true, false, false, false, false, true, true, false, true, true, false, false, true, true, false, true),
      List(true, true, true, false, true, false, false, false, true, true, false, false, false, false, false, true, true, true, false, false, true, true, false, true, true, true)
    )
    assignments.map(a => SortedSet.from(range.zip(a)))
  }

  override def predicate(variable: Proposition.Variable): Set[SortedSet[(Char, Boolean)]] =
    universe.filter(_.contains((variable.name(0), true)))
end CircuitModel

now we can ask the model to see if there are any assignment that fits out needs, e.g., if we need an assignment such that a\implies b \iff h\implies k, we can call interpret[SortedSet[(Char, Boolean)]](Equivalence(Implication(Variable("a"), Variable("b")), Implication(Variable("h"), Variable("k")))) and get the result.

[Definition] Validity and Entailment

  A proposition p is said to be valid in model \mathcal{M} if \llbracket p\rrbracket_{\mathcal{M}} = \mathcal{U_M}. It measn that p is true for all states of \mathcal{M}, i.e., p is a tautology in \mathcal{M}. For propositions p and q, p entails q iff \llbracket p\rrbracket_\mathcal{M}\sube \llbracket q\rrbracket_\mathcal{M}, i.e., if a statement satisifes p, then it also satisfies q.
  We say a proposition p is valid iff it's valid in all models, written:

\vDash p

Similarly, we write

p\vDash q

to show that p entails q. If p entails q in all models, we say that p and q are equivalent, give us p = q, this indicates that p\vDash q and q\vDash p, i.e., \llbracket p\rrbracket_{\mathcal{M}}=\llbracket q\rrbracket_{\mathcal{M}} in all models \mathcal{M}

Difference between entailments and implications

  Implications themselves are also propositions, while this is not true for entailments, entailments are relations between propositions. How ever, they do have subtle connections which can be captured by following statement:

p entails q in a model \mathcal{M} iff p\implies q is valid in \mathcal{M}, i.e.,:

p\vDash q \iff \vDash (p\implies q)

Analogously, we can deduce that:

p = q\iff \vDash (p\iff q)

  1. Note this interpretation is not allowed in intuitionistic logic ↩︎

We Choose to Go to the Moon