propositional/model_theory/bool-zf.elf

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder%read "bool.elf".
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder%read "../../../set_theories/zfc/bool.elf".
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder%read "../../meta/sttifol-zf.elf".
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder%view Bool-ZF : Bool -> Boolean = {
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder   %include STTIFOLEQ-ZF.
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder   bool' := cbool.
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder   0     := ⊥.
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder   1     := ⊤.
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder   cons  := ccons.
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder   boole := ctnd.
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder   ifte  := Lambda [c] Lambda [t] Lambda [e] ifte c t e.
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder   ifteT := [C][T][E] impI [p] trans beta3 (EqcongEr ([x] ifte x T E Eq T) p ifte1).
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder   ifteE := [C][T][E] impI [p] trans beta3 (EqcongEr ([x] ifte x T E Eq E) p ifte0).
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder}.