Basic definitions and properties of proof system related notions

This file defines a characterization of the system/proof/provability/calculus of formulae. Also defines soundness and completeness.

Main Definitions

• FFL.Entailment S F: a general framework of deductive system S for formulae F.
• FFL.Entailment.Inconsistent 𝓢: a proposition that states that all formulae in F is provable from 𝓢.
• FFL.Entailment.Consistent 𝓢: a proposition that states that 𝓢 is not inconsistent.
• FFL.Entailment.Sound 𝓢 𝓜: provability from 𝓢 implies satisfiability on 𝓜.
• FFL.Entailment.Complete 𝓢 𝓜: satisfiability on 𝓜 implies provability from 𝓢.

Notation

• 𝓢 ⊢! φ: a type of formalized proofs of φ : F from deductive system 𝓢 : S.
• 𝓢 ⊢ φ: a proposition that states there is a proof of φ from 𝓢, i.e. φ is provable from 𝓢.
• 𝓢 ⊬ φ: a proposition that states φ is not provable from 𝓢.
• 𝓢 ⊢!* T: a type of formalized proofs for each formulae in a set T from 𝓢.
• 𝓢 ⊢* T: a proposition that states each formulae in T is provable from 𝓢.

class FFL.Entailment (S : Type u_1) (F : outParam (Type u_2)) : Type (max (max u_1 u_2) (u_3 + 1))

Entailment relation on proof system S and formula F

• Prf : S → F → Type u_3

def FFL.«term_⊢!_» : Lean.TrailingParserDescr

Equations

• FFL.«term_⊢!_» = Lean.ParserDescr.trailingNode `FFL.«term_⊢!_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢! ") (Lean.ParserDescr.cat `term 46))

def FFL.Entailment.Provable {F : Type u_1} {S : Type u_2} [Entailment S F] (𝓢 : S) (φ : F) : Prop

Proposition that states φ is provable.

Equations

• (𝓢 ⊢ φ) = Nonempty (𝓢 ⊢! φ)

@[reducible, inline]

abbrev FFL.Entailment.Unprovable {F : Type u_1} {S : Type u_2} [Entailment S F] (𝓢 : S) (φ : F) : Prop

Abbreviation for unprovability.

Equations

• (𝓢 ⊬ φ) = ¬𝓢 ⊢ φ

def FFL.Entailment.«term_⊢_» : Lean.TrailingParserDescr

Equations

• FFL.Entailment.«term_⊢_» = Lean.ParserDescr.trailingNode `FFL.Entailment.«term_⊢_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢ ") (Lean.ParserDescr.cat `term 46))

def FFL.Entailment.«term_⊬_» : Lean.TrailingParserDescr

Equations

• FFL.Entailment.«term_⊬_» = Lean.ParserDescr.trailingNode `FFL.Entailment.«term_⊬_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊬ ") (Lean.ParserDescr.cat `term 46))

def FFL.Entailment.PrfSet {F : Type u_1} {S : Type u_2} [Entailment S F] (𝓢 : S) (s : Set F) : Type (max u_1 u_5)

Proofs of set of formulae.

Equations

• (𝓢 ⊢!* s) = (⦃φ : F⦄ → φ ∈ s → 𝓢 ⊢! φ)

def FFL.Entailment.ProvableSet {F : Type u_1} {S : Type u_2} [Entailment S F] (𝓢 : S) (s : Set F) : Prop

Proposition for existance of proofs of set of formulae.

Equations

• (𝓢 ⊢* s) = ∀ {φ : F}, φ ∈ s → 𝓢 ⊢ φ

def FFL.Entailment.«term_⊢!*_» : Lean.TrailingParserDescr

Equations

• FFL.Entailment.«term_⊢!*_» = Lean.ParserDescr.trailingNode `FFL.Entailment.«term_⊢!*_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢!* ") (Lean.ParserDescr.cat `term 46))

def FFL.Entailment.«term_⊢*_» : Lean.TrailingParserDescr

Equations

• FFL.Entailment.«term_⊢*_» = Lean.ParserDescr.trailingNode `FFL.Entailment.«term_⊢*_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢* ") (Lean.ParserDescr.cat `term 46))

def FFL.Entailment.theory {F : Type u_1} {S : Type u_2} [Entailment S F] (𝓢 : S) : Set F

Set of all provable formulae.

Equations

• FFL.Entailment.theory 𝓢 = {φ : F | 𝓢 ⊢ φ}

def FFL.Entailment.cast {F : Type u_1} {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} (b : 𝓢 ⊢! φ) (e : φ = ψ := by simp) : 𝓢 ⊢! ψ

Equations

• FFL.Entailment.cast b e = e ▸ b

theorem FFL.Entailment.cast! {F : Type u_1} {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} (b : 𝓢 ⊢ φ) (e : φ = ψ := by simp) : 𝓢 ⊢ ψ

theorem FFL.Entailment.unprovable_iff_isEmpty {F : Type u_1} {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} : 𝓢 ⊬ φ ↔ IsEmpty (𝓢 ⊢! φ)

noncomputable def FFL.Entailment.Provable.get {F : Type u_1} {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} (h : 𝓢 ⊢ φ) : 𝓢 ⊢! φ

Equations

• h.get = Classical.choice h

theorem FFL.Entailment.provableSet_iff {F : Type u_1} {S : Type u_2} [Entailment S F] {𝓢 : S} {s : Set F} : 𝓢 ⊢* s ↔ Nonempty (𝓢 ⊢!* s)

noncomputable def FFL.Entailment.ProvableSet.get {F : Type u_1} {S : Type u_2} [Entailment S F] {𝓢 : S} {s : Set F} (h : 𝓢 ⊢* s) : 𝓢 ⊢!* s

Equations

• h.get = Classical.choice ⋯

class FFL.Entailment.WeakerThan {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] (𝓢 : S) (𝓣 : T) : Prop

