namespace latin:/

/T   Interdefinability of logics is formalized in various views. ❚

import rules scala://lf.mmt.kwarc.info
fixmeta ur:?LF

/T   The views currently still need single theories as a domain and codomain, which 
  forces us to provide spurious named theories. This should be refactored when
  multi-theory domains and codomains are possible. ❚
  
theory NegationTruth =
  include ?Negation
  include ?Truth


theory NegationFalsity =
  include ?Negation
  include ?Falsity


theory NegationTruthND =
  include ?NegationTruth
  include ?NegationNDE
  include ?TruthND


theory NegationFalsityND =
  include ?NegationFalsity
  include ?NegationND
  include ?FalsityND


view FalsityNegTruth : ?Falsity  ?NegationTruth =
  include ?Propositions 
  false = ¬ true 


view FalsityNegTruthND : ?FalsityND  ?NegationTruthND =
  include ?FalsityNegTruth
  include ?Proofs
  falseE = [p] p notE trueI 


view TruthNegFalsity : ?Truth  ?NegationFalsity =
  include ?Propositions 
  true = ¬ false 


view TruthNegFalsityND : ?TruthND  ?NegationFalsityND =
  include ?Propositions  
  include ?Proofs
  include ?TruthNegFalsity
  trueI = notI [p] p falseE


theory NegationConjunction =
  include ?Negation
  include ?Conjunction


view DisjNegConj : ?Disjunction  ?NegationConjunction =
  include ?Propositions 
  or = [a,b] ¬(¬a ∧ ¬b)


theory NegationDisjunction =
  include ?Negation
  include ?Disjunction


view ConjNegDisj : ?Conjunction  ?NegationDisjunction =
  include ?Propositions 
  and = [a,b] ¬(¬a ∨ ¬b)


theory NegationImplication =
  include ?Negation
  include ?Implication


view DisjNegConj : ?Disjunction  ?NegationImplication =
  include ?Propositions 
  or = [a,b] ¬a ⇒ b


theory NegationDisjunction =
  include ?Negation
  include ?Disjunction


view ImplNegDisj : ?Implication  ?NegationDisjunction =
  include ?Propositions 
  impl = [a,b] ¬a ∨ b


theory NegationConjunction =
  include ?Negation
  include ?Conjunction


view ImplNegConj : ?Implication  ?NegationConjunction =
  include ?Propositions 
  impl = [a,b] ¬(a ∧ ¬b)


theory ImplicationConjunction =
  include ?Implication
  include ?Conjunction


view EquivImplConj : ?Equivalence  ?ImplicationConjunction =
  include ?Propositions 
  equiv = [a,b] (a ⇒ b) ∧ (b ⇒ a)


theory ImplicationFalsity =
  include ?Implication
  include ?Falsity


view NegImplFalsity : ?Negation  ?ImplicationFalsity =
  include ?Propositions 
  not = [a] a ⇒ false