namespace latin:/❚

/T A fully modular specification of intuitionistic and classical propositional
  logics.
  Every connective and all proof rules are specified in their own theories to maximize reusability.
  
  Proof rules follow natural deduction except that a judgment for inconsistency is used in some rules.
❚

/T Naming conventions for theory name suffixes
   * ND: natural deduction rules
   * I resp. E: introduction resp. elimination rules
❚

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

theory Truth =
  include ?Propositions❙
  true  : prop❙
❚

theory TruthND =
  include ?Truth❙
  include ?Proofs❙
  trueI : ⊦ true❙
❚

theory Falsity =
  include ?Propositions❙
  false  : prop❙
❚

theory FalsityND =
  include ?Falsity❙
  include ?Proofs❙
  falseE : ⊦ false ⟶ ↯❘# 1 falseE❙
❚

theory Negation =
  include ?Propositions❙
  not   : prop ⟶ prop❘# ¬ 1   prec 20❙
❚

theory NegationNDI =
  include ?Negation❙
  include ?Proofs❙
  notI  : {F} (⊦ F ⟶ ↯) ⟶ ⊦ ¬ F❘# notI 2❙
❚

theory NegationNDE =
  include ?Negation❙
  include ?Proofs❙
  notE  : {F} ⊦ ¬ F ⟶ ⊦ F ⟶ ↯❘# 2 notE 3❙
❚

theory NegationND =
  include ?NegationNDI❙
  include ?NegationNDE❙
❚

theory AlternativeNegationAndFalsityND =
  include ?Proofs ❙
  include ?Falsity ❙
  include ?Negation ❙
  include ?Disjunction ❙
  notIntroduction : {A} (⊦ A ⟶ ⊦ false) ⟶ (⊦ ¬ A) ❘ # altNotI 2 ❙
  notElimination : {A} ⊦ ¬ ¬ A ⟶ ⊦ A ❘ # altNotE 2 ❙
  falseIntroduction : {A} ⊦ ¬ A ⟶ ⊦ A ⟶ ⊦ false ❘ # altFI 2 3 ❘ role EliminationRule ❙
  falseElimination : {A} ⊦ false ⟶ ⊦ A ❘ # altFE 1 2 ❙
❚

theory Conjunction =
  include ?Propositions❙
  and   : prop ⟶ prop ⟶ prop❘# 1 ∧ 2 prec 15❙
❚

theory ConjunctionNDI =
  include ?Conjunction❙
  include ?Proofs❙
  andI  : {F,G} ⊦ F ⟶ ⊦ G ⟶ ⊦ F ∧ G❙
❚

theory ConjunctionNDE =
  include ?Conjunction❙
  include ?Proofs❙
  andEl : {F,G} ⊦ F ∧ G ⟶ ⊦ F❘# 3 andEl❘role ForwardRule❙
  andEr : {F,G} ⊦ F ∧ G ⟶ ⊦ G❘# 3 andEr❘role ForwardRule❙
❚

theory ConjunctionND =
  include ?ConjunctionNDI❙
  include ?ConjunctionNDE❙
❚

theory Disjunction =
  include ?Propositions❙
  or    : prop ⟶ prop ⟶ prop❘# 1 ∨ 2 prec 15❙
❚

theory DisjunctionNDI =
  include ?Disjunction❙
  include ?Proofs❙
  orIl  : {F,G} ⊦ F ⟶ ⊦ F ∨ G❘# 3 orIl❙
  orIr  : {F,G} ⊦ G ⟶ ⊦ F ∨ G❘# 3 orIr❙
❚

theory DisjunctionNDE =
  include ?Disjunction❙
  include ?Proofs❙
  orE   : {F,G,C} ⊦ F ∨ G ⟶ (⊦ F ⟶ ⊦ C) ⟶ (⊦ G ⟶ ⊦ C) ⟶ ⊦ C❘# 4 orE 5 6❘role EliminationRule❙
❚

theory DisjunctionND =
  include ?DisjunctionNDI❙
  include ?DisjunctionNDE❙
❚

theory Implication =
  include ?Propositions❙
  impl  : prop ⟶ prop ⟶ prop❘# 1 %R⇒ 2 prec 10❙  
❚

theory ImplicationNDI =
  include ?Implication❙
  include ?Proofs❙
  impI  : {F,G} (⊦ F ⟶ ⊦ G) ⟶ ⊦ F ⇒ G❙
❚

theory ImplicationNDE =
  include ?Implication❙
  include ?Proofs❙
  impE  : {F,G} ⊦ F ⇒ G ⟶ ⊦ F ⟶ ⊦ G❘# 3 impE 4❘role ForwardRule❙
❚

theory ImplicationND =
  include ?ImplicationNDI❙
  include ?ImplicationNDE❙
  
  total structure impl_preorder : ?Preorder =
    carrier = prop❙
    rel = [x,y] ⊦ x ⇒ y❙
    refl = [F] impI [f] f❙
    trans = [F,G,H,fg,gh] impI [f] gh impE (fg impE f)❙ 
  ❚
❚

theory Equivalence =
  include ?Propositions❙
  equiv : prop ⟶ prop ⟶ prop❘# 1 ⇔ 2 prec 10❙
 ❚

theory EquivalenceNDI =
  include ?Equivalence❙
  include ?Proofs❙
  equivI : {F,G} (⊦ F ⟶ ⊦ G) ⟶ (⊦ G ⟶ ⊦ F) ⟶ ⊦ F ⇔ G❙
❚

