Flypitch.FOL.Proof defines the natural-deduction proof system for the first-order language developed in this repository, together with the structural operations on derivations that are used throughout the completeness proof.

inductive Flypitch.fol.prf {L : Language} : Set (formula L) → formula L → Type u

Natural-deduction derivations from a set of assumptions.

• axm {L : Language} {Γ : Set (formula L)} {A : formula L} : A ∈ Γ → Γ ⊢ A
• impI {L : Language} {Γ : Set (formula L)} {A B : formula L} : insert A Γ ⊢ B → Γ ⊢ A ⟹ B
• impE {L : Language} {Γ : Set (formula L)} (A : preformula L 0) {B : preformula L 0} : Γ ⊢ A ⟹ B → Γ ⊢ A → Γ ⊢ B
• falsumE {L : Language} {Γ : Set (formula L)} {A : formula L} : insert (∼A) Γ ⊢ ⊥ → Γ ⊢ A
• allI {L : Language} {Γ : Set (preformula L 0)} {A : formula L} : lift_formula1 '' Γ ⊢ A → Γ ⊢ ∀' A
• allE₂ {L : Language} {Γ : Set (formula L)} (A : formula L) (t : term L) : Γ ⊢ ∀' A → Γ ⊢ subst_formula A t 0
• ref {L : Language} (Γ : Set (formula L)) (t : term L) : Γ ⊢ t ≃ t
• subst₂ {L : Language} {Γ : Set (formula L)} (s t : term L) (f : formula L) : Γ ⊢ s ≃ t → Γ ⊢ subst_formula f s 0 → Γ ⊢ subst_formula f t 0

def Flypitch.fol.«term_⊢_» : Lean.TrailingParserDescr

Equations

• Flypitch.fol.«term_⊢_» = Lean.ParserDescr.trailingNode `Flypitch.fol.«term_⊢_» 51 52 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢ ") (Lean.ParserDescr.cat `term 52))

def Flypitch.fol.provable {L : Language} (T : Set (formula L)) (f : formula L) : Prop

Propositional truncation of derivability.

Equations

• T ⊢' f = Nonempty (T ⊢ f)

def Flypitch.fol.«term_⊢'_» : Lean.TrailingParserDescr

Equations

• Flypitch.fol.«term_⊢'_» = Lean.ParserDescr.trailingNode `Flypitch.fol.«term_⊢'_» 51 52 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢' ") (Lean.ParserDescr.cat `term 52))

noncomputable def Flypitch.fol.allE {L : Language} {Γ : Set (formula L)} (A : formula L) (t : term L) {B : formula L} (h₁ : Γ ⊢ ∀' A) (h₂ : subst_formula A t 0 = B) : Γ ⊢ B

Eliminate a universal quantifier and rewrite to a chosen target formula.

Equations

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

noncomputable def Flypitch.fol.subst {L : Language} {Γ : Set (formula L)} {s t : term L} (f₁ : formula L) {f₂ : formula L} (h₁ : Γ ⊢ s ≃ t) (h₂ : Γ ⊢ subst_formula f₁ s 0) (h₃ : subst_formula f₁ t 0 = f₂) : Γ ⊢ f₂

Equality substitution followed by a rewrite to a chosen target formula.

Equations

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

noncomputable def Flypitch.fol.axm1 {L : Language} {Γ : Set (formula L)} {A : formula L} : insert A Γ ⊢ A

The most recently inserted assumption is available immediately.

Equations

• Flypitch.fol.axm1 = Flypitch.fol.prf.axm ⋯

noncomputable def Flypitch.fol.axm2 {L : Language} {Γ : Set (formula L)} {A B : formula L} : insert A (insert B Γ) ⊢ B

The second most recently inserted assumption is available immediately.

Equations

• Flypitch.fol.axm2 = Flypitch.fol.prf.axm ⋯

noncomputable def Flypitch.fol.weakening {L : Language} {Γ Δ : Set (formula L)} {f : formula L} (h₁ : Γ ⊆ Δ) (h₂ : Γ ⊢ f) : Δ ⊢ f

Weakening of assumptions for derivations.

Equations

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

noncomputable def Flypitch.fol.weakening1 {L : Language} {Γ : Set (formula L)} {f₁ f₂ : formula L} (h : Γ ⊢ f₂) : insert f₁ Γ ⊢ f₂

One-step weakening by adding an irrelevant assumption.

Equations

• Flypitch.fol.weakening1 h = Flypitch.fol.weakening ⋯ h

noncomputable def Flypitch.fol.weakening2 {L : Language} {Γ : Set (formula L)} {f₁ f₂ f₃ : formula L} (h : insert f₁ Γ ⊢ f₂) : insert f₁ (insert f₃ Γ) ⊢ f₂

Two-step weakening that preserves the distinguished first inserted assumption.

Equations

• Flypitch.fol.weakening2 h = Flypitch.fol.weakening ⋯ h

theorem Flypitch.fol.impI' {L : Language} {Γ : Set (formula L)} {A B : formula L} (h : insert A Γ ⊢' B) : Γ ⊢' A ⟹ B

