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

fixmeta found:?NaturalDeduction ❚

theory Lexicon =
example :  type ❙
Tweety_example : example ❙
Meta_Tweety_example : example ❙
have : example ⟶ prop ❙
use : example ⟶ prop ❙
standard : example ⟶ prop ❙
better_than : example ⟶ example ⟶ prop ❘# 1 better 2 ❙
met : example ⟶ prop ❙ /T should be meta but unfortunately meta is an mmt keyword, hence not usable.❙
too_complicated : example ⟶ prop ❙


❚

theory Knowledge_Base =
include ?Lexicon ❙
a : ⊦ have Tweety_example ❙
b : ⊦ have Meta_Tweety_example ❙
ax1 : ⊦ (¬ ∃[x] x better Tweety_example) ⇒ use Tweety_example ❙
ax2 : ⊦ met Meta_Tweety_example❙
ax3: ⊦ standard Tweety_example ❙
ax4 :  ⊦ (∃[x] x better Tweety_example) ⇒ ¬ use Tweety_example ❙
❚

theory Use_Tweety =
include ?Knowledge_Base ❙
c: ⊦ use Tweety_example ❙
❚

theory Not_Tweety =
include ?Knowledge_Base ❙
d: ⊦ ¬ use Tweety_example ❙
❚

// theory Joint_Inconsistency =
include ?Use_Tweety ❙
include ?Not_Tweety ❙
❚

theory Proposition =
proposition : prop❙
❚

theory Pro =
include ?Proposition ❙
pro: ⊦ proposition ❙
❚

theory Con =
include ?Proposition ❙
con:  ⊦ ¬ proposition ❙
❚

// view Contradiction : ?Conflict_Theory → ?Joint_Inconsistency =
conflict = fals_introduction c d ❙
❚

view prop_Tweety : ?Proposition → ?Lexicon =
proposition = use Tweety_example ❙
❚

view pro_Tweety : ?Pro → ?Joint_Inconsistency =
include ?prop_Tweety❙
pro = c ❙
❚

view con_Tweety : ?Con → ?Joint_Inconsistency =
include ?prop_Tweety ❙
con = d ❙
❚