AUX-007. Theory Extension

This module defines the ordinary operations used to combine commitment theories and to adjoin one object-language proposition.

Theory extension introduces no additional logical semantics. It is ordinary set union and singleton insertion.

def SE.Logic.Theory.combine {P : Language.PropositionCarrier} (T U : CommitmentTheory P) : CommitmentTheory P

Combines two commitment theories by set union.

Equations

• SE.Logic.Theory.combine T U = T ∪ U

def SE.Logic.Theory.adjoin {P : Language.PropositionCarrier} (T : CommitmentTheory P) (p : P.Proposition) : CommitmentTheory P

Adjoins one object-language proposition to a commitment theory.

Equations

• SE.Logic.Theory.adjoin T p = T ∪ {p}

@[simp]

theorem SE.Logic.Theory.mem_combine_iff {P : Language.PropositionCarrier} {T U : CommitmentTheory P} {p : P.Proposition} : p ∈ combine T U ↔ p ∈ T ∨ p ∈ U

Membership in a combined commitment theory is membership in either component.

@[simp]

theorem SE.Logic.Theory.mem_adjoin_iff {P : Language.PropositionCarrier} {T : CommitmentTheory P} {p q : P.Proposition} : p ∈ adjoin T q ↔ p ∈ T ∨ p = q

Membership after adjoining a proposition is membership in the original theory or equality with the adjoined proposition.

theorem SE.Logic.Theory.subset_combine_left {P : Language.PropositionCarrier} (T U : CommitmentTheory P) : T ⊆ combine T U

The left component is contained in the combined commitment theory.

theorem SE.Logic.Theory.subset_combine_right {P : Language.PropositionCarrier} (T U : CommitmentTheory P) : U ⊆ combine T U

The right component is contained in the combined commitment theory.

theorem SE.Logic.Theory.subset_adjoin {P : Language.PropositionCarrier} (T : CommitmentTheory P) (p : P.Proposition) : T ⊆ adjoin T p

A commitment theory is contained in the theory obtained by adjoining a proposition.