Truncated implication introduction.

theorem Flypitch.fol.impE' {L : Language} {Γ : Set (formula L)} (A : formula L) {B : formula L} (h₁ : Γ ⊢' A ⟹ B) (h₂ : Γ ⊢' A) : Γ ⊢' B

Truncated implication elimination.

theorem Flypitch.fol.falsumE' {L : Language} {Γ : Set (formula L)} {A : formula L} (h : insert (∼A) Γ ⊢' ⊥) : Γ ⊢' A

Truncated ex falso rule under an explicit negated assumption.

theorem Flypitch.fol.allI' {L : Language} {Γ : Set (formula L)} {A : formula L} (h : lift_formula1 '' Γ ⊢' A) : Γ ⊢' ∀' A

Truncated universal introduction.

theorem Flypitch.fol.allE₂' {L : Language} {Γ : Set (formula L)} {A : formula L} {t : term L} (h : Γ ⊢' ∀' A) : Γ ⊢' subst_formula A t 0

Truncated universal elimination.

theorem Flypitch.fol.ref' {L : Language} (Γ : Set (formula L)) (t : term L) : Γ ⊢' t ≃ t

Truncated reflexivity of equality.

theorem Flypitch.fol.subst₂' {L : Language} {Γ : Set (formula L)} (s t : term L) (f : formula L) (h₁ : Γ ⊢' s ≃ t) (h₂ : Γ ⊢' subst_formula f s 0) : Γ ⊢' subst_formula f t 0

Truncated equality substitution.

theorem Flypitch.fol.weakening' {L : Language} {Γ Δ : Set (formula L)} {f : formula L} (h₁ : Γ ⊆ Δ) (h₂ : Γ ⊢' f) : Δ ⊢' f

Weakening for truncated derivations.

theorem Flypitch.fol.weakening1' {L : Language} {Γ : Set (formula L)} {f₁ f₂ : formula L} (h : Γ ⊢' f₂) : insert f₁ Γ ⊢' f₂

One-step weakening for truncated derivations.

theorem Flypitch.fol.weakening2' {L : Language} {Γ : Set (formula L)} {f₁ f₂ f₃ : formula L} (h : insert f₁ Γ ⊢' f₂) : insert f₁ (insert f₃ Γ) ⊢' f₂

Two-step weakening for truncated derivations.

noncomputable def Flypitch.fol.deduction {L : Language} {Γ : Set (formula L)} {A B : formula L} (h : Γ ⊢ A ⟹ B) : insert A Γ ⊢ B

Modus ponens with the antecedent inserted as an extra assumption.

Equations

• Flypitch.fol.deduction h = Flypitch.fol.prf.impE A (Flypitch.fol.weakening1 h) Flypitch.fol.axm1

noncomputable def Flypitch.fol.exfalso {L : Language} {Γ : Set (formula L)} {A : formula L} (h : Γ ⊢ ⊥) : Γ ⊢ A

Derive any formula from falsum.

Equations

• Flypitch.fol.exfalso h = (Flypitch.fol.weakening1 h).falsumE

theorem Flypitch.fol.exfalso' {L : Language} {Γ : Set (formula L)} {A : formula L} (h : Γ ⊢' ⊥) : Γ ⊢' A

Truncated version of exfalso.

noncomputable def Flypitch.fol.notI {L : Language} {Γ : Set (formula L)} {A : formula L} (h : Γ ⊢ A ⟹ ⊥) : Γ ⊢ ∼A

Repackage a proof of A ⟹ ⊥ as a proof of ∼A.

Equations

• Flypitch.fol.notI h = id h

noncomputable def Flypitch.fol.andI {L : Language} {Γ : Set (formula L)} {f₁ f₂ : formula L} (h₁ : Γ ⊢ f₁) (h₂ : Γ ⊢ f₂) : Γ ⊢ and f₁ f₂

Conjunction introduction.

Equations

• Flypitch.fol.andI h₁ h₂ = (Flypitch.fol.prf.impE f₂ (Flypitch.fol.prf.impE f₁ Flypitch.fol.axm1 (Flypitch.fol.weakening1 h₁)) (Flypitch.fol.weakening1 h₂)).impI

noncomputable def Flypitch.fol.andE1 {L : Language} {Γ : Set (formula L)} {f₁ : formula L} (f₂ : formula L) (h : Γ ⊢ and f₁ f₂) : Γ ⊢ f₁

Left projection from a conjunction.

Equations

• Flypitch.fol.andE1 f₂ h = (Flypitch.fol.prf.impE (f₁ ⟹ ∼f₂) (Flypitch.fol.weakening1 h) (Flypitch.fol.exfalso (Flypitch.fol.prf.impE f₁ Flypitch.fol.axm2 Flypitch.fol.axm1)).impI).falsumE

