inductive FFL.Polarity : Type

• sigma : Polarity
• pi : Polarity

@[instance_reducible]

instance FFL.Polarity.instSigmaSymbol : SigmaSymbol Polarity

Equations

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

@[instance_reducible]

instance FFL.Polarity.instPiSymbol : PiSymbol Polarity

Equations

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

def FFL.Polarity.alt : Polarity → Polarity

Equations

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

@[simp]

theorem FFL.Polarity.eq_sigma : sigma = 𝚺

@[simp]

theorem FFL.Polarity.eq_pi : pi = 𝚷

@[simp]

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

@[simp]

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

@[simp]

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

@[reducible, inline]

abbrev FFL.Polarity.altItr (Γ : Polarity) (k : ℕ) : Polarity

Γ with its polarity flipped k times.

Equations

• Γ.altItr k = FFL.Polarity.alt^[k] Γ

@[simp]

theorem FFL.Polarity.altItr_zero (Γ : Polarity) : Γ.altItr 0 = Γ

theorem FFL.Polarity.altItr_succ (Γ : Polarity) (k : ℕ) : Γ.altItr (k + 1) = (Γ.altItr k).alt

theorem FFL.Polarity.altItr_succ' (Γ : Polarity) (k : ℕ) : Γ.altItr (k + 1) = Γ.alt.altItr k

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

Equations

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

@[instance_reducible]

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

Equations

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

@[simp]

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

@[simp]

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

inductive FFL.SigmaPiDelta : Type

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

@[instance_reducible]

instance FFL.SigmaPiDelta.instSigmaSymbol : SigmaSymbol SigmaPiDelta

Equations

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

@[instance_reducible]

instance FFL.SigmaPiDelta.instPiSymbol : PiSymbol SigmaPiDelta

Equations

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

@[instance_reducible]

instance FFL.SigmaPiDelta.instDeltaSymbol : DeltaSymbol SigmaPiDelta

Equations

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

def FFL.SigmaPiDelta.alt : SigmaPiDelta → SigmaPiDelta

Equations

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

@[simp]

theorem FFL.SigmaPiDelta.eq_sigma : sigma = 𝚺

@[simp]

theorem FFL.SigmaPiDelta.eq_pi : pi = 𝚷

@[simp]

theorem FFL.SigmaPiDelta.eq_delta : delta = 𝚫

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

First-order quantifiers

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

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

def FFL.FirstOrder.«term∀¹_» : Lean.ParserDescr

Equations

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

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

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

def FFL.FirstOrder.«term∃¹_» : Lean.ParserDescr

Equations

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

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

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

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

Logical Connectives with Quantifiers.

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance FFL.FirstOrder.instLogicalNeutralOfLCWQ (α : ℕ → Type u_1) [LCWQ α] (n : ℕ) : LogicalNeutral (α n)

Equations

• FFL.FirstOrder.instLogicalNeutralOfLCWQ α n = FFL.FirstOrder.LCWQ.neutrals n

@[instance_reducible]

instance FFL.FirstOrder.instLCWQOfQuantifierOfLogicalConnectiveOfLogicalNeutral (α : ℕ → Type u_1) [Quantifier α] [(n : ℕ) → LogicalConnective (α n)] [(n : ℕ) → LogicalNeutral (α n)] : LCWQ α

Equations

• FFL.FirstOrder.instLCWQOfQuantifierOfLogicalConnectiveOfLogicalNeutral α = { toQuantifier := inst✝², connectives := inferInstance, neutrals := inferInstance }

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

Equations

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

def FFL.FirstOrder.«term∀¹*_» : Lean.ParserDescr

The universal closure of a formula.

Equations

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

@[simp]

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

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

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

Equations

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

def FFL.FirstOrder.«term∀¹^[_]_» : Lean.ParserDescr

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

def FFL.FirstOrder.«term∃¹*_» : Lean.ParserDescr

The existential closure of a formula.

Equations

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

@[simp]

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

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

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

Equations

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

def FFL.FirstOrder.«term∃¹^[_]_» : Lean.ParserDescr

Iterated application of k existential quantifiers.

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

Equations

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

def FFL.FirstOrder.«term∀¹[_]_» : Lean.ParserDescr

A bounded universal quantifier. ∀¹[φ] ψ is defined as ∀¹ (φ 🡒 ψ).

Equations

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

def FFL.FirstOrder.«term∃¹[_]_» : Lean.ParserDescr

A bounded existential quantifier. ∃¹[φ] ψ is defined as ∃¹ (φ ⋏ ψ).

Equations

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

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

Equations

• FFL.Polarity.sigma.quant = FFL.FirstOrder.ExsQuantifier.exs
• FFL.Polarity.pi.quant = FFL.FirstOrder.UnivQuantifier.all

@[simp]

theorem FFL.Polarity.quant_sigma {α : ℕ → Type u_1} [FirstOrder.UnivQuantifier α] [FirstOrder.ExsQuantifier α] {n : ℕ} (φ : α (n + 1)) : 𝚺.quant φ = ∃¹ φ

@[simp]

theorem FFL.Polarity.quant_pi {α : ℕ → Type u_1} [FirstOrder.UnivQuantifier α] [FirstOrder.ExsQuantifier α] {n : ℕ} (φ : α (n + 1)) : 𝚷.quant φ = ∀¹ φ

def FFL.Polarity.quantItr {α : ℕ → Type u_1} [FirstOrder.UnivQuantifier α] [FirstOrder.ExsQuantifier α] (Γ : Polarity) (k : ℕ) {n : ℕ} : α (n + k) → α n

Prefixes k alternating quantifiers starting with Γ.

Equations

• Γ.quantItr 0 x✝ = x✝
• Γ.quantItr k.succ x✝ = Γ.quant (Γ.alt.quantItr k (cast ⋯ x✝))

@[simp]

theorem FFL.Polarity.quantItr_zero {α : ℕ → Type u_1} [FirstOrder.UnivQuantifier α] [FirstOrder.ExsQuantifier α] {n : ℕ} {Γ : Polarity} (φ : α n) : Γ.quantItr 0 φ = φ

@[simp]

theorem FFL.Polarity.quantItr_one {α : ℕ → Type u_1} [FirstOrder.UnivQuantifier α] [FirstOrder.ExsQuantifier α] {n : ℕ} {Γ : Polarity} (φ : α (n + 1)) : Γ.quantItr 1 φ = Γ.quant φ

theorem FFL.Polarity.quantItr_succ {α : ℕ → Type u_1} [FirstOrder.UnivQuantifier α] [FirstOrder.ExsQuantifier α] {n : ℕ} {Γ : Polarity} {k : ℕ} (φ : α (n + (k + 1))) : Γ.quantItr (k + 1) φ = Γ.quant (Γ.alt.quantItr k (cast ⋯ φ))

theorem FFL.Polarity.cast_quant {α : ℕ → Type u_1} [FirstOrder.UnivQuantifier α] [FirstOrder.ExsQuantifier α] {m₁ m₂ : ℕ} (h : m₁ = m₂) (Γ : Polarity) (φ : α (m₁ + 1)) : cast ⋯ (Γ.quant φ) = Γ.quant (cast ⋯ φ)

theorem FFL.Polarity.quantItr_succ' {α : ℕ → Type u_1} [FirstOrder.UnivQuantifier α] [FirstOrder.ExsQuantifier α] {n : ℕ} {Γ : Polarity} {k : ℕ} (φ : α (n + (k + 1))) : Γ.quantItr (k + 1) φ = Γ.quantItr k ((Γ.altItr k).quant φ)

Second-order quantifiers

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

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

def FFL.SecondOrder.«term∀²_» : Lean.ParserDescr

Equations

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

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

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

def FFL.SecondOrder.«term∃²_» : Lean.ParserDescr

Equations

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

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

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

class FFL.SecondOrder.LCWQ (α : ℕ → ℕ → Type u_1) extends FFL.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)

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

Equations

• ∀²* a = a
• ∀²* a = ∀²* ∀² a

def FFL.SecondOrder.«term∀²*_» : Lean.ParserDescr

Equations

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

@[simp]

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

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

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

Equations

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

def FFL.SecondOrder.«term∀²^[_]_» : Lean.ParserDescr

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

• ∃²* a = a
• ∃²* a = ∃²* ∃² a

def FFL.SecondOrder.«term∃²*_» : Lean.ParserDescr

Equations

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

@[simp]

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

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

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

Equations

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

def FFL.SecondOrder.«term∃²^[_]_» : Lean.ParserDescr

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

Equations

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

def FFL.SecondOrder.«term∀²[_]_» : Lean.ParserDescr

Equations

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

def FFL.SecondOrder.«term∃²[_]_» : Lean.ParserDescr

Equations

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