c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view TruthMOD-ZF : TruthMOD -> Boolean = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BasePLMOD-ZF.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder true1 := refl.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view FalsityMOD-ZF : FalsityMOD -> Boolean = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BasePLMOD-ZF.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder false0 := refl.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view NEGMOD-ZF : NEGMOD -> Boolean = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BasePLMOD-ZF.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder not' := lambda [a] ¬ a.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder not1 := [A:ℬ] impI [p: ded A Eq ⊥] trans beta (EqcongEr ([a] ¬ a Eq ⊤) p ∖neut).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder not0 := [A:ℬ] impI [p: ded A Eq ⊤] trans beta (EqcongEr ([a] ¬ a Eq ⊥) p ∖rep).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view IMPMOD-ZF : IMPMOD -> Boolean = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BasePLMOD-ZF.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder imp' := Lambda [a] Lambda [b] a → b.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder imp1 := [A][B] impI [p] trans beta2 (EqcongEr ([x] ⊤ ∖ x Eq ⊤)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder (orE p ([q: ded A Eq ⊥] EqcongEr ([a] a ∖ B Eq ⊥) q ∖attr)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([q: ded B Eq ⊤] EqcongEr ([b] A ∖ b Eq ⊥) q ∖rep )
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder imp0 := [A][B] impI [p] trans beta2 (EqcongEr ([x] ⊤ ∖ x Eq ⊥)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder (trans (EqcongEr ([x] A ∖ x Eq A) (andEr p) ∖neut) (andEl p))
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view CONJMOD-ZF : CONJMOD -> Boolean = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BasePLMOD-ZF.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder and' := Lambda [a] Lambda [b] a ∧ b.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder and1 := [A][B] impI [p : ded A Eq ⊤ and B Eq ⊤] trans beta2
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder (EqcongEr ([x:ℬ] A ∧ x Eq ⊤)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder (EqcongEr ([x:ℬ] x ∧ ⊤ Eq ⊤) (andEl p) ∩idem)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder and0 := [A][B] impI [p : ded A Eq ⊥ or B Eq ⊥] trans beta2
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([pl : ded A Eq ⊥] EqcongEr ([x:ℬ] x ∧ B Eq ⊥) pl (EqcongEl ([x:ℬ] x Eq ⊥) ∩comm ∩attr))
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([pr : ded B Eq ⊥] EqcongEr ([x:ℬ] A ∧ x Eq ⊥) pr ∩attr)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view DISJMOD-ZF : DISJMOD -> Boolean = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include BasePLMOD-ZF.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder or' := Lambda [a] Lambda [b] a ∨ b.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder or1 := [A][B] impI [p : ded A Eq ⊤ or B Eq ⊤] trans beta2
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([pl : ded A Eq ⊤] EqcongEr ([x:ℬ] x ∨ B Eq ⊤) pl (EqcongEl ([x:ℬ] x Eq ⊤) ∪comm ∪attr))
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([pr : ded B Eq ⊤] EqcongEr ([x:ℬ] A ∨ x Eq ⊤) pr ∪attr)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder or0 := [A][B] impI [p : ded A Eq ⊥ and B Eq ⊥] trans beta2
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder (EqcongEr ([x:ℬ] A ∨ x Eq ⊥)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder (EqcongEr ([x:ℬ] x ∨ ⊥ Eq ⊥) (andEl p) ∪idem)).