inductive LO.Polarity : Type

• sigma : Polarity
• pi : Polarity

@[implicit_reducible]

instance LO.Polarity.instSigmaSymbol : SigmaSymbol Polarity

Equations

• LO.Polarity.instSigmaSymbol = { sigma := LO.Polarity.sigma }

@[implicit_reducible]

instance LO.Polarity.instPiSymbol : PiSymbol Polarity

Equations

• LO.Polarity.instPiSymbol = { pi := LO.Polarity.pi }

def LO.Polarity.alt : Polarity → Polarity

Equations

• LO.Polarity.sigma.alt = 𝚷
• LO.Polarity.pi.alt = 𝚺

@[simp]

theorem LO.Polarity.eq_sigma : sigma = 𝚺

@[simp]

theorem LO.Polarity.eq_pi : pi = 𝚷

@[simp]

theorem LO.Polarity.alt_sigma : 𝚺.alt = 𝚷

@[simp]

theorem LO.Polarity.alt_pi : 𝚷.alt = 𝚺

@[simp]

theorem LO.Polarity.alt_alt (Γ : Polarity) : Γ.alt.alt = Γ

def LO.Polarity.coe {α : Type u_1} [SigmaSymbol α] [PiSymbol α] : Polarity → α

Equations

• LO.Polarity.sigma.coe = 𝚺
• LO.Polarity.pi.coe = 𝚷

@[implicit_reducible]

instance LO.Polarity.instCoe {α : Type u_1} [SigmaSymbol α] [PiSymbol α] : Coe Polarity α

Equations

• LO.Polarity.instCoe = { coe := LO.Polarity.coe }

@[simp]

theorem LO.Polarity.coe_sigma {α : Type u_1} [SigmaSymbol α] [PiSymbol α] : 𝚺.coe = 𝚺

@[simp]

theorem LO.Polarity.coe_pi {α : Type u_1} [SigmaSymbol α] [PiSymbol α] : 𝚷.coe = 𝚷

inductive LO.SigmaPiDelta : Type

• sigma : SigmaPiDelta
• pi : SigmaPiDelta
• delta : SigmaPiDelta

@[implicit_reducible]

instance LO.SigmaPiDelta.instSigmaSymbol : SigmaSymbol SigmaPiDelta

Equations

• LO.SigmaPiDelta.instSigmaSymbol = { sigma := LO.SigmaPiDelta.sigma }

@[implicit_reducible]

instance LO.SigmaPiDelta.instPiSymbol : PiSymbol SigmaPiDelta

Equations

• LO.SigmaPiDelta.instPiSymbol = { pi := LO.SigmaPiDelta.pi }

@[implicit_reducible]

instance LO.SigmaPiDelta.instDeltaSymbol : DeltaSymbol SigmaPiDelta

Equations

• LO.SigmaPiDelta.instDeltaSymbol = { delta := LO.SigmaPiDelta.delta }

def LO.SigmaPiDelta.alt : SigmaPiDelta → SigmaPiDelta

Equations

• LO.SigmaPiDelta.sigma.alt = 𝚷
• LO.SigmaPiDelta.pi.alt = 𝚺
• LO.SigmaPiDelta.delta.alt = 𝚫

@[simp]

theorem LO.SigmaPiDelta.eq_sigma : sigma = 𝚺

@[simp]

theorem LO.SigmaPiDelta.eq_pi : pi = 𝚷

@[simp]

theorem LO.SigmaPiDelta.eq_delta : delta = 𝚫

@[simp]

theorem LO.SigmaPiDelta.alt_sigma : 𝚺.alt = 𝚷

@[simp]

theorem LO.SigmaPiDelta.alt_pi : 𝚷.alt = 𝚺

@[simp]

theorem LO.SigmaPiDelta.alt_delta : 𝚫.alt = 𝚫

@[simp]

theorem LO.SigmaPiDelta.alt_alt (Γ : SigmaPiDelta) : Γ.alt.alt = Γ

@[simp]

theorem LO.SigmaPiDelta.alt_coe (Γ : Polarity) : Γ.coe.alt = Γ.alt.coe

First-order quantifiers

class LO.FirstOrder.UnivQuantifier (α : ℕ → Type u_1) : Type u_1

• all {n : ℕ} : α (n + 1) → α n

def LO.FirstOrder.«term∀⁰_» : Lean.ParserDescr

Equations

• LO.FirstOrder.«term∀⁰_» = Lean.ParserDescr.node `LO.FirstOrder.«term∀⁰_» 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∀⁰ ") (Lean.ParserDescr.cat `term 64))

class LO.FirstOrder.ExsQuantifier (α : ℕ → Type u_1) : Type u_1

