Disjunctive

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

Imported declaration from the Incompleteness formalization.

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

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

Alias of LO.Entailment.Disjunctive.disjunctive.

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

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