theory EquivalenceNDE =
  include ?Equivalence❙
  include ?Proofs❙
  equivEl : {F,G} ⊦ F ⇔ G ⟶ ⊦ F ⟶ ⊦ G❘# 3 equivEl 4❘role ForwardRule❙
  equivEr : {F,G} ⊦ F ⇔ G ⟶ ⊦ G ⟶ ⊦ F❘# 3 equivEr 4❘role ForwardRule❙
❚

theory EquivalenceND =
  include ?EquivalenceNDI❙
  include ?EquivalenceNDE❙
  
  total structure equiv_equivalence : ?EquivalenceRelation =
    carrier = prop❙
    rel = [x,y] ⊦ x ⇔ y❙
    refl = [F] equivI ([p]p) ([p]p)❙
    sym  = [F,G,p] equivI ([q] p equivEr q) ([q] p equivEl q)❙
    trans = [F,G,H,fg,gh] equivI ([f] gh equivEl (fg equivEl f))
                                 ([h] fg equivEr (gh equivEr h))❙
  ❚
❚

theory IPL =
  include ?Propositions❙
  include ?Truth❙
  include ?Falsity❙
  include ?Negation❙
  include ?Conjunction❙
  include ?Disjunction❙
  include ?Implication❙
  include ?Equivalence❙
❚

theory IPLND =
  include ?IPL❙
  include ?Logic❙
  include ?TruthND❙
  include ?FalsityND❙
  include ?NegationND❙
  include ?ConjunctionND❙
  include ?DisjunctionND❙
  include ?ImplicationND❙
  include ?EquivalenceND❙
  
  not_or_left : {F,G} ⊦ ¬(F∨G) ⟶ ⊦¬F ❘= [F,G,p] notI [q] p notE (q orIl)❙
  not_or_right : {F,G} ⊦ ¬(F∨G) ⟶ ⊦¬G ❘= [F,G,p] notI [q] p notE (q orIr)❙
  nntnd : {F} ⊦¬¬(F∨¬F)❘= [F] notI [p] (not_or_right p) notE (not_or_left p)❙

  total structure impl_order : ?Order =
    include ?ImplicationND/impl_preorder❙ 
    structure equalityRel = ?EquivalenceND/equiv_equivalence❙
    antisym = [F,G,fg,gf] equivI ([f] fg impE f) ([g] gf impE g)❙
  ❚
❚

theory Classical =
  include ?Logic❙
  classical : {F} ((⊦ F ⟶ ↯) ⟶ ↯) ⟶ ⊦ F❘# classical 2❙
❚

theory ProofIrrelevance =
  include ?Logic❙
  rule rules?TermIrrelevanceRule ded❙
❚

theory PL =
  include ?IPL❙
❚

theory PLND =
  include ?PL❙
  include ?IPLND❙
  include ?ProofIrrelevance❙
  include ?Classical❙

  indirect : {F} (⊦¬F ⟶ ↯) ⟶ ⊦ F❘= [F,h] classical [q] h (notI q)❘# indirect 2❙  
  dne : {F} ⊦¬¬F ⟶ ⊦F❘= [F,p] indirect [q] p notE q❙
  tnd : {F} ⊦F∨¬F❘= [F] dne nntnd❙
❚

/T Conjunction where the second conjunct's well-formedness may depend on the truth of the first conjunct
   Curry-Howard analogue of Sigma types ❚
theory DependentConjunction =
  include ?Logic❙
  dand   : {F} (⊦ F ⟶ prop) ⟶ prop❘# 1 ∧- 2 prec 10❙
❚

theory DependentConjunctionND =
  include ?DependentConjunction❙
  dandI  : {F,G} {p:⊦ F} ⊦ G p ⟶ ⊦ F ∧- G❙
  dandEl : {F,G} ⊦ F ∧- G ⟶ ⊦ F❘# 3 dandEl❘role ForwardRule❙
  dandEr : {F,G} {p: ⊦ F ∧- G} ⊦ G (p dandEl)❘# 3 dandEr❘role ForwardRule❙
❚

/T Disjunction where the second disjunct's well-formedness may depend on the falsity of the first disjunct
   Curry-Howard analogue of an unusual union type where the second argument is only considered if the first one is empty❚ 
theory DependentDisjunction =
  include ?Logic❙
  dor    : {F} ((⊦ F ⟶ ↯) ⟶ prop) ⟶ prop❘# 1 ∨- 2 prec 10❙
❚

theory DependentDisjunctionND =
  include ?DependentDisjunction❙
  dorIl  : {F,G} ⊦ F ⟶ ⊦ F ∨- G❘# 3 dorIl❙
  dorIr  : {F,G} ({p:⊦ F ⟶ ↯} ⊦ G p) ⟶ ⊦ F ∨- G❘# 3 dorIr❙
  dorE   : {F,G,C} ⊦ F ∨- G ⟶ (⊦ F ⟶ ⊦ C) ⟶ ({p: ⊦ F ⟶ ↯} ⊦ G p ⟶ ⊦ C) ⟶ ⊦ C❘# 4 dorE 5 6❙
❚

/T Implication where the implicate's well-formedness may depend on the truth of the implicant
   Curry-Howard analogue of Pi types ❚
theory DependentImplication =
  include ?Logic❙
  dimpl  : {F} (⊦ F ⟶ prop) ⟶ prop❘# 1 ⇒- 2 prec 10❙
❚

theory DependentImplicationND =
  include ?DependentImplication❙
  dimpI  : {F,G} ({p} ⊦ G p) ⟶ ⊦ F ⇒- G❙
  dimpE  : {F,G} ⊦ F ⇒- G ⟶ {p:⊦ F} ⊦ G p❘# 3 dimpE 4❘role ForwardRule❙
❚