P. 160 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15901-16000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bdstab 15901	Stability of a bounded formula is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED STAB ph
Theorem	bddc 15902	Decidability of a bounded formula is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED DECID ph
Theorem	bd3or 15903	A disjunction of three bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED ph   &    |- BOUNDED ps   &    |- BOUNDED ch   =>    |- BOUNDED ( ph \/ ps \/ ch )
Theorem	bd3an 15904	A conjunction of three bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED ph   &    |- BOUNDED ps   &    |- BOUNDED ch   =>    |- BOUNDED ( ph /\ ps /\ ch )
Theorem	bdth 15905	A truth (a (closed) theorem) is a bounded formula. (Contributed by BJ, 6-Oct-2019.)
|- ph   =>    |- BOUNDED ph
Theorem	bdtru 15906	The truth value T. is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED T.
Theorem	bdfal 15907	The truth value F. is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED F.
Theorem	bdnth 15908	A falsity is a bounded formula. (Contributed by BJ, 6-Oct-2019.)
|- -. ph   =>    |- BOUNDED ph
Theorem	bdnthALT 15909	Alternate proof of bdnth 15908 not using bdfal 15907. Then, bdfal 15907 can be proved from this theorem, using fal 1380. The total number of proof steps would be 17 (for bdnthALT 15909) + 3 = 20, which is more than 8 (for bdfal 15907) + 9 (for bdnth 15908) = 17. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- -. ph   =>    |- BOUNDED ph
Theorem	bdxor 15910	The exclusive disjunction of two bounded formulas is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED ph   &    |- BOUNDED ps   =>    |- BOUNDED ( ph \/_ ps )
Theorem	bj-bdcel 15911*	Boundedness of a membership formula. (Contributed by BJ, 8-Dec-2019.)
|- BOUNDED y = A   =>    |- BOUNDED A e. x
Theorem	bdab 15912	Membership in a class defined by class abstraction using a bounded formula, is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED x e. { y | ph }
Theorem	bdcdeq 15913	Conditional equality of a bounded formula is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED CondEq ( x = y -> ph )
14.2.8.2  Bounded classes In line with our definitions of classes as extensions of predicates, it is useful to define a predicate for bounded classes, which is done in df-bdc 15915. Note that this notion is only a technical device which can be used to shorten proofs of (semantic) boundedness of formulas. As will be clear by the end of this subsection (see for instance bdop 15949), one can prove the boundedness of any concrete term using only setvars and bounded formulas, for instance, |- BOUNDED ph => |- BOUNDED <. { x | ph } , ( { y , suc z } X. <. t , (/) >. ) >.. The proofs are long since one has to prove boundedness at each step of the construction, without being able to prove general theorems like |- BOUNDED A => |- BOUNDED { A }.
Syntax	wbdc 15914	Syntax for the predicate BOUNDED.
wff BOUNDED A
Definition	df-bdc 15915*	Define a bounded class as one such that membership in this class is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
|- (BOUNDED A <-> A. xBOUNDED x e. A )
Theorem	bdceq 15916	Equality property for the predicate BOUNDED. (Contributed by BJ, 3-Oct-2019.)
|- A = B   =>    |- (BOUNDED A <-> BOUNDED B )
Theorem	bdceqi 15917	A class equal to a bounded one is bounded. Note the use of ax-ext 2188. See also bdceqir 15918. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- A = B   =>    |- BOUNDED B
Theorem	bdceqir 15918	A class equal to a bounded one is bounded. Stated with a commuted (compared with bdceqi 15917) equality in the hypothesis, to work better with definitions ( B is the definiendum that one wants to prove bounded; see comment of bd0r 15899). (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- B = A   =>    |- BOUNDED B
Theorem	bdel 15919*	The belonging of a setvar in a bounded class is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
|- (BOUNDED A -> BOUNDED x e. A )
Theorem	bdeli 15920*	Inference associated with bdel 15919. Its converse is bdelir 15921. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED x e. A
Theorem	bdelir 15921*	Inference associated with df-bdc 15915. Its converse is bdeli 15920. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED x e. A   =>    |- BOUNDED A
Theorem	bdcv 15922	A setvar is a bounded class. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED x
Theorem	bdcab 15923	A class defined by class abstraction using a bounded formula is bounded. (Contributed by BJ, 6-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED { x | ph }
Theorem	bdph 15924	A formula which defines (by class abstraction) a bounded class is bounded. (Contributed by BJ, 6-Oct-2019.)
|- BOUNDED { x | ph }   =>    |- BOUNDED ph
Theorem	bds 15925*	Boundedness of a formula resulting from implicit substitution in a bounded formula. Note that the proof does not use ax-bdsb 15896; therefore, using implicit instead of explicit substitution when boundedness is important, one might avoid using ax-bdsb 15896. (Contributed by BJ, 19-Nov-2019.)
|- BOUNDED ph   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- BOUNDED ps
Theorem	bdcrab 15926*	A class defined by restricted abstraction from a bounded class and a bounded formula is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- BOUNDED ph   =>    |- BOUNDED { x e. A | ph }
Theorem	bdne 15927	Inequality of two setvars is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED x =/= y
Theorem	bdnel 15928*	Non-membership of a setvar in a bounded formula is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED x e/ A
Theorem	bdreu 15929*	Boundedness of existential uniqueness. Remark regarding restricted quantifiers: the formula A. x e. A ph need not be bounded even if A and ph are. Indeed, _V is bounded by bdcvv 15931, and |- ( A. x e. _V ph <-> A. x ph ) (in minimal propositional calculus), so by bd0 15898, if A. x e. _V ph were bounded when ph is bounded, then A. x ph would be bounded as well when ph is bounded, which is not the case. The same remark holds with E. , E! , E*. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED E! x e. y ph
Theorem	bdrmo 15930*	Boundedness of existential at-most-one. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED E* x e. y ph
Theorem	bdcvv 15931	The universal class is bounded. The formulation may sound strange, but recall that here, "bounded" means "Δ0". (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED _V
Theorem	bdsbc 15932	A formula resulting from proper substitution of a setvar for a setvar in a bounded formula is bounded. See also bdsbcALT 15933. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED ph   =>    |- BOUNDED [. y / x ]. ph
Theorem	bdsbcALT 15933	Alternate proof of bdsbc 15932. (Contributed by BJ, 16-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- BOUNDED ph   =>    |- BOUNDED [. y / x ]. ph
Theorem	bdccsb 15934	A class resulting from proper substitution of a setvar for a setvar in a bounded class is bounded. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED [_ y / x ]_ A
Theorem	bdcdif 15935	The difference of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- BOUNDED B   =>    |- BOUNDED ( A \ B )
Theorem	bdcun 15936	The union of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- BOUNDED B   =>    |- BOUNDED ( A u. B )
Theorem	bdcin 15937	The intersection of two bounded classes is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   &    |- BOUNDED B   =>    |- BOUNDED ( A i^i B )
Theorem	bdss 15938	The inclusion of a setvar in a bounded class is a bounded formula. Note: apparently, we cannot prove from the present axioms that equality of two bounded classes is a bounded formula. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED x C_ A
Theorem	bdcnul 15939	The empty class is bounded. See also bdcnulALT 15940. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED (/)
Theorem	bdcnulALT 15940	Alternate proof of bdcnul 15939. Similarly, for the next few theorems proving boundedness of a class, one can either use their definition followed by bdceqir 15918, or use the corresponding characterizations of its elements followed by bdelir 15921. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- BOUNDED (/)
Theorem	bdeq0 15941	Boundedness of the formula expressing that a setvar is equal to the empty class. (Contributed by BJ, 21-Nov-2019.)
|- BOUNDED x = (/)
Theorem	bj-bd0el 15942	Boundedness of the formula "the empty set belongs to the setvar x". (Contributed by BJ, 30-Nov-2019.)
|- BOUNDED (/) e. x
Theorem	bdcpw 15943	The power class of a bounded class is bounded. (Contributed by BJ, 3-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED ~P A
Theorem	bdcsn 15944	The singleton of a setvar is bounded. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED { x }
Theorem	bdcpr 15945	The pair of two setvars is bounded. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED { x , y }
Theorem	bdctp 15946	The unordered triple of three setvars is bounded. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED { x , y , z }
Theorem	bdsnss 15947*	Inclusion of a singleton of a setvar in a bounded class is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED { x } C_ A
Theorem	bdvsn 15948*	Equality of a setvar with a singleton of a setvar is a bounded formula. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED x = { y }
Theorem	bdop 15949	The ordered pair of two setvars is a bounded class. (Contributed by BJ, 21-Nov-2019.)
|- BOUNDED <. x , y >.
Theorem	bdcuni 15950	The union of a setvar is a bounded class. (Contributed by BJ, 15-Oct-2019.)
|- BOUNDED U. x
Theorem	bdcint 15951	The intersection of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED |^| x
Theorem	bdciun 15952*	The indexed union of a bounded class with a setvar indexing set is a bounded class. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED U_ x e. y A
Theorem	bdciin 15953*	The indexed intersection of a bounded class with a setvar indexing set is a bounded class. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED A   =>    |- BOUNDED |^|_ x e. y A
Theorem	bdcsuc 15954	The successor of a setvar is a bounded class. (Contributed by BJ, 16-Oct-2019.)
|- BOUNDED suc x
Theorem	bdeqsuc 15955*	Boundedness of the formula expressing that a setvar is equal to the successor of another. (Contributed by BJ, 21-Nov-2019.)
|- BOUNDED x = suc y
Theorem	bj-bdsucel 15956	Boundedness of the formula "the successor of the setvar x belongs to the setvar y". (Contributed by BJ, 30-Nov-2019.)
|- BOUNDED suc x e. y
Theorem	bdcriota 15957*	A class given by a restricted definition binder is bounded, under the given hypotheses. (Contributed by BJ, 24-Nov-2019.)
|- BOUNDED ph   &    |- E! x e. y ph   =>    |- BOUNDED ( iota_ x e. y ph )
14.2.9  CZF: Bounded separation In this section, we state the axiom scheme of bounded separation, which is part of CZF set theory.
Axiom	ax-bdsep 15958*	Axiom scheme of bounded (or restricted, or Δ0) separation. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. For the full axiom of separation, see ax-sep 4170. (Contributed by BJ, 5-Oct-2019.)
|- BOUNDED ph   =>    |- A. a E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
Theorem	bdsep1 15959*	Version of ax-bdsep 15958 without initial universal quantifier. (Contributed by BJ, 5-Oct-2019.)
|- BOUNDED ph   =>    |- E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
Theorem	bdsep2 15960*	Version of ax-bdsep 15958 with one disjoint variable condition removed and without initial universal quantifier. Use bdsep1 15959 when sufficient. (Contributed by BJ, 5-Oct-2019.)
|- BOUNDED ph   =>    |- E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
Theorem	bdsepnft 15961*	Closed form of bdsepnf 15962. Version of ax-bdsep 15958 with one disjoint variable condition removed, the other disjoint variable condition replaced by a nonfreeness antecedent, and without initial universal quantifier. Use bdsep1 15959 when sufficient. (Contributed by BJ, 19-Oct-2019.)
|- BOUNDED ph   =>    |- ( A. x F/ b ph -> E. b A. x ( x e. b <-> ( x e. a /\ ph ) ) )
Theorem	bdsepnf 15962*	Version of ax-bdsep 15958 with one disjoint variable condition removed, the other disjoint variable condition replaced by a nonfreeness hypothesis, and without initial universal quantifier. See also bdsepnfALT 15963. Use bdsep1 15959 when sufficient. (Contributed by BJ, 5-Oct-2019.)
|- F/ b ph   &    |- BOUNDED ph   =>    |- E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
Theorem	bdsepnfALT 15963*	Alternate proof of bdsepnf 15962, not using bdsepnft 15961. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ b ph   &    |- BOUNDED ph   =>    |- E. b A. x ( x e. b <-> ( x e. a /\ ph ) )
Theorem	bdzfauscl 15964*	Closed form of the version of zfauscl 4172 for bounded formulas using bounded separation. (Contributed by BJ, 13-Nov-2019.)
|- BOUNDED ph   =>    |- ( A e. V -> E. y A. x ( x e. y <-> ( x e. A /\ ph ) ) )
Theorem	bdbm1.3ii 15965*	Bounded version of bm1.3ii 4173. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- BOUNDED ph   &    |- E. x A. y ( ph -> y e. x )   =>    |- E. x A. y ( y e. x <-> ph )
Theorem	bj-axemptylem 15966*	Lemma for bj-axempty 15967 and bj-axempty2 15968. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4178 instead. (New usage is discouraged.)
|- E. x A. y ( y e. x -> F. )
Theorem	bj-axempty 15967*	Axiom of the empty set from bounded separation. It is provable from bounded separation since the intuitionistic FOL used in iset.mm assumes a nonempty universe. See axnul 4177. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4178 instead. (New usage is discouraged.)
|- E. x A. y e. x F.
Theorem	bj-axempty2 15968*	Axiom of the empty set from bounded separation, alternate version to bj-axempty 15967. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 4178 instead. (New usage is discouraged.)
|- E. x A. y -. y e. x
Theorem	bj-nalset 15969*	nalset 4182 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. E. x A. y y e. x
Theorem	bj-vprc 15970	vprc 4184 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. _V e. _V
Theorem	bj-nvel 15971	nvel 4185 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. _V e. A
Theorem	bj-vnex 15972	vnex 4183 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- -. E. x x = _V
Theorem	bdinex1 15973	Bounded version of inex1 4186. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED B   &    |- A e. _V   =>    |- ( A i^i B ) e. _V
Theorem	bdinex2 15974	Bounded version of inex2 4187. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED B   &    |- A e. _V   =>    |- ( B i^i A ) e. _V
Theorem	bdinex1g 15975	Bounded version of inex1g 4188. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED B   =>    |- ( A e. V -> ( A i^i B ) e. _V )
Theorem	bdssex 15976	Bounded version of ssex 4189. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   &    |- B e. _V   =>    |- ( A C_ B -> A e. _V )
Theorem	bdssexi 15977	Bounded version of ssexi 4190. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   &    |- B e. _V   &    |- A C_ B   =>    |- A e. _V
Theorem	bdssexg 15978	Bounded version of ssexg 4191. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   =>    |- ( ( A C_ B /\ B e. C ) -> A e. _V )
Theorem	bdssexd 15979	Bounded version of ssexd 4192. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- ( ph -> B e. C )   &    |- ( ph -> A C_ B )   &    |- BOUNDED A   =>    |- ( ph -> A e. _V )
Theorem	bdrabexg 15980*	Bounded version of rabexg 4195. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED ph   &    |- BOUNDED A   =>    |- ( A e. V -> { x e. A | ph } e. _V )
Theorem	bj-inex 15981	The intersection of two sets is a set, from bounded separation. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
|- ( ( A e. V /\ B e. W ) -> ( A i^i B ) e. _V )
Theorem	bj-intexr 15982	intexr 4202 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- ( |^| A e. _V -> A =/= (/) )
Theorem	bj-intnexr 15983	intnexr 4203 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.)
|- ( |^| A = _V -> -. |^| A e. _V )
Theorem	bj-zfpair2 15984	Proof of zfpair2 4262 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- { x , y } e. _V
Theorem	bj-prexg 15985	Proof of prexg 4263 using only bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- ( ( A e. V /\ B e. W ) -> { A , B } e. _V )
Theorem	bj-snexg 15986	snexg 4236 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- ( A e. V -> { A } e. _V )
Theorem	bj-snex 15987	snex 4237 from bounded separation. (Contributed by BJ, 5-Oct-2019.) (Proof modification is discouraged.)
|- A e. _V   =>    |- { A } e. _V
Theorem	bj-sels 15988*	If a class is a set, then it is a member of a set. (Copied from set.mm.) (Contributed by BJ, 3-Apr-2019.)
|- ( A e. V -> E. x A e. x )
Theorem	bj-axun2 15989*	axun2 4490 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.)
|- E. y A. z ( z e. y <-> E. w ( z e. w /\ w e. x ) )
Theorem	bj-uniex2 15990*	uniex2 4491 from bounded separation. (Contributed by BJ, 15-Oct-2019.) (Proof modification is discouraged.)
|- E. y y = U. x
Theorem	bj-uniex 15991	uniex 4492 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- A e. _V   =>    |- U. A e. _V
Theorem	bj-uniexg 15992	uniexg 4494 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- ( A e. V -> U. A e. _V )
Theorem	bj-unex 15993	unex 4496 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- A e. _V   &    |- B e. _V   =>    |- ( A u. B ) e. _V
Theorem	bdunexb 15994	Bounded version of unexb 4497. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- BOUNDED A   &    |- BOUNDED B   =>    |- ( ( A e. _V /\ B e. _V ) <-> ( A u. B ) e. _V )
Theorem	bj-unexg 15995	unexg 4498 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- ( ( A e. V /\ B e. W ) -> ( A u. B ) e. _V )
Theorem	bj-sucexg 15996	sucexg 4554 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- ( A e. V -> suc A e. _V )
Theorem	bj-sucex 15997	sucex 4555 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.)
|- A e. _V   =>    |- suc A e. _V
14.2.9.1  Delta_0-classical logic
Axiom	ax-bj-d0cl 15998	Axiom for Δ0-classical logic. (Contributed by BJ, 2-Jan-2020.)
|- BOUNDED ph   =>    |- DECID ph
Theorem	bj-d0clsepcl 15999	Δ0-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.)
|- DECID ph
14.2.9.2  Inductive classes and the class of natural number ordinals
Syntax	wind 16000	Syntax for inductive classes.
wff Ind A