• exs {n : ℕ} : α (n + 1) → α n

def LO.FirstOrder.«term∃⁰_» : Lean.ParserDescr

Equations

• LO.FirstOrder.«term∃⁰_» = Lean.ParserDescr.node `LO.FirstOrder.«term∃⁰_» 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∃⁰ ") (Lean.ParserDescr.cat `term 64))

class LO.FirstOrder.Quantifier (α : ℕ → Type u_1) extends LO.FirstOrder.UnivQuantifier α, LO.FirstOrder.ExsQuantifier α : Type u_1

• all {n : ℕ} : α (n + 1) → α n
• exs {n : ℕ} : α (n + 1) → α n

class LO.FirstOrder.LCWQ (α : ℕ → Type u_1) extends LO.FirstOrder.Quantifier α : Type u_1

Logical Connectives with Quantifiers.

• all {n : ℕ} : α (n + 1) → α n
• exs {n : ℕ} : α (n + 1) → α n
• connectives (n : ℕ) : LogicalConnective (α n)

@[implicit_reducible]

instance LO.FirstOrder.instLogicalConnectiveOfLCWQ (α : ℕ → Type u_1) [LCWQ α] (n : ℕ) : LogicalConnective (α n)

Equations

• LO.FirstOrder.instLogicalConnectiveOfLCWQ α n = LO.FirstOrder.LCWQ.connectives n

@[implicit_reducible]

instance LO.FirstOrder.instLCWQOfQuantifierOfLogicalConnective (α : ℕ → Type u_1) [Quantifier α] [(n : ℕ) → LogicalConnective (α n)] : LCWQ α

Equations

• LO.FirstOrder.instLCWQOfQuantifierOfLogicalConnective α = { toQuantifier := inst✝¹, connectives := inferInstance }

def LO.FirstOrder.allClosure {α : ℕ → Type u_1} [UnivQuantifier α] {n : ℕ} : α n → α 0

Equations

• ∀⁰* a = a
• ∀⁰* a = ∀⁰* ∀⁰ a

def LO.FirstOrder.«term∀⁰*_» : Lean.ParserDescr

The universal closure of a formula.

Equations

• LO.FirstOrder.«term∀⁰*_» = Lean.ParserDescr.node `LO.FirstOrder.«term∀⁰*_» 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∀⁰* ") (Lean.ParserDescr.cat `term 64))

@[simp]

theorem LO.FirstOrder.allClosure_zero {α : ℕ → Type u_1} [UnivQuantifier α] (a : α 0) : ∀⁰* a = a

theorem LO.FirstOrder.allClosure_succ {α : ℕ → Type u_1} [UnivQuantifier α] {n : ℕ} (a : α (n + 1)) : ∀⁰* a = ∀⁰* ∀⁰ a

def LO.FirstOrder.allItr {α : ℕ → Type u_1} [UnivQuantifier α] {n : ℕ} (k : ℕ) : α (n + k) → α n

Equations

• ∀⁰^[0] a = a
• ∀⁰^[k.succ] a = ∀⁰^[k] ∀⁰ a

def LO.FirstOrder.«term∀⁰^[_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LO.FirstOrder.allItr_zero {α : ℕ → Type u_1} [UnivQuantifier α] {n : ℕ} (a : α n) : ∀⁰^[0] a = a

@[simp]

theorem LO.FirstOrder.allItr_one {α : ℕ → Type u_1} [UnivQuantifier α] {n : ℕ} (a : α (n + 1)) : ∀⁰^[1] a = ∀⁰ a

theorem LO.FirstOrder.allItr_succ {α : ℕ → Type u_1} [UnivQuantifier α] {n k : ℕ} (a : α (n + (k + 1))) : ∀⁰^[k + 1] a = ∀⁰^[k] ∀⁰ a

def LO.FirstOrder.exsClosure {α : ℕ → Type u_1} [ExsQuantifier α] {n : ℕ} : α n → α 0

Equations

• ∃⁰* a = a
• ∃⁰* a = ∃⁰* ∃⁰ a

def LO.FirstOrder.«term∃⁰*_» : Lean.ParserDescr

The existential closure of a formula.

Equations

• LO.FirstOrder.«term∃⁰*_» = Lean.ParserDescr.node `LO.FirstOrder.«term∃⁰*_» 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∃⁰* ") (Lean.ParserDescr.cat `term 64))

@[simp]

theorem LO.FirstOrder.exsClosure_zero {α : ℕ → Type u_1} [ExsQuantifier α] (a : α 0) : ∃⁰* a = a

