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

• sigma : α

Instances

• LO.Polarity.instSigmaSymbol
• LO.SigmaPiDelta.instSigmaSymbol

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

• pi : α

Instances

• LO.Polarity.instPiSymbol
• LO.SigmaPiDelta.instPiSymbol

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

• delta : α

Instances

• LO.SigmaPiDelta.instDeltaSymbol

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 : Polarity
• pi : Polarity

Instances For

• LO.Polarity.instCoe_arithmetization
• LO.Polarity.instPiSymbol
• LO.Polarity.instSigmaSymbol

instance LO.Polarity.instSigmaSymbol : SigmaSymbol Polarity

Equations

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

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 = Γ

inductive LO.SigmaPiDelta : Type

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

Instances For

• LO.SigmaPiDelta.instDeltaSymbol
• LO.SigmaPiDelta.instPiSymbol
• LO.SigmaPiDelta.instSigmaSymbol

instance LO.SigmaPiDelta.instSigmaSymbol : SigmaSymbol SigmaPiDelta

Equations

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

instance LO.SigmaPiDelta.instPiSymbol : PiSymbol SigmaPiDelta

Equations

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

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 = Γ

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

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

Instances

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instUnivQuantifierMkPiSigmaPiDeltaHAddNatOfNat

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

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

Instances

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instExQuantifierMkSigmaSigmaPiDeltaHAddNatOfNat

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

Instances

• LO.FirstOrder.Semiformula.instQuantifier
• LO.FirstOrder.Semiformulaᵢ.instQuantifier

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 : ℕ) : LogicalConnective (α n)

Instances

• LO.instLCWQOfQuantifierOfLogicalConnective

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

Equations

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

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

Equations

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

def LO.quant {α : ℕ → Type u_1} [UnivQuantifier α] [ExQuantifier α] {n : ℕ} : 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} [UnivQuantifier α] [ExQuantifier α] {n : ℕ} (φ : α (n + 1)) : quant 𝚺 φ = ∃' φ

@[simp]

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

def LO.univClosure {α : ℕ → Type u_1} [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} [UnivQuantifier α] (a : α 0) : ∀* a = a

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

def LO.univItr {α : ℕ → Type u_1} [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} [UnivQuantifier α] {n : ℕ} (a : α n) : ∀^[0] a = a

@[simp]

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

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

def LO.exClosure {α : ℕ → Type u_1} [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} [ExQuantifier α] (a : α 0) : ∃* a = a

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

def LO.exItr {α : ℕ → Type u_1} [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} [ExQuantifier α] {n : ℕ} (a : α n) : ∃^[0] a = a

@[simp]

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

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

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

Equations

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

def LO.bex {α : ℕ → Type u_1} {n : ℕ} [ExQuantifier α] [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.