Documentation

Trestle.Model.Quantifiers

Quantification #

This file characterizes existential and universal quantification of variables in a PropFun.

source
noncomputable def Trestle.Model.PropFun.existsAssn {ν' : Type u_1} [Fintype ν'] {ν : Type u_2} (f : PropAssignment ν → PropAssignment ν') (φ : PropFun ν) :
PropFun ν'

Most general form of existential quantification. True at τ iff there exists a model of φ whose image under f is τ.

Equations
Instances For
    source
    @[simp]
    theorem Trestle.Model.PropFun.satisfies_exists {ν' : Type u_2} [Fintype ν'] {ν : Type u_1} {φ : PropFun ν} (f : PropAssignment ν → PropAssignment ν') (τ : PropAssignment ν') :
    τ ⊨ existsAssn f φ ↔ ∃ (σ : PropAssignment ν), σ ⊨ φ ∧ τ = f σ
    source
    noncomputable def Trestle.Model.PropFun.existsInv {ν' : Type u_1} [Fintype ν'] {ν : Type u_2} (f : ν' → ν) (φ : PropFun ν) :
    PropFun ν'
    Equations
    Instances For
      source
      @[simp]
      theorem Trestle.Model.PropFun.satisfies_existsInv {ν' : Type u_2} [Fintype ν'] {ν : Type u_1} (f : ν' → ν) (φ : PropFun ν) (τ : PropAssignment ν') :
      τ ⊨ existsInv f φ ↔ ∃ (σ : PropAssignment ν), σ ⊨ φ ∧ τ = PropAssignment.map f σ
      source
      @[simp]
      theorem Trestle.Model.PropFun.existsInv_existsInv {ν' : Type u_3} [Fintype ν'] {ν'' : Type u_1} {ν : Type u_2} [Fintype ν''] (f : ν'' → ν') (g : ν' → ν) (φ : PropFun ν) :
      existsInv f (existsInv g φ) = existsInv (g ∘ f) φ
      source
      noncomputable def Trestle.Model.PropFun.forallAssn {ν' : Type u_1} [Fintype ν'] {ν : Type u_2} (f : PropAssignment ν → PropAssignment ν') (φ : PropFun ν) :
      PropFun ν'

      Most general form of universal quantification. True at τ iff for all models of φ, their image under f is τ.

      Equations
      Instances For
        source
        @[simp]
        theorem Trestle.Model.PropFun.satisfies_forallAssn {ν' : Type u_2} [Fintype ν'] {ν : Type u_1} {φ : PropFun ν} (f : PropAssignment ν → PropAssignment ν') (τ : PropAssignment ν') :
        τ ⊨ forallAssn f φ ↔ ∀ (σ : PropAssignment ν), σ ⊨ φ → τ = f σ
        source
        noncomputable def Trestle.Model.PropFun.forallInv {ν' : Type u_1} [Fintype ν'] {ν : Type u_2} (f : ν' → ν) (φ : PropFun ν) :
        PropFun ν'
        Equations
        Instances For
          source
          @[simp]
          theorem Trestle.Model.PropFun.satisfies_forallInv {ν' : Type u_2} [Fintype ν'] {ν : Type u_1} (f : ν' → ν) (φ : PropFun ν) (τ : PropAssignment ν') :
          τ ⊨ forallInv f φ ↔ ∀ (σ : PropAssignment ν), σ ⊨ φ → τ = PropAssignment.map f σ