Supporting results for pointwise provable equality.

Alternative definition of proof

inductive PointwiseComposition.FFL.FirstOrder.LK2.Derivation {L : Language} [L.DecidableEq] (T : Theory L) : Finset (Proposition L) → Type u_1

Data and laws for Derivation in FFL.FirstOrder.LK2.

• closed {L : Language} [L.DecidableEq] {T : Theory L} (Γ : Finset (Proposition L)) (φ : Proposition L) : φ ∈ Γ → ∼φ ∈ Γ → Derivation T Γ
• axm {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} (φ : Sentence L) : φ ∈ T → Rewriting.emb φ ∈ Γ → Derivation T Γ
• verum {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} : ⊤ ∈ Γ → Derivation T Γ
• and {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} {φ ψ : Proposition L} : φ ⋏ ψ ∈ Γ → Derivation T (insert φ Γ) → Derivation T (insert ψ Γ) → Derivation T Γ
• or {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} {φ ψ : Proposition L} : φ ⋎ ψ ∈ Γ → Derivation T (insert φ (insert ψ Γ)) → Derivation T Γ
• all {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} {φ : Semiproposition L 1} : ∀¹ φ ∈ Γ → Derivation T (insert (Rewriting.free φ) (Finset.image (⇑Rewriting.shift) Γ)) → Derivation T Γ
• exs {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} {φ : Semiproposition L 1} : ∃¹ φ ∈ Γ → (t : SyntacticTerm L) → Derivation T (insert (φ/[t]) Γ) → Derivation T Γ
• wk {L : Language} [L.DecidableEq] {T : Theory L} {Δ Γ : Finset (Proposition L)} : Derivation T Δ → Δ ⊆ Γ → Derivation T Γ
• shift {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} : Derivation T Γ → Derivation T (Finset.image (⇑Rewriting.shift) Γ)
• cut {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} {φ : Proposition L} : Derivation T (insert φ Γ) → Derivation T (insert (∼φ) Γ) → Derivation T Γ

def PointwiseComposition.FFL.FirstOrder.«term_⟹₂_» : Lean.TrailingParserDescr

The «term ⟹₂ » construction in FFL.FirstOrder.

Equations

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

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.LK2.Derivable {L : Language} [L.DecidableEq] (T : Theory L) (Γ : Finset (Proposition L)) : Prop

The Derivable construction in FFL.FirstOrder.LK2.

Equations

• PointwiseComposition.FFL.FirstOrder.LK2.Derivable T Γ = Nonempty (PointwiseComposition.FFL.FirstOrder.LK2.Derivation T Γ)

def PointwiseComposition.FFL.FirstOrder.«term_⟹₂!_» : Lean.TrailingParserDescr

The «term ⟹₂! » construction in FFL.FirstOrder.

Equations

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

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Theory.Proof2 {L : Language} [L.DecidableEq] (T : Theory L) (φ : Proposition L) : Type u_1

The Proof2 construction in FFL.FirstOrder.Theory.

Equations

• T.Proof2 φ = PointwiseComposition.FFL.FirstOrder.LK2.Derivation T {φ}

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

The «term ⊢₂! » construction in FFL.FirstOrder.

Equations

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

theorem PointwiseComposition.FFL.FirstOrder.shifts_toFinset_eq_image_shift {L : Language} [L.DecidableEq] (Γ : LK.Sequent L) : (Rewriting.shifts Γ).toFinset = Finset.image (⇑Rewriting.shift) (Multiset.toFinset Γ)

def PointwiseComposition.FFL.FirstOrder.LK.Derivation.toDerivation2 {L : Language} [L.DecidableEq] (T : Theory L) {Γ : Sequent L} : ⊢ᴸᴷ¹ Γ → LK2.Derivation T (Multiset.toFinset Γ)

The to Derivation2 construction in FFL.FirstOrder.LK.Derivation.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.FirstOrder.LK.Derivation.toDerivation2 T PointwiseComposition.FFL.FirstOrder.LK.Derivation.verum = PointwiseComposition.FFL.FirstOrder.LK2.Derivation.verum ⋯
• PointwiseComposition.FFL.FirstOrder.LK.Derivation.toDerivation2 T d.contraction = (PointwiseComposition.FFL.FirstOrder.LK.Derivation.toDerivation2 T d).wk ⋯
• PointwiseComposition.FFL.FirstOrder.LK.Derivation.toDerivation2 T d.weakening = (PointwiseComposition.FFL.FirstOrder.LK.Derivation.toDerivation2 T d).wk ⋯

