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

• disjunctive {φ ψ : F} : 𝓢 ⊢! φ ⋎ ψ → 𝓢 ⊢! φ ∨ 𝓢 ⊢! ψ

theorem LO.System.disjunctive {F : Type u_1} {inst✝ : LogicalConnective F} {S : Type u_2} {inst✝¹ : System F S} {𝓢 : S} [self : Disjunctive 𝓢] {φ ψ : F} : 𝓢 ⊢! φ ⋎ ψ → 𝓢 ⊢! φ ∨ 𝓢 ⊢! ψ

Alias of LO.System.Disjunctive.disjunctive.

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

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