Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > ax-cb1 | Unicode version |
Description: A context has type
boolean.
This and the next few axioms are not strictly necessary, and are conservative on any theorem for which every variable has a specified type, but by adding this axiom we can save some typehood hypotheses in many theorems. The easy way to see that this axiom is conservative is to note that every axiom and inference rule that constructs a theorem of the form where and are type variables, also ensures that and . Thus it is impossible to prove any theorem unless both and had been previously derived, so it is conservative to deduce from . The same remark applies to the construction of the theorem - there is only one rule that creates a formula of this type, namely wct 44, and it requires that and be previously established, so it is safe to reverse the process in wctl 31 and wctr 32. |
Ref | Expression |
---|---|
ax-cb.1 |
Ref | Expression |
---|---|
ax-cb1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hb 3 | . 2 type | |
2 | tr | . 2 term | |
3 | 1, 2 | wffMMJ2t 12 | 1 wff |
Colors of variables: type var term |
This axiom is referenced by: mpdan 33 syldan 34 trul 37 wtru 40 eqcomx 47 ancoms 49 adantr 50 ct1 52 ct2 53 sylan 54 an32s 55 anasss 56 anassrs 57 dfov1 66 dfov2 67 eqtru 76 ceq1 79 ceq2 80 oveq123 88 oveq1 89 oveq12 90 oveq2 91 oveq 92 hbxfrf 97 hbxfr 98 hbth 99 hbc 100 hbov 101 hbl 102 insti 104 clf 105 ax4g 139 ax4 140 alrimiv 141 cla4v 142 dfan2 144 hbct 145 mpd 146 imp 147 ex 148 notnot1 150 con2d 151 ecase 153 exlimdv2 156 exlimdv 157 cbvf 167 leqf 169 alrimi 170 exlimd 171 alimdv 172 eximdv 173 alnex 174 isfree 176 ac 184 exmid 186 ax3 192 ax5 194 ax11 201 axext 206 axrep 207 |
Copyright terms: Public domain | W3C validator |