Higher-Order Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HOLE Home  >  Th. List  >  ax-cb1 Unicode version

Axiom ax-cb1 29
 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.
Hypothesis
Ref Expression
ax-cb.1
Assertion
Ref Expression
ax-cb1

Detailed syntax breakdown of Axiom ax-cb1
StepHypRef Expression
1 hb 3 . 2 type
2 tr . 2 term
31, 2wffMMJ2t 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