Polarity of formulas #

source

def LO.FirstOrder.Semiformula.polarity {L : Language} {ξ : Type u_1} {n : ℕ} :

Semiformula L ξ n → Bool

A polarity of a formula

Equations

(LO.FirstOrder.Semiformula.rel a a_1).polarity = true
(LO.FirstOrder.Semiformula.nrel a a_1).polarity = false
LO.FirstOrder.Semiformula.verum.polarity = true
LO.FirstOrder.Semiformula.falsum.polarity = false
(φ.and ψ).polarity = (φ.polarity || ψ.polarity)
(φ.or ψ).polarity = (φ.polarity && ψ.polarity)
a.all.polarity = false
a.exs.polarity = true

Instances For

source

@[simp]

theorem LO.FirstOrder.Semiformula.polarity_rel {L : Language} {ξ : Type u_1} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) :

(rel r v).polarity = true

source

@[simp]

theorem LO.FirstOrder.Semiformula.polarity_nrel {L : Language} {ξ : Type u_1} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) :

(nrel r v).polarity = false

source

@[simp]

theorem LO.FirstOrder.Semiformula.polarity_verum {L : Language} {ξ : Type u_1} {n : ℕ} :

⊤.polarity = true

source

@[simp]

theorem LO.FirstOrder.Semiformula.polarity_falsum {L : Language} {ξ : Type u_1} {n : ℕ} :

⊥.polarity = false

source

@[simp]

theorem LO.FirstOrder.Semiformula.polarity_and {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) :

(φ ⋏ ψ).polarity = (φ.polarity || ψ.polarity)

source

@[simp]

theorem LO.FirstOrder.Semiformula.polarity_or {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) :

(φ ⋎ ψ).polarity = (φ.polarity && ψ.polarity)

source

@[simp]

theorem LO.FirstOrder.Semiformula.polarity_all {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ (n + 1)) :

(∀⁰ φ).polarity = false

source

@[simp]

theorem LO.FirstOrder.Semiformula.polarity_ex {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ (n + 1)) :

(∃⁰ φ).polarity = true

source

@[simp]

theorem LO.FirstOrder.Semiformula.polarity_neg {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) :

(∼φ).polarity = !φ.polarity

source

@[simp]

theorem LO.FirstOrder.Semiformula.polarity_imply {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) :

(φ ➝ ψ).polarity = (!φ.polarity && ψ.polarity)

source

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.Positive {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) :

Prop

Equations

φ.Positive = (φ.polarity = true)

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.Negative {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) :

Prop

Equations

φ.Negative = (φ.polarity = false)

Instances For

source

@[simp]

theorem LO.FirstOrder.Semiformula.rel_positive {L : Language} {ξ : Type u_1} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) :

(rel r v).Positive

source

@[simp]

theorem LO.FirstOrder.Semiformula.rel_negative {L : Language} {ξ : Type u_1} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) :

¬(rel r v).Negative

source

@[simp]

theorem LO.FirstOrder.Semiformula.nrel_positive {L : Language} {ξ : Type u_1} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) :

¬(nrel r v).Positive

source

@[simp]

theorem LO.FirstOrder.Semiformula.nrel_negative {L : Language} {ξ : Type u_1} {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) :

(nrel r v).Negative

source

@[simp]

theorem LO.FirstOrder.Semiformula.verum_positive {L : Language} {ξ : Type u_1} {n : ℕ} :

⊤.Positive

source

@[simp]

theorem LO.FirstOrder.Semiformula.verum_negative {L : Language} {ξ : Type u_1} {n : ℕ} :

¬⊤.Negative

source

@[simp]

theorem LO.FirstOrder.Semiformula.falsum_positive {L : Language} {ξ : Type u_1} {n : ℕ} :

¬⊥.Positive

source

@[simp]

theorem LO.FirstOrder.Semiformula.falsum_negative {L : Language} {ξ : Type u_1} {n : ℕ} :

⊥.Negative

source

@[simp]

theorem LO.FirstOrder.Semiformula.and_positive_iff {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) :

(φ ⋏ ψ).Positive ↔ φ.Positive ∨ ψ.Positive

source

@[simp]

theorem LO.FirstOrder.Semiformula.and_negative_iff {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) :

(φ ⋏ ψ).Negative ↔ φ.Negative ∧ ψ.Negative

source

@[simp]

theorem LO.FirstOrder.Semiformula.or_positive_iff {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) :

(φ ⋎ ψ).Positive ↔ φ.Positive ∧ ψ.Positive

source

@[simp]

theorem LO.FirstOrder.Semiformula.or_negative_iff {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) :

(φ ⋎ ψ).Negative ↔ φ.Negative ∨ ψ.Negative

source

@[simp]

theorem LO.FirstOrder.Semiformula.ex_positive_iff {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ (n + 1)) :

(∃⁰ φ).Positive

source

@[simp]

theorem LO.FirstOrder.Semiformula.ex_negative_iff {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ (n + 1)) :

¬(∃⁰ φ).Negative

source

@[simp]

theorem LO.FirstOrder.Semiformula.all_positive_iff {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ (n + 1)) :

¬(∀⁰ φ).Positive

source

@[simp]

theorem LO.FirstOrder.Semiformula.all_negative_iff {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ (n + 1)) :

(∀⁰ φ).Negative

source

@[simp]

theorem LO.FirstOrder.Semiformula.neg_positive_iff {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) :

(∼φ).Positive ↔ φ.Negative

source

@[simp]

theorem LO.FirstOrder.Semiformula.neg_negative_iff {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ n) :

(∼φ).Negative ↔ φ.Positive

source

theorem LO.FirstOrder.Semiformula.Positive.eq_true {L : Language} {ξ : Type u_1} {n : ℕ} {φ : Semiformula L ξ n} (h : φ.Positive) :

φ.polarity = true

source

theorem LO.FirstOrder.Semiformula.Negative.eq_false {L : Language} {ξ : Type u_1} {n : ℕ} {φ : Semiformula L ξ n} (h : φ.Negative) :

φ.polarity = false

source

@[simp]

theorem LO.FirstOrder.Semiformula.polarity_rew {L : Language} {ξ₁ : Type u_2} {n₁ : ℕ} {ξ₂ : Type u_3} {n₂ : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (φ : Semiformula L ξ₁ n₁) :

((Rewriting.app ω) φ).polarity = φ.polarity

Documentation

Foundation.FirstOrder.Polarity

Polarity of formulas #