Supporting results for pointwise provable equality.

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 PointwiseComposition.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

  The Prf construction in FFL.Entailment.

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

The «term ⊢! » construction in FFL.

Equations

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

def PointwiseComposition.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 PointwiseComposition.FFL.Entailment.Unprovable {F : Type u_1} {S : Type u_2} [Entailment S F] (𝓢 : S) (φ : F) : Prop

Abbreviation for unprovability.

Equations

• (𝓢 ⊬ φ) = ¬𝓢 ⊢ φ

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

The «term ⊢ » construction in FFL.Entailment.

Equations

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

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

The «term ⊬ » construction in FFL.Entailment.

Equations

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

def PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.Entailment.«term_⊢!*_» : Lean.TrailingParserDescr

The «term ⊢!* » construction in FFL.Entailment.

Equations

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

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

The «term ⊢* » construction in FFL.Entailment.

Equations

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

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

Set of all provable formulae.

Equations

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

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

The cast construction in FFL.Entailment.

Equations

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

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

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

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

The get construction in FFL.Entailment.Provable.

Equations

• h.get = Classical.choice h

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

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

The get construction in FFL.Entailment.ProvableSet.

Equations

• h.get = Classical.choice ⋯

class PointwiseComposition.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 PointwiseComposition.FFL.Entailment.«term_≼_» : Lean.TrailingParserDescr

The «term ≼ » construction in FFL.Entailment.

Equations

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

class PointwiseComposition.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 PointwiseComposition.FFL.Entailment.«term_≺_» : Lean.TrailingParserDescr

The «term ≺ » construction in FFL.Entailment.

Equations

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

class PointwiseComposition.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 PointwiseComposition.FFL.Entailment.«term_≊_» : Lean.TrailingParserDescr

The «term ≊ » construction in FFL.Entailment.

Equations

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

Provability strength

@[simp]

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

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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

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

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.Entailment.instWeakerThanOfStrictlyWeakerThan {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] {𝓢 : S} {𝓣 : T} [𝓢 ≺ 𝓣] : 𝓢 ≼ 𝓣

theorem PointwiseComposition.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 PointwiseComposition.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

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

@[instance_reducible]

instance PointwiseComposition.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

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

@[instance_reducible]

instance PointwiseComposition.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

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

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.Entailment.Equiv.refl {F : Type u_1} {S : Type u_2} [Entailment S F] (𝓢 : S) : 𝓢 ≊ 𝓢

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.Entailment.Equiv.antisymm_iff.

theorem PointwiseComposition.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 PointwiseComposition.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

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

@[instance_reducible]

instance PointwiseComposition.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

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

@[instance_reducible]

instance PointwiseComposition.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

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

@[instance_reducible]

instance PointwiseComposition.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

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

@[instance_reducible]

instance PointwiseComposition.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

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

@[instance_reducible]

instance PointwiseComposition.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

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

theorem PointwiseComposition.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 PointwiseComposition.FFL.Entailment.Incomparable {F : Type u_1} {S : Type u_2} {T : Type u_3} [Entailment S F] [Entailment T F] (𝓢 : S) (𝓣 : T) : Prop

Data and laws for Incomparable in FFL.Entailment.

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

theorem PointwiseComposition.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 PointwiseComposition.FFL.Entailment.provableSet_theory {F : Type u_1} {S : Type u_2} [Entailment S F] (𝓢 : S) : 𝓢 ⊢* theory 𝓢

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

The Inconsistent construction in FFL.Entailment.

Equations

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

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

Data and laws for Consistent in FFL.Entailment.

• not_inconsistent : ¬Inconsistent 𝓢

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

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

@[simp]

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

theorem PointwiseComposition.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 PointwiseComposition.FFL.Entailment.not_inconsistent_iff_consistent.

@[simp]

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

theorem PointwiseComposition.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 PointwiseComposition.FFL.Entailment.not_consistent_iff_inconsistent.

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

theorem PointwiseComposition.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 PointwiseComposition.FFL.Entailment.consistent_iff_exists_unprovable.

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

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

theorem PointwiseComposition.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 PointwiseComposition.FFL.Entailment.inconsistent_iff_theory_eq_univ.

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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)

Data and laws for Deductive Explosion in FFL.Entailment.

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

  The dexp construction in FFL.Entailment.DeductiveExplosion.

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

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

theorem PointwiseComposition.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 PointwiseComposition.FFL.Entailment.inconsistent_iff_provable_bot.

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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

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

class PointwiseComposition.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 PointwiseComposition.FFL.Entailment.complete_def {F : Type u_1} {S : Type u_2} [Entailment S F] [Tilde F] {𝓢 : S} : Complete 𝓢 ↔ ∀ (φ : F), 𝓢 ⊢ φ ∨ 𝓢 ⊢ ∼φ

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

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.Entailment.not_complete_iff_incomplete {F : Type u_1} {S : Type u_2} [Entailment S F] [Tilde F] {𝓢 : S} : ¬Complete 𝓢 ↔ Incomplete 𝓢

@[simp]

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

instance PointwiseComposition.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 PointwiseComposition.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)

Data and laws for Axiomatized in FFL.Entailment.

• prfAxm {𝓢 : S} : 𝓢 ⊢!* AdjunctiveSet.set 𝓢

  The prf Axm construction in FFL.Entailment.Axiomatized.

• weakening {φ : F} {𝓢 𝓣 : S} : 𝓢 ⊆ 𝓣 → 𝓢 ⊢! φ → 𝓣 ⊢! φ

  The weakening construction in FFL.Entailment.Axiomatized.

