Formulas of first-order logic #
This file defines the formulas of first-order logic.
φ : Semiformula L ξ n
is a (semi-)formula of language L
with bounded variables of Fin n
and free variables of ξ
.
The quantification is represented by de Bruijn index.
- verum: {L : LO.FirstOrder.Language} → {ξ : Type u_1} → {n : ℕ} → LO.FirstOrder.Semiformula L ξ n
- falsum: {L : LO.FirstOrder.Language} → {ξ : Type u_1} → {n : ℕ} → LO.FirstOrder.Semiformula L ξ n
- rel: {L : LO.FirstOrder.Language} → {ξ : Type u_1} → {n arity : ℕ} → L.Rel arity → (Fin arity → LO.FirstOrder.Semiterm L ξ n) → LO.FirstOrder.Semiformula L ξ n
- nrel: {L : LO.FirstOrder.Language} → {ξ : Type u_1} → {n arity : ℕ} → L.Rel arity → (Fin arity → LO.FirstOrder.Semiterm L ξ n) → LO.FirstOrder.Semiformula L ξ n
- and: {L : LO.FirstOrder.Language} → {ξ : Type u_1} → {n : ℕ} → LO.FirstOrder.Semiformula L ξ n → LO.FirstOrder.Semiformula L ξ n → LO.FirstOrder.Semiformula L ξ n
- or: {L : LO.FirstOrder.Language} → {ξ : Type u_1} → {n : ℕ} → LO.FirstOrder.Semiformula L ξ n → LO.FirstOrder.Semiformula L ξ n → LO.FirstOrder.Semiformula L ξ n
- all: {L : LO.FirstOrder.Language} → {ξ : Type u_1} → {n : ℕ} → LO.FirstOrder.Semiformula L ξ (n + 1) → LO.FirstOrder.Semiformula L ξ n
- ex: {L : LO.FirstOrder.Language} → {ξ : Type u_1} → {n : ℕ} → LO.FirstOrder.Semiformula L ξ (n + 1) → LO.FirstOrder.Semiformula L ξ n
Instances For
@[reducible, inline]
Equations
- LO.FirstOrder.Formula L ξ = LO.FirstOrder.Semiformula L ξ 0
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
def
LO.FirstOrder.Semiformula.neg
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
:
LO.FirstOrder.Semiformula L ξ n → LO.FirstOrder.Semiformula L ξ n
Equations
- LO.FirstOrder.Semiformula.verum.neg = LO.FirstOrder.Semiformula.falsum
- LO.FirstOrder.Semiformula.falsum.neg = LO.FirstOrder.Semiformula.verum
- (LO.FirstOrder.Semiformula.rel r v).neg = LO.FirstOrder.Semiformula.nrel r v
- (LO.FirstOrder.Semiformula.nrel r v).neg = LO.FirstOrder.Semiformula.rel r v
- (φ.and ψ).neg = φ.neg.or ψ.neg
- (φ.or ψ).neg = φ.neg.and ψ.neg
- φ.all.neg = φ.neg.ex
- φ.ex.neg = φ.neg.all
Instances For
theorem
LO.FirstOrder.Semiformula.neg_neg
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ : LO.FirstOrder.Semiformula L ξ n)
:
φ.neg.neg = φ
instance
LO.FirstOrder.Semiformula.instLogicalConnective
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
:
Equations
- LO.FirstOrder.Semiformula.instLogicalConnective = LO.LogicalConnective.mk
instance
LO.FirstOrder.Semiformula.instDeMorgan
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
:
LO.DeMorgan (LO.FirstOrder.Semiformula L ξ n)
Equations
- ⋯ = ⋯
Equations
- LO.FirstOrder.Semiformula.instQuantifier = LO.Quantifier.mk
def
LO.FirstOrder.Semiformula.toStr
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
[(k : ℕ) → ToString (L.Func k)]
[(k : ℕ) → ToString (L.Rel k)]
[ToString ξ]
{n : ℕ}
:
LO.FirstOrder.Semiformula L ξ n → String
Equations
- LO.FirstOrder.Semiformula.verum.toStr = "\\top"
- LO.FirstOrder.Semiformula.falsum.toStr = "\\bot"
- (LO.FirstOrder.Semiformula.rel r a).toStr = "{" ++ toString r ++ "}"
- (LO.FirstOrder.Semiformula.rel r v).toStr = ("{" ++ toString r ++ "} \\left(" ++ String.vecToStr fun (i : Fin (n_1 + 1)) => toString (v i)) ++ "\\right)"
- (LO.FirstOrder.Semiformula.nrel r a).toStr = "\\lnot {" ++ toString r ++ "}"
- (LO.FirstOrder.Semiformula.nrel r v).toStr = ("\\lnot {" ++ toString r ++ "} \\left(" ++ String.vecToStr fun (i : Fin (n_1 + 1)) => toString (v i)) ++ "\\right)"
- (φ.and ψ).toStr = "\\left(" ++ φ.toStr ++ " \\land " ++ ψ.toStr ++ "\\right)"
- (φ.or ψ).toStr = "\\left(" ++ φ.toStr ++ " \\lor " ++ ψ.toStr ++ "\\right)"
- φ.all.toStr = "(\\forall x_{" ++ toString n ++ "}) " ++ φ.toStr
- φ.ex.toStr = "(\\exists x_{" ++ toString n ++ "}) " ++ φ.toStr
Instances For
instance
LO.FirstOrder.Semiformula.instRepr
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[(k : ℕ) → ToString (L.Func k)]
[(k : ℕ) → ToString (L.Rel k)]
[ToString ξ]
:
Repr (LO.FirstOrder.Semiformula L ξ n)
Equations
- LO.FirstOrder.Semiformula.instRepr = { reprPrec := fun (t : LO.FirstOrder.Semiformula L ξ n) (x : ℕ) => Std.Format.text t.toStr }
instance
LO.FirstOrder.Semiformula.instToString
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[(k : ℕ) → ToString (L.Func k)]
[(k : ℕ) → ToString (L.Rel k)]
[ToString ξ]
:
ToString (LO.FirstOrder.Semiformula L ξ n)
Equations
- LO.FirstOrder.Semiformula.instToString = { toString := LO.FirstOrder.Semiformula.toStr }
@[simp]
@[simp]
@[simp]
theorem
LO.FirstOrder.Semiformula.neg_rel
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n k : ℕ}
(r : L.Rel k)
(v : Fin k → LO.FirstOrder.Semiterm L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.neg_nrel
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n k : ℕ}
(r : L.Rel k)
(v : Fin k → LO.FirstOrder.Semiterm L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.neg_and
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.neg_or
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.neg_all
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ : LO.FirstOrder.Semiformula L ξ (n + 1))
:
@[simp]
theorem
LO.FirstOrder.Semiformula.neg_ex
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ : LO.FirstOrder.Semiformula L ξ (n + 1))
:
@[simp]
theorem
LO.FirstOrder.Semiformula.neg_neg'
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.neg_inj
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.neg_univClosure
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.neg_exClosure
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ : LO.FirstOrder.Semiformula L ξ n)
:
theorem
LO.FirstOrder.Semiformula.neg_eq
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ : LO.FirstOrder.Semiformula L ξ n)
:
theorem
LO.FirstOrder.Semiformula.imp_eq
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
theorem
LO.FirstOrder.Semiformula.iff_eq
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
theorem
LO.FirstOrder.Semiformula.ball_eq
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ (n + 1))
:
theorem
LO.FirstOrder.Semiformula.bex_eq
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ (n + 1))
:
@[simp]
theorem
LO.FirstOrder.Semiformula.neg_ball
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ (n + 1))
:
@[simp]
theorem
LO.FirstOrder.Semiformula.neg_bex
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ (n + 1))
:
@[simp]
theorem
LO.FirstOrder.Semiformula.and_inj
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ₁ ψ₁ φ₂ ψ₂ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.or_inj
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ₁ ψ₁ φ₂ ψ₂ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.all_inj
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ (n + 1))
:
@[simp]
theorem
LO.FirstOrder.Semiformula.ex_inj
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ (n + 1))
:
@[simp]
theorem
LO.FirstOrder.Semiformula.univClosure_inj
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.exClosure_inj
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.univItr_inj
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n k : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ (n + k))
:
@[simp]
theorem
LO.FirstOrder.Semiformula.exItr_inj
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n k : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ (n + k))
:
@[simp]
theorem
LO.FirstOrder.Semiformula.imp_inj
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
{φ₁ φ₂ ψ₁ ψ₂ : LO.FirstOrder.Semiformula L ξ n}
:
@[reducible, inline]
abbrev
LO.FirstOrder.Semiformula.rel!
{ξ : Type u_1}
{n : ℕ}
(L : LO.FirstOrder.Language)
(k : ℕ)
(r : L.Rel k)
(v : Fin k → LO.FirstOrder.Semiterm L ξ n)
:
Equations
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Semiformula.nrel!
{ξ : Type u_1}
{n : ℕ}
(L : LO.FirstOrder.Language)
(k : ℕ)
(r : L.Rel k)
(v : Fin k → LO.FirstOrder.Semiterm L ξ n)
:
Equations
Instances For
def
LO.FirstOrder.Semiformula.complexity
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
:
LO.FirstOrder.Semiformula L ξ n → ℕ
Equations
- LO.FirstOrder.Semiformula.verum.complexity = 0
- LO.FirstOrder.Semiformula.falsum.complexity = 0
- (LO.FirstOrder.Semiformula.rel r v).complexity = 0
- (LO.FirstOrder.Semiformula.nrel r v).complexity = 0
- (φ.and ψ).complexity = φ.complexity ⊔ ψ.complexity + 1
- (φ.or ψ).complexity = φ.complexity ⊔ ψ.complexity + 1
- φ.all.complexity = φ.complexity + 1
- φ.ex.complexity = φ.complexity + 1
Instances For
@[simp]
theorem
LO.FirstOrder.Semiformula.complexity_top
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
:
@[simp]
theorem
LO.FirstOrder.Semiformula.complexity_bot
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
:
@[simp]
theorem
LO.FirstOrder.Semiformula.complexity_rel
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n k : ℕ}
(r : L.Rel k)
(v : Fin k → LO.FirstOrder.Semiterm L ξ n)
:
(LO.FirstOrder.Semiformula.rel r v).complexity = 0
@[simp]
theorem
LO.FirstOrder.Semiformula.complexity_nrel
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n k : ℕ}
(r : L.Rel k)
(v : Fin k → LO.FirstOrder.Semiterm L ξ n)
:
(LO.FirstOrder.Semiformula.nrel r v).complexity = 0
@[simp]
theorem
LO.FirstOrder.Semiformula.complexity_and
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.complexity_and'
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.complexity_or
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.complexity_or'
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.complexity_all
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ : LO.FirstOrder.Semiformula L ξ (n + 1))
:
@[simp]
theorem
LO.FirstOrder.Semiformula.complexity_all'
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ : LO.FirstOrder.Semiformula L ξ (n + 1))
:
@[simp]
theorem
LO.FirstOrder.Semiformula.complexity_ex
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ : LO.FirstOrder.Semiformula L ξ (n + 1))
:
@[simp]
theorem
LO.FirstOrder.Semiformula.complexity_ex'
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ : LO.FirstOrder.Semiformula L ξ (n + 1))
:
def
LO.FirstOrder.Semiformula.cases'
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{C : (n : ℕ) → LO.FirstOrder.Semiformula L ξ n → Sort w}
(hverum : {n : ℕ} → C n ⊤)
(hfalsum : {n : ℕ} → C n ⊥)
(hrel :
{n k : ℕ} → (r : L.Rel k) → (v : Fin k → LO.FirstOrder.Semiterm L ξ n) → C n (LO.FirstOrder.Semiformula.rel r v))
(hnrel :
{n k : ℕ} → (r : L.Rel k) → (v : Fin k → LO.FirstOrder.Semiterm L ξ n) → C n (LO.FirstOrder.Semiformula.nrel r v))
(hand : {n : ℕ} → (φ ψ : LO.FirstOrder.Semiformula L ξ n) → C n (φ ⋏ ψ))
(hor : {n : ℕ} → (φ ψ : LO.FirstOrder.Semiformula L ξ n) → C n (φ ⋎ ψ))
(hall : {n : ℕ} → (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) → C n (∀' φ))
(hex : {n : ℕ} → (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) → C n (∃' φ))
{n : ℕ}
(φ : LO.FirstOrder.Semiformula L ξ n)
:
C n φ
Equations
- LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hex LO.FirstOrder.Semiformula.verum = hverum
- LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hex LO.FirstOrder.Semiformula.falsum = hfalsum
- LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hex (LO.FirstOrder.Semiformula.rel r v) = hrel r v
- LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hex (LO.FirstOrder.Semiformula.nrel r v) = hnrel r v
- LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hex (φ.and ψ) = hand φ ψ
- LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hex (φ.or ψ) = hor φ ψ
- LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hex φ.all = hall φ
- LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hex φ.ex = hex φ
Instances For
def
LO.FirstOrder.Semiformula.rec'
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{C : (n : ℕ) → LO.FirstOrder.Semiformula L ξ n → Sort w}
(hverum : {n : ℕ} → C n ⊤)
(hfalsum : {n : ℕ} → C n ⊥)
(hrel :
{n k : ℕ} → (r : L.Rel k) → (v : Fin k → LO.FirstOrder.Semiterm L ξ n) → C n (LO.FirstOrder.Semiformula.rel r v))
(hnrel :
{n k : ℕ} → (r : L.Rel k) → (v : Fin k → LO.FirstOrder.Semiterm L ξ n) → C n (LO.FirstOrder.Semiformula.nrel r v))
(hand : {n : ℕ} → (φ ψ : LO.FirstOrder.Semiformula L ξ n) → C n φ → C n ψ → C n (φ ⋏ ψ))
(hor : {n : ℕ} → (φ ψ : LO.FirstOrder.Semiformula L ξ n) → C n φ → C n ψ → C n (φ ⋎ ψ))
(hall : {n : ℕ} → (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) → C (n + 1) φ → C n (∀' φ))
(hex : {n : ℕ} → (φ : LO.FirstOrder.Semiformula L ξ (n + 1)) → C (n + 1) φ → C n (∃' φ))
{n : ℕ}
(φ : LO.FirstOrder.Semiformula L ξ n)
:
C n φ
Equations
- One or more equations did not get rendered due to their size.
- LO.FirstOrder.Semiformula.rec' hverum hfalsum hrel hnrel hand hor hall hex LO.FirstOrder.Semiformula.verum = hverum
- LO.FirstOrder.Semiformula.rec' hverum hfalsum hrel hnrel hand hor hall hex LO.FirstOrder.Semiformula.falsum = hfalsum
- LO.FirstOrder.Semiformula.rec' hverum hfalsum hrel hnrel hand hor hall hex (LO.FirstOrder.Semiformula.rel r v) = hrel r v
- LO.FirstOrder.Semiformula.rec' hverum hfalsum hrel hnrel hand hor hall hex (LO.FirstOrder.Semiformula.nrel r v) = hnrel r v
Instances For
@[simp]
theorem
LO.FirstOrder.Semiformula.complexity_neg
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ : LO.FirstOrder.Semiformula L ξ n)
:
def
LO.FirstOrder.Semiformula.hasDecEq
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
[DecidableEq ξ]
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
Instances For
instance
LO.FirstOrder.Semiformula.instDecidableEq
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[(k : ℕ) → DecidableEq (L.Func k)]
[(k : ℕ) → DecidableEq (L.Rel k)]
[DecidableEq ξ]
:
DecidableEq (LO.FirstOrder.Semiformula L ξ n)
Equations
- LO.FirstOrder.Semiformula.instDecidableEq = LO.FirstOrder.Semiformula.hasDecEq
Quantifier Rank
def
LO.FirstOrder.Semiformula.qr
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
:
LO.FirstOrder.Semiformula L ξ n → ℕ
Equations
Instances For
@[simp]
@[simp]
@[simp]
theorem
LO.FirstOrder.Semiformula.qr_rel
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n k : ℕ}
(r : L.Rel k)
(v : Fin k → LO.FirstOrder.Semiterm L ξ n)
:
(LO.FirstOrder.Semiformula.rel r v).qr = 0
@[simp]
theorem
LO.FirstOrder.Semiformula.qr_nrel
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n k : ℕ}
(r : L.Rel k)
(v : Fin k → LO.FirstOrder.Semiterm L ξ n)
:
(LO.FirstOrder.Semiformula.nrel r v).qr = 0
@[simp]
theorem
LO.FirstOrder.Semiformula.qr_and
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.qr_or
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.qr_all
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ : LO.FirstOrder.Semiformula L ξ (n + 1))
:
@[simp]
theorem
LO.FirstOrder.Semiformula.qr_ex
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ : LO.FirstOrder.Semiformula L ξ (n + 1))
:
@[simp]
theorem
LO.FirstOrder.Semiformula.qr_neg
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.qr_imply
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.qr_iff
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
Open (Semi-)Formula
def
LO.FirstOrder.Semiformula.Open
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ : LO.FirstOrder.Semiformula L ξ n)
:
Instances For
@[simp]
theorem
LO.FirstOrder.Semiformula.open_top
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
:
⊤.Open
@[simp]
theorem
LO.FirstOrder.Semiformula.open_bot
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
:
⊥.Open
@[simp]
theorem
LO.FirstOrder.Semiformula.open_rel
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n k : ℕ}
(r : L.Rel k)
(v : Fin k → LO.FirstOrder.Semiterm L ξ n)
:
(LO.FirstOrder.Semiformula.rel r v).Open
@[simp]
theorem
LO.FirstOrder.Semiformula.open_nrel
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n k : ℕ}
(r : L.Rel k)
(v : Fin k → LO.FirstOrder.Semiterm L ξ n)
:
(LO.FirstOrder.Semiformula.nrel r v).Open
@[simp]
theorem
LO.FirstOrder.Semiformula.open_and
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
{φ ψ : LO.FirstOrder.Semiformula L ξ n}
:
@[simp]
theorem
LO.FirstOrder.Semiformula.open_or
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
{φ ψ : LO.FirstOrder.Semiformula L ξ n}
:
@[simp]
theorem
LO.FirstOrder.Semiformula.not_open_all
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
{φ : LO.FirstOrder.Semiformula L ξ (n + 1)}
:
@[simp]
theorem
LO.FirstOrder.Semiformula.not_open_ex
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
{φ : LO.FirstOrder.Semiformula L ξ (n + 1)}
:
@[simp]
theorem
LO.FirstOrder.Semiformula.open_neg
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
{φ : LO.FirstOrder.Semiformula L ξ n}
:
@[simp]
theorem
LO.FirstOrder.Semiformula.open_imply
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
{φ ψ : LO.FirstOrder.Semiformula L ξ n}
:
@[simp]
theorem
LO.FirstOrder.Semiformula.open_iff
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
{φ ψ : LO.FirstOrder.Semiformula L ξ n}
:
Free Variables
def
LO.FirstOrder.Semiformula.freeVariables
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
[DecidableEq ξ]
{n : ℕ}
:
LO.FirstOrder.Semiformula L ξ n → Finset ξ
Equations
- (LO.FirstOrder.Semiformula.rel a v).freeVariables = Finset.univ.biUnion fun (i : Fin arity) => (v i).freeVariables
- (LO.FirstOrder.Semiformula.nrel a v).freeVariables = Finset.univ.biUnion fun (i : Fin arity) => (v i).freeVariables
- LO.FirstOrder.Semiformula.verum.freeVariables = ∅
- LO.FirstOrder.Semiformula.falsum.freeVariables = ∅
- (φ.and ψ).freeVariables = φ.freeVariables ∪ ψ.freeVariables
- (φ.or ψ).freeVariables = φ.freeVariables ∪ ψ.freeVariables
- φ.all.freeVariables = φ.freeVariables
- φ.ex.freeVariables = φ.freeVariables
Instances For
theorem
LO.FirstOrder.Semiformula.freeVariables_rel
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
{k : ℕ}
(r : L.Rel k)
(v : Fin k → LO.FirstOrder.Semiterm L ξ n)
:
(LO.FirstOrder.Semiformula.rel r v).freeVariables = Finset.univ.biUnion fun (i : Fin k) => (v i).freeVariables
theorem
LO.FirstOrder.Semiformula.freeVariables_nrel
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
{k : ℕ}
(r : L.Rel k)
(v : Fin k → LO.FirstOrder.Semiterm L ξ n)
:
(LO.FirstOrder.Semiformula.nrel r v).freeVariables = Finset.univ.biUnion fun (i : Fin k) => (v i).freeVariables
@[simp]
theorem
LO.FirstOrder.Semiformula.freeVariables_verum
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
:
@[simp]
theorem
LO.FirstOrder.Semiformula.freeVariables_falsum
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
:
@[simp]
theorem
LO.FirstOrder.Semiformula.freeVariables_and
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.freeVariables_or
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.freeVariables_all
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
(φ : LO.FirstOrder.Semiformula L ξ (n + 1))
:
@[simp]
theorem
LO.FirstOrder.Semiformula.freeVariables_ex
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
(φ : LO.FirstOrder.Semiformula L ξ (n + 1))
:
@[simp]
theorem
LO.FirstOrder.Semiformula.freeVariables_not
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
(φ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.freeVariables_imp
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.freeVariables_univClosure
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
(φ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.freeVariables_sentence
{L : LO.FirstOrder.Language}
{n : ℕ}
{ο : Type u_5}
[IsEmpty ο]
(φ : LO.FirstOrder.Semiformula L ο n)
:
@[reducible, inline]
abbrev
LO.FirstOrder.Semiformula.FVar?
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
(φ : LO.FirstOrder.Semiformula L ξ n)
(x : ξ)
:
Instances For
@[simp]
theorem
LO.FirstOrder.Semiformula.fvar?_rel
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
{x : ξ}
{k : ℕ}
{R : L.Rel k}
{v : Fin k → LO.FirstOrder.Semiterm L ξ n}
:
(LO.FirstOrder.Semiformula.rel R v).FVar? x ↔ ∃ (i : Fin k), (v i).FVar? x
@[simp]
theorem
LO.FirstOrder.Semiformula.fvar?_nrel
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
{x : ξ}
{k : ℕ}
{R : L.Rel k}
{v : Fin k → LO.FirstOrder.Semiterm L ξ n}
:
(LO.FirstOrder.Semiformula.nrel R v).FVar? x ↔ ∃ (i : Fin k), (v i).FVar? x
@[simp]
theorem
LO.FirstOrder.Semiformula.fvar?_top
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
(x : ξ)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.fvar?_falsum
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
(x : ξ)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.fvar?_and
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
(x : ξ)
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.fvar?_or
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
(x : ξ)
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.fvar?_all
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
(x : ξ)
(φ : LO.FirstOrder.Semiformula L ξ (n + 1))
:
@[simp]
theorem
LO.FirstOrder.Semiformula.fvar?_ex
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
(x : ξ)
(φ : LO.FirstOrder.Semiformula L ξ (n + 1))
:
@[simp]
theorem
LO.FirstOrder.Semiformula.fvar?_univClosure
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
[DecidableEq ξ]
(x : ξ)
(φ : LO.FirstOrder.Semiformula L ξ n)
:
def
LO.FirstOrder.Semiformula.fvSup
{L : LO.FirstOrder.Language}
{n : ℕ}
(φ : LO.FirstOrder.SyntacticSemiformula L n)
:
Equations
Instances For
theorem
LO.FirstOrder.Semiformula.lt_fvSup_of_fvar?
{L : LO.FirstOrder.Language}
{n m : ℕ}
{φ : LO.FirstOrder.SyntacticSemiformula L n}
:
theorem
LO.FirstOrder.Semiformula.not_fvar?_of_lt_fvSup
{L : LO.FirstOrder.Language}
{n m : ℕ}
(φ : LO.FirstOrder.SyntacticSemiformula L n)
(h : LO.FirstOrder.Semiformula.fvSup φ ≤ m)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.not_fvar?_fvSup
{L : LO.FirstOrder.Language}
{n : ℕ}
(φ : LO.FirstOrder.SyntacticSemiformula L n)
:
theorem
LO.FirstOrder.Semiformula.List.maximam?_some_of_not_nil
{α : Type u_5}
[LinearOrder α]
{l : List α}
(h : l ≠ [])
:
theorem
LO.FirstOrder.Semiformula.List.maximam?_eq_some
{α : Type u_5}
[LinearOrder α]
{l : List α}
{a : α}
(h : l.max? = some a)
(x : α)
:
theorem
LO.FirstOrder.Semiformula.ne_of_ne_complexity
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
{φ ψ : LO.FirstOrder.Semiformula L ξ n}
(h : φ.complexity ≠ ψ.complexity)
:
φ ≠ ψ
@[simp]
theorem
LO.FirstOrder.Semiformula.ne_or_left
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
@[simp]
theorem
LO.FirstOrder.Semiformula.ne_or_right
{L : LO.FirstOrder.Language}
{ξ : Type u_1}
{n : ℕ}
(φ ψ : LO.FirstOrder.Semiformula L ξ n)
:
def
LO.FirstOrder.Semiformula.lMapAux
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
(Φ : L₁.Hom L₂)
{n : ℕ}
:
LO.FirstOrder.Semiformula L₁ ξ n → LO.FirstOrder.Semiformula L₂ ξ n
Equations
- LO.FirstOrder.Semiformula.lMapAux Φ LO.FirstOrder.Semiformula.verum = ⊤
- LO.FirstOrder.Semiformula.lMapAux Φ LO.FirstOrder.Semiformula.falsum = ⊥
- LO.FirstOrder.Semiformula.lMapAux Φ (LO.FirstOrder.Semiformula.rel r v) = LO.FirstOrder.Semiformula.rel (Φ.rel r) (LO.FirstOrder.Semiterm.lMap Φ ∘ v)
- LO.FirstOrder.Semiformula.lMapAux Φ (LO.FirstOrder.Semiformula.nrel r v) = LO.FirstOrder.Semiformula.nrel (Φ.rel r) (LO.FirstOrder.Semiterm.lMap Φ ∘ v)
- LO.FirstOrder.Semiformula.lMapAux Φ (φ.and ψ) = LO.FirstOrder.Semiformula.lMapAux Φ φ ⋏ LO.FirstOrder.Semiformula.lMapAux Φ ψ
- LO.FirstOrder.Semiformula.lMapAux Φ (φ.or ψ) = LO.FirstOrder.Semiformula.lMapAux Φ φ ⋎ LO.FirstOrder.Semiformula.lMapAux Φ ψ
- LO.FirstOrder.Semiformula.lMapAux Φ φ.all = ∀' LO.FirstOrder.Semiformula.lMapAux Φ φ
- LO.FirstOrder.Semiformula.lMapAux Φ φ.ex = ∃' LO.FirstOrder.Semiformula.lMapAux Φ φ
Instances For
theorem
LO.FirstOrder.Semiformula.lMapAux_neg
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
{Φ : L₁.Hom L₂}
{n : ℕ}
(φ : LO.FirstOrder.Semiformula L₁ ξ n)
:
def
LO.FirstOrder.Semiformula.lMap
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
(Φ : L₁.Hom L₂)
{n : ℕ}
:
LO.FirstOrder.Semiformula L₁ ξ n →ˡᶜ LO.FirstOrder.Semiformula L₂ ξ n
Equations
- LO.FirstOrder.Semiformula.lMap Φ = { toTr := LO.FirstOrder.Semiformula.lMapAux Φ, map_top' := ⋯, map_bot' := ⋯, map_neg' := ⋯, map_imply' := ⋯, map_and' := ⋯, map_or' := ⋯ }
Instances For
theorem
LO.FirstOrder.Semiformula.lMap_rel
{n : ℕ}
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
{Φ : L₁.Hom L₂}
{k : ℕ}
(r : L₁.Rel k)
(v : Fin k → LO.FirstOrder.Semiterm L₁ ξ n)
:
(LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.rel r v) = LO.FirstOrder.Semiformula.rel (Φ.rel r) fun (i : Fin k) => LO.FirstOrder.Semiterm.lMap Φ (v i)
@[simp]
theorem
LO.FirstOrder.Semiformula.lMap_rel₀
{n : ℕ}
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
{Φ : L₁.Hom L₂}
(r : L₁.Rel 0)
(v : Fin 0 → LO.FirstOrder.Semiterm L₁ ξ n)
:
(LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.rel r v) = LO.FirstOrder.Semiformula.rel (Φ.rel r) ![]
@[simp]
theorem
LO.FirstOrder.Semiformula.lMap_rel₁
{n : ℕ}
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
{Φ : L₁.Hom L₂}
(r : L₁.Rel 1)
(t : LO.FirstOrder.Semiterm L₁ ξ n)
:
(LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.rel r ![t]) = LO.FirstOrder.Semiformula.rel (Φ.rel r) ![LO.FirstOrder.Semiterm.lMap Φ t]
@[simp]
theorem
LO.FirstOrder.Semiformula.lMap_rel₂
{n : ℕ}
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
{Φ : L₁.Hom L₂}
(r : L₁.Rel 2)
(t₁ t₂ : LO.FirstOrder.Semiterm L₁ ξ n)
:
(LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.rel r ![t₁, t₂]) = LO.FirstOrder.Semiformula.rel (Φ.rel r) ![LO.FirstOrder.Semiterm.lMap Φ t₁, LO.FirstOrder.Semiterm.lMap Φ t₂]
theorem
LO.FirstOrder.Semiformula.lMap_nrel
{n : ℕ}
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
{Φ : L₁.Hom L₂}
{k : ℕ}
(r : L₁.Rel k)
(v : Fin k → LO.FirstOrder.Semiterm L₁ ξ n)
:
(LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.nrel r v) = LO.FirstOrder.Semiformula.nrel (Φ.rel r) fun (i : Fin k) => LO.FirstOrder.Semiterm.lMap Φ (v i)
@[simp]
theorem
LO.FirstOrder.Semiformula.lMap_nrel₀
{n : ℕ}
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
{Φ : L₁.Hom L₂}
(r : L₁.Rel 0)
(v : Fin 0 → LO.FirstOrder.Semiterm L₁ ξ n)
:
(LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.nrel r v) = LO.FirstOrder.Semiformula.nrel (Φ.rel r) ![]
@[simp]
theorem
LO.FirstOrder.Semiformula.lMap_nrel₁
{n : ℕ}
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
{Φ : L₁.Hom L₂}
(r : L₁.Rel 1)
(t : LO.FirstOrder.Semiterm L₁ ξ n)
:
(LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.nrel r ![t]) = LO.FirstOrder.Semiformula.nrel (Φ.rel r) ![LO.FirstOrder.Semiterm.lMap Φ t]
@[simp]
theorem
LO.FirstOrder.Semiformula.lMap_nrel₂
{n : ℕ}
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
{Φ : L₁.Hom L₂}
(r : L₁.Rel 2)
(t₁ t₂ : LO.FirstOrder.Semiterm L₁ ξ n)
:
(LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.nrel r ![t₁, t₂]) = LO.FirstOrder.Semiformula.nrel (Φ.rel r) ![LO.FirstOrder.Semiterm.lMap Φ t₁, LO.FirstOrder.Semiterm.lMap Φ t₂]
@[simp]
theorem
LO.FirstOrder.Semiformula.lMap_all
{n : ℕ}
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
{Φ : L₁.Hom L₂}
(φ : LO.FirstOrder.Semiformula L₁ ξ (n + 1))
:
(LO.FirstOrder.Semiformula.lMap Φ) (∀' φ) = ∀' (LO.FirstOrder.Semiformula.lMap Φ) φ
@[simp]
theorem
LO.FirstOrder.Semiformula.lMap_ex
{n : ℕ}
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
{Φ : L₁.Hom L₂}
(φ : LO.FirstOrder.Semiformula L₁ ξ (n + 1))
:
(LO.FirstOrder.Semiformula.lMap Φ) (∃' φ) = ∃' (LO.FirstOrder.Semiformula.lMap Φ) φ
@[simp]
theorem
LO.FirstOrder.Semiformula.lMap_ball
{n : ℕ}
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
{Φ : L₁.Hom L₂}
(φ ψ : LO.FirstOrder.Semiformula L₁ ξ (n + 1))
:
(LO.FirstOrder.Semiformula.lMap Φ) (∀[φ] ψ) = ∀[(LO.FirstOrder.Semiformula.lMap Φ) φ] (LO.FirstOrder.Semiformula.lMap Φ) ψ
@[simp]
theorem
LO.FirstOrder.Semiformula.lMap_bex
{n : ℕ}
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
{Φ : L₁.Hom L₂}
(φ ψ : LO.FirstOrder.Semiformula L₁ ξ (n + 1))
:
(LO.FirstOrder.Semiformula.lMap Φ) (∃[φ] ψ) = ∃[(LO.FirstOrder.Semiformula.lMap Φ) φ] (LO.FirstOrder.Semiformula.lMap Φ) ψ
@[simp]
theorem
LO.FirstOrder.Semiformula.lMap_univClosure
{n : ℕ}
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
{Φ : L₁.Hom L₂}
(φ : LO.FirstOrder.Semiformula L₁ ξ n)
:
(LO.FirstOrder.Semiformula.lMap Φ) (∀* φ) = ∀* (LO.FirstOrder.Semiformula.lMap Φ) φ
@[simp]
theorem
LO.FirstOrder.Semiformula.lMap_exClosure
{n : ℕ}
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
{Φ : L₁.Hom L₂}
(φ : LO.FirstOrder.Semiformula L₁ ξ n)
:
(LO.FirstOrder.Semiformula.lMap Φ) (∃* φ) = ∃* (LO.FirstOrder.Semiformula.lMap Φ) φ
@[simp]
theorem
LO.FirstOrder.Semiformula.lMap_univItr
{n : ℕ}
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
{Φ : L₁.Hom L₂}
{k : ℕ}
(φ : LO.FirstOrder.Semiformula L₁ ξ (n + k))
:
(LO.FirstOrder.Semiformula.lMap Φ) (∀^[k] φ) = ∀^[k] (LO.FirstOrder.Semiformula.lMap Φ) φ
@[simp]
theorem
LO.FirstOrder.Semiformula.lMap_exItr
{n : ℕ}
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
{Φ : L₁.Hom L₂}
{k : ℕ}
(φ : LO.FirstOrder.Semiformula L₁ ξ (n + k))
:
(LO.FirstOrder.Semiformula.lMap Φ) (∃^[k] φ) = ∃^[k] (LO.FirstOrder.Semiformula.lMap Φ) φ
@[simp]
theorem
LO.FirstOrder.Semiformula.freeVariables_lMap
{n : ℕ}
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
{ξ : Type u_5}
[DecidableEq ξ]
(Φ : L₁.Hom L₂)
(φ : LO.FirstOrder.Semiformula L₁ ξ n)
:
((LO.FirstOrder.Semiformula.lMap Φ) φ).freeVariables = φ.freeVariables
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
Equations
- LO.FirstOrder.instCollectionSyntacticFormulaTheory = inferInstance
Equations
- LO.FirstOrder.instCollectionSentenceClosedTheory = inferInstance
def
LO.FirstOrder.Theory.lMap
{L₁ : LO.FirstOrder.Language}
{L₂ : LO.FirstOrder.Language}
(Φ : L₁.Hom L₂)
(T : LO.FirstOrder.Theory L₁)
:
Equations
Instances For
Equations
- LO.FirstOrder.Theory.instAdd = { add := fun (x1 x2 : LO.FirstOrder.Theory L) => x1 ∪ x2 }