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

fixmeta ?Convenience ❚

theory Ordinary_Premise =
include ?Knowledge_Base ❙
op: ⊦ ¬ too_complicated Meta_Tweety_example ❙

❚

theory Too_Complicated_Cond =
include ?Lexicon ❙
comp:  example ❙
comp_ax: ⊦ met comp  ❙

❚

theory Too_Complicated_Rule =
include ?Too_Complicated_Cond ❙
too_complicated_proposition = too_complicated comp❙
too_complicated_rule: |~ met comp ⇒ too_complicated_proposition❙
too_complicated_arg : ⊦ too_complicated_proposition ❘= MP (aid too_complicated_rule) comp_ax❙
❚

view its_complicated : ?Too_Complicated_Cond → ?Knowledge_Base =
include ?Lexicon❙
comp = Meta_Tweety_example ❙
comp_ax = ax2❙
❚

theory Too_Complicated_Pushout =
include ?Knowledge_Base ❙
too_complicated_app: |~ met Meta_Tweety_example ⇒ too_complicated Meta_Tweety_example❙
too_complicated_met : ⊦ too_complicated Meta_Tweety_example ❘= MP (aid too_complicated_app) ax2❙
❚

view met_is_complicated : ?Too_Complicated_Rule → ?Too_Complicated_Pushout =
include ?its_complicated❙
too_complicated_rule = too_complicated_app ❙
too_complicated_arg = too_complicated_met ❙
❚

view Prop_complicated : ?Proposition → ?Knowledge_Base =
proposition = too_complicated Meta_Tweety_example ❙
❚

view Pro_complicated : ?Pro → ?Too_Complicated_Pushout =
include ?Prop_complicated ❙
pro = too_complicated_met ❙
❚

view Con_complicated : ?Con → ?Ordinary_Premise =
include ?Prop_complicated ❙
con = op ❙
❚

theory Meta_is_Better_Cond =
include ?Lexicon ❙
ex1 : example ❙
ex2 : example❙
cond_normal : ⊦ standard ex2 ❙
cond_met : ⊦ met ex1❙

❚

theory Meta_is_Better_Rule =
include ?Meta_is_Better_Cond ❙
better_proposition = ex1 better ex2❙
better_rule : |~ met ex1 ∧ standard ex2 ⇒ better_proposition❙
better_arg : ⊦ better_proposition ❘ = MP (aid better_rule) and_introduction cond_met cond_normal ❙

❚

view its_better : ?Meta_is_Better_Cond → ?Ordinary_Premise =
include ?Lexicon❙
ex1 = Meta_Tweety_example ❙
ex2 = Tweety_example ❙
cond_met = ax2❙
cond_normal = ax3 ❙
❚

theory Meta_Pushout =
include ?Ordinary_Premise ❙
met_Tweety_better_proposition = Meta_Tweety_example better Tweety_example❙
met_Tweety_better_rule : |~ met Meta_Tweety_example ∧ standard Tweety_example ⇒ met_Tweety_better_proposition❙
better_arg : ⊦ met_Tweety_better_proposition ❘ = MP (aid met_Tweety_better_rule) and_introduction ax2 ax3 ❙
❚

theory Dont_Use_Tweety_Example =
include ?Meta_Pushout ❙
no_Tweety: ⊦ ¬ use Tweety_example❙
❚

view conservatively_Dont_Use_Tweety : ?Dont_Use_Tweety_Example → ?Meta_Pushout  =
include ?Meta_Pushout ❙
no_Tweety =  MP ax4 (existsI better_arg)❙
❚

theory Default_Cond =
Prop : bool ❙
❚

theory Default_Rule =
include ?Default_Cond ❙
default_proposition = Prop ❙
default : |~ ¬ default_proposition ❙
❚

view Default_App_Knowledge_Base : ?Default_Cond → ?Knowledge_Base =
Prop = ∃[x] x better Tweety_example ❙

❚

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

view Pushout_Along_Default_App : ?Default_Rule → ?Def_Pushout =
include ?Default_App_Knowledge_Base ❙
default = Def_better ❙
❚

theory Use_Tweety =
include ?Def_Pushout ❙
Tweety : ⊦ use Tweety_example❙
❚

view conservatively_Use_Tweety : ?Use_Tweety → ?Def_Pushout =
include ?Def_Pushout ❙
Tweety =  MP ax1 (aid Def_better)❙
❚

view undercut1 : ?Kernel → ?Knowledge_Base =
w= met Meta_Tweety_example ∧ standard Tweety_example ⇒ Meta_Tweety_example better Tweety_example ❙
❚

view undercut2 : ?Assumption → ?Meta_Pushout =
include ?undercut1 ❙
con1 = met_Tweety_better_rule❙
❚

view undercut3 : ?Defeater → ?Def_Pushout =
include ?undercut1 ❙
con2 = not_introduction [x](fals_introduction (MP x (and_introduction ax2 ax3)) forallE (exch aid Def_better) Meta_Tweety_example) ❙
❚