class LO.SigmaSymbol (α : Type u_1) : Type u_1

• sigma : α

class LO.PiSymbol (α : Type u_1) : Type u_1

• pi : α

class LO.DeltaSymbol (α : Type u_1) : Type u_1

• delta : α

def LO.«term𝚺» : Lean.ParserDescr

Equations

• LO.«term𝚺» = Lean.ParserDescr.node `LO.«term𝚺» 1024 (Lean.ParserDescr.symbol "𝚺")

def LO.«term𝚷» : Lean.ParserDescr

Equations

• LO.«term𝚷» = Lean.ParserDescr.node `LO.«term𝚷» 1024 (Lean.ParserDescr.symbol "𝚷")

def LO.«term𝚫» : Lean.ParserDescr

Equations

• LO.«term𝚫» = Lean.ParserDescr.node `LO.«term𝚫» 1024 (Lean.ParserDescr.symbol "𝚫")

inductive LO.Polarity : Type

• sigma: LO.Polarity
• pi: LO.Polarity

instance LO.Polarity.instSigmaSymbol : LO.SigmaSymbol LO.Polarity

Equations

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

instance LO.Polarity.instPiSymbol : LO.PiSymbol LO.Polarity

Equations

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

def LO.Polarity.alt : LO.Polarity → LO.Polarity

Equations

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

@[simp]

theorem LO.Polarity.eq_sigma : LO.Polarity.sigma = 𝚺

@[simp]

theorem LO.Polarity.eq_pi : LO.Polarity.pi = 𝚷

@[simp]

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

@[simp]

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

@[simp]

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

inductive LO.SigmaPiDelta : Type

• sigma: LO.SigmaPiDelta
• pi: LO.SigmaPiDelta
• delta: LO.SigmaPiDelta

instance LO.SigmaPiDelta.instSigmaSymbol : LO.SigmaSymbol LO.SigmaPiDelta

Equations

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

instance LO.SigmaPiDelta.instPiSymbol : LO.PiSymbol LO.SigmaPiDelta

Equations

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

instance LO.SigmaPiDelta.instDeltaSymbol : LO.DeltaSymbol LO.SigmaPiDelta

Equations

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

def LO.SigmaPiDelta.alt : LO.SigmaPiDelta → LO.SigmaPiDelta

Equations

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

@[simp]

theorem LO.SigmaPiDelta.eq_sigma : LO.SigmaPiDelta.sigma = 𝚺

@[simp]

theorem LO.SigmaPiDelta.eq_pi : LO.SigmaPiDelta.pi = 𝚷

@[simp]

theorem LO.SigmaPiDelta.eq_delta : LO.SigmaPiDelta.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 (Γ : LO.SigmaPiDelta) : Γ.alt.alt = Γ

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

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

class LO.ExQuantifier (α : ℕ → Type u_1) : Type u_1

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

def LO.«term∀'_» : Lean.ParserDescr

Equations

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

def LO.«term∃'_» : Lean.ParserDescr

Equations

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

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

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

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

Logical Connectives with Quantifiers.

• univ : {n : ℕ} → α (n + 1) → α n
• ex : {n : ℕ} → α (n + 1) → α n
• connectives : (n : ℕ) → LO.LogicalConnective (α n)

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

Equations

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

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

Equations

• LO.instLCWQOfQuantifierOfLogicalConnective α = LO.LCWQ.mk inferInstance

def LO.quant {α : ℕ → Type u_1} [LO.UnivQuantifier α] [LO.ExQuantifier α] {n : ℕ} : LO.Polarity → α (n + 1) → α n

Equations

• LO.quant LO.Polarity.sigma x = ∃' x
• LO.quant LO.Polarity.pi x = ∀' x

@[simp]

theorem LO.quant_sigma {α : ℕ → Type u_1} [LO.UnivQuantifier α] [LO.ExQuantifier α] {n : ℕ} (φ : α (n + 1)) : LO.quant 𝚺 φ = ∃' φ

@[simp]

theorem LO.quant_pi {α : ℕ → Type u_1} [LO.UnivQuantifier α] [LO.ExQuantifier α] {n : ℕ} (φ : α (n + 1)) : LO.quant 𝚷 φ = ∀' φ

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

Equations

• ∀* a = a
• ∀* a = ∀* ∀' a

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

Equations

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

@[simp]

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

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

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

def LO.exClosure {α : ℕ → Type u_1} [LO.ExQuantifier α] {n : ℕ} : α n → α 0

Equations

• ∃* a = a
• ∃* a = ∃* ∃' a

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

Equations

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

@[simp]

theorem LO.exClosure_zero {α : ℕ → Type u_1} [LO.ExQuantifier α] (a : α 0) : ∃* a = a

theorem LO.exClosure_succ {α : ℕ → Type u_1} [LO.ExQuantifier α] {n : ℕ} (a : α (n + 1)) : ∃* a = ∃* ∃' a

def LO.exItr {α : ℕ → Type u_1} [LO.ExQuantifier α] {n : ℕ} (k : ℕ) : α (n + k) → α n

Equations

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

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

Equations

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

@[simp]

theorem LO.exItr_zero {α : ℕ → Type u_1} [LO.ExQuantifier α] {n : ℕ} (a : α n) : ∃^[0] a = a

@[simp]

theorem LO.exItr_one {α : ℕ → Type u_1} [LO.ExQuantifier α] {n : ℕ} (a : α (n + 1)) : ∃^[1] a = ∃' a

theorem LO.exItr_succ {α : ℕ → Type u_1} [LO.ExQuantifier α] {n k : ℕ} (a : α (n + (k + 1))) : ∃^[k + 1] a = ∃^[k] ∃' a

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

Equations

• (∀[φ] ψ) = ∀' (φ ➝ ψ)

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

Equations

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

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

Equations

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

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

Equations

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