P. 11 of Theorem List - bfol.mm Proof Explorer

Theorem List for bfol.mm Proof Explorer - 1001-1100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	exe-P7r.VR12of2 1001*	exe-P7r 998 with two variable restrictions. † '𝑥' cannot occur in either '𝛾' or '𝜓'.
⊢ (𝛾 → (𝜑 → 𝜓))    &   ⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	exe-P7r.RC 1002	Inference Form of exe-P7r 998. †
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → 𝜓)    &   ⊢ ∃𝑥𝜑    ⇒   ⊢ 𝜓
Theorem	exe-P7r.RC.VR 1003*	exe-P7r.RC 1002 with variable restriction. † '𝑥' cannot occur in '𝜓'.
⊢ (𝜑 → 𝜓)    &   ⊢ ∃𝑥𝜑    ⇒   ⊢ 𝜓
8.3.2.1  alle-P7 and exi-P7 Combined.
Theorem	alleexi-P7 1004	'∀' Elimination and '∃' Introduction Combined. †
⊢ (𝛾 → ∀𝑥𝜑)    ⇒   ⊢ (𝛾 → ∃𝑥𝜑)
Theorem	alleexi-P7.RC 1005	Inference Form of alleexi-P7 1004. †
⊢ ∀𝑥𝜑    ⇒   ⊢ ∃𝑥𝜑
Theorem	alleexi-P7.CL 1006	Closed Form of alleexi-P7 1004. †
⊢ (∀𝑥𝜑 → ∃𝑥𝜑)
8.3.2.2  Variants of alli-P7 and exe-P7.
Theorem	allic-P7 1007	Introduce Universal Quantifier as Consequent. † The inference form is alli-P7r 990.
⊢ Ⅎ𝑥𝛾    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (𝜑 → ∀𝑥𝜓))
Theorem	allic-P7.VR1of2 1008*	allic-P7 1007 with one variable restriction. † '𝑥' cannot occur in '𝛾'.
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (𝜑 → ∀𝑥𝜓))
Theorem	allic-P7.VR2of2 1009*	allic-P7 1007 with one variable restriction. † '𝑥' cannot occur in '𝜑'.
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (𝜑 → ∀𝑥𝜓))
Theorem	allic-P7.VR12of2 1010*	allic-P7 1007 with two variable restrictions. † '𝑥' cannot occur in either '𝛾' or '𝜑'.
⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (𝜑 → ∀𝑥𝜓))
Theorem	exia-P7r 1011	Introduce Existential Quantifier as Antecedent. † This is the restatement of a previously proven result. Do not use in proofs. Use exia-P7 953 instead.
⊢ Ⅎ𝑥𝛾    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∃𝑥𝜑 → 𝜓))
Theorem	exia-P7r.VR1of2 1012*	exia-P7r 1011 with one variable restriction. † '𝑥' cannot occur in '𝛾'.
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∃𝑥𝜑 → 𝜓))
Theorem	exia-P7r.VR2of2 1013*	exia-P7r 1011 with one variable restriction. † '𝑥' cannot occur in '𝜓'.
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∃𝑥𝜑 → 𝜓))
Theorem	exia-P7r.VR12of2 1014*	exia-P7r 1011 with two variable restrictions. † '𝑥' cannot occur in either '𝛾' or '𝜓'.
⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∃𝑥𝜑 → 𝜓))
Theorem	exia-P7r.RC 1015	Inference Form of exia-P7r 1011. † This is the restatement of a previously proven result. Do not use in proofs. Use exia-P7 953 instead.
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → 𝜓)
Theorem	exia-P7r.RC.VR 1016*	exia-P7r.RC 1015 with variable restriction. † '𝑥' cannot occur in '𝜓'.
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → 𝜓)
8.3.3  Distributive Laws Producing Universal Quantifiers.
Theorem	alloverim-P7r 1017	'∀𝑥' Distributes Over '→'. † The closed form is axL4-P7 945. This is the restatement of a previously proven result. Do not use in proofs. Use alloverim-P7 970 instead.
⊢ (𝛾 → ∀𝑥(𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	alloverim-P7r.RC 1018	Inference Form of alloverim-P7r 1017. †
⊢ ∀𝑥(𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)
Theorem	alloverim-P7r.GENF 1019	alloverim-P7r 1017 with generalization augmentation (non-freeness condition). † This is the restatement of a previously proven result. Do not use in proofs. Use alloverim-P7.GENF 971 instead.
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	alloverim-P7r.GENV 1020*	alloverim-P7r 1017 with generalization augmentation (variable restriction). † '𝑥' cannot occur in '𝛾'.
⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	alloverim-P7r.GENF.RC 1021	Inference Form of alloverim-P7r.GENF 1019. † This is the restatement of a previously proven result. Do not use in proofs. Use alloverim-P7.GENF.RC 972 instead.
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)
Theorem	dalloverim-P7 1022	Double '∀𝑥' Distribution Over '→'. †
⊢ (𝛾 → ∀𝑥(𝜑 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
Theorem	dalloverim-P7.RC 1023	Inference Form of dalloverim-P7 1022. †
⊢ ∀𝑥(𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Theorem	dalloverim-P7.CL 1024	Closed Form of dalloverim-P7 1022. †
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
Theorem	dalloverim-P7.GENF 1025	dalloverim-P7 1022 with generalization augmentation (non-freeness condition). †
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → (𝜑 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
Theorem	dalloverim-P7.GENV 1026*	dalloverim-P7 1022 with generalization augmentation (variable restriction). † '𝑥' cannot occur in '𝛾'.
⊢ (𝛾 → (𝜑 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
Theorem	dalloverim-P7.GENF.RC 1027	Inference form of dalloverim-P7.GENF 1025. †
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
8.3.4  Distributive Laws Producing Existential Quantifiers.
Theorem	alloverimex-P7r 1028	Alternate version of alloverim-P7r 1017 that produces existential quantifiers. † The closed form is axL4ex-P7 946. This is a restatement of a previously proven result. Do not use in proofs. Use alloverimex-P7 948 instead.
⊢ (𝛾 → ∀𝑥(𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	alloverimex-P7r.RC 1029	Inference Form of alloverimex-P7 948. †
⊢ ∀𝑥(𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)
Theorem	alloverimex-P7r.GENF 1030	alloverimex-P7r 1028 with generalization augmentation (non-freeness condition). † This is a restatement of a previously proven result. Do not use in proofs. Use alloverimex-P7.GENF 949 instead.
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	alloverimex-P7r.GENV 1031*	alloverimex-P7r 1028 with generalization augmentation (variable restriction). † '𝑥' cannot occur in '𝛾'.
⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	alloverimex-P7r.GENF.RC 1032	Inference Form of alloverimex-P7r.GENF 1030. † This is a restatement of a previously proven result. Do not use in proofs. Use alloverimex-P7.GENF.RC 950 instead.
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)
Theorem	dalloverimex-P7 1033	Alternate version of dalloverim-P7 1022 that produces existential quantifiers. †
⊢ (𝛾 → ∀𝑥(𝜑 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)))
Theorem	dalloverimex-P7.RC 1034	Inference Form of dalloverimex-P7 1033. †
⊢ ∀𝑥(𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	dalloverimex-P7.CL 1035	Closed Form of dalloverimex-P7 1033. †
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)))
Theorem	dalloverimex-P7.GENF 1036	dalloverimex-P7 1033 with generalization augmentation (non-freeness condition). †
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → (𝜑 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)))
Theorem	dalloverimex-P7.GENV 1037*	dalloverimex-P7 1033 with generalization augmentation (variable restriction). † '𝑥' cannot occur in '𝛾'.
⊢ (𝛾 → (𝜑 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)))
Theorem	dalloverimex-P7.GENF.RC 1038	Inference Form of dalloverimex-P7.GENF 1036. †
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
8.3.5  Quantifier Substitution Laws.
Theorem	suball-P7r 1039	Substitution Law for '∀𝑥' (non-freeness condition). † This is the restatement of a previously proven result. Do not use in proofs. Use suball-P7 973 instead.
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
Theorem	suball-P7r.VR 1040*	Substitution Law for '∀𝑥' (variable restriction). † '𝑥' cannot occur in '𝛾'.
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
Theorem	suball-P7r.RC 1041	Inference Form of suball-P7r 1039. † This is the restatement of a previously proven result. Do not use in proofs. Use suball-P7.RC 974 instead.
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓)
Theorem	subex-P7 1042	Substitution Law for '∃𝑥' (non-freeness condition). †
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
Theorem	subex-P7.VR 1043*	Substitution Law for '∃𝑥' (variable restriction). † '𝑥' cannot occur in '𝛾'.
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
Theorem	subex-P7.RC 1044	Inference Form of subex-P7 1042. †
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)
8.3.6  Dual Properties of Universal / Existential Quantification. '(∃𝑥𝜑 ↔ ¬ ∀¬ 𝜑)' is dfexists-P7 959.
Theorem	allnegex-P7r 1045	"For all not" is Equivalent to "Does not exist". † This statement is deducible with intuitionist logic. This is the restatement of a previously proven result. Do not use in proofs. Use allnegex-P7 958 instead.
⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
Theorem	exnegall-P7 1046	"There exists a negative" is Equivalent to "Not for all". This statement is not deducible with intuitionist logic.
⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
Theorem	exnegallint-P7 1047	"There exists a negative" Implies "Not for all". † This direction is deducible with intuitionist logic.
⊢ (∃𝑥 ¬ 𝜑 → ¬ ∀𝑥𝜑)
Theorem	allasex-P7 1048	Dual of dfexists-P7 959. This statement is not deducible with intuitionist logic.
⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
8.3.7  Quantified Implication Equivalence Laws.
Theorem	qimeqallhalf-P7r 1049	Partial Quantified Implication Equivalence Law ( ( E → U ) → U ). † The reverse implication is also true if '𝑥' is ENF in either '𝜑' (see qimeqalla-P7 1050) or '𝜓' (see qimeqallb-P7r 1052). This is the restatement of a previously proven result. Do not use in proofs. Use qimeqallhalf-P7 975 instead.
⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
Theorem	qimeqalla-P7 1050	Quantified Implication Equivalence Law ( U ↔ ( E → U ) ) (non-freeness condition a). †
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓))
Theorem	qimeqalla-P7.VR 1051*	qimeqalla-P7 1050 with variable restriction. † '𝑥' cannot occur in '𝜑'.
⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓))
Theorem	qimeqallb-P7r 1052	Quantified Implication Equivalence Law ( U ↔ ( E → U ) ) (non-freeness condition b). † This is the restatement of a previously proven result. Do not use in proofs. Use qimeqallb-P7 976 instead.
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓))
Theorem	qimeqallb-P7r.VR 1053*	qimeqallb-P7r 1052 with variable restriction. † '𝑥' cannot occur in '𝜓'.
⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓))
Theorem	qimeqex-P7-L1 1054	Lemma for qimeqex-P7 1056. [Auxiliary lemma - not displayed.]
Theorem	qimeqex-P7-L2 1055	Lemma for qimeqex-P7 1056. † [Auxiliary lemma - not displayed.]
Theorem	qimeqex-P7 1056	Quantified Implication Equivalence Law ( E ↔ ( U → E ) ). This statement is not deducible with intuitionist logic.
⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
Theorem	qimeqexint-P7 1057	One Direction of Quantified Implication Equivalence Law ( E → ( U → E ) ). † This direction is deducible with intuitionist logic.
⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
8.3.8  Quantifier Commutivity Laws.
Theorem	allcomm-P7 1058*	Universal Quantifier Commutivity. †
⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑)
Theorem	excomm-P7 1059*	Existential Quantifier Commutivity. †
⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)
8.3.9  Change of Bound Variable Laws.
Theorem	cbvall-P7-L1 1060*	Lemma for cbvall-P7 1061. † [Auxiliary lemma - not displayed.]
Theorem	cbvall-P7 1061*	Change of Bound Variable Theorem for '∀𝑥'. †
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvall-P7.VR1of2 1062*	cbvall-P7 1061 with one variable restriction. † '𝑥' cannot occur in '𝜓'.
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvall-P7.VR2of2 1063*	cbvall-P7 1061 with one variable restriction. † '𝑦' cannot occur in '𝜑'.
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvall-P7.VR12of2 1064*	cbvall-P7 1061 with two variable restrictions. † '𝑥' cannot occur in '𝜓' and '𝑦' cannot occur in '𝜑'.
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvex-P7-L1 1065*	Lemma for cbvex-P7 1066. † [Auxiliary lemma - not displayed.]
Theorem	cbvex-P7 1066*	Change of Bound Variable Theorem for '∃𝑥'. †
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	cbvex-P7.VR1of2 1067*	cbvex-P7 1066 with one variable restriction. † '𝑥' cannot occur in '𝜓'.
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	cbvex-P7.VR2of2 1068*	cbvex-P7 1066 with one variable restriction. † '𝑦' cannot occur in '𝜑'.
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	cbvex-P7.VR12of2 1069*	cbvex-P7 1066 with two variable restrictions. † '𝑥' cannot occur in '𝜓' and '𝑦' cannot occur in '𝜑'.
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
8.3.9.1  Proper Substitution Variants of cbvall-P7 and cbvex-P7.
Theorem	cbvallpsub-P7 1070*	Change of Bound Variable for '∀𝑥' with Proper Substitution. †
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	cbvallpsub-P7.VR 1071*	cbvallpsub-P7 1070 with variable restriction. † '𝑦' cannot occur in '𝜑'.
⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	cbvexpsub-P7 1072*	Change of Bound Variable for '∃𝑥' with Proper Substitution. †
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑)
Theorem	cbvexpsub-P7.VR 1073*	cbvexpsub-P7 1072 with variable restriction. † '𝑦' cannot occur in '𝜑'.
⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑)
8.4  Examples.
8.4.1  Conditional Non-Freeness Does Not Always Imply Effective Non-Freeness.
Theorem	example-E7.1a 1074*	'𝑥' is conditionally not free in the statement '(𝑥 ⋅ 𝑦) = 0' when '𝑦 = 0'. † Since no arithmetic axioms have been introduced, we state '(𝑥 ⋅ 0) = 0' as a hypothesis.
⊢ (𝑥 ⋅ 0) = 0    ⇒   ⊢ (𝑦 = 0 → Ⅎ𝑥 (𝑥 ⋅ 𝑦) = 0)
Theorem	example-E7.1b 1075*	'𝑥' is effectively free in the statement '(𝑥 ⋅ 𝑦 = 0)'. † Note that if we could show '⊢ Ⅎ𝑥(𝑥 ⋅ 𝑦) = 0', then we would also be able to show that '⊢ ∀𝑦Ⅎ𝑥(𝑥 ⋅ 𝑦) = 0', which would contradict the conclusion of this example. This means that, without any extra hypotheses, '𝑥' is effectively free (and thus also grammatically free, obviously) in the WFF '(𝑥 ⋅ 𝑦) = 0'. However, adding the open hypothesis '𝑦 = 0', either as a theorem hypothesis or as an antecedent, causes '𝑥' to become effectively not free in '(𝑥 ⋅ 𝑦) = 0'. This is why we say that '𝑥' is *conditionally* not free in '𝜑' when we can deduce 'Ⅎ𝑥𝜑' with the addition of one or more hypotheses, but cannot do so working strictly from axioms. Since no arithmetic axioms have been introduced, we state '(0 ⋅ 𝑦) = 0' as a hypothesis. We also state '¬ ∀𝑥∀𝑦(𝑥 ⋅ 𝑦) = 0' as a hypothesis. With the Peano Axioms, we will define '1'. The second hypothesis then follows from the case '¬ (1⋅1) = 0'.
⊢ (0 ⋅ 𝑦) = 0    &   ⊢ ¬ ∀𝑥∀𝑦 (𝑥 ⋅ 𝑦) = 0    ⇒   ⊢ ¬ ∀𝑦Ⅎ𝑥 (𝑥 ⋅ 𝑦) = 0
PART 9  Chapter 8: Predicate Calculus (Continued)
9.1  Revisiting Chapter 6.
9.1.1  "General For" / "Not Free" Conversion.
9.1.1.1  Standard Forms.
Theorem	nfrgen-P8 1076	ENF ⇒ General For. † The inference form is axGEN-P7 933. This is the restatement of a previously proven result. Do not use in proofs. Use nfrgen-P7 928 instead.
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝛾 → 𝜑)    ⇒   ⊢ (𝛾 → ∀𝑥𝜑)
Theorem	nfrgen-P7.VR 1077*	nfrgen-P8 1076 with variable restriction. † '𝑥' cannot occur in '𝜑'.
⊢ (𝛾 → 𝜑)    ⇒   ⊢ (𝛾 → ∀𝑥𝜑)
Theorem	nfrgen-P8.CL 1078	Closed Form of nfrgen-P8 1076. † The variable restricted form is axL5-P7 934. This is the restatement of a previously proven result. Do not use in proofs. Use nfrgen-P7.CL 930 instead.
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (𝜑 → ∀𝑥𝜑)
Theorem	gennfr-P8 1079	General For ⇒ ENF. †
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ Ⅎ𝑥𝜑
9.1.1.2  Dual Forms.
Theorem	nfrexgen-P8 1080	Dual Form of nfrgen-P8 1076. † This is the restatement of a previously proven result. Do not use in proofs. Use nfrexgen-P7 931 instead.
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜑)
Theorem	nfrexgen-P8.VR 1081*	nfrexgen-P8 1080 with variable restriction. † '𝑥' cannot occur in '𝜑'.
⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜑)
Theorem	nfrexgen-P8.RC 1082	Inference Form of nfrexgen-P8 1080. †
⊢ Ⅎ𝑥𝜑    &   ⊢ ∃𝑥𝜑    ⇒   ⊢ 𝜑
Theorem	nfrexgen-P8.RC.VR 1083*	nfrexgen-P8.RC 1082 with variable restriction. † '𝑥' cannot occur in '𝜑'
⊢ ∃𝑥𝜑    ⇒   ⊢ 𝜑
Theorem	nfrexgen-P8.CL 1084	Closed Form of nfrexgen-P8 1080. † The variable restricted form is axL5ex-P7 935. This is the restatement of a previously proven result. Do not use in proofs. Use nfrexgen-P7.CL 932 instead.
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 → 𝜑)
Theorem	exgennfr-P8 1085	Dual Form of gennfr-P8 1079. †
⊢ (∃𝑥𝜑 → 𝜑)    ⇒   ⊢ Ⅎ𝑥𝜑
9.1.1.3  Combined Forms.
Theorem	nfrexall-P8 1086	Combining of nfrgen-P8 1076 and nfrexgen-P8 1080. †
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → ∀𝑥𝜑)
Theorem	nfrexall-P8.VR 1087*	nfrexall-P8 1086 with variable restriction. † '𝑥' cannot occur in '𝜑'.
⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → ∀𝑥𝜑)
Theorem	nfrexall-P8.RC 1088	Inference form of nfrexall-P8 1086. †
⊢ Ⅎ𝑥𝜑    &   ⊢ ∃𝑥𝜑    ⇒   ⊢ ∀𝑥𝜑
Theorem	nfrexall-P8.RC.VR 1089*	nfrexall-P8.RC 1088 with variable restriction . † '𝑥' cannot occur in '𝜑'.
⊢ ∃𝑥𝜑    ⇒   ⊢ ∀𝑥𝜑
Theorem	nfrexall-P8.CL 1090	Closed Form of nfrexall-P8 1086. †
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 → ∀𝑥𝜑)
Theorem	nfrexall-P8.CL.VR 1091*	nfrexall-P8.CL 1090 with variable restriction . † '𝑥' cannot occur in '𝜑'.
⊢ (∃𝑥𝜑 → ∀𝑥𝜑)
Theorem	exallnfr-P8 1092	Converse of nfrexall-P8.CL 1090. †
⊢ (∃𝑥𝜑 → ∀𝑥𝜑)    ⇒   ⊢ Ⅎ𝑥𝜑
9.1.2  Nested Quantifier Idempotency Laws.
Theorem	idempotall-P8 1093	Idempotency Law for '∀𝑥'. †
⊢ (∀𝑥∀𝑥𝜑 ↔ ∀𝑥𝜑)
Theorem	idempotex-P8 1094	Idempotency Law for '∃𝑥'. †
⊢ (∃𝑥∃𝑥𝜑 ↔ ∃𝑥𝜑)
Theorem	idempotallex-P8 1095	Idempotency Law for '∀𝑥' over '∃𝑥'. †
⊢ (∀𝑥∃𝑥𝜑 ↔ ∃𝑥𝜑)
Theorem	idempotexall-P8 1096	Idempotency Law for '∃𝑥' over '∀𝑥'. †
⊢ (∃𝑥∀𝑥𝜑 ↔ ∀𝑥𝜑)
Theorem	idempotallnall-P8 1097	Idempotency Law for '∀𝑥' over '¬ ∀𝑥'. †
⊢ (∀𝑥 ¬ ∀𝑥𝜑 ↔ ¬ ∀𝑥𝜑)
Theorem	idempotexnex-P8 1098	Idempotency Law for '∃𝑥' over '¬ ∃𝑥'. †
⊢ (∃𝑥 ¬ ∃𝑥𝜑 ↔ ¬ ∃𝑥𝜑)
Theorem	idempotallnex-P8 1099	Idempotency Law for '∀𝑥' over '¬ ∃𝑥'. †
⊢ (∀𝑥 ¬ ∃𝑥𝜑 ↔ ¬ ∃𝑥𝜑)
Theorem	idempotexnall-P8 1100	Idempotency Law for '∃𝑥' over '¬ ∀𝑥'. †
⊢ (∃𝑥 ¬ ∀𝑥𝜑 ↔ ¬ ∀𝑥𝜑)