IndisputableMonolith.Loom.Semantics

   1import IndisputableMonolith.Loom.Grammar
   2
   3/-!
   4# What the content means, so that "different content" is not a matter of taste
   5
   6The separation theorem says two utterances lie in different gauge orbits. That is only
   7interesting if the two pieces of content really are different claims, and syntactic
   8inequality does not establish it: two formulas can differ as trees and agree as claims, and
   9a pair of them would be an EMBARRASSMENT rather than a witness, since the language would be
  10drawing a distinction the logic does not.
  11
  12So content gets a semantics here, and the witness's distinctness becomes a theorem: exhibit
  13one finite model in which one member holds and the other fails.
  14
  15The interpretation is the plainest one available. There is a single finite universe, shared
  16by every bound name, and a bound name is a variable rather than a sort. That choice is the
  17load-bearing part of this file. A two-sorted reading, where `door` ranges over the doors,
  18would make more pairs distinct and would be perfectly defensible as English, but it is a
  19stronger assumption, and a witness that needs it is a weaker witness. Measured before
  20choosing: 88 of the 112 pairs in the searched family that defeat a labelled-adjacency
  21reading remain distinct on this plainer reading, so insisting on it cost almost nothing
  22(`Loom/family/sorted_reading_probe.json`).
  23
  24`Expr` is in negation normal form, so denial rides on the atom and there is no separate
  25case for it.
  26-/
  27
  28namespace IndisputableMonolith
  29namespace Loom
  30
  31/-- An interpretation over the universe `Fin n`: which tuples each relation holds of.
  32Relations are given as a predicate on the argument list, so arity is whatever the atom
  33brings and nothing has to be declared in advance. -/
  34structure Model (n : Nat) where
  35  holds : Nat → List (Fin n) → Bool
  36
  37/-- An assignment of bound names to elements. Names not bound above an atom never reach
  38it, because `weave` refuses content with a free name. -/
  39abbrev Assign (n : Nat) := Nat → Fin n
  40
  41def Assign.set {n : Nat} (env : Assign n) (name : Nat) (x : Fin n) : Assign n :=
  42  fun m => if m = name then x else env m
  43
  44/-- Truth of content in a model, decidable because the universe is finite. -/
  45def evalExpr {n : Nat} (M : Model n) (env : Assign n) : Expr → Bool
  46  | .atom p args denied =>
  47      let v := M.holds p (args.map env)
  48      if denied then !v else v
  49  | .conj a b => evalExpr M env a && evalExpr M env b
  50  | .quant universal name body =>
  51      if universal then
  52        (List.finRange n).all fun x => evalExpr M (env.set name x) body
  53      else
  54        (List.finRange n).any fun x => evalExpr M (env.set name x) body
  55
  56/-- Two pieces of content are DIFFERENT CLAIMS when some model tells them apart. This is
  57the property a separation witness needs, and syntactic inequality is not it. -/
  58def SeparatedBy {n : Nat} (M : Model n) (env : Assign n) (a b : Expr) : Prop :=
  59  evalExpr M env a ≠ evalExpr M env b
  60
  61instance {n : Nat} (M : Model n) (env : Assign n) (a b : Expr) :
  62    Decidable (SeparatedBy M env a b) := by
  63  unfold SeparatedBy; infer_instance
  64
  65end Loom
  66end IndisputableMonolith
  67