Flypitch.FOL.Theory packages closed formulas into theories and records the proof-theoretic and semantic notions attached to them. It also defines consistency, completeness, and the basic operations for working inside a theory rather than an arbitrary set of formulas.

def Flypitch.fol.bounded_term_at {L : Language} {l : ℕ} : preterm L l → ℕ → Prop

bounded_term_at t n means that every free variable of t is strictly below n.

Equations

• Flypitch.fol.bounded_term_at (&k) x✝ = (k < x✝)
• Flypitch.fol.bounded_term_at (Flypitch.fol.preterm.func a) x✝ = True
• Flypitch.fol.bounded_term_at (t₁.app t₂) x✝ = (Flypitch.fol.bounded_term_at t₁ x✝ ∧ Flypitch.fol.bounded_term_at t₂ x✝)

def Flypitch.fol.bounded_formula_at {L : Language} {l : ℕ} : preformula L l → ℕ → Prop

bounded_formula_at f n means that every free variable of f is strictly below n.

Equations

• Flypitch.fol.bounded_formula_at Flypitch.fol.preformula.falsum x✝ = True
• Flypitch.fol.bounded_formula_at (t₁ ≃ t₂) x✝ = (Flypitch.fol.bounded_term_at t₁ x✝ ∧ Flypitch.fol.bounded_term_at t₂ x✝)
• Flypitch.fol.bounded_formula_at (Flypitch.fol.preformula.rel a) x✝ = True
• Flypitch.fol.bounded_formula_at (f.apprel t) x✝ = (Flypitch.fol.bounded_formula_at f x✝ ∧ Flypitch.fol.bounded_term_at t x✝)
• Flypitch.fol.bounded_formula_at (f₁ ⟹ f₂) x✝ = (Flypitch.fol.bounded_formula_at f₁ x✝ ∧ Flypitch.fol.bounded_formula_at f₂ x✝)
• Flypitch.fol.bounded_formula_at (∀' f) x✝ = Flypitch.fol.bounded_formula_at f (x✝ + 1)

theorem Flypitch.fol.bounded_term_at_mono {L : Language} {l : ℕ} (t : preterm L l) {n m : ℕ} : bounded_term_at t n → n ≤ m → bounded_term_at t m

Increasing the bound preserves boundedness of terms.

theorem Flypitch.fol.bounded_formula_at_mono {L : Language} {l : ℕ} (f : preformula L l) {n m : ℕ} : bounded_formula_at f n → n ≤ m → bounded_formula_at f m

Increasing the bound preserves boundedness of formulas.

theorem Flypitch.fol.bounded_term_at_lift_irrel {L : Language} {l : ℕ} (t : preterm L l) (n m : ℕ) : bounded_term_at t m → (t ↑' n # m) = t

Lifting above a bound already respected by a term has no effect.

theorem Flypitch.fol.bounded_formula_at_lift_irrel {L : Language} {l : ℕ} (f : preformula L l) (n m : ℕ) : bounded_formula_at f m → lift_formula_at f n m = f

Lifting above a bound already respected by a formula has no effect.

theorem Flypitch.fol.bounded_term_at_subst_irrel {L : Language} {l : ℕ} (t : preterm L l) {n : ℕ} : bounded_term_at t n → ∀ (s : term L), t[s // n] = t

Substituting at a variable bound already respected by a term has no effect.

theorem Flypitch.fol.bounded_formula_at_subst_irrel {L : Language} {l : ℕ} (f : preformula L l) {n : ℕ} : bounded_formula_at f n → ∀ (s : term L), subst_formula f s n = f

Substituting at a variable bound already respected by a formula has no effect.

theorem Flypitch.fol.bounded_term_at_subst_closed {L : Language} {l : ℕ} (t : preterm L l) {n : ℕ} {s : term L} : bounded_term_at t (n + 1) → bounded_term_at s 0 → bounded_term_at (t[s // n]) n

Substituting a closed term into a term bounded by n + 1 lowers the bound to n.

theorem Flypitch.fol.bounded_formula_at_subst_closed {L : Language} {l : ℕ} (f : preformula L l) {n : ℕ} {s : term L} : bounded_formula_at f (n + 1) → bounded_term_at s 0 → bounded_formula_at (subst_formula f s n) n

Substituting a closed term into a formula bounded by n + 1 lowers the bound to n.

theorem Flypitch.fol.lift_subst_term_cancel {L : Language} {l : ℕ} (t : preterm L l) (n : ℕ) : (t ↑' 1 # n + 1)[&0 // n] = t

Lifting above a bound and then substituting the new variable back in cancels for terms.

theorem Flypitch.fol.lift_subst_formula_cancel {L : Language} {l : ℕ} (f : preformula L l) (n : ℕ) : subst_formula (lift_formula_at f 1 (n + 1)) (&0) n = f

Lifting above a bound and then substituting the new variable back in cancels for formulas.

def Flypitch.fol.sentence (L : Language) : Type u

Closed formulas, represented as formulas with no free variables.

Equations

• Flypitch.fol.sentence L = { f : Flypitch.fol.formula L // Flypitch.fol.bounded_formula_at f 0 }

@[implicit_reducible]

instance Flypitch.fol.instCoeSentenceFormula {L : Language} : Coe (sentence L) (formula L)

Equations

• Flypitch.fol.instCoeSentenceFormula = { coe := fun (f : Flypitch.fol.sentence L) => ↑f }

@[implicit_reducible]

instance Flypitch.fol.instBotSentence {L : Language} : Bot (sentence L)

Equations

• Flypitch.fol.instBotSentence = { bot := ⟨⊥, trivial⟩ }

def Flypitch.fol.sentence.imp {L : Language} (f₁ f₂ : sentence L) : sentence L

Implication of closed formulas.

Equations

• f₁ ⟹ f₂ = ⟨↑f₁ ⟹ ↑f₂, ⋯⟩

def Flypitch.fol.«term_⟹__1» : Lean.TrailingParserDescr

Equations

• Flypitch.fol.«term_⟹__1» = Lean.ParserDescr.trailingNode `Flypitch.fol.«term_⟹__1» 62 63 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟹ ") (Lean.ParserDescr.cat `term 62))

def Flypitch.fol.sentence.not {L : Language} (f : sentence L) : sentence L

Negation of a sentence.

Equations

• ∼f = f ⟹ ⊥

def Flypitch.fol.«term∼__1» : Lean.ParserDescr

Equations

• Flypitch.fol.«term∼__1» = Lean.ParserDescr.node `Flypitch.fol.«term∼__1» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∼") (Lean.ParserDescr.cat `term 1024))

@[implicit_reducible]

instance Flypitch.fol.instTopSentence {L : Language} : Top (sentence L)

Equations

• Flypitch.fol.instTopSentence = { top := ∼⊥ }

def Flypitch.fol.sentence.and {L : Language} (f₁ f₂ : sentence L) : sentence L

Conjunction of sentences.

Equations

• f₁.and f₂ = ∼(f₁ ⟹ ∼f₂)

def Flypitch.fol.sentence.or {L : Language} (f₁ f₂ : sentence L) : sentence L

Disjunction of sentences.

Equations

• f₁.or f₂ = ∼f₁ ⟹ f₂

def Flypitch.fol.sentence.biimp {L : Language} (f₁ f₂ : sentence L) : sentence L

Biconditional of sentences.

Equations

• f₁.biimp f₂ = (f₁ ⟹ f₂).and (f₂ ⟹ f₁)

def Flypitch.fol.sentence.all {L : Language} (f : sentence L) : sentence L

Universal quantification of a sentence, viewed as opening one bound variable.

Equations

• f.all = ⟨∀' ↑f, ⋯⟩

def Flypitch.fol.sentence.ex {L : Language} (f : sentence L) : sentence L

Existential quantification of a sentence.

Equations

• f.ex = ∼(∼f).all

theorem Flypitch.fol.lift_sentence_irrel {L : Language} (f : sentence L) : lift_formula1 ↑f = ↑f

Lifting a closed formula is definitionally irrelevant.

theorem Flypitch.fol.subst_sentence_irrel {L : Language} (f : sentence L) (s : term L) : subst_formula (↑f) s 0 = ↑f

Substituting into a closed formula is definitionally irrelevant.

structure Flypitch.fol.Theory (L : Language) : Type (u + 1)

A theory is a set of closed formulas.

• carrier : Set (sentence L)

@[implicit_reducible]

instance Flypitch.fol.Theory.instMembershipSentence {L : Language} : Membership (sentence L) (Theory L)

Equations

• Flypitch.fol.Theory.instMembershipSentence = { mem := fun (T : Flypitch.fol.Theory L) (x : Flypitch.fol.sentence L) => x ∈ T.carrier }

@[implicit_reducible]

instance Flypitch.fol.Theory.instEmptyCollection {L : Language} : EmptyCollection (Theory L)

Equations

• Flypitch.fol.Theory.instEmptyCollection = { emptyCollection := { carrier := ∅ } }

@[implicit_reducible]

instance Flypitch.fol.Theory.instInsertSentence {L : Language} : Insert (sentence L) (Theory L)

Equations

• Flypitch.fol.Theory.instInsertSentence = { insert := fun (a : Flypitch.fol.sentence L) (T : Flypitch.fol.Theory L) => { carrier := Set.insert a T.carrier } }

@[implicit_reducible]

instance Flypitch.fol.Theory.instSingletonSentence {L : Language} : Singleton (sentence L) (Theory L)

Equations

• Flypitch.fol.Theory.instSingletonSentence = { singleton := fun (a : Flypitch.fol.sentence L) => { carrier := {a} } }

@[implicit_reducible]

instance Flypitch.fol.Theory.instUnion {L : Language} : Union (Theory L)

Equations

• Flypitch.fol.Theory.instUnion = { union := fun (T T' : Flypitch.fol.Theory L) => { carrier := T.carrier ∪ T'.carrier } }

@[implicit_reducible]

instance Flypitch.fol.Theory.instCoeSetSentence {L : Language} : Coe (Set (sentence L)) (Theory L)

Equations

• Flypitch.fol.Theory.instCoeSetSentence = { coe := fun (S : Set (Flypitch.fol.sentence L)) => { carrier := S } }

def Flypitch.fol.Theory.Subset {L : Language} (T T' : Theory L) : Prop

Inclusion of theories.

Equations

• T.Subset T' = (T.carrier ⊆ T'.carrier)

theorem Flypitch.fol.Theory.ext {L : Language} {T T' : Theory L} (h : ∀ (x : sentence L), x ∈ T ↔ x ∈ T') : T = T'

theorem Flypitch.fol.Theory.ext_iff {L : Language} {T T' : Theory L} : T = T' ↔ ∀ (x : sentence L), x ∈ T ↔ x ∈ T'

@[reducible]

def Flypitch.fol.Theory.fst {L : Language} (T : Theory L) : Set (formula L)

Equations

• T.fst = Subtype.val '' T.carrier

theorem Flypitch.fol.Theory.image_subset {L : Language} {T T' : Theory L} (h : T.Subset T') : T.fst ⊆ T'.fst

Inclusion of theories induces inclusion of the underlying sets of formulas.

@[simp]

theorem Flypitch.fol.Theory.fst_insert {L : Language} (A : sentence L) (T : Theory L) : (insert A T).fst = Set.insert (↑A) T.fst

theorem Flypitch.fol.lift_Theory_irrel {L : Language} (T : Theory L) : lift_formula1 '' T.fst = T.fst

Lifting does nothing on the underlying formulas of a theory of sentences.

@[reducible, inline]

abbrev Flypitch.fol.sprf {L : Language} (T : Theory L) (f : sentence L) : Type u

Proofs from a theory, viewed through its underlying set of formulas.

Equations

• T ⊢ f = T.fst ⊢ ↑f

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

Equations

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

@[reducible, inline]

abbrev Flypitch.fol.sprovable {L : Language} (T : Theory L) (f : sentence L) : Prop

Truncated provability from a theory.

Equations

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

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

Equations

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

def Flypitch.fol.saxm {L : Language} {T : Theory L} {A : sentence L} (h : A ∈ T) : T ⊢ A

Any sentence already in the theory is provable from it.

Equations

• Flypitch.fol.saxm h = Flypitch.fol.prf.axm ⋯

def Flypitch.fol.saxm1 {L : Language} {T : Theory L} {A : sentence L} : insert A T ⊢ A

The newest inserted sentence is provable immediately.

Equations

• Flypitch.fol.saxm1 = Flypitch.fol.saxm ⋯

def Flypitch.fol.saxm2 {L : Language} {T : Theory L} {A B : sentence L} : insert A (insert B T) ⊢ B

The second newest inserted sentence is provable immediately.

Equations

• Flypitch.fol.saxm2 = Flypitch.fol.saxm ⋯

def Flypitch.fol.simpI {L : Language} {T : Theory L} {A B : sentence L} (h : insert A T ⊢ B) : T ⊢ A ⟹ B

Implication introduction internal to theories.

Equations

• Flypitch.fol.simpI h = (⋯.mp h).impI

theorem Flypitch.fol.simpI' {L : Language} {T : Theory L} {A B : sentence L} (h : insert A T ⊢' B) : T ⊢' A ⟹ B

Truncated implication introduction internal to theories.

def Flypitch.fol.simpE {L : Language} {T : Theory L} (A : sentence L) {B : sentence L} (h₁ : T ⊢ A ⟹ B) (h₂ : T ⊢ A) : T ⊢ B

Implication elimination internal to theories.

Equations

• Flypitch.fol.simpE A h₁ h₂ = Flypitch.fol.prf.impE (↑A) h₁ h₂

def Flypitch.fol.sfalsumE {L : Language} {T : Theory L} {A : sentence L} (h : insert (∼A) T ⊢ ⊥) : T ⊢ A

Ex falso internal to theories using an explicit negated assumption.

Equations

• Flypitch.fol.sfalsumE h = (⋯.mp h).falsumE

theorem Flypitch.fol.sfalsumE' {L : Language} {T : Theory L} {A : sentence L} (h : insert (∼A) T ⊢' ⊥) : T ⊢' A

noncomputable def Flypitch.fol.sweakening {L : Language} {T T' : Theory L} (hsub : T'.Subset T) {ψ : sentence L} (h : T' ⊢ ψ) : T ⊢ ψ

Weakening of theory proofs along inclusion of theories.

Equations

• Flypitch.fol.sweakening hsub h = Flypitch.fol.weakening ⋯ h

noncomputable def Flypitch.fol.sweakening1 {L : Language} {T : Theory L} {ψ₁ ψ₂ : sentence L} (h : T ⊢ ψ₂) : insert ψ₁ T ⊢ ψ₂

One-step weakening for theory proofs.

Equations

• Flypitch.fol.sweakening1 h = Flypitch.fol.sweakening ⋯ h

noncomputable def Flypitch.fol.sweakening2 {L : Language} {T : Theory L} {ψ₁ ψ₂ ψ₃ : sentence L} (h : insert ψ₁ T ⊢ ψ₃) : insert ψ₁ (insert ψ₂ T) ⊢ ψ₃

Two-step weakening for theory proofs.

Equations

• Flypitch.fol.sweakening2 h = Flypitch.fol.sweakening ⋯ h

theorem Flypitch.fol.simpE' {L : Language} {T : Theory L} (A : sentence L) {B : sentence L} (h₁ : T ⊢' A ⟹ B) (h₂ : T ⊢' A) : T ⊢' B

Truncated implication elimination internal to theories.

theorem Flypitch.fol.snot_and_self'' {L : Language} {T : Theory L} {A : sentence L} (h₁ : T ⊢' A) (h₂ : T ⊢' ∼A) : T ⊢' ⊥

A sentence and its negation yield falsum.

theorem Flypitch.fol.sprf_by_cases {L : Language} {Γ : Theory L} (f₁ : sentence L) {f₂ : sentence L} (h₁ : insert f₁ Γ ⊢' f₂) (h₂ : insert (∼f₁) Γ ⊢' f₂) : Γ ⊢' f₂

Proof by cases inside a theory.

def Flypitch.fol.sprovable_of_provable {L : Language} {T : Theory L} {f : sentence L} (h : T.fst ⊢ ↑f) : T ⊢ f

Reinterpret a formula-level proof as a sentence-level proof.

Equations

• Flypitch.fol.sprovable_of_provable h = h

def Flypitch.fol.provable_of_sprovable {L : Language} {T : Theory L} {f : sentence L} (h : T ⊢ f) : T.fst ⊢ ↑f

Forget that a sentence-level proof came from a theory.

Equations

• Flypitch.fol.provable_of_sprovable h = h

theorem Flypitch.fol.sprovable_of_sprf {L : Language} {T : Theory L} {f : sentence L} (h : T ⊢ f) : T ⊢' f

theorem Flypitch.fol.sprovable.elim {L : Language} {P : Prop} {T : Theory L} {f : sentence L} (ih : ∀ (a : T ⊢ f), P) (h : T ⊢' f) : P

Eliminate the truncation in sprovable.

@[reducible, inline]

abbrev Flypitch.fol.realize_sentence {L : Language} (M : Structure L) (f : sentence L) : Prop

Satisfaction of a sentence in a structure.

Equations

• Flypitch.fol.realize_sentence M f = Flypitch.fol.satisfied_in M ↑f

@[reducible, inline]

abbrev Flypitch.fol.all_realize_sentence {L : Language} (M : Structure L) (T : Theory L) : Prop

Every sentence in T is satisfied in M.

Equations

• Flypitch.fol.all_realize_sentence M T = ∀ ⦃f : Flypitch.fol.sentence L⦄, f ∈ T → Flypitch.fol.realize_sentence M f

theorem Flypitch.fol.all_realize_sentence_of_subset {L : Language} {M : Structure L} {T₁ T₂ : Theory L} (h : all_realize_sentence M T₂) (hsub : T₁.Subset T₂) : all_realize_sentence M T₁

Satisfaction is monotone along inclusion of theories.

theorem Flypitch.fol.all_realize_sentence_axm {L : Language} {M : Structure L} {f : sentence L} {T : Theory L} (h : all_realize_sentence M (insert f T)) : realize_sentence M f ∧ all_realize_sentence M T

Satisfaction of an inserted sentence splits into the new axiom and the old theory.

@[simp]

theorem Flypitch.fol.all_realize_sentence_axm_rw {L : Language} {M : Structure L} {f : sentence L} {T : Theory L} : all_realize_sentence M (insert f T) ↔ realize_sentence M f ∧ all_realize_sentence M T

Rewriting version of all_realize_sentence_axm.

@[simp]

theorem Flypitch.fol.all_realize_sentence_singleton {L : Language} {M : Structure L} {f : sentence L} : all_realize_sentence M {f} ↔ realize_sentence M f

A singleton theory is satisfied exactly when its unique sentence is.

theorem Flypitch.fol.realize_sentence_of_mem {L : Language} {M : Structure L} {T : Theory L} {f : sentence L} (h : all_realize_sentence M T) (hf : f ∈ T) : realize_sentence M f

Extract satisfaction of a particular member of a theory.

def Flypitch.fol.ssatisfied {L : Language} (T : Theory L) (f : sentence L) : Prop

Semantic consequence between theories and sentences.

Equations

• Flypitch.fol.ssatisfied T f = ∀ {M : Flypitch.fol.Structure L}, Nonempty M.carrier → Flypitch.fol.all_realize_sentence M T → Flypitch.fol.realize_sentence M f

theorem Flypitch.fol.ssatisfied_of_mem {L : Language} {T : Theory L} {f : sentence L} (hf : f ∈ T) : ssatisfied T f

Any sentence already in a theory is a semantic consequence of it.

def Flypitch.fol.is_consistent {L : Language} (T : Theory L) : Prop

A theory is consistent when it does not prove falsum.

Equations

• Flypitch.fol.is_consistent T = ¬T ⊢' ⊥

theorem Flypitch.fol.is_consistent.intro {L : Language} {T : Theory L} (h : ¬T ⊢' ⊥) : is_consistent T

theorem Flypitch.fol.is_consistent.elim {L : Language} {T : Theory L} (h : is_consistent T) : ¬T ⊢' ⊥

theorem Flypitch.fol.consis_not_of_not_provable {L : Language} {T : Theory L} {f : sentence L} (h₁ : ¬T ⊢' f) : is_consistent (T ∪ {∼f})

If f is not provable, adjoining ¬f preserves consistency.

def Flypitch.fol.is_complete {L : Language} (T : Theory L) : Prop

A complete theory is consistent and decides every sentence.

Equations

• Flypitch.fol.is_complete T = (Flypitch.fol.is_consistent T ∧ ∀ (f : Flypitch.fol.sentence L), f ∈ T ∨ ∼f ∈ T)

theorem Flypitch.fol.mem_of_sprf {L : Language} {T : Theory L} (h : is_complete T) {f : sentence L} (hf : T ⊢ f) : f ∈ T

In a complete theory, every provable sentence is already an axiom.

theorem Flypitch.fol.mem_of_sprovable {L : Language} {T : Theory L} (h : is_complete T) {f : sentence L} (hf : T ⊢' f) : f ∈ T

Truncated version of mem_of_sprf.

theorem Flypitch.fol.impI_of_is_complete {L : Language} {T : Theory L} (h : is_complete T) {f₁ f₂ : sentence L} (hf : T ⊢' f₁ → T ⊢' f₂) : T ⊢' f₁ ⟹ f₂

In a complete theory, implication can be introduced from a meta-level implication on provability.

theorem Flypitch.fol.notI_of_is_complete {L : Language} {T : Theory L} (h : is_complete T) {f : sentence L} (hf : ¬T ⊢' f) : T ⊢' ∼f

In a complete theory, non-provability of f yields provability of ¬f.

@[reducible, inline]

abbrev Flypitch.fol.Theory.Consistent {L : Language} (T : Theory L) : Prop

Synonym for is_consistent under the Theory namespace.

Equations

• T.Consistent = Flypitch.fol.is_consistent T

@[reducible, inline]

abbrev Flypitch.fol.Theory.Complete {L : Language} (T : Theory L) : Prop

Synonym for is_complete under the Theory namespace.

Equations

• T.Complete = Flypitch.fol.is_complete T

def Flypitch.fol.TheoryOver {L : Language} (T : Theory L) (hT : is_consistent T) : Type (u + 1)

Consistent theory extensions ordered by inclusion.

Equations

• Flypitch.fol.TheoryOver T hT = { T' : Flypitch.fol.Theory L // T.Subset T' ∧ Flypitch.fol.is_consistent T' }

def Flypitch.fol.over_self {L : Language} (T : Theory L) (hT : is_consistent T) : TheoryOver T hT

The base theory regarded as an extension of itself.

Equations

• Flypitch.fol.over_self T hT = ⟨T, ⋯⟩

@[reducible, inline]

abbrev Flypitch.fol.complete_theory {L : Language} (T : Theory L) : Prop

Alias used when completeness is the relevant viewpoint.

Equations

• Flypitch.fol.complete_theory T = Flypitch.fol.is_complete T