def Flypitch.list_except {α : 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

Equations

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

@[reducible]

def Flypitch.fol.finTheory {L : Language} (Γ : Finset (sentence L)) : Theory L

Equations

• Flypitch.fol.finTheory Γ = { carrier := ↑Γ }

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

Equations

• Flypitch.fol.image_lift hx = ⟨Classical.choose ⋯, ⋯⟩

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

Equations

• One or more equations did not get rendered due to their size.
• Flypitch.fol.image_lift_list x_2 = ⟨[], ⋯⟩

theorem Flypitch.fol.proof_compactness {L : Language} {ψ : formula L} {T : Set (formula L)} : T ⊢' ψ → ∃ (Γ : Finset (formula L)), ↑Γ ⊢' ψ ∧ ↑Γ ⊆ T

theorem Flypitch.fol.theory_proof_compactness {L : Language} {T : Theory L} {ψ : sentence L} (hψ : T ⊢' ψ) : ∃ (Γ : Finset (sentence L)), finTheory Γ ⊢' ψ ∧ ↑Γ ⊆ T.carrier

theorem Flypitch.fol.theory_proof_compactness_iff {L : Language} {T : Theory L} {ψ : sentence L} : T ⊢' ψ ↔ ∃ (Γ : Finset (sentence L)), finTheory Γ ⊢' ψ ∧ ↑Γ ⊆ T.carrier

theorem Flypitch.fol.is_consistent_union {L : Language} {T₁ T₂ : Theory L} (h₁ : is_consistent T₁) (h₂ : ∀ ψ ∈ T₂, insert (∼ψ) T₁ ⊢' ⊥) : is_consistent (T₁ ∪ T₂)