structure PointwiseComposition.FFL.FirstOrder.LK2.Derivation.ProofData {L : Language} (T : Theory L) (Γ : Finset (Proposition L)) : Type u_1

Data and laws for Proof Data in FFL.FirstOrder.LK2.Derivation.

• axioms : Multiset (Sentence L)

  The axioms construction in FFL.FirstOrder.LK2.Derivation.ProofData.

• axioms_mem (ψ : Sentence L) : ψ ∈ self.axioms → ψ ∈ T
• derivation : ⊢ᴸᴷ¹ Γ.val + ∼LK.Sequent.embed self.axioms

  The derivation construction in FFL.FirstOrder.LK2.Derivation.ProofData.

noncomputable def PointwiseComposition.FFL.FirstOrder.LK2.Derivation.cast {L : Language} [L.DecidableEq] {T : Theory L} {Γ Δ : Finset (Proposition L)} (d : Derivation T Γ) (h : Γ = Δ := by simp) : Derivation T Δ

The cast construction in FFL.FirstOrder.LK2.Derivation.

Equations

• d.cast h = h ▸ d

theorem PointwiseComposition.FFL.FirstOrder.LK2.Derivation.shifts_tilde_embed {L : Language} (A : Multiset (Sentence L)) : Rewriting.shifts (∼LK.Sequent.embed A) = ∼LK.Sequent.embed A

@[reducible]

noncomputable def PointwiseComposition.FFL.FirstOrder.LK2.Derivation.cutManyProof {L : Language} [L.DecidableEq] {T : Theory L} {φ : Proposition L} (A : Multiset (Sentence L)) (hA : ∀ ψ ∈ A, ψ ∈ T) (d : Derivation T (insert φ (Multiset.toFinset (∼LK.Sequent.embed A)))) : Derivation T {φ}

The cut Many Proof construction in FFL.FirstOrder.LK2.Derivation.

Equations

• PointwiseComposition.FFL.FirstOrder.LK2.Derivation.cutManyProof A hA d = PointwiseComposition.FFL.FirstOrder.LK2.Derivation.cutManyProof.go A.toList ⋯ (d.cast ⋯)

noncomputable def PointwiseComposition.FFL.FirstOrder.LK2.Derivation.cutManyProof.go {L : Language} [L.DecidableEq] {T : Theory L} {φ : Proposition L} (l : List (Sentence L)) : (∀ ψ ∈ l, ψ ∈ T) → Derivation T (insert φ (Multiset.toFinset (∼LK.Sequent.embed ↑l))) → Derivation T {φ}

The go construction in FFL.FirstOrder.LK2.Derivation.cutManyProof.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.FirstOrder.LK2.Derivation.cutManyProof.go [] x_3 d = d.cast ⋯

noncomputable def PointwiseComposition.FFL.FirstOrder.LK2.Derivation.toProofData {L : Language} [L.DecidableEq] {T : Theory L} {Γ : Finset (Proposition L)} : Derivation T Γ → ProofData T Γ

The to Proof Data construction in FFL.FirstOrder.LK2.Derivation.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Theory.Proof.toProof2 {L : Language} [L.DecidableEq] {T : Theory L} {φ : Sentence L} (b : T ⊢! φ) : T.Proof2 (Rewriting.emb φ)

The to Proof2 construction in FFL.FirstOrder.Theory.Proof.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Theory.Proof2.toProof {L : Language} [L.DecidableEq] {T : Theory L} {φ : Sentence L} (d : T.Proof2 (Rewriting.emb φ)) : T ⊢! φ

The to Proof construction in FFL.FirstOrder.Theory.Proof2.

Equations

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

theorem PointwiseComposition.FFL.FirstOrder.provable_iff_derivable2 {L : Language} [L.DecidableEq] {T : Theory L} {φ : Sentence L} : T ⊢ φ ↔ Nonempty (T.Proof2 (Rewriting.emb φ))