namespace http://mathhub.info/ALMANAC/JLogic/Context_Graph❚
import found http://mathhub.info/MitM/Foundation ❚

theory ABA : found:?NaturalDeduction =

assumption: bool ⟶ type ❘ # |~ 1 prec -500❙
aid: {X} |~ X ⟶ ⊦ X ❘ # aid 2 ❙
❚

theory Contrary : ?ABA =
contrary = not❘# con 1 ❙
❚

theory Convenience : ?ABA =
include ?Contrary ❙
/T some derivable rules for convenience:❙
or_elim: {A,B,C} ⊦ (A ∨ B) ⟶ (⊦ A ⟶ ⊦ C) ⟶ (⊦ B ⟶ ⊦ C) ⟶ ⊦ C ❘ # orel 4 5 6❙
double_negation_introduction: {A} ⊦ A ⟶ ⊦ (¬ ¬ A) ❘ # NI 2 ❙
quantifier_exchange : {A:𝒰 100, B: A ⟶ prop} (⊦ ¬ ∃ [x:A] B x) ⟶ (⊦ ∀ [x:A] ¬ B x) ❘# exch 3❙
❚

fixmeta ?Convenience ❚

theory Arg1 =
include ?Knowledge_Base ❙
a1 : |~ ¬ use Tweety_example ❙
❚

theory Arg2 =
include ?Knowledge_Base ❙
a2 : |~ ¬ ∃[x] x better Tweety_example ❙
❚

theory Kernel =
w: prop ❙
❚

theory Assumption =
include ?Kernel ❙
con1: |~ w ❙
❚

theory Defeater =
include ?Kernel ❙
con2: ⊦ con w ❙
❚

view δ : ?Kernel → ?Knowledge_Base =
w = ¬ use Tweety_example ❙
❚

view φ : ?Assumption → ?Arg1 =
include ?δ❙
con1 = a1 ❙
❚

view ψ : ?Defeater → ?Arg2 =
include ?δ❙
con2 = NI (MP ax1 (aid a2)) ❙
❚