theorem LO.FirstOrder.exsClosure_succ {α : ℕ → Type u_1} [ExsQuantifier α] {n : ℕ} (a : α (n + 1)) : ∃⁰* a = ∃⁰* ∃⁰ a

def LO.FirstOrder.exsItr {α : ℕ → Type u_1} [ExsQuantifier α] {n : ℕ} (k : ℕ) : α (n + k) → α n

Equations

• ∃⁰^[0] a = a
• ∃⁰^[k.succ] a = ∃⁰^[k] ∃⁰ a

def LO.FirstOrder.«term∃⁰^[_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LO.FirstOrder.exsItr_zero {α : ℕ → Type u_1} [ExsQuantifier α] {n : ℕ} (a : α n) : ∃⁰^[0] a = a

@[simp]

theorem LO.FirstOrder.exsItr_one {α : ℕ → Type u_1} [ExsQuantifier α] {n : ℕ} (a : α (n + 1)) : ∃⁰^[1] a = ∃⁰ a

theorem LO.FirstOrder.exsItr_succ {α : ℕ → Type u_1} [ExsQuantifier α] {n k : ℕ} (a : α (n + (k + 1))) : ∃⁰^[k + 1] a = ∃⁰^[k] ∃⁰ a

def LO.FirstOrder.ball {α : ℕ → Type u_1} {n : ℕ} [UnivQuantifier α] [Arrow (α (n + 1))] (φ ψ : α (n + 1)) : α n

Equations

• (∀⁰[φ] ψ) = ∀⁰ (φ 🡒 ψ)

def LO.FirstOrder.bexs {α : ℕ → Type u_1} {n : ℕ} [ExsQuantifier α] [Wedge (α (n + 1))] (φ ψ : α (n + 1)) : α n

Equations

• (∃⁰[φ] ψ) = ∃⁰ φ ⋏ ψ

def LO.FirstOrder.«term∀⁰[_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def LO.FirstOrder.«term∃⁰[_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

Second-order quantifiers

class LO.SecondOrder.UnivQuantifier (α : ℕ → ℕ → Type u_1) : Type u_1

• all₁ {m n : ℕ} : α (m + 1) n → α m n

def LO.SecondOrder.«term∀¹_» : Lean.ParserDescr

Equations

• LO.SecondOrder.«term∀¹_» = Lean.ParserDescr.node `LO.SecondOrder.«term∀¹_» 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∀¹ ") (Lean.ParserDescr.cat `term 64))

class LO.SecondOrder.ExsQuantifier (α : ℕ → ℕ → Type u_1) : Type u_1

• exs₁ {m n : ℕ} : α (m + 1) n → α m n

def LO.SecondOrder.«term∃¹_» : Lean.ParserDescr

Equations

• LO.SecondOrder.«term∃¹_» = Lean.ParserDescr.node `LO.SecondOrder.«term∃¹_» 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∃¹ ") (Lean.ParserDescr.cat `term 64))

class LO.SecondOrder.Quantifier (α : ℕ → ℕ → Type u_1) extends LO.SecondOrder.UnivQuantifier α, LO.SecondOrder.ExsQuantifier α : Type u_1

• all₁ {m n : ℕ} : α (m + 1) n → α m n
• exs₁ {m n : ℕ} : α (m + 1) n → α m n

class LO.SecondOrder.LCWQ (α : ℕ → ℕ → Type u_1) extends LO.SecondOrder.Quantifier α : Type u_1

Logical Connectives with Quantifiers.

• all₁ {m n : ℕ} : α (m + 1) n → α m n
• exs₁ {m n : ℕ} : α (m + 1) n → α m n
• firstOrder (m : ℕ) : FirstOrder.LCWQ (α m)

@[implicit_reducible]

instance LO.SecondOrder.instLCWQOfLCWQ (α : ℕ → ℕ → Type u_1) [LCWQ α] (m : ℕ) : FirstOrder.LCWQ (α m)

Equations

• LO.SecondOrder.instLCWQOfLCWQ α m = LO.SecondOrder.LCWQ.firstOrder m

@[implicit_reducible]

instance LO.SecondOrder.instLCWQOfQuantifierOfLCWQ (α : ℕ → ℕ → Type u_1) [Quantifier α] [(m : ℕ) → FirstOrder.LCWQ (α m)] : LCWQ α

Equations

• LO.SecondOrder.instLCWQOfQuantifierOfLCWQ α = { toQuantifier := inst✝¹, firstOrder := inferInstance }

def LO.SecondOrder.allClosure {α : ℕ → ℕ → Type u_1} [UnivQuantifier α] {n m : ℕ} : α m n → α 0 n

Equations

• ∀¹* a = a
• ∀¹* a = ∀¹* ∀¹ a

