Theory logics_consequence

theory logics_consequence
  imports boolean_algebra
begin

section ‹Logics based on Topological Boolean Algebras›

subsection ‹Logical Consequence and Validity›

text‹Logical validity can be defined as truth in all points (i.e. as denoting the top element).›
abbreviation (input) gtrue::"'w σ ⇒ bool" ("[⊢ _]") 
  where  "[⊢ A] ≡ ∀w. A w"   
lemma gtrue_def: "[⊢ A] ≡ A ❙= ❙⊤" by (simp add: setequ_def top_def)

text‹When defining a logic over an existing algebra we have two choices: a global (truth preserving)
and a local (degree preserving) notion of logical consequence. For LFIs/LFUs we prefer the latter.›
abbreviation (input) conseq_global1::"'w σ ⇒ 'w σ⇒bool" ("[_ ⊢⇩g _]") 
  where "[A ⊢⇩g B] ≡ [⊢ A] ⟶ [⊢ B]"
abbreviation (input) conseq_global21::"'w σ ⇒ 'w σ ⇒ 'w σ ⇒ bool" ("[_,_ ⊢⇩g _]") 
  where "[A⇩1, A⇩2 ⊢⇩g B] ≡ [⊢ A⇩1] ∧ [⊢ A⇩2] ⟶ [⊢ B]"
abbreviation (input) conseq_global31::"'w σ ⇒ 'w σ ⇒ 'w σ ⇒ 'w σ ⇒ bool" ("[_,_,_ ⊢⇩g _]") 
  where "[A⇩1, A⇩2, A⇩3 ⊢⇩g B] ≡ [⊢ A⇩1] ∧ [⊢ A⇩2] ∧ [⊢ A⇩3] ⟶ [⊢ B]"

abbreviation (input) conseq_local1::"'w σ ⇒ 'w σ ⇒ bool" ("[_ ⊢ _]") 
  where "[A ⊢ B] ≡ A ❙≤ B"
abbreviation (input) conseq_local21::"'w σ ⇒ 'w σ ⇒ 'w σ ⇒ bool" ("[_,_ ⊢ _]") 
  where "[A⇩1, A⇩2 ⊢ B] ≡ A⇩1 ❙∧ A⇩2 ❙≤ B"
abbreviation (input) conseq_local12::"'w σ ⇒ 'w σ ⇒ 'w σ ⇒ bool" ("[_ ⊢ _,_]") 
  where "[A ⊢ B⇩1, B⇩2] ≡ A ❙≤ B⇩1 ❙∨ B⇩2"
abbreviation (input) conseq_local31::"'w σ ⇒ 'w σ ⇒ 'w σ ⇒ 'w σ ⇒ bool" ("[_,_,_ ⊢ _]") 
  where "[A⇩1, A⇩2, A⇩3 ⊢ B] ≡ A⇩1 ❙∧ A⇩2 ❙∧ A⇩3 ❙≤ B"
(*add more as the need arises...*)

end