class LO.System.Disjunctive {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] (𝓢 : S) : Prop

• disjunctive : ∀ {p q : F}, 𝓢 ⊢! p ⋎ q → 𝓢 ⊢! p ∨ 𝓢 ⊢! q

theorem LO.System.Disjunctive.disjunctive {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [self : LO.System.Disjunctive 𝓢] {p : F} {q : F} : 𝓢 ⊢! p ⋎ q → 𝓢 ⊢! p ∨ 𝓢 ⊢! q

theorem LO.System.iff_disjunctive {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} : LO.System.Disjunctive 𝓢 ↔ ∀ {p q : F}, 𝓢 ⊢! p ⋎ q → 𝓢 ⊢! p ∨ 𝓢 ⊢! q

theorem LO.System.iff_complete_disjunctive {F : Type u_1} [LO.LogicalConnective F] {S : Type u_2} [LO.System F S] [DecidableEq F] {𝓢 : S} [LO.System.Classical 𝓢] : LO.System.Complete 𝓢 ↔ LO.System.Disjunctive 𝓢