Quantifier

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

Imported declaration from the Incompleteness formalization.

• sigma : α

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

• pi : α

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

• delta : α

  Imported declaration from the Incompleteness formalization.

def LO.termSg : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.termSg = Lean.ParserDescr.node `LO.termSg 1024 (Lean.ParserDescr.symbol "Sg")

def LO.termPg : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.termPg = Lean.ParserDescr.node `LO.termPg 1024 (Lean.ParserDescr.symbol "Pg")

def LO.termDlt : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.termDlt = Lean.ParserDescr.node `LO.termDlt 1024 (Lean.ParserDescr.symbol "Dlt")

inductive LO.Polarity : Type

Imported declaration from the Incompleteness formalization.

• 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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Polarity.sigma.alt = Pg
• LO.Polarity.pi.alt = Sg

theorem LO.Polarity.eq_sigma : sigma = Sg

theorem LO.Polarity.eq_pi : pi = Pg

@[simp]

theorem LO.Polarity.alt_sigma : Sg.alt = Pg

@[simp]

theorem LO.Polarity.alt_pi : Pg.alt = Sg

@[simp]

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

inductive LO.SigmaPiDelta : Type

Imported declaration from the Incompleteness formalization.

• 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

Imported declaration from the Incompleteness formalization.

Equations

• LO.SigmaPiDelta.sigma.alt = Pg
• LO.SigmaPiDelta.pi.alt = Sg
• LO.SigmaPiDelta.delta.alt = Dlt

theorem LO.SigmaPiDelta.eq_sigma : sigma = Sg

theorem LO.SigmaPiDelta.eq_pi : pi = Pg

theorem LO.SigmaPiDelta.eq_delta : delta = Dlt

@[simp]

theorem LO.SigmaPiDelta.alt_sigma : Sg.alt = Pg

@[simp]

theorem LO.SigmaPiDelta.alt_pi : Pg.alt = Sg

@[simp]

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

@[simp]

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

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

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 Sg φ = ∃' φ

@[simp]

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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