theorem LO.IntProp.Hilbert.iff_provable_dn_efq_dne_provable {α : Type u_1} [DecidableEq α] {φ : Formula α} : Hilbert.Int α ⊢! ∼∼φ ↔ Hilbert.Cl α ⊢! φ

theorem LO.IntProp.Hilbert.glivenko {α : Type u_1} [DecidableEq α] {φ : Formula α} : Hilbert.Int α ⊢! ∼∼φ ↔ Hilbert.Cl α ⊢! φ

Alias of LO.IntProp.Hilbert.iff_provable_dn_efq_dne_provable.

theorem LO.IntProp.Hilbert.iff_provable_neg_efq_provable_neg_efq {α : Type u_1} [DecidableEq α] {φ : Formula α} : Hilbert.Int α ⊢! ∼φ ↔ Hilbert.Cl α ⊢! ∼φ