Provability strength relation of proof systems

• subset : theory 𝓢 ⊆ theory 𝓣

def FFL.Entailment.«term_⪯_» : Lean.TrailingParserDescr

Equations

• FFL.Entailment.«term_⪯_» = Lean.ParserDescr.trailingNode `FFL.Entailment.«term_⪯_» 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⪯ ") (Lean.ParserDescr.cat `term 41))

class FFL.Entailment.StrictlyWeakerThan {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] (𝓢 : S) (𝓣 : T) : Prop

Strict provability strength relation of proof systems

• weakerThan : 𝓢 ⪯ 𝓣
• notWT : ¬𝓣 ⪯ 𝓢

def FFL.Entailment.«term_⪱_» : Lean.TrailingParserDescr

Equations

• FFL.Entailment.«term_⪱_» = Lean.ParserDescr.trailingNode `FFL.Entailment.«term_⪱_» 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⪱ ") (Lean.ParserDescr.cat `term 41))

class FFL.Entailment.Equiv {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] (𝓢 : S) (𝓣 : T) : Prop

Provability equivalence relation of proof systems

• eq : theory 𝓢 = theory 𝓣

def FFL.Entailment.«term_≊_» : Lean.TrailingParserDescr

Equations

• FFL.Entailment.«term_≊_» = Lean.ParserDescr.trailingNode `FFL.Entailment.«term_≊_» 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≊ ") (Lean.ParserDescr.cat `term 41))

Provability strength

@[simp]

instance FFL.Entailment.WeakerThan.refl {F : Type u_1} {S : Type u_2} [Entailment S F] (𝓢 : S) : 𝓢 ⪯ 𝓢

theorem FFL.Entailment.WeakerThan.wk {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] {𝓢 : S} {𝓣 : T} (h : 𝓢 ⪯ 𝓣) {φ : F} : 𝓢 ⊢ φ → 𝓣 ⊢ φ

theorem FFL.Entailment.WeakerThan.pbl {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] {𝓢 : S} {𝓣 : T} [h : 𝓢 ⪯ 𝓣] {φ : F} : 𝓢 ⊢ φ → 𝓣 ⊢ φ

