NF weak partition development: Flypitch4.Compactness.

list_except

def NFChoice.Fol.listExcept {α : Type u} [DecidableEq α] (xs : List α) (x : α) (T : Set α) (h : ∀ y ∈ xs, y ≠ x → y ∈ T) : (ys : List α) ×' ({ϕ : α | ϕ ∈ ys} ⊆ T ∧ ∀ y ∈ ys, y ≠ x) ∧ ∀ y ∈ xs, y ≠ x → y ∈ ys

Given a list xs, an element x, and a set T such that everything in xs which is not x is in T, return the sublist excluding x, a proof it's a subset of T, and a proof none of its elements equal x.

Equations

• NFChoice.Fol.listExcept xs x T h = ⟨List.filter (fun (y : α) => decide (y ≠ x)) xs, ⋯⟩

image_lift

noncomputable def NFChoice.Fol.imageLift {α : Type u} {β : Type v} {f : α → β} {S : Set α} (x : β) (hx : x ∈ f '' S) : (x' : α) ×' x' ∈ S ∧ f x' = x

Given x ∈ f '' S, choose a lift x' in the preimage of x.

Equations

• NFChoice.Fol.imageLift x hx = ⟨Exists.choose hx, ⋯⟩

noncomputable def NFChoice.Fol.imageLiftList {α : Type u} {β : Type v} {f : α → β} {S : Set α} {xs : List β} (h_sub : {x : β | x ∈ xs} ⊆ f '' S) : (ys : List α) ×' {y' : α | y' ∈ ys} ⊆ S ∧ f '' {y : α | y ∈ ys} = {x : β | x ∈ xs}

Given a list xs, a set S, and a proof that {x | x ∈ xs} ⊆ f '' S, return a list of lifts ys ⊆ S such that f '' {y | y ∈ ys} = {x | x ∈ xs}.

Equations

• NFChoice.Fol.imageLiftList h_sub = ⟨⋯.choose, ⋯⟩

proof_compactness

theorem NFChoice.Fol.proof_compactness {L : Language} {ψ : formula L} {T : Set (formula L)} : provable T ψ → ∃ (Γ : Finset (formula L)), provable (↑Γ) ψ ∧ ↑Γ ⊆ T

Any proof from a set of formulas is provable from a finite subset.

theorem NFChoice.Fol.theory_proof_compactness {L : Language} {T : SentTheory L} {ψ : sentence L} (hψ : T.sprovable ψ) : ∃ (Γ : Finset (sentence L)), SentTheory.sprovable (↑Γ) ψ ∧ ↑Γ ⊆ T

Any proof from a sentence theory is provable from a finite sub-theory.

theorem NFChoice.Fol.theory_proof_compactness_iff {L : Language} {T : SentTheory L} {ψ : sentence L} : T.sprovable ψ ↔ ∃ (Γ : Finset (sentence L)), SentTheory.sprovable (↑Γ) ψ ∧ ↑Γ ⊆ T

sprf_by_cases

theorem NFChoice.Fol.sprf_by_cases {L : Language} {T : SentTheory L} (f₁ : sentence L) {f₂ : sentence L} (H₁ : (insert f₁ T).sprovable f₂) (H₂ : (insert (bdNot f₁) T).sprovable f₂) : T.sprovable f₂

Sentence-level by-cases principle (wrapper for prf_by_cases).

is_consistent_union

theorem NFChoice.Fol.is_consistent_union {L : Language} {T₁ T₂ : SentTheory L} (h₁ : T₁.isConsistent) (h₂ : ∀ ψ ∈ T₂, (insert (bdNot ψ) T₁).sprovable bd_falsum) : (T₁ ∪ T₂).isConsistent