def LO.SecondOrder.«term∀¹*_» : Lean.ParserDescr

Equations

• LO.SecondOrder.«term∀¹*_» = Lean.ParserDescr.node `LO.SecondOrder.«term∀¹*_» 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∀¹* ") (Lean.ParserDescr.cat `term 64))

@[simp]

theorem LO.SecondOrder.allClosure_zero {α : ℕ → ℕ → Type u_1} [UnivQuantifier α] {n : ℕ} (a : α 0 n) : ∀¹* a = a

theorem LO.SecondOrder.allClosure_succ {α : ℕ → ℕ → Type u_1} [UnivQuantifier α] {n : ℕ} (a : α (n + 1) n) : ∀¹* a = ∀¹* ∀¹ a

def LO.SecondOrder.allItr {α : ℕ → ℕ → Type u_1} [UnivQuantifier α] {m n : ℕ} (k : ℕ) : α (m + k) n → α m n

Equations

• ∀¹^[0] a = a
• ∀¹^[k.succ] a = ∀¹^[k] ∀¹ a

def LO.SecondOrder.«term∀¹^[_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LO.SecondOrder.allItr_zero {α : ℕ → ℕ → Type u_1} [UnivQuantifier α] {m n : ℕ} (a : α m n) : ∀¹^[0] a = a

@[simp]

theorem LO.SecondOrder.allItr_one {α : ℕ → ℕ → Type u_1} [UnivQuantifier α] {m n : ℕ} (a : α (m + 1) n) : ∀¹^[1] a = ∀¹ a

theorem LO.SecondOrder.allItr_succ {α : ℕ → ℕ → Type u_1} [UnivQuantifier α] {m n k : ℕ} (a : α (m + (k + 1)) n) : ∀¹^[k + 1] a = ∀¹^[k] ∀¹ a

def LO.SecondOrder.exsClosure {α : ℕ → ℕ → Type u_1} [ExsQuantifier α] {n m : ℕ} : α m n → α 0 n

Equations

• ∃¹* a = a
• ∃¹* a = ∃¹* ∃¹ a

def LO.SecondOrder.«term∃¹*_» : Lean.ParserDescr

Equations

• LO.SecondOrder.«term∃¹*_» = Lean.ParserDescr.node `LO.SecondOrder.«term∃¹*_» 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∃¹* ") (Lean.ParserDescr.cat `term 64))

@[simp]

theorem LO.SecondOrder.exsClosure_zero {α : ℕ → ℕ → Type u_1} [ExsQuantifier α] {n : ℕ} (a : α 0 n) : ∃¹* a = a

theorem LO.SecondOrder.exsClosure_succ {α : ℕ → ℕ → Type u_1} [ExsQuantifier α] {m n : ℕ} (a : α (m + 1) n) : ∃¹* a = ∃¹* ∃¹ a

def LO.SecondOrder.exsItr {α : ℕ → ℕ → Type u_1} [ExsQuantifier α] {m n : ℕ} (k : ℕ) : α (m + k) n → α m n

Equations

• ∃¹^[0] a = a
• ∃¹^[k.succ] a = ∃¹^[k] ∃¹ a

def LO.SecondOrder.«term∃¹^[_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LO.SecondOrder.exsItr_zero {α : ℕ → ℕ → Type u_1} [ExsQuantifier α] {m n : ℕ} (a : α m n) : ∃¹^[0] a = a

@[simp]

theorem LO.SecondOrder.exsItr_one {α : ℕ → ℕ → Type u_1} [ExsQuantifier α] {m n : ℕ} (a : α (m + 1) n) : ∃¹^[1] a = ∃¹ a

theorem LO.SecondOrder.exsItr_succ {α : ℕ → ℕ → Type u_1} [ExsQuantifier α] {m n k : ℕ} (a : α (m + (k + 1)) n) : ∃¹^[k + 1] a = ∃¹^[k] ∃¹ a

def LO.SecondOrder.ball {α : ℕ → ℕ → Type u_1} {m n : ℕ} [UnivQuantifier α] [Arrow (α (m + 1) n)] (φ ψ : α (m + 1) n) : α m n

Equations

• (∀¹[φ] ψ) = ∀¹ (φ 🡒 ψ)

def LO.SecondOrder.bexs {α : ℕ → ℕ → Type u_1} {m n : ℕ} [ExsQuantifier α] [Wedge (α (m + 1) n)] (φ ψ : α (m + 1) n) : α m n

Equations

• (∃¹[φ] ψ) = ∃¹ φ ⋏ ψ

def LO.SecondOrder.«term∀¹[_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def LO.SecondOrder.«term∃¹[_]_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.