theorem FFL.Entailment.WeakerThan.trans {F : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [Entailment S F] [Entailment T F] [Entailment U F] {𝓢 : S} {𝓣 : T} {𝓤 : U} : 𝓢 ⪯ 𝓣 → 𝓣 ⪯ 𝓤 → 𝓢 ⪯ 𝓤

@[instance_reducible]

instance FFL.Entailment.instTransWeakerThan {F : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [Entailment S F] [Entailment T F] [Entailment U F] : Trans (fun (x1 : S) (x2 : T) => x1 ⪯ x2) (fun (x1 : T) (x2 : U) => x1 ⪯ x2) fun (x1 : S) (x2 : U) => x1 ⪯ x2

Equations

• FFL.Entailment.instTransWeakerThan = { trans := ⋯ }

theorem FFL.Entailment.weakerThan_iff {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] {𝓢 : S} {𝓣 : T} : 𝓢 ⪯ 𝓣 ↔ ∀ {φ : F}, 𝓢 ⊢ φ → 𝓣 ⊢ φ

theorem FFL.Entailment.not_weakerThan_iff {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] {𝓢 : S} {𝓣 : T} : ¬𝓢 ⪯ 𝓣 ↔ ∃ (φ : F), 𝓢 ⊢ φ ∧ 𝓣 ⊬ φ

theorem FFL.Entailment.strictlyWeakerThan_iff {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] {𝓢 : S} {𝓣 : T} : 𝓢 ⪱ 𝓣 ↔ (∀ {φ : F}, 𝓢 ⊢ φ → 𝓣 ⊢ φ) ∧ ∃ (φ : F), 𝓢 ⊬ φ ∧ 𝓣 ⊢ φ

theorem FFL.Entailment.swt_of_swt_of_wt {F : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [Entailment S F] [Entailment T F] [Entailment U F] {𝓢 : S} {𝓣 : T} {𝓤 : U} : 𝓢 ⪱ 𝓣 → 𝓣 ⪯ 𝓤 → 𝓢 ⪱ 𝓤

theorem FFL.Entailment.swt_of_wt_of_swt {F : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [Entailment S F] [Entailment T F] [Entailment U F] {𝓢 : S} {𝓣 : T} {𝓤 : U} : 𝓢 ⪯ 𝓣 → 𝓣 ⪱ 𝓤 → 𝓢 ⪱ 𝓤

instance FFL.Entailment.instWeakerThanOfStrictlyWeakerThan {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] {𝓢 : S} {𝓣 : T} [𝓢 ⪱ 𝓣] : 𝓢 ⪯ 𝓣

theorem FFL.Entailment.StrictlyWeakerThan.trans {F : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [Entailment S F] [Entailment T F] [Entailment U F] {𝓢 : S} {𝓣 : T} {𝓤 : U} : 𝓢 ⪱ 𝓣 → 𝓣 ⪱ 𝓤 → 𝓢 ⪱ 𝓤

@[instance_reducible]

instance FFL.Entailment.instTransStrictlyWeakerThanWeakerThan {F : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [Entailment S F] [Entailment T F] [Entailment U F] : Trans (fun (x1 : S) (x2 : T) => x1 ⪱ x2) (fun (x1 : T) (x2 : U) => x1 ⪯ x2) fun (x1 : S) (x2 : U) => x1 ⪱ x2

Equations

• FFL.Entailment.instTransStrictlyWeakerThanWeakerThan = { trans := ⋯ }

@[instance_reducible]

instance FFL.Entailment.instTransWeakerThanStrictlyWeakerThan {F : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [Entailment S F] [Entailment T F] [Entailment U F] : Trans (fun (x1 : S) (x2 : T) => x1 ⪯ x2) (fun (x1 : T) (x2 : U) => x1 ⪱ x2) fun (x1 : S) (x2 : U) => x1 ⪱ x2

Equations

• FFL.Entailment.instTransWeakerThanStrictlyWeakerThan = { trans := ⋯ }

@[instance_reducible]

instance FFL.Entailment.instTransStrictlyWeakerThan {F : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [Entailment S F] [Entailment T F] [Entailment U F] : Trans (fun (x1 : S) (x2 : T) => x1 ⪱ x2) (fun (x1 : T) (x2 : U) => x1 ⪱ x2) fun (x1 : S) (x2 : U) => x1 ⪱ x2

Equations

• FFL.Entailment.instTransStrictlyWeakerThan = { trans := ⋯ }

theorem FFL.Entailment.weakening {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] {𝓢 : S} {𝓣 : T} (h : 𝓢 ⪯ 𝓣) {φ : F} : 𝓢 ⊢ φ → 𝓣 ⊢ φ

theorem FFL.Entailment.StrictlyWeakerThan.of_unprovable_provable {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] {𝓢 : S} {𝓣 : T} [𝓢 ⪯ 𝓣] {φ : F} (hS : 𝓢 ⊬ φ) (hT : 𝓣 ⊢ φ) : 𝓢 ⪱ 𝓣

theorem FFL.Entailment.Equiv.iff {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] {𝓢 : S} {𝓣 : T} : 𝓢 ≊ 𝓣 ↔ ∀ (φ : F), 𝓢 ⊢ φ ↔ 𝓣 ⊢ φ

@[simp]

instance FFL.Entailment.Equiv.refl {F : Type u_1} {S : Type u_2} [Entailment S F] (𝓢 : S) : 𝓢 ≊ 𝓢

theorem FFL.Entailment.Equiv.symm {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] {𝓢 : S} {𝓣 : T} : 𝓢 ≊ 𝓣 → 𝓣 ≊ 𝓢

theorem FFL.Entailment.Equiv.trans {F : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [Entailment S F] [Entailment T F] [Entailment U F] {𝓢 : S} {𝓣 : T} {𝓤 : U} : 𝓢 ≊ 𝓣 → 𝓣 ≊ 𝓤 → 𝓢 ≊ 𝓤

theorem FFL.Entailment.Equiv.antisymm_iff {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] {𝓢 : S} {𝓣 : T} : 𝓢 ≊ 𝓣 ↔ 𝓢 ⪯ 𝓣 ∧ 𝓣 ⪯ 𝓢

theorem FFL.Entailment.Equiv.antisymm {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] {𝓢 : S} {𝓣 : T} : 𝓢 ⪯ 𝓣 ∧ 𝓣 ⪯ 𝓢 → 𝓢 ≊ 𝓣

Alias of the reverse direction of FFL.Entailment.Equiv.antisymm_iff.

theorem FFL.Entailment.Equiv.le {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] {𝓢 : S} {𝓣 : T} : 𝓢 ≊ 𝓣 → 𝓢 ⪯ 𝓣

@[instance_reducible]

instance FFL.Entailment.instTransEquiv {F : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [Entailment S F] [Entailment T F] [Entailment U F] : Trans (fun (x1 : S) (x2 : T) => x1 ≊ x2) (fun (x1 : T) (x2 : U) => x1 ≊ x2) fun (x1 : S) (x2 : U) => x1 ≊ x2

Equations

• FFL.Entailment.instTransEquiv = { trans := ⋯ }

@[instance_reducible]

instance FFL.Entailment.instTransEquivWeakerThan {F : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [Entailment S F] [Entailment T F] [Entailment U F] : Trans (fun (x1 : S) (x2 : T) => x1 ≊ x2) (fun (x1 : T) (x2 : U) => x1 ⪯ x2) fun (x1 : S) (x2 : U) => x1 ⪯ x2

Equations

• FFL.Entailment.instTransEquivWeakerThan = { trans := ⋯ }

@[instance_reducible]

instance FFL.Entailment.instTransEquivWeakerThan_1 {F : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [Entailment S F] [Entailment T F] [Entailment U F] : Trans (fun (x1 : S) (x2 : T) => x1 ≊ x2) (fun (x1 : T) (x2 : U) => x1 ≊ x2) fun (x1 : S) (x2 : U) => x1 ⪯ x2

Equations

• FFL.Entailment.instTransEquivWeakerThan_1 = { trans := ⋯ }

@[instance_reducible]

instance FFL.Entailment.instTransWeakerThanEquiv {F : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [Entailment S F] [Entailment T F] [Entailment U F] : Trans (fun (x1 : S) (x2 : T) => x1 ⪯ x2) (fun (x1 : T) (x2 : U) => x1 ≊ x2) fun (x1 : S) (x2 : U) => x1 ⪯ x2

Equations

• FFL.Entailment.instTransWeakerThanEquiv = { trans := ⋯ }

@[instance_reducible]

instance FFL.Entailment.instTransEquivStrictlyWeakerThan {F : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [Entailment S F] [Entailment T F] [Entailment U F] : Trans (fun (x1 : S) (x2 : T) => x1 ≊ x2) (fun (x1 : T) (x2 : U) => x1 ⪱ x2) fun (x1 : S) (x2 : U) => x1 ⪱ x2

Equations

• FFL.Entailment.instTransEquivStrictlyWeakerThan = { trans := ⋯ }

@[instance_reducible]

instance FFL.Entailment.instTransStrictlyWeakerThanEquiv {F : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [Entailment S F] [Entailment T F] [Entailment U F] : Trans (fun (x1 : S) (x2 : T) => x1 ⪱ x2) (fun (x1 : T) (x2 : U) => x1 ≊ x2) fun (x1 : S) (x2 : U) => x1 ⪱ x2

Equations

• FFL.Entailment.instTransStrictlyWeakerThanEquiv = { trans := ⋯ }

theorem FFL.Entailment.iff_strictlyWeakerThan_weakerThan_not_equiv {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] {𝓢 : S} {𝓣 : T} : 𝓢 ⪱ 𝓣 ↔ 𝓢 ⪯ 𝓣 ∧ ¬𝓢 ≊ 𝓣

class FFL.Entailment.Incomparable {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] (𝓢 : S) (𝓣 : T) : Prop

• notWT₁ : ¬𝓢 ⪯ 𝓣
• notWT₂ : ¬𝓣 ⪯ 𝓢

theorem FFL.Entailment.Incomparable.of_unprovable {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] {𝓢 : S} {𝓣 : T} (h₁ : ∃ (φ : F), 𝓢 ⊢ φ ∧ 𝓣 ⊬ φ) (h₂ : ∃ (ψ : F), 𝓣 ⊢ ψ ∧ 𝓢 ⊬ ψ) : Incomparable 𝓢 𝓣

Consistency and inconsistency

@[simp]

theorem FFL.Entailment.provableSet_theory {F : Type u_1} {S : Type u_2} [Entailment S F] (𝓢 : S) : 𝓢 ⊢* theory 𝓢

def FFL.Entailment.Inconsistent {F : Type u_1} {S : Type u_2} [Entailment S F] (𝓢 : S) : Prop

Equations

• FFL.Entailment.Inconsistent 𝓢 = ∀ (φ : F), 𝓢 ⊢ φ

class FFL.Entailment.Consistent {F : Type u_1} {S : Type u_2} [Entailment S F] (𝓢 : S) : Prop

• not_inconsistent : ¬Inconsistent 𝓢

theorem FFL.Entailment.inconsistent_def {F : Type u_1} {S : Type u_2} [Entailment S F] {𝓢 : S} : Inconsistent 𝓢 ↔ ∀ (φ : F), 𝓢 ⊢ φ

theorem FFL.Entailment.inconsistent_iff_theory_eq {F : Type u_1} {S : Type u_2} [Entailment S F] {𝓢 : S} : Inconsistent 𝓢 ↔ theory 𝓢 = Set.univ

@[simp]

theorem FFL.Entailment.not_inconsistent_iff_consistent {F : Type u_1} {S : Type u_2} [Entailment S F] {𝓢 : S} : ¬Inconsistent 𝓢 ↔ Consistent 𝓢

theorem FFL.Entailment.Consistent.not_inc {F : Type u_1} {S : Type u_2} [Entailment S F] {𝓢 : S} : Consistent 𝓢 → ¬Inconsistent 𝓢

Alias of the reverse direction of FFL.Entailment.not_inconsistent_iff_consistent.

@[simp]

theorem FFL.Entailment.not_consistent_iff_inconsistent {F : Type u_1} {S : Type u_2} [Entailment S F] {𝓢 : S} : ¬Consistent 𝓢 ↔ Inconsistent 𝓢

theorem FFL.Entailment.Inconsistent.not_con {F : Type u_1} {S : Type u_2} [Entailment S F] {𝓢 : S} : Inconsistent 𝓢 → ¬Consistent 𝓢

Alias of the reverse direction of FFL.Entailment.not_consistent_iff_inconsistent.

theorem FFL.Entailment.consistent_iff_exists_unprovable {F : Type u_1} {S : Type u_2} [Entailment S F] {𝓢 : S} : Consistent 𝓢 ↔ ∃ (φ : F), 𝓢 ⊬ φ

theorem FFL.Entailment.Consistent.exists_unprovable {F : Type u_1} {S : Type u_2} [Entailment S F] {𝓢 : S} : Consistent 𝓢 → ∃ (φ : F), 𝓢 ⊬ φ

Alias of the forward direction of FFL.Entailment.consistent_iff_exists_unprovable.

theorem FFL.Entailment.Consistent.of_unprovable {F : Type u_1} {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} (h : 𝓢 ⊬ φ) : Consistent 𝓢

theorem FFL.Entailment.inconsistent_iff_theory_eq_univ {F : Type u_1} {S : Type u_2} [Entailment S F] {𝓢 : S} : Inconsistent 𝓢 ↔ theory 𝓢 = Set.univ

theorem FFL.Entailment.Inconsistent.theory_eq {F : Type u_1} {S : Type u_2} [Entailment S F] {𝓢 : S} : Inconsistent 𝓢 → theory 𝓢 = Set.univ

Alias of the forward direction of FFL.Entailment.inconsistent_iff_theory_eq_univ.

theorem FFL.Entailment.Inconsistent.of_ge {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] {𝓢 : S} {𝓣 : T} (h𝓢 : Inconsistent 𝓢) (h : 𝓢 ⪯ 𝓣) : Inconsistent 𝓣

theorem FFL.Entailment.Consistent.of_le {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] {𝓢 : S} {𝓣 : T} (h𝓢 : Consistent 𝓢) (h : 𝓣 ⪯ 𝓢) : Consistent 𝓣

class FFL.Entailment.DeductiveExplosion {F : Type u_1} (S : Type u_2) [Entailment S F] [LogicalNeutral F] : Type (max (max u_1 u_2) u_5)

• dexp {𝓢 : S} : 𝓢 ⊢! ⊥ → (φ : F) → 𝓢 ⊢! φ

theorem FFL.Entailment.DeductiveExplosion.dexp! {F : Type u_1} {S : Type u_2} [Entailment S F] [LogicalNeutral F] [DeductiveExplosion S] {𝓢 : S} (h : 𝓢 ⊢ ⊥) (φ : F) : 𝓢 ⊢ φ

theorem FFL.Entailment.inconsistent_iff_provable_bot {F : Type u_1} {S : Type u_2} [Entailment S F] [LogicalNeutral F] [DeductiveExplosion S] {𝓢 : S} : Inconsistent 𝓢 ↔ 𝓢 ⊢ ⊥

theorem FFL.Entailment.inconsistent_of_provable {F : Type u_1} {S : Type u_2} [Entailment S F] [LogicalNeutral F] [DeductiveExplosion S] {𝓢 : S} : 𝓢 ⊢ ⊥ → Inconsistent 𝓢

Alias of the reverse direction of FFL.Entailment.inconsistent_iff_provable_bot.

theorem FFL.Entailment.consistent_iff_unprovable_bot {F : Type u_1} {S : Type u_2} [Entailment S F] [LogicalNeutral F] [DeductiveExplosion S] {𝓢 : S} : Consistent 𝓢 ↔ 𝓢 ⊬ ⊥

@[simp]

theorem FFL.Entailment.Consistent.not_bot {F : Type u_1} {S : Type u_2} [Entailment S F] [LogicalNeutral F] [DeductiveExplosion S] {𝓢 : S} [Consistent 𝓢] : 𝓢 ⊬ ⊥

Completeness and incompleteness

class FFL.Entailment.Complete {F : Type u_1} {S : Type u_2} [Entailment S F] [Tilde F] (𝓢 : S) : Prop

𝓢 is complete if, for every formula, either it or its negation is provable by 𝓢.

• con (φ : F) : 𝓢 ⊢ φ ∨ 𝓢 ⊢ ∼φ

def FFL.Entailment.Independent {F : Type u_1} {S : Type u_2} [Entailment S F] [Tilde F] (𝓢 : S) (φ : F) : Prop

A formula φ is independent from 𝓢 if, neither it nor its negation is provable by 𝓢.

Equations

• FFL.Entailment.Independent 𝓢 φ = (𝓢 ⊬ φ ∧ 𝓢 ⊬ ∼φ)

class FFL.Entailment.Incomplete {F : Type u_1} {S : Type u_2} [Entailment S F] [Tilde F] (𝓢 : S) : Prop

A proof system is incomplete if and only if there exists a formula that is both unprovable and irrefutable.

• indep : ∃ (φ : F), Independent 𝓢 φ

theorem FFL.Entailment.complete_def {F : Type u_1} {S : Type u_2} [Entailment S F] [Tilde F] {𝓢 : S} : Complete 𝓢 ↔ ∀ (φ : F), 𝓢 ⊢ φ ∨ 𝓢 ⊢ ∼φ

theorem FFL.Entailment.incomplete_def {F : Type u_1} {S : Type u_2} [Entailment S F] [Tilde F] {𝓢 : S} : Incomplete 𝓢 ↔ ∃ (φ : F), Independent 𝓢 φ

theorem FFL.Entailment.Equiv.unprovable {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] {𝓢 : S} {𝓣 : T} (e : 𝓢 ≊ 𝓣) {φ : F} : 𝓢 ⊬ φ ↔ 𝓣 ⊬ φ

theorem FFL.Entailment.Equiv.incomplete {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] [Tilde F] {𝓢 : S} {𝓣 : T} (e : 𝓢 ≊ 𝓣) : Incomplete 𝓢 → Incomplete 𝓣

theorem FFL.Entailment.Equiv.incomplete_iff {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] [Tilde F] {𝓢 : S} {𝓣 : T} (e : 𝓢 ≊ 𝓣) : Incomplete 𝓢 ↔ Incomplete 𝓣

@[simp]

theorem FFL.Entailment.not_complete_iff_incomplete {F : Type u_1} {S : Type u_2} [Entailment S F] [Tilde F] {𝓢 : S} : ¬Complete 𝓢 ↔ Incomplete 𝓢

@[simp]

theorem FFL.Entailment.not_incomplete_iff_complete {F : Type u_1} {S : Type u_2} [Entailment S F] [Tilde F] {𝓢 : S} : ¬Incomplete 𝓢 ↔ Complete 𝓢

instance FFL.Entailment.consistent_of_incomplete {F : Type u_1} {S : Type u_2} [Entailment S F] [Tilde F] {𝓢 : S} [h : Incomplete 𝓢] : Consistent 𝓢

Axiomatized provability

class FFL.Entailment.Axiomatized {F : Type u_1} (S : Type u_2) [Entailment S F] [AdjunctiveSet F S] : Type (max (max u_1 u_2) u_5)

• prfAxm {𝓢 : S} : 𝓢 ⊢!* AdjunctiveSet.set 𝓢
• weakening {φ : F} {𝓢 𝓣 : S} : 𝓢 ⊆ 𝓣 → 𝓢 ⊢! φ → 𝓣 ⊢! φ

def FFL.Entailment.wk {F : Type u_1} {S : Type u_2} {inst✝ : Entailment S F} {inst✝¹ : AdjunctiveSet F S} [self : Axiomatized S] {φ : F} {𝓢 𝓣 : S} : 𝓢 ⊆ 𝓣 → 𝓢 ⊢! φ → 𝓣 ⊢! φ

Alias of FFL.Entailment.Axiomatized.weakening.

Equations

• @FFL.Entailment.wk = @FFL.Entailment.Axiomatized.weakening

class FFL.Entailment.StrongCut {F : Type u_1} (S : Type u_2) (T : Type u_3) [Entailment S F] [Entailment T F] [AdjunctiveSet F T] : Type (max (max (max (max u_1 u_2) u_3) u_5) u_6)

• cut {𝓢 : S} {𝓣 : T} {φ : F} : 𝓢 ⊢!* AdjunctiveSet.set 𝓣 → 𝓣 ⊢! φ → 𝓢 ⊢! φ

def FFL.Entailment.Axiomatized.byAxm {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] {φ : F} {𝓢 : S} (h : φ ∈ 𝓢) : 𝓢 ⊢! φ

Equations

• FFL.Entailment.Axiomatized.byAxm h = FFL.Entailment.Axiomatized.prfAxm ⋯

theorem FFL.Entailment.Axiomatized.by_axm {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] {φ : F} {𝓢 : S} (h : φ ∈ 𝓢) : 𝓢 ⊢ φ

@[simp]

theorem FFL.Entailment.Axiomatized.provable_refl {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] (𝓢 : S) : 𝓢 ⊢* AdjunctiveSet.set 𝓢

theorem FFL.Entailment.Axiomatized.axm_subset {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] (𝓢 : S) : AdjunctiveSet.set 𝓢 ⊆ theory 𝓢

def FFL.Entailment.Axiomatized.adjoin {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] (φ : F) (𝓢 : S) : adjoin φ 𝓢 ⊢! φ

Equations

• FFL.Entailment.Axiomatized.adjoin φ 𝓢 = FFL.Entailment.Axiomatized.prfAxm ⋯

@[simp]

theorem FFL.Entailment.Axiomatized.adjoin! {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] (φ : F) (𝓢 : S) : adjoin φ 𝓢 ⊢ φ

theorem FFL.Entailment.Axiomatized.le_of_subset {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] {𝓢 𝓣 : S} (h : 𝓢 ⊆ 𝓣) : 𝓢 ⪯ 𝓣

theorem FFL.Entailment.Axiomatized.weakening! {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] {𝓢 𝓣 : S} (h : 𝓢 ⊆ 𝓣 := by simp) {φ : F} : 𝓢 ⊢ φ → 𝓣 ⊢ φ

@[reducible, inline]

abbrev FFL.Entailment.Axiomatized.weakerThanOfSubset {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] {𝓢 𝓣 : S} (h : 𝓢 ⊆ 𝓣) : 𝓢 ⪯ 𝓣

Equations

• ⋯ = ⋯

def FFL.Entailment.Axiomatized.toAdjoin {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] {ψ φ : F} {𝓢 : S} : 𝓢 ⊢! ψ → adjoin φ 𝓢 ⊢! ψ

Equations

• FFL.Entailment.Axiomatized.toAdjoin b = FFL.Entailment.wk ⋯ b

theorem FFL.Entailment.Axiomatized.to_adjoin {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] {ψ φ : F} {𝓢 : S} : 𝓢 ⊢ ψ → adjoin φ 𝓢 ⊢ ψ

def FFL.Entailment.byAxm {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] {φ : F} {𝓢 : S} (h : φ ∈ 𝓢) : 𝓢 ⊢! φ

Alias of FFL.Entailment.Axiomatized.byAxm.

Equations

• @FFL.Entailment.byAxm = @FFL.Entailment.Axiomatized.byAxm

theorem FFL.Entailment.by_axm {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] {φ : F} {𝓢 : S} (h : φ ∈ 𝓢) : 𝓢 ⊢ φ

Alias of FFL.Entailment.Axiomatized.by_axm.

theorem FFL.Entailment.wk! {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] {𝓢 𝓣 : S} (h : 𝓢 ⊆ 𝓣 := by simp) {φ : F} : 𝓢 ⊢ φ → 𝓣 ⊢ φ

Alias of FFL.Entailment.Axiomatized.weakening!.

def FFL.Entailment.FiniteAxiomatizable {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] (𝓢 : S) : Prop

Equations

• FFL.Entailment.FiniteAxiomatizable 𝓢 = ∃ (𝓕 : S), AdjunctiveSet.Finite 𝓕 ∧ 𝓕 ≊ 𝓢

theorem FFL.Entailment.Consistent.of_subset {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] {𝓢 𝓣 : S} (h𝓢 : Consistent 𝓢) (h : 𝓣 ⊆ 𝓢) : Consistent 𝓣

theorem FFL.Entailment.Inconsistent.of_supset {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] {𝓢 𝓣 : S} (h𝓢 : Inconsistent 𝓢) (h : 𝓢 ⊆ 𝓣) : Inconsistent 𝓣

theorem FFL.Entailment.StrongCut.cut! {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] [AdjunctiveSet F T] [StrongCut S T] {𝓢 : S} {𝓣 : T} {φ : F} (H : 𝓢 ⊢* AdjunctiveSet.set 𝓣) (hp : 𝓣 ⊢ φ) : 𝓢 ⊢ φ

@[reducible, inline]

noncomputable abbrev FFL.Entailment.WeakerThan.ofAxm! {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [StrongCut S S] {𝓢₁ 𝓢₂ : S} (B : 𝓢₂ ⊢* AdjunctiveSet.set 𝓢₁) : 𝓢₁ ⪯ 𝓢₂

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev FFL.Entailment.WeakerThan.ofSubset {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] {𝓢 𝓣 : S} (h : 𝓢 ⊆ 𝓣) : 𝓢 ⪯ 𝓣

Equations

• ⋯ = ⋯

Compactness

class FFL.Entailment.Compact {F : Type u_1} (S : Type u_2) [Entailment S F] [AdjunctiveSet F S] : Type (max (max u_1 u_2) u_5)

• core {𝓢 : S} {φ : F} : 𝓢 ⊢! φ → S
• corePrf {𝓢 : S} {φ : F} (b : 𝓢 ⊢! φ) : core b ⊢! φ
• core_subset {𝓢 : S} {φ : F} (b : 𝓢 ⊢! φ) : core b ⊆ 𝓢
• core_finite {𝓢 : S} {φ : F} (b : 𝓢 ⊢! φ) : AdjunctiveSet.Finite (core b)

theorem FFL.Entailment.Compact.finite_provable {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Compact S] {φ : F} {𝓢 : S} (h : 𝓢 ⊢ φ) : ∃ 𝓕 ⊆ 𝓢, AdjunctiveSet.Finite 𝓕 ∧ 𝓕 ⊢ φ

theorem FFL.Entailment.inconsistent_compact {S : Type u_1} {F : Type u_2} [LogicalNeutral F] [Entailment S F] [DeductiveExplosion S] [AdjunctiveSet F S] [Axiomatized S] [Compact S] {𝓢 : S} : Inconsistent 𝓢 ↔ ∃ 𝓕 ⊆ 𝓢, AdjunctiveSet.Finite 𝓕 ∧ Inconsistent 𝓕

theorem FFL.Entailment.consistent_compact {S : Type u_1} {F : Type u_2} [LogicalNeutral F] [Entailment S F] [DeductiveExplosion S] [AdjunctiveSet F S] [Axiomatized S] [Compact S] {𝓢 : S} : Consistent 𝓢 ↔ ∀ 𝓕 ⊆ 𝓢, AdjunctiveSet.Finite 𝓕 → Consistent 𝓕

Deduction theorem

class FFL.Entailment.Deduction (S : Type u_1) {F : Type u_2} [LogicalConnective F] [Entailment S F] [Adjoin F S] : Type (max (max u_1 u_2) u_3)

• ofInsert {φ ψ : F} {𝓢 : S} : adjoin φ 𝓢 ⊢! ψ → 𝓢 ⊢! φ 🡒 ψ
• inv {φ ψ : F} {𝓢 : S} : 𝓢 ⊢! φ 🡒 ψ → adjoin φ 𝓢 ⊢! ψ

def FFL.Entailment.deduction {S : Type u_1} {F : Type u_2} {inst✝ : LogicalConnective F} {inst✝¹ : Entailment S F} {inst✝² : Adjoin F S} [self : Deduction S] {φ ψ : F} {𝓢 : S} : adjoin φ 𝓢 ⊢! ψ → 𝓢 ⊢! φ 🡒 ψ

Alias of FFL.Entailment.Deduction.ofInsert.

Equations

• @FFL.Entailment.deduction = @FFL.Entailment.Deduction.ofInsert

theorem FFL.Entailment.Deduction.of_insert! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] [Adjoin F S] [Deduction S] {𝓢 : S} {φ ψ : F} (h : adjoin φ 𝓢 ⊢ ψ) : 𝓢 ⊢ φ 🡒 ψ

theorem FFL.Entailment.deduction! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] [Adjoin F S] [Deduction S] {𝓢 : S} {φ ψ : F} (h : adjoin φ 𝓢 ⊢ ψ) : 𝓢 ⊢ φ 🡒 ψ

Alias of FFL.Entailment.Deduction.of_insert!.

theorem FFL.Entailment.Deduction.inv! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] [Adjoin F S] [Deduction S] {𝓢 : S} {φ ψ : F} (h : 𝓢 ⊢ φ 🡒 ψ) : adjoin φ 𝓢 ⊢ ψ

theorem FFL.Entailment.deduction_iff {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] [Adjoin F S] [Deduction S] {𝓢 : S} {φ ψ : F} : adjoin φ 𝓢 ⊢ ψ ↔ 𝓢 ⊢ φ 🡒 ψ

Soundness and Completeness

class FFL.Sound {S : Type u_1} {F : Type u_2} [Entailment S F] {M : Type u_3} [Semantics M F] (𝓢 : S) (𝓜 : M) : Prop

• sound {φ : F} : 𝓢 ⊢ φ → 𝓜 ⊧ φ

class FFL.Complete {S : Type u_1} {F : Type u_2} [Entailment S F] {M : Type u_3} [Semantics M F] (𝓢 : S) (𝓜 : M) : Prop

• complete {φ : F} : 𝓜 ⊧ φ → 𝓢 ⊢ φ

theorem FFL.Sound.not_provable_of_countermodel {S : Type u_1} {F : Type u_2} [Entailment S F] {M : Type u_3} [Semantics M F] {𝓢 : S} {𝓜 : M} [Sound 𝓢 𝓜] {φ : F} (hp : 𝓜 ⊭ φ) : 𝓢 ⊬ φ

theorem FFL.Sound.consistent_of_meaningful {S : Type u_1} {F : Type u_2} [Entailment S F] {M : Type u_3} [Semantics M F] {𝓢 : S} {𝓜 : M} [Sound 𝓢 𝓜] : Semantics.Meaningful 𝓜 → Entailment.Consistent 𝓢

theorem FFL.Sound.consistent_of_model {S : Type u_1} {F : Type u_2} [Entailment S F] {M : Type u_3} [Semantics M F] {𝓢 : S} [LogicalNeutral F] [Semantics.Bot M] (𝓜 : M) [Sound 𝓢 𝓜] : Entailment.Consistent 𝓢

theorem FFL.Sound.modelsSet_of_prfSet {S : Type u_1} {F : Type u_2} [Entailment S F] {M : Type u_3} [Semantics M F] {𝓢 : S} {𝓜 : M} [Sound 𝓢 𝓜] {T : Set F} (b : 𝓢 ⊢* T) : 𝓜 ⊧* T

theorem FFL.Sound.consequence_of_provable {S : Type u_1} {F : Type u_2} [Entailment S F] {M : Type u_3} [Semantics M F] {𝓢 : S} {T : Set F} [Sound 𝓢 (Semantics.models M T)] {φ : F} : 𝓢 ⊢ φ → T ⊨[M] φ

theorem FFL.Sound.consistent_of_satisfiable {S : Type u_1} {F : Type u_2} [Entailment S F] {M : Type u_3} [Semantics M F] {𝓢 : S} {T : Set F} [Sound 𝓢 (Semantics.models M T)] [∀ (𝓜 : M), Semantics.Meaningful 𝓜] : Semantics.Satisfiable M T → Entailment.Consistent 𝓢

theorem FFL.Complete.exists_countermodel_of_not_provable {S : Type u_1} {F : Type u_2} [Entailment S F] {M : Type u_3} [Semantics M F] {𝓢 : S} {𝓜 : M} [Complete 𝓢 𝓜] {φ : F} (h : 𝓢 ⊬ φ) : 𝓜 ⊭ φ

theorem FFL.Complete.meaningful_of_consistent {S : Type u_1} {F : Type u_2} [Entailment S F] {M : Type u_3} [Semantics M F] {𝓢 : S} {𝓜 : M} [Complete 𝓢 𝓜] : Entailment.Consistent 𝓢 → Semantics.Meaningful 𝓜

theorem FFL.Complete.provable_of_consequence {S : Type u_1} {F : Type u_2} [Entailment S F] {M : Type u_3} [Semantics M F] {𝓢 : S} {s : Set F} [Complete 𝓢 (Semantics.models M s)] {φ : F} : s ⊨[M] φ → 𝓢 ⊢ φ

theorem FFL.Complete.provable_iff_consequence {S : Type u_1} {F : Type u_2} [Entailment S F] {M : Type u_3} [Semantics M F] {𝓢 : S} {s : Set F} [Complete 𝓢 (Semantics.models M s)] [Sound 𝓢 (Semantics.models M s)] {φ : F} : s ⊨[M] φ ↔ 𝓢 ⊢ φ

theorem FFL.Complete.satisfiable_of_consistent {S : Type u_1} {F : Type u_2} [Entailment S F] {M : Type u_3} [Semantics M F] {𝓢 : S} {s : Set F} [Complete 𝓢 (Semantics.models M s)] [∀ (𝓜 : M), Semantics.Meaningful 𝓜] : Entailment.Consistent 𝓢 → Semantics.Satisfiable M s

theorem FFL.Complete.inconsistent_of_unsatisfiable {S : Type u_1} {F : Type u_2} [Entailment S F] {M : Type u_3} [Semantics M F] {𝓢 : S} {s : Set F} [Complete 𝓢 (Semantics.models M s)] [∀ (𝓜 : M), Semantics.Meaningful 𝓜] : ¬Semantics.Satisfiable M s → Entailment.Inconsistent 𝓢

theorem FFL.Complete.consistent_iff_satisfiable {S : Type u_1} {F : Type u_2} [Entailment S F] {M : Type u_3} [Semantics M F] {𝓢 : S} {s : Set F} [Complete 𝓢 (Semantics.models M s)] [∀ (𝓜 : M), Semantics.Meaningful 𝓜] [Sound 𝓢 (Semantics.models M s)] : Entailment.Consistent 𝓢 ↔ Semantics.Satisfiable M s

theorem FFL.Complete.weakerthan_of_models {S : Type u_1} {F : Type u_2} [Entailment S F] {M : Type u_3} [Semantics M F] {𝓢 : S} {s : Set F} [Complete 𝓢 (Semantics.models M s)] {𝓣 : S} {t : Set F} [Sound 𝓣 (Semantics.models M t)] (H : ∀ (𝓜 : M), 𝓜 ⊧* s → 𝓜 ⊧* t) : 𝓣 ⪯ 𝓢

structure FFL.Entailment.Pullback (S : Type u_1) {F : Type u_2} {G : Sort u_3} (f : G → F) : Type u_1

• forget : S

@[reducible, inline]

abbrev FFL.Entailment.pullback {S : Type u_1} {F : Type u_2} {G : Sort u_3} (𝓢 : S) (f : G → F) : Pullback S f

Equations

• FFL.Entailment.pullback 𝓢 f = { forget := 𝓢 }

@[instance_reducible]

instance FFL.Entailment.instPullback {S : Type u_1} {F : Type u_2} [Entailment S F] {G : Type u_4} (f : G → F) : Entailment (Pullback S f) G

Equations

• FFL.Entailment.instPullback f = { Prf := fun (𝓢 : FFL.Entailment.Pullback S f) (φ : G) => 𝓢.forget ⊢! f φ }

@[simp]

theorem FFL.Entailment.Pullback.pullback_forget {G : Sort u_3} {S : Type u_1} {F : Type u_2} {f : G → F} (𝓢 : S) : (pullback 𝓢 f).forget = 𝓢

@[simp]

theorem FFL.Entailment.Pullback.provable_iff {G : Type u_3} {S : Type u_1} {F : Type u_2} [Entailment S F] {f : G → F} {𝓢 : S} {φ : G} : pullback 𝓢 f ⊢ φ ↔ 𝓢 ⊢ f φ

@[simp]

theorem FFL.Entailment.Pullback.unprovable_iff {G : Type u_3} {S : Type u_1} {F : Type u_2} [Entailment S F] {f : G → F} {𝓢 : S} {φ : G} : pullback 𝓢 f ⊬ φ ↔ 𝓢 ⊬ f φ

@[simp]

theorem FFL.Entailment.Pullback.provableSet_iff {G : Type u_3} {S : Type u_1} {F : Type u_2} [Entailment S F] {f : G → F} {𝓢 : S} {s : Set G} : pullback 𝓢 f ⊢* s ↔ 𝓢 ⊢* f '' s

@[simp]

theorem FFL.Entailment.Pullback.theory_eq {G : Type u_3} {S : Type u_1} {F : Type u_2} [Entailment S F] {f : G → F} (𝓢 : S) : theory (pullback 𝓢 f) = f ⁻¹' theory 𝓢

theorem FFL.Entailment.Pullback.weakerThan {G : Type u_4} {S : Type u_1} {F : Type u_2} [Entailment S F] {f : G → F} (𝓢 𝓣 : S) (h : 𝓢 ⪯ 𝓣) : pullback 𝓢 f ⪯ pullback 𝓣 f

theorem FFL.Entailment.Pullback.inconsistent {G : Type u_4} {S : Type u_1} {F : Type u_2} [Entailment S F] {f : G → F} {𝓢 : S} : Inconsistent 𝓢 → Inconsistent (pullback 𝓢 f)

theorem FFL.Entailment.Pullback.consistent {G : Type u_3} {S : Type u_1} {F : Type u_2} [Entailment S F] {f : G → F} {𝓢 : S} : Consistent (pullback 𝓢 f) → Consistent 𝓢