noncomputable def Flypitch.fol.andE2 {L : Language} {Γ : Set (formula L)} (f₁ : formula L) {f₂ : formula L} (h : Γ ⊢ and f₁ f₂) : Γ ⊢ f₂

Right projection from a conjunction.

Equations

• Flypitch.fol.andE2 f₁ h = (Flypitch.fol.prf.impE (f₁ ⟹ ∼f₂) (Flypitch.fol.weakening1 h) Flypitch.fol.axm2.impI).falsumE

noncomputable def Flypitch.fol.orI1 {L : Language} {Γ : Set (formula L)} {A B : formula L} (h : Γ ⊢ A) : Γ ⊢ or A B

Left introduction rule for disjunction.

Equations

• Flypitch.fol.orI1 h = (Flypitch.fol.exfalso (Flypitch.fol.prf.impE A Flypitch.fol.axm1 (Flypitch.fol.weakening1 h))).impI

noncomputable def Flypitch.fol.orI2 {L : Language} {Γ : Set (formula L)} {A B : formula L} (h : Γ ⊢ B) : Γ ⊢ or A B

Right introduction rule for disjunction.

Equations

• Flypitch.fol.orI2 h = id (Flypitch.fol.weakening1 h).impI

noncomputable def Flypitch.fol.orE {L : Language} {Γ : Set (formula L)} {A B C : formula L} (h₁ : Γ ⊢ or A B) (h₂ : insert A Γ ⊢ C) (h₃ : insert B Γ ⊢ C) : Γ ⊢ C

Disjunction elimination.

Equations

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

noncomputable def Flypitch.fol.biimpI {L : Language} {Γ : Set (formula L)} {f₁ f₂ : formula L} (h₁ : insert f₁ Γ ⊢ f₂) (h₂ : insert f₂ Γ ⊢ f₁) : Γ ⊢ biimp f₁ f₂

Biconditional introduction.

Equations

• Flypitch.fol.biimpI h₁ h₂ = Flypitch.fol.andI h₁.impI h₂.impI

noncomputable def Flypitch.fol.biimpE1 {L : Language} {Γ : Set (formula L)} {f₁ f₂ : formula L} (h : Γ ⊢ biimp f₁ f₂) : insert f₁ Γ ⊢ f₂

Extract the forward implication from a biconditional.

Equations

• Flypitch.fol.biimpE1 h = Flypitch.fol.deduction (Flypitch.fol.andE1 (f₂ ⟹ f₁) h)

noncomputable def Flypitch.fol.biimpE2 {L : Language} {Γ : Set (formula L)} {f₁ f₂ : formula L} (h : Γ ⊢ biimp f₁ f₂) : insert f₂ Γ ⊢ f₁

Extract the backward implication from a biconditional.

Equations

• Flypitch.fol.biimpE2 h = Flypitch.fol.deduction (Flypitch.fol.andE2 (f₁ ⟹ f₂) h)

noncomputable def Flypitch.fol.exI {L : Language} {Γ : Set (formula L)} {f : formula L} (t : term L) (h : Γ ⊢ subst_formula f t 0) : Γ ⊢ ex f

Existential introduction by providing a witness term.

Equations

• Flypitch.fol.exI t h = (Flypitch.fol.prf.impE (Flypitch.fol.subst_formula f t 0) (Flypitch.fol.prf.allE₂ (∼f) t Flypitch.fol.axm1) (Flypitch.fol.weakening1 h)).impI

noncomputable def Flypitch.fol.exE {L : Language} {Γ : Set (formula L)} {f₁ f₂ : formula L} (h₁ : Γ ⊢ ex f₁) (h₂ : insert f₁ (lift_formula1 '' Γ) ⊢ lift_formula1 f₂) : Γ ⊢ f₂

Existential elimination using a lifted derivation from a fresh witness.

Equations

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

noncomputable def Flypitch.fol.prf_lift {L : Language} {Γ : Set (formula L)} {f : formula L} (n m : ℕ) (h : Γ ⊢ f) : (fun (g : formula L) => lift_formula_at g n m) '' Γ ⊢ lift_formula_at f n m

Lift every formula appearing in a derivation by the same shift.

Equations

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

noncomputable def Flypitch.fol.substitution {L : Language} {Γ : Set (formula L)} {f : formula L} (t : term L) (n : ℕ) (h : Γ ⊢ f) : (fun (g : formula L) => subst_formula g t n) '' Γ ⊢ subst_formula f t n

Substitute a term throughout a derivation and all of its assumptions.

Equations

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

noncomputable def Flypitch.fol.reflect_prf_lift1 {L : Language} {Γ : Set (formula L)} {f : formula L} (h : lift_formula1 '' Γ ⊢ lift_formula f 1) : Γ ⊢ f

Cancel a single lifting step by substituting the fresh variable back in.

Equations

• Flypitch.fol.reflect_prf_lift1 h = ⋯.mp (cast ⋯ (⋯.mpr (⋯.mp (Flypitch.fol.substitution (&0) 0 h))))