def PointwiseComposition.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 PointwiseComposition.FFL.Entailment.Axiomatized.weakening.

---

The weakening construction in FFL.Entailment.Axiomatized.

Equations

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

class PointwiseComposition.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)

Data and laws for Strong Cut in FFL.Entailment.

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

  The cut construction in FFL.Entailment.StrongCut.

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

The by Axm construction in FFL.Entailment.Axiomatized.

Equations

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

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.Entailment.Axiomatized.adjoin {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] (φ : F) (𝓢 : S) : adjoin φ 𝓢 ⊢! φ

The adjoin construction in FFL.Entailment.Axiomatized.

Equations

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

@[simp]

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

theorem PointwiseComposition.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 PointwiseComposition.FFL.Entailment.Axiomatized.weakeningProof {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] {𝓢 𝓣 : S} (h : 𝓢 ⊆ 𝓣 := by simp) {φ : F} : 𝓢 ⊢ φ → 𝓣 ⊢ φ

@[reducible, inline]

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

The weaker Than Of Subset construction in FFL.Entailment.Axiomatized.

Equations

• ⋯ = ⋯

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

The to Adjoin construction in FFL.Entailment.Axiomatized.

Equations

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

theorem PointwiseComposition.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 PointwiseComposition.FFL.Entailment.byAxm {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [Axiomatized S] {φ : F} {𝓢 : S} (h : φ ∈ 𝓢) : 𝓢 ⊢! φ

Alias of PointwiseComposition.FFL.Entailment.Axiomatized.byAxm.

---

The by Axm construction in FFL.Entailment.Axiomatized.

Equations

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

theorem PointwiseComposition.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 PointwiseComposition.FFL.Entailment.Axiomatized.by_axm.

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

Alias of PointwiseComposition.FFL.Entailment.Axiomatized.weakeningProof.

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

The Finite Axiomatizable construction in FFL.Entailment.

Equations

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

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.Entailment.StrongCut.cutProof {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 PointwiseComposition.FFL.Entailment.WeakerThan.ofAxmProof {F : Type u_1} {S : Type u_2} [Entailment S F] [AdjunctiveSet F S] [StrongCut S S] {𝓢₁ 𝓢₂ : S} (B : 𝓢₂ ⊢* AdjunctiveSet.set 𝓢₁) : 𝓢₁ ≼ 𝓢₂

The of Axm! construction in FFL.Entailment.WeakerThan.

Equations

• ⋯ = ⋯

@[reducible, inline]

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

The of Subset construction in FFL.Entailment.WeakerThan.

Equations

• ⋯ = ⋯

Compactness

class PointwiseComposition.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)

Data and laws for Compact in FFL.Entailment.

• core {𝓢 : S} {φ : F} : 𝓢 ⊢! φ → S

  The core construction in FFL.Entailment.Compact.

• corePrf {𝓢 : S} {φ : F} (b : 𝓢 ⊢! φ) : core b ⊢! φ

  The core Prf construction in FFL.Entailment.Compact.

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

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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)

Data and laws for Deduction in FFL.Entailment.

• ofInsert {φ ψ : F} {𝓢 : S} : adjoin φ 𝓢 ⊢! ψ → 𝓢 ⊢! φ ⇒ₗ ψ

  The of Insert construction in FFL.Entailment.Deduction.

• inv {φ ψ : F} {𝓢 : S} : 𝓢 ⊢! φ ⇒ₗ ψ → adjoin φ 𝓢 ⊢! ψ

  The inv construction in FFL.Entailment.Deduction.

def PointwiseComposition.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 PointwiseComposition.FFL.Entailment.Deduction.ofInsert.

---

The of Insert construction in FFL.Entailment.Deduction.

Equations

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

theorem PointwiseComposition.FFL.Entailment.Deduction.of_insertProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] [Adjoin F S] [Deduction S] {𝓢 : S} {φ ψ : F} (h : adjoin φ 𝓢 ⊢ ψ) : 𝓢 ⊢ φ ⇒ₗ ψ

theorem PointwiseComposition.FFL.Entailment.deductionProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] [Adjoin F S] [Deduction S] {𝓢 : S} {φ ψ : F} (h : adjoin φ 𝓢 ⊢ ψ) : 𝓢 ⊢ φ ⇒ₗ ψ

Alias of PointwiseComposition.FFL.Entailment.Deduction.of_insertProof.

theorem PointwiseComposition.FFL.Entailment.Deduction.invProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] [Adjoin F S] [Deduction S] {𝓢 : S} {φ ψ : F} (h : 𝓢 ⊢ φ ⇒ₗ ψ) : adjoin φ 𝓢 ⊢ ψ

theorem PointwiseComposition.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 PointwiseComposition.FFL.Sound {S : Type u_1} {F : Type u_2} [Entailment S F] {M : Type u_3} [Semantics M F] (𝓢 : S) (𝓜 : M) : Prop

Data and laws for Sound in FFL.

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

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

Data and laws for Complete in FFL.

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

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.Entailment.Pullback (S : Type u_1) {F : Type u_2} {G : Sort u_3} (f : G → F) : Type u_1

Data and laws for Pullback in FFL.Entailment.

• forget : S

  The forget construction in FFL.Entailment.Pullback.

@[reducible, inline]

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

The pullback construction in FFL.Entailment.

Equations

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

@[instance_reducible]

instance PointwiseComposition.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

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

@[simp]

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 𝓢