Foundation.Propositional.Entailment.Corsi.VF

source

Type (max u_2 u_3)

and₁ {φ ψ : F} : 𝓢 ⊢! Axioms.AndElim₁ φ ψ
and₂ {φ ψ : F} : 𝓢 ⊢! Axioms.AndElim₂ φ ψ
or₁ {φ ψ : F} : 𝓢 ⊢! Axioms.OrInst₁ φ ψ
or₂ {φ ψ : F} : 𝓢 ⊢! Axioms.OrInst₂ φ ψ
distributeAndOr! {φ ψ χ : F} : 𝓢 ⊢! Axioms.DistributeAndOr φ ψ χ
impId! {φ : F} : 𝓢 ⊢! Axioms.ImpId φ
verum : 𝓢 ⊢! Axioms.Verum
efq {φ : F} : 𝓢 ⊢! Axioms.EFQ φ
mdp {φ ψ : F} : 𝓢 ⊢! φ ➝ ψ → 𝓢 ⊢! φ → 𝓢 ⊢! ψ
af! {φ ψ : F} : 𝓢 ⊢! φ → 𝓢 ⊢! ψ ➝ φ
andIR! {φ ψ : F} : 𝓢 ⊢! φ → 𝓢 ⊢! ψ → 𝓢 ⊢! φ ⋏ ψ
ruleC! {φ ψ χ : F} : 𝓢 ⊢! φ ➝ ψ → 𝓢 ⊢! φ ➝ χ → 𝓢 ⊢! φ ➝ ψ ⋏ χ
ruleD! {φ ψ χ : F} : 𝓢 ⊢! φ ➝ χ → 𝓢 ⊢! ψ ➝ χ → 𝓢 ⊢! φ ⋎ ψ ➝ χ
ruleI! {φ ψ χ : F} : 𝓢 ⊢! φ ➝ ψ → 𝓢 ⊢! ψ ➝ χ → 𝓢 ⊢! φ ➝ χ

Instances

source

instance LO.Propositional.Entailment.Corsi.instHasCollectOrAnd {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.VF 𝓢] :

HasCollectOrAnd 𝓢

Equations

One or more equations did not get rendered due to their size.

source

@[simp, deprecated ]

theorem LO.Propositional.Entailment.Corsi.not_bot {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.VF 𝓢] [Entailment.Consistent 𝓢] :

𝓢 ⊬ ⊥

source

theorem LO.Propositional.Entailment.Corsi.CA_replace_both {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.VF 𝓢] {φ' ψ' : F} (h₁ : 𝓢 ⊢ φ ➝ φ') (h₂ : 𝓢 ⊢ ψ ➝ ψ') :

𝓢 ⊢ φ ⋎ ψ ➝ φ' ⋎ ψ'

source

theorem LO.Propositional.Entailment.Corsi.CA_replace_left {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.VF 𝓢] {φ' : F} (h : 𝓢 ⊢ φ' ➝ φ) :

𝓢 ⊢ φ' ⋎ ψ ➝ φ ⋎ ψ

source

theorem LO.Propositional.Entailment.Corsi.CA_replace_right {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.VF 𝓢] {ψ' : F} (h : 𝓢 ⊢ ψ ➝ ψ') :

𝓢 ⊢ φ ⋎ ψ ➝ φ ⋎ ψ'

source

theorem LO.Propositional.Entailment.Corsi.C_replace_both {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.VF 𝓢] {φ' ψ' : F} (h : 𝓢 ⊢ φ ➝ ψ) (h₁ : 𝓢 ⊢ φ' ➝ φ) (h₂ : 𝓢 ⊢ ψ ➝ ψ') :

𝓢 ⊢ φ' ➝ ψ'

source

theorem LO.Propositional.Entailment.Corsi.CKK_right_replace {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.VF 𝓢] {ψ' : F} (h : 𝓢 ⊢ ψ ➝ ψ') :

𝓢 ⊢ φ ⋏ ψ ➝ φ ⋏ ψ'

source

theorem LO.Propositional.Entailment.Corsi.insert_LConj {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ : F} [Entailment.VF 𝓢] {Γ : List F} :

𝓢 ⊢ φ ⋏ ⋀Γ ➝ ⋀(φ :: Γ)

source

@[simp]

theorem LO.Propositional.Entailment.Corsi.conjconj {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.VF 𝓢] {Γ : Finset F} :

𝓢 ⊢ Γ.conj ➝ ⋀Γ.toList

source

theorem LO.Propositional.Entailment.Corsi.LConj₂Conj₂_of_provable {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.VF 𝓢] {γ : F} {Δ : List F} (h : ∀ δ ∈ Δ, 𝓢 ⊢ γ ➝ δ) :

𝓢 ⊢ γ ➝ ⋀Δ

source

theorem LO.Propositional.Entailment.Corsi.ruleC_lconj₂ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ : F} [Entailment.VF 𝓢] {Γ : List F} (h : ∀ γ ∈ Γ, 𝓢 ⊢ φ ➝ γ) :

𝓢 ⊢ φ ➝ ⋀Γ

source

theorem LO.Propositional.Entailment.Corsi.ruleC_fconj {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ : F} [Entailment.VF 𝓢] {Γ : Finset F} (h : ∀ γ ∈ Γ, 𝓢 ⊢ φ ➝ γ) :

𝓢 ⊢ φ ➝ Γ.conj

source

theorem LO.Propositional.Entailment.Corsi.ruleC_fconj' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ : F} [Entailment.VF 𝓢] {ι : Type u_3} {Γ : Finset ι} (Φ : ι → F) (h : ∀ i ∈ Γ, 𝓢 ⊢ φ ➝ Φ i) :

𝓢 ⊢ φ ➝ ⩕ (i : ι) ∈ Γ, Φ i

source

theorem LO.Propositional.Entailment.Corsi.mem_lconj₂ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ : F} [Entailment.VF 𝓢] {Γ : List F} (h : φ ∈ Γ) :

𝓢 ⊢ ⋀Γ ➝ φ

source

theorem LO.Propositional.Entailment.Corsi.mem_fconj {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ : F} [Entailment.VF 𝓢] {Γ : Finset F} (h : φ ∈ Γ) :

𝓢 ⊢ Γ.conj ➝ φ

source

theorem LO.Propositional.Entailment.Corsi.mem_fconj' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {ψ : F} [Entailment.VF 𝓢] {ι : Type u_3} {Γ : Finset ι} (Φ : ι → F) (hΦ : ∃ i ∈ Γ, Φ i = ψ) :

𝓢 ⊢ (⩕ (i : ι) ∈ Γ, Φ i) ➝ ψ

source

theorem LO.Propositional.Entailment.Corsi.LConj₂Conj₂_of_subset {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.VF 𝓢] {Γ Δ : List F} (h : ∀ φ ∈ Δ, φ ∈ Γ) :

𝓢 ⊢ ⋀Γ ➝ ⋀Δ

source

theorem LO.Propositional.Entailment.Corsi.CFConjFConj_of_subset {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.VF 𝓢] {Γ Δ : Finset F} (h : Δ ⊆ Γ) :

𝓢 ⊢ Γ.conj ➝ Δ.conj

source

theorem LO.Propositional.Entailment.Corsi.FConj₂_of_LConj {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.VF 𝓢] [DecidableEq F] {Γ : List F} :

𝓢 ⊢ ⋀Γ ➝ Γ.toFinset.conj

source

theorem LO.Propositional.Entailment.Corsi.insert_FConj {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ : F} [Entailment.VF 𝓢] [DecidableEq F] {Γ : Finset F} :

𝓢 ⊢ φ ⋏ Γ.conj ➝ (insert φ Γ).conj

source

theorem LO.Propositional.Entailment.Corsi.CFConjFConj_of_provable {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.VF 𝓢] {γ : F} {Δ : Finset F} (h : ∀ δ ∈ Δ, 𝓢 ⊢ γ ➝ δ) :

𝓢 ⊢ γ ➝ Δ.conj

source

theorem LO.Propositional.Entailment.Corsi.mem_ldisj₂ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {ψ : F} [Entailment.VF 𝓢] {Γ : List F} (h : ψ ∈ Γ) :

𝓢 ⊢ ψ ➝ ⋁Γ

source

theorem LO.Propositional.Entailment.Corsi.mem_fdisj' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {ψ : F} [Entailment.VF 𝓢] {ι : Type u_3} {Γ : Finset ι} (Φ : ι → F) (hΦ : ∃ i ∈ Γ, Φ i = ψ) :

𝓢 ⊢ ψ ➝ ⩖ (i : ι) ∈ Γ, Φ i

source

theorem LO.Propositional.Entailment.Corsi.ruleD_ldisj₂ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ : F} [Entailment.VF 𝓢] {Γ : List F} (h : ∀ γ ∈ Γ, 𝓢 ⊢ γ ➝ φ) :

𝓢 ⊢ ⋁Γ ➝ φ

source

theorem LO.Propositional.Entailment.Corsi.ruleD_fdisj' {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ : F} [Entailment.VF 𝓢] {ι : Type u_3} {Γ : Finset ι} (Φ : ι → F) (h : ∀ i ∈ Γ, 𝓢 ⊢ Φ i ➝ φ) :

𝓢 ⊢ (⩖ (i : ι) ∈ Γ, Φ i) ➝ φ

source

theorem LO.Propositional.Entailment.Corsi.DP_ldisj₂ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.VF 𝓢] [Entailment.Disjunctive 𝓢] [Entailment.Consistent 𝓢] {Γ : List F} (h : 𝓢 ⊢ ⋁Γ) :

∃ γ ∈ Γ, 𝓢 ⊢ γ

source

theorem LO.Propositional.Entailment.Corsi.DP_fdisj {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.VF 𝓢] [Entailment.Disjunctive 𝓢] [Entailment.Consistent 𝓢] {ι : Type u_3} {Γ : Finset ι} (Φ : ι → F) (h : 𝓢 ⊢ ⩖ (i : ι) ∈ Γ, Φ i) :

∃ i ∈ Γ, 𝓢 ⊢ Φ i