Canonical model for classical first-order logic

Main reference: Jeremy Avigad, Algebraic proofs of cut elimination [Avi01]

def FFL.FirstOrder.LK.Derivation.Canonical.ConsistentSequent (L : Language) : Type u_1

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.ConsistentSequent L = { Γ : FFL.FirstOrder.LK.Sequent L // IsEmpty (⊢ᴸᴷ¹ ∼Γ) }

@[instance_reducible]

instance FFL.FirstOrder.LK.Derivation.Canonical.ConsistentSequent.instPreorder {L : Language} : Preorder (ConsistentSequent L)

Equations

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

def FFL.FirstOrder.LK.Derivation.Canonical.ConsistentSequent.nil {L : Language} : ConsistentSequent L

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.ConsistentSequent.nil = ⟨0, ⋯⟩

@[instance_reducible]

instance FFL.FirstOrder.LK.Derivation.Canonical.ConsistentSequent.instOrderTop {L : Language} : OrderTop (ConsistentSequent L)

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.ConsistentSequent.instOrderTop = { top := FFL.FirstOrder.LK.Derivation.Canonical.ConsistentSequent.nil, le_top := ⋯ }

def FFL.FirstOrder.LK.Derivation.Canonical.ConsistentSequent.ofUnprovable {L : Language} (φ : Proposition L) (h : 𝐋𝐊¹ ⊬ ∼φ) : ConsistentSequent L

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.ConsistentSequent.ofUnprovable φ h = ⟨⦃φ⦄, ⋯⟩

@[reducible, inline]

abbrev FFL.FirstOrder.LK.Derivation.Canonical.IsForced {L : Language} (p : ConsistentSequent L) (φ : Propositionᵢ L) : Prop

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.IsForced p φ = Nonempty (FFL.FirstOrder.LK.Derivation.Canonical.Forces (↑p) φ)

@[instance_reducible]

instance FFL.FirstOrder.LK.Derivation.Canonical.instForcingRelationConsistentSequentPropositionᵢ {L : Language} : ForcingRelation (ConsistentSequent L) (Propositionᵢ L)

Equations

• FFL.FirstOrder.LK.Derivation.Canonical.instForcingRelationConsistentSequentPropositionᵢ = { Forces := FFL.FirstOrder.LK.Derivation.Canonical.IsForced }

@[instance_reducible]

instance FFL.FirstOrder.LK.Derivation.Canonical.instWeakForcingRelationConsistentSequentProposition {L : Language} : WeakForcingRelation (ConsistentSequent L) (Proposition L)

Equations

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

@[simp]

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsForced.rel {L : Language} {p : ConsistentSequent L} {k : ℕ} {R : L.Rel k} {v : Fin k → Semiterm L ℕ 0} : p ⊩ Semiformulaᵢ.rel R v ↔ Nonempty (⊢ᴸᴷ¹ ∼↑p + ⦃Semiformula.rel R v⦄)

@[simp]

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsForced.fal {L : Language} {φ : Semipropositionᵢ L (0 + 1)} {p : ConsistentSequent L} : p ⊩ ∀¹ φ ↔ ∀ (t : Semiterm L ℕ 0), p ⊩ φ/[t]

@[simp]

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsForced.and {L : Language} {p : ConsistentSequent L} {φ ψ : Propositionᵢ L} : p ⊩ φ ⋏ ψ ↔ p ⊩ φ ∧ p ⊩ ψ

@[simp]

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsForced.or {L : Language} {p : ConsistentSequent L} {φ ψ : Propositionᵢ L} : p ⊩ φ ⋎ ψ ↔ p ⊩ φ ∨ p ⊩ ψ

@[simp]

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsForced.not_falsum {L : Language} (p : ConsistentSequent L) : ¬p ⊩ ⊥

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsForced.imply {L : Language} {p : ConsistentSequent L} {φ ψ : Propositionᵢ L} : p ⊩ φ 🡒 ψ ↔ ∀ q ≤ p, q ⊩ φ → q ⊩ ψ

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsForced.not {L : Language} {p : ConsistentSequent L} {φ : Propositionᵢ L} : p ⊩ ∼φ ↔ ∀ q ≤ p, ¬q ⊩ φ

@[simp]

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsForced.exs {L : Language} {φ : Semipropositionᵢ L (0 + 1)} {p : ConsistentSequent L} : p ⊩ ∃¹ φ ↔ ∃ (t : Semiterm L ℕ 0), p ⊩ φ/[t]

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsForced.monotone {L : Language} {p q : ConsistentSequent L} (hqp : q ≤ p) {φ : Propositionᵢ L} (hφ : p ⊩ φ) : q ⊩ φ

instance FFL.FirstOrder.LK.Derivation.Canonical.IsForced.instIntKripkeConsistentSequentPropositionᵢGe {L : Language} : ForcingRelation.IntKripke (ConsistentSequent L) fun (x1 x2 : ConsistentSequent L) => x1 ≥ x2

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsForced.sound {L : Language} [L.DecidableEq] {φ : Propositionᵢ L} : 𝐋𝐉¹ ⊢ φ → ConsistentSequent L ∀⊩ φ

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsWeaklyForced.iff_isForced {L : Language} {φ : Proposition L} {p : ConsistentSequent L} : p ⊩ᶜ φ ↔ p ⊩ Semiformula.doubleNegation φ

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsWeaklyForced.dn_neg_iff {L : Language} {φ : Proposition L} {p : ConsistentSequent L} : p ⊩ᶜ ∼φ ↔ p ⊩ ∼Semiformula.doubleNegation φ

@[simp]

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsWeaklyForced.verum {L : Language} (p : ConsistentSequent L) : p ⊩ᶜ ⊤

@[simp]

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsWeaklyForced.falsum {L : Language} (p : ConsistentSequent L) : ¬p ⊩ᶜ ⊥

@[simp]

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsWeaklyForced.not {L : Language} {φ : Proposition L} {p : ConsistentSequent L} : p ⊩ᶜ ∼φ ↔ ∀ q ≤ p, ¬q ⊩ᶜ φ

@[simp]

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsWeaklyForced.and {L : Language} {φ ψ : Proposition L} {p : ConsistentSequent L} : p ⊩ᶜ φ ⋏ ψ ↔ p ⊩ᶜ φ ∧ p ⊩ᶜ ψ

@[simp]

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsWeaklyForced.or {L : Language} {φ ψ : Proposition L} {p : ConsistentSequent L} : p ⊩ᶜ φ ⋎ ψ ↔ ∀ q ≤ p, ∃ r ≤ q, r ⊩ᶜ φ ∨ r ⊩ᶜ ψ

@[simp]

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsWeaklyForced.all {L : Language} {φ : Semiproposition L 1} {p : ConsistentSequent L} : p ⊩ᶜ ∀¹ φ ↔ ∀ (t : Semiterm L ℕ 0), p ⊩ᶜ φ/[t]

@[simp]

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsWeaklyForced.exs {L : Language} {φ : Semiproposition L 1} {p : ConsistentSequent L} : p ⊩ᶜ ∃¹ φ ↔ ∀ q ≤ p, ∃ r ≤ q, ∃ (t : Semiterm L ℕ 0), r ⊩ᶜ φ/[t]

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsWeaklyForced.monotone {L : Language} {φ : Proposition L} {p q : ConsistentSequent L} (h : q ≤ p) : p ⊩ᶜ φ → q ⊩ᶜ φ

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsWeaklyForced.gnericity {L : Language} {φ : Proposition L} {p : ConsistentSequent L} : p ⊩ᶜ φ ↔ ∀ q ≤ p, ∃ r ≤ q, r ⊩ᶜ φ

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsWeaklyForced.complete {L : Language} {φ : Proposition L} : ConsistentSequent L ∀⊩ᶜ φ ↔ 𝐋𝐊¹ ⊢ φ

theorem FFL.FirstOrder.LK.Derivation.Canonical.IsWeaklyForced.refl {L : Language} (φ : Proposition L) (h : 𝐋𝐊¹ ⊬ ∼φ) : ConsistentSequent.ofUnprovable φ h ⊩ᶜ φ