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

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

Type	Label	Description
Statement
Theorem	qimeqallb-P6 701	Quantified Implication Equivalence Law ( U ↔ ( E → U ) ) (non-freeness condition b).
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓))
Theorem	qremallw-P6 702*	Universal Quantifier Removal (non-freeness condition - weakened form). Requires the existence of '𝜑₁(𝑥₁)' as a replacement for '𝜑(𝑥)'.
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥𝜑 ↔ 𝜑)
Theorem	qremexw-P6 703*	Existential Quantifier Removal (non-freeness condition - weakened form). Requires the existence of '𝜑₁(𝑥₁)' as a replacement for '𝜑(𝑥)'.
⊢ (𝑥 = 𝑥₁ → (𝜑 ↔ 𝜑₁))    &   ⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 ↔ 𝜑)
7.2  Explicit Substitution.
7.2.1  Motivation.
Theorem	solvesub-P6a 704*	Solve for Substitution Formula ('𝑥' does not occur in '𝑡'). Requires the existence of '𝜓₁(𝑥₁)' as a replacement for '𝜓(𝑥)'. Also, '𝑥' cannot occur in '𝑡'. The idea here is that we replace all free occurences of '𝑥' in '𝜑' with '𝑡', first changing any bound variables that conflict with '𝑡' with fresh variables. The result of this process, which is guaranteed to exist, will be called '𝜓'. So long as '𝑥' does not appear in '𝑡', '𝑥' will not occur free in the result, '𝜓'. This fact is needed to prove this statement. Using the process described above, the existence of a formula, '𝜓', that satisfies the hypotheses of this statement can be proven through induction on formula length. With the assumption that such a formula exists, this statement then "solves" for a direct formula that is gauranteed to be logically equivalent to '𝜓' in every case. The only limitation of this direct formula is the rule that '𝑥' is not allowed to occur in '𝑡'. An even more general formula where '𝑡' is allowed to contain '𝑥' can be produced by applying this substitution twice, recursively, with an intermediate dummy variable. This is shown in solvedsub-P6a 711.
⊢ (𝑥 = 𝑥₁ → (𝜓 ↔ 𝜓₁))    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝜓 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))
Theorem	solvesub-P6a.VR 705*	Variable Restricted Form of solvesub-P6a 704. '𝑥' cannot occur in either '𝜓' or '𝑡'. If we know '𝑥' does not occur in '𝜓' ahead of time, we can remove some of the hypotheses.
⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝜓 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))
Theorem	example-E6.01a 706*	Eliminating Hypothesis to solvesub-P6a 704. In this example we replace '𝑏' in 𝜑 with '𝑥'. Because '𝑥' is a bound variable in '𝜑', we use cbvallv-P5 659 to change the bound variable '𝑥' to '𝑦' so as not to conflict with the substituted '𝑥'. The WFF metavariables '𝜑' and '𝜓', defined as hypotheses, exist only to make this example easier to follow. It is easy to locate the important steps, which are... 'Ⅎ𝑏𝜓', and '(𝑏 = 𝑥 → (𝜑 ↔ 𝜓))'.
⊢ (𝑏 = 𝑏₁ → (𝜓 ↔ 𝜓₁))    &   ⊢ (𝜑 ↔ ∀𝑥(𝑥 ∈ 𝑏 → 𝑥 ∈ 𝑎))    &   ⊢ (𝜓 ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑎))    ⇒   ⊢ (𝜓 ↔ ∀𝑏(𝑏 = 𝑥 → 𝜑))
Theorem	solvesub-P6b 707*	solvesub-P6a 704 with result substituted back into hypothesis. Requires the existence of '𝜓₁(𝑥₁)' as a replacement for '𝜓(𝑥)'. Also, '𝑥' cannot occur in '𝑡'.
⊢ (𝑥 = 𝑥₁ → (𝜓 ↔ 𝜓₁))    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝑥 = 𝑡 → (𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)))
Theorem	eqmiddle-P6 708*	Introduce Intermediate Middle Variable from Equality. '𝑦' cannot occur in either '𝛾' or '𝑡'.
⊢ (𝛾 → 𝑥 = 𝑡)    ⇒   ⊢ (𝛾 → ∃𝑦(𝑥 = 𝑦 ∧ 𝑦 = 𝑡))
Theorem	eqmiddle-P6.CL 709*	Closed Form of eqmiddle-P6 708. '𝑦' cannot occur in '𝑡'.
⊢ (𝑥 = 𝑡 → ∃𝑦(𝑥 = 𝑦 ∧ 𝑦 = 𝑡))
Theorem	trnsvsubw-P6 710*	Transitive Dummy Variable Substitution (weakened form). Requires the existence of '𝜒₁(𝑦₁)' as a replacement for '𝜒(𝑦)'. Also, neither '𝑦' nor '𝑦₁' can occur in '𝜑' and '𝑦' cannot occur in '𝑡'.
⊢ Ⅎ𝑦𝜒    &   ⊢ (𝑦 = 𝑦₁ → (𝜒 ↔ 𝜒₁))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑡 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜒))
Theorem	solvedsub-P6a 711*	Solve for Double Substitution Formula ('𝑥' may occur in '𝑡'). Requires the existence of '𝜓₁(𝑥₁)' as a replacement for '𝜓(𝑥)' and '𝜒₁(𝑦₁)' as a replacement for '𝜒(𝑦)'. Also, '𝑦' cannot occur in '𝑡'. The idea is the same as in solvesub-P6a 704, but we perform two substitutions in sequence. We first replace all free occurences of '𝑥' in '𝜑' with a fresh variable '𝑦' to get '𝜓'. We then replace all free occurences of '𝑦' in '𝜓' with '𝑡' (remembering to change any conflicting bound variables) in order to obtain '𝜒'. The double substitution above is needed to allow '𝑥' to occur in the term '𝑡'. Again, it can be proved inductively that the formulas '𝜓' and '𝜒', obtained by the double substitution described above, satisfy the hypotheses of this statement. We can then "solve" for an equivalent direct formula.
⊢ (𝑥 = 𝑥₁ → (𝜓 ↔ 𝜓₁))    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑦 = 𝑦₁ → (𝜒 ↔ 𝜒₁))    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑡 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜒 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	example-E6.02a 712*	Eliminating Hypothesis to solvedsub-P6a 711. In this example we replace '𝑏' in 𝜑 with '(𝑥 ⋅ 𝑏)'. Because '𝑏' occurs in the term '(𝑥 ⋅ 𝑏)', we first replace '𝑏' with '𝑐' to obtain '𝜓'. Because '𝑥' is a bound variable in '𝜑', we again use cbvallv-P5 659 to change the bound variable '𝑥' to '𝑦' so as not to conflict with the substituted term, '(𝑥 ⋅ 𝑏)'. The WFF metavariables '𝜑', '𝜓', and '𝜒' defined as hypotheses, exist only to make this example easier to follow. It is easy to locate the important steps, which are... 'Ⅎ𝑏𝜓', 'Ⅎ𝑐𝜒, '(𝑏 = 𝑐 → (𝜑 ↔ 𝜓))', and '(𝑐 = (𝑥 ⋅ 𝑏)) → (𝜓 ↔ 𝜒))'.
⊢ (𝑏 = 𝑏₁ → (𝜓 ↔ 𝜓₁))    &   ⊢ (𝑐 = 𝑐₁ → (𝜒 ↔ 𝜒₁))    &   ⊢ (𝜑 ↔ ∃𝑥 𝑏 = (𝑥 ⋅ 𝑎))    &   ⊢ (𝜓 ↔ ∃𝑥 𝑐 = (𝑥 ⋅ 𝑎))    &   ⊢ (𝜒 ↔ ∃𝑦 (𝑥 ⋅ 𝑏) = (𝑦 ⋅ 𝑎))    ⇒   ⊢ (𝜒 ↔ ∀𝑐(𝑐 = (𝑥 ⋅ 𝑏) → ∀𝑏(𝑏 = 𝑐 → 𝜑)))
Theorem	solvedsub-P6b 713*	solvedsub-P6a 711 with result substituted back into hypothesis. Requires the existence of '𝜓₁(𝑥₁)' as a replacement for '𝜓(𝑥)' and '𝜒₁(𝑦₁)' as a replacement for '𝜒(𝑦)'. Also, neither '𝑦' nor '𝑦₁' can occur in '𝜑' and '𝑦' cannot occur in '𝑡'. Note that trnsvsubw-P6 710 must be used to show that '(𝑥 = 𝑡 → (𝜑 ↔ 𝜒))', and from there we can substitute the explicit formula from solvedsub-P6a 711 for '𝜒'.
⊢ (𝑥 = 𝑥₁ → (𝜓 ↔ 𝜓₁))    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑦 = 𝑦₁ → (𝜒 ↔ 𝜒₁))    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑡 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝑥 = 𝑡 → (𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
7.2.2  Define Proper Substitution.
7.2.2.1  Syntax Definition.
Syntax	wff-psub 714	Extend WFF definition to include proper substitution syntax, '[𝑡 / 𝑥]'.
wff [𝑡 / 𝑥]𝜑
7.2.2.2  Justification Theorem.
Theorem	psubjust-P6 715*	Justification Theorem for df-psub-D6.2 716. '𝑦' and '𝑧' are distinct from all other variables.
⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑦 = 𝑥 → 𝜑)) ↔ ∀𝑧(𝑧 = 𝑡 → ∀𝑥(𝑧 = 𝑥 → 𝜑)))
7.2.2.3  Formal Definition.
Definition	df-psub-D6.2 716*	Definition of Proper Substitution, '[𝑡 / 𝑥]𝜑'. Read as "The formula resulting from properly substituting '𝑡' for '𝑥' in '𝜑'". '𝑦' is distinct from all other variables.
⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
7.2.3  Simplified Definition.
Theorem	dfpsubv-P6 717*	Simplified Definition of Proper Substitution (restriction on '𝑡'). This form can be used whenever '𝑥' does not occur in '𝑡'.
⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))
7.3  Scheme Completion Axiom ax-L12. Notice that ax-L12 29 is really just the result of solvesub-P6b 707... '(𝑥 = 𝑡 → (𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)))', with the only the forward direction of the biconditional stated. Therefore you might expect that it will allow us to eliminate the hypotheses associated with this theorem. Also, note that given an arbitrary WFF '𝜑', the existence of WFFs, '𝜓' and '𝜓₁', satisfying all the hypotheses of solvesub-P6b 707, can be shown to exist using meta-theorems. Because of this, ax-L12 29 can also be proved as a meta-theorem. This means ax-L12 29 logically follows from the FOL axioms ( L1 through L9 ) alone. Indeed, specific cases can always be proven within the metamath language, as shown by the hypothesis elimination examples. However, within the metamath language, general statements of the conclusion of solvesub-P6b 707, i.e. ones containing WFF meta-variables, will require ax-L12 29. ax-L12 29 will also allow us to eliminate the hypothesis on the Law of Specialization (specw-P5 661) and its dual (exiw-P5 662). We also state the traditional texbook forms of these two laws (specpsub-P6 721 and exipsub-P6 720), based on proper substitution. Note that these textbook forms do not require ax-L12 29 (or any meta-theorems). This may lead one to think that ax-L12 29 is unnecessary. The problem is, though logically equivalent to the standard definition, the explicit definition of proper substitution requires ax-L12 29 to be of any practical use.
7.3.1  Existential Quantifier Introduction and Specialization Revisited.
7.3.1.1  Basic Forms. These forms require ax-L12 29.
Theorem	exi-P6 718	Existential Quantifier Introduction Law. See exiw-P5 662 for a version that requires only FOL axioms.
⊢ (𝜑 → ∃𝑥𝜑)
Theorem	spec-P6 719	Law of Specialization. See specw-P5 661 for a version that requires only FOL axioms.
⊢ (∀𝑥𝜑 → 𝜑)
7.3.1.2  Traditional Textbook Forms. These forms do not require ax-L12 29.
Theorem	exipsub-P6 720	Existential Quantifier Introduction Law (proper substitution). This is the form most often seen in logic text books.
⊢ ([𝑡 / 𝑥]𝜑 → ∃𝑥𝜑)
Theorem	specpsub-P6 721	Law of Specialization. (proper substitution). This is the form most often seen in logic text books.
⊢ (∀𝑥𝜑 → [𝑡 / 𝑥]𝜑)
7.3.2  Strengthened Quantifier Removal Laws.
Theorem	qremall-P6 722	Universal Quantifier Removal (non-freeness condition). See qremallw-P6 702 for a version that requires only FOL axioms.
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥𝜑 ↔ 𝜑)
Theorem	qremex-P6 723	Existential Quantifier Removal (non-freeness condition). See qremexw-P6 703 for a version that requires only FOL axioms.
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 ↔ 𝜑)
7.3.3  Implicit / Explicit Substitution Conversion. The need for a proof of the statement, lemma-L6.01a 724, is was the main motivation for ax-L12 29.
Theorem	lemma-L6.01a 724*	This lemma is the result of solvesub-P6b 707 with no hypothesis required. '𝑥' cannot occur in '𝑡'.
⊢ (𝑥 = 𝑡 → (𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)))
Theorem	psubtoisubv-P6 725*	Conversion From Explicit to Implicit Substitution (for when '𝑡' does not contain '𝑥'). '𝑥' cannot occur in '𝑡'. The full form is proved later as psubtoisub-P6 765.
⊢ (𝑥 = 𝑡 → (𝜑 ↔ [𝑡 / 𝑥]𝜑))
Theorem	lemma-L6.02a 726*	Simular to solvesub-P6a 704, but using ax-L12 29. '𝑥' cannot occur in '𝑡'.
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑡 → 𝜑) ↔ 𝜓)
Theorem	isubtopsubv-P6 727*	Conversion from Implicit to Explicit Substitution (restriction on '𝑡'). '𝑥' cannot occur in '𝑡'.
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜓)
Theorem	lemma-L6.03a 728*	Similar to solvedsub-P6a 711 but using ax-L12 29. '𝑦' cannot occur in '𝑡'.
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑡 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ 𝜒)
Theorem	isubtopsub-P6 729*	Conversion from Implicit to Explicit Substitution with Intermediate Formula. '𝑦' cannot occur in either '𝜑' or '𝑡'. If '𝑦' is a fresh variable that appears in the intermediate WFF '𝜓', then we can substitute '𝑡' for '𝑥' even when '𝑥' occurs in '𝑡'.
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑡 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜒)
7.4  Scheme Completion Axioms ax-L10 and ax-L11.
7.4.1  Strengthened "General For" Laws (first half). These laws require ax-L10 27 but not ax-L12 29.
Theorem	gennall-P6 730	The WFF '¬ ∀𝑥𝜑' is General For '𝑥'. If this result is stated as an axiom (ax-L10 27), then all the other related "general for" rules will follow (though half will require ax-L12 29 as well). See gennallw-P6 678 for a version that requires only FOL axioms.
⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
Theorem	genex-P6 731	The WFF '∃𝑥𝜑' is General For '𝑥'. See genexw-P6 677 for a version that requires only FOL axioms.
⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑)
Theorem	exgenall-P6 732	Dual of gennall-P6 730. See exgenallw-P6 680 for a version that requires only FOL axioms.
⊢ (∃𝑥∀𝑥𝜑 → ∀𝑥𝜑)
7.4.2  Strengthened "General For" / "Not Free" Conversion Laws. The inference "𝑥 is ENF in 𝜑 ⇒ 𝜑 is general for 𝑥" requires ax-L12 29 but not ax-L10 27. The inference "𝜑 is general for 𝑥 ⇒ 𝑥 is ENF in 𝜑" requires ax-L10 27 but not ax-L12 29.
Theorem	nfrgen-P6 733	ENF in ⇒ General for. If '𝑥' is effectively not free in '𝜑', then '𝜑' is general for '𝑥'. See nfrgenw-P6 684 for a version that requires only FOL axioms.
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (𝜑 → ∀𝑥𝜑)
Theorem	gennfr-P6 734	General for ⇒ ENF in. If '𝜑' is general for '𝑥', then '𝑥' is effectively not free in '𝜑'. See gennfrw-P6 685 for a version that requires only FOL axioms.
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ Ⅎ𝑥𝜑
Theorem	nfrexgen-P6 735	Dual Form of nfrgen-P6 733. See nfrexgenw-P6 696 for a version that requires only FOL axioms.
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 → 𝜑)
Theorem	exgennfr-P6 736	Dual Form of gennfr-P6 734. See exgennfrw-P6 697 for a version that requires only FOL axioms.
⊢ (∃𝑥𝜑 → 𝜑)    ⇒   ⊢ Ⅎ𝑥𝜑
7.4.3  Strengthened "General For" Laws (second half). These rules require ax-L10 27 and ax-L12 29.
Theorem	genall-P6 737	The WFF '∀𝑥𝜑' is General For '𝑥'. See genallw-P6 676 for a version that requires only FOL axioms.
⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
Theorem	gennex-P6 738	The WFF '¬ ∃𝑥𝜑' is General For '𝑥'. See gennexw-P6 679 for a version that requires only FOL axioms.
⊢ (¬ ∃𝑥𝜑 → ∀𝑥 ¬ ∃𝑥𝜑)
7.4.4  Strengthened Quantifier Commutivity Laws. These laws require ax-L11 28.
Theorem	allcomm-P6 739*	Universal Quantifier Commutivity. See allcommw-P5 669 for a version that requires only FOL axioms.
⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑)
Theorem	excomm-P6 740*	Existential Quantifier Commutivity. See excommw-P5 670 for a version that requires only FOL axioms.
⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)
7.4.5  Strengthened Effective Non-Freeness Properties. nfrex1-P6 742 and nfrex2-P6 744 require ax-L12 29. nfrall1-P6 741 and nfrall2-P6 743 require ax-L10 27 and ax-L12 29. nfrall2-P6 743 and nfrex2-P6 744 require ax-L11 28.
Theorem	nfrall1-P6 741	ENF Over Universal Quantifier (same variable). See nfrall1w-P6 692 for a version that requires only FOL axioms.
⊢ Ⅎ𝑥∀𝑥𝜑
Theorem	nfrex1-P6 742	ENF Over Existential Quantifier (same variable). See nfrex1w-P6 693 for a version that requires only FOL axioms.
⊢ Ⅎ𝑥∃𝑥𝜑
Theorem	nfrall2-P6 743*	ENF Over Universal Quantifier (different variable). See nfrall2w-P6 694 for a version that requires only FOL axioms.
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦𝜑
Theorem	nfrex2-P6 744*	ENF Over Existential Quantifier (different variable). See nfrex2w-P6 695 for a version that requires only FOL axioms.
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃𝑦𝜑
7.5  Replacing Variable Restrictions with Non-Freeness Conditions.
7.5.1  Basic Quantifier Rules with Non-Freeness Conditions.
Theorem	allic-P6 745	Introduction of Universal Quantifier as Consequent (non-freeness condition). This proposition is equivalent to the '∀' introduction rule in the natural deduction system.
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥𝜓)
Theorem	exia-P6 746	Introduction of Existential Quantifier as Antecedent (non-freeness condition). This proposition is equivalent to the '∃' elimination rule in the natural deduction system.
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → 𝜓)
Theorem	alloverim-P5.GENF 747	alloverim-P5 588 with Generalization (non-freeness condition).
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	alloverimex-P5.GENF 748	alloverimex-P5 601 with Generalization (non-freeness condition).
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∃𝑥𝜑 → ∃𝑥𝜓))
7.5.2  Change of Bound Variables Laws with Non-Freeness Conditions.
Theorem	lemma-L6.04a 749*	Version of lemma-L5.02a 653 with non-freeness condition. '𝑥 cannot occur in '𝑡'.
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑡 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	cbvall-P6-L1 750*	Lemma for cbvall-P6 751. [Auxiliary lemma - not displayed.]
Theorem	cbvall-P6 751*	Change of Bound Variable Law for '∀𝑥' (non-freeness condition).
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvex-P6 752*	Change of Bound Variable Law for '∃𝑥' (non-freeness condition).
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
7.5.3  (Implicit) Substitution Laws with Non-Freeness Conditions.
Theorem	suball-P6 753	Substitution Law for '∀𝑥' (non-freeness condition).
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
Theorem	subex-P6 754	Substitution Law for '∃𝑥'(non-freeness condition).
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
Theorem	subnfr-P6 755	Substitution Law for 'Ⅎ𝑥' Predicate.
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓))
Theorem	subnfr-P6.VR 756*	Variable Restricted Form of subnfr-P6 755. '𝑥' cannot occur in '𝛾'.
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓))
7.5.4  Quantifier Collection Laws with Non-Freeness Conditions.
Theorem	qcallimr-P6 757	Quantifier Collection Law: Universal Quantifier Right on Implication (non-freeness condition).
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ((𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓))
Theorem	qceximr-P6 758	Quantifier Collection Law: Existential Quantifier Right on Implication (non-freeness condition).
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ((𝜑 → ∃𝑥𝜓) ↔ ∃𝑥(𝜑 → 𝜓))
Theorem	qcalliml-P6 759	Quantifier Collection Law: Universal Quantifier Left on Implication (non-freeness condition).
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ ((∀𝑥𝜑 → 𝜓) ↔ ∃𝑥(𝜑 → 𝜓))
Theorem	qceximl-P6 760	Quantifier Collection Law: Existential Quantifier Left on Implication (non-freeness condition).
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ ((∃𝑥𝜑 → 𝜓) ↔ ∀𝑥(𝜑 → 𝜓))
Theorem	qcexandr-P6 761	Quantifier Collection Law: Existential Quantifier Right on Conjunction (non-freeness condition).
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ ∃𝑥(𝜑 ∧ 𝜓))
Theorem	qcexandl-P6 762	Quantifier Collection Law: Existential Quantifier Left on Conjunction (non-freeness condition).
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ ((∃𝑥𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ 𝜓))
7.6  More on Proper Substitution.
7.6.1  Explicit to Implicit Substitution Conversion. We will now prove the more general formulation of psubtoisubv-P6 725.
Theorem	trnsvsub-P6 763*	Strengthened Form of trnsvsubw-P6 710. '𝑦' cannot occur in '𝑡'.
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝑡 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜒))
Theorem	lemma-L6.05a 764*	This lemma is the result of solvedsub-P6b 713 with no hypothesis required. '𝑦' cannot occur in '𝑡'.
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (𝑥 = 𝑡 → (𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Theorem	psubtoisub-P6 765	Conversion from Explicit to Implicit Substitution. This theorem holds even when '𝑡' contains '𝑥'.
⊢ (𝑥 = 𝑡 → (𝜑 ↔ [𝑡 / 𝑥]𝜑))
Theorem	lemma-L6.06a 766*	Effective Non-Freeness Over Proper Substitution (restriction on '𝑡'). Note this only holds when '𝑡' does not contain '𝑥'.
⊢ Ⅎ𝑥[𝑡 / 𝑥]𝜑
Theorem	psubcomp-P6 767*	Composition of Proper Substitutions. This can be taken as a definition of proper substitution for when '𝑥' occurs in '𝑡', given the definition where '𝑥' does not occur in '𝑡'. '𝑦' cannot occur in either '𝜑' or '𝑡'.
⊢ ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑦][𝑦 / 𝑥]𝜑)
7.6.2  Change of Bound Variable Using Proper Substitution.
Theorem	cbvallpsub-P6 768*	Change of Bound Variable for '∀𝑥' with Proper Substitution.
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	cbvexpsub-P6 769*	Change of Bound Variable for '∃𝑥' with Proper Substitution.
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑)
7.6.3  An Alternate Definition of Proper Substitution.
Theorem	lemma-L6.07a-L1 770*	Lemma for lemma-L6.06a 766. [Auxiliary lemma - not displayed.]
Theorem	lemma-L6.07a-L2 771*	Lemma for lemma-L6.06a 766. [Auxiliary lemma - not displayed.]
Theorem	lemma-L6.07a 772*	This lemma is used to construct an alternate definition of proper substitution. '𝑥' cannot occur in '𝑡'.
⊢ (∀𝑥(𝑥 = 𝑡 → 𝜑) ↔ ∃𝑥(𝑥 = 𝑡 ∧ 𝜑))
Theorem	lemma-L6.08a 773*	Equivalency of definitions lemma. '𝑦' cannot occur in '𝑡'.
⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∃𝑦(𝑦 = 𝑡 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
Theorem	dfpsubalt-P6 774*	Alternate Definition of Proper Substitution. '𝑦' cannot occur in either '𝜑' or 𝑡'.
⊢ ([𝑡 / 𝑥]𝜑 ↔ ∃𝑦(𝑦 = 𝑡 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
7.6.4  Separating Atomic WFF Terms.
7.6.4.1  Split Equality.
Theorem	spliteq-P6-L1 775*	Lemma for spliteq-P6-L1 775. [Auxiliary lemma - not displayed.]
Theorem	spliteq-P6 776*	Split Equality Into Left and Right Halves. '𝑎' is distinct from all other variables.
⊢ (𝑡 = 𝑢 ↔ ∃𝑎(𝑎 = 𝑡 ∧ 𝑎 = 𝑢))
7.6.4.2  Split Primitive Predicate.
Theorem	splitelof-P6-L1 777*	Lemma for splitelof-P6 778. [Auxiliary lemma - not displayed.]
Theorem	splitelof-P6 778*	Split "Element Of" Predicate Into Left and Right Halves. '𝑎' and '𝑏' are distinct from all other variables.
⊢ (𝑡 ∈ 𝑢 ↔ ∃𝑎∃𝑏((𝑎 = 𝑡 ∧ 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏))
7.6.4.3  Effective Non-Freeness Over Terms.
Theorem	nfrterm-P6 779*	Changing the dummy variable doesn't change the ENF state. '𝑎' and '𝑏' are distinct from all other variables.
⊢ Ⅎ𝑥 𝑎 = 𝑡    ⇒   ⊢ Ⅎ𝑥 𝑏 = 𝑡
Theorem	nfrsucc-P6 780*	If '𝑥' is ENF a term '𝑡', then '𝑥' is also ENF in its successor 's‘𝑡'. '𝑎' is distinct from all other variables.
⊢ Ⅎ𝑥 𝑎 = 𝑡    ⇒   ⊢ Ⅎ𝑥 𝑎 = s‘𝑡
Theorem	nfradd-P6 781*	If '𝑥' is ENF in the terms '𝑡₁' and '𝑡₂', then '𝑥' is ENF in the sum term '(𝑡₁ + 𝑡₂)'. '𝑎' is distinct from all other variables.
⊢ Ⅎ𝑥 𝑎 = 𝑡₁    &   ⊢ Ⅎ𝑥 𝑎 = 𝑡₂    ⇒   ⊢ Ⅎ𝑥 𝑎 = (𝑡₁ + 𝑡₂)
Theorem	nfrmult-P6 782*	If '𝑥' is ENF in the terms '𝑡₁' and '𝑡₂', then '𝑥' is ENF in the product term '(𝑡₁ ⋅ 𝑡₂)'. '𝑎' is distinct from all other variables.
⊢ Ⅎ𝑥 𝑎 = 𝑡₁    &   ⊢ Ⅎ𝑥 𝑎 = 𝑡₂    ⇒   ⊢ Ⅎ𝑥 𝑎 = (𝑡₁ ⋅ 𝑡₂)
7.6.5  Relationship to Textbook Definition. Let '𝜑' be a well formed formula, '𝑡' be a term, and '𝑥' be an object variable. Now read '(𝑡 / 𝑥)𝜑' as "the formula with '𝑥' properly replaced by '𝑡'". If '𝜑' is in primitive form, we define grammatical proper substitution using the following recursive rules... Case 1: '𝜑' is an atomic formula. '(𝑡 / 𝑥)𝜑 ≔ 𝜑*', where '𝜑*' is just '𝜑' with every occurence of '𝑥' replaced with '𝑡'. case 2: '𝜑 ≔ ¬ 𝜓'. '(𝑡 / 𝑥)𝜑 ≔ ¬ (𝑡 / 𝑥)𝜓'. Case 3: '𝜑 ≔ (𝜓 → 𝜒)'. '(𝑡 / 𝑥)𝜑 ≔ ((𝑡 / 𝑥)𝜓 → (𝑡 / 𝑥)𝜒)'. Case 4: '𝜑 ≔ ∀𝑥𝜓'. '(𝑡 / 𝑥)𝜑 ≔ 𝜑'. Case 5: '𝜑 ≔ ∀𝑦𝜓' ('𝑦' is different from '𝑥'). '(𝑡 / 𝑥)𝜑 ≔ ∀𝑧(𝑡 / 𝑥)(𝑧 / 𝑦)𝜓', where '𝑧' is a fresh variable that does not occur in '𝑡' or '𝜑'. We will call '[𝑡 / 𝑥]𝜑' (as defined earlier) *effective* proper substitution as opposed to *grammatical* proper substitution (as defined above.) We will now prove that '([𝑡 / 𝑥]𝜑 ↔ (𝑡 / 𝑥)𝜑)' in the case where '𝜑' is primitive (i.e. contains only '→', '¬', and '∀'). For the general case to follow, we need to impose the same constraint on definitions as discussed in the note regarding effective non-freeness. ---------------------------------------------------------------------------- Proof: We first consider the atomic formula (i.e. case 1). psubspliteq-P6 800 shows that applying effective proper substitution to each side of an equality and then combining the two sides via the given formula is the same as applying effective proper substitution to the entire formula. psubsplitelof-P6 801 shows that the same splitting and combining property applies to predicate formulas. Actually, the same technique will work for any predicate that takes individual terms as arguments, including ones that have an arity other than 2. Since effective proper substitution can only be applied to full formulas, we use psubspliteq-P6 800 or psubsplitelof-P6 801 to assign a fresh variable to the left of each term. We now use induction on term length to show that the form '𝑎 = 𝑡', where '𝑎' is a distinct object variable, is preserved under effective proper substitution, and that the effect of applying effective proper substitution is the same as that of applying grammatical proper substitution. That is... '(𝜑 ↔ 𝑎 = 𝑡) ⇒ ([𝑤 / 𝑥]𝜑 ↔ 𝑎 = 𝑡* )' where we have used the syntax '𝑡*' to indicate '𝑡' with all occurrences of '𝑥' replaced with '𝑤'. For simplicity, we first prove the result above for the case where '𝑥' does not occur in '𝑡'. We can later generalize to the case where '𝑥' can occur in '𝑤'. Now for the induction. First, let 'n' be the length of the term '𝑡' When 'n = 1' (i.e. no functions) we one of the following... '𝜑 ≔ 𝑎 = 𝑥', or '𝜑 ≔ 𝑎 = 𝑦' ('𝑦' different from '𝑥'), or '𝜑 ≔ 𝑎 = 0'. Now, from psubvar1-P6 802 we have ... '([𝑤 / 𝑥]𝑎 = 𝑥 ↔ 𝑎 = 𝑤)', from psubvar2-P6 803 we have ... '([𝑤 / 𝑥]𝑎 = 𝑦 ↔ 𝑎 = 𝑦)', and from psubzero-P6 804 we have ... '([𝑤 / 𝑥]𝑎 = 0 ↔ 𝑎 = 0)'. Since we expect '(𝑥)*≔ 𝑤', '(𝑦)*≔ 𝑦', and '(0)*≔ 0', in all three cases the equivalency is exactly as desired. Now consider a term '𝑡' (not containing '𝑥') of length 'n', where for every term '𝑠' (not containing '𝑥') of length less than 'n'... '([𝑤 / 𝑥]𝑎 = 𝑠 ↔ 𝑎 = 𝑠*)'. For '0 < n' the term '𝑡' will have the form... '𝑡 ≔s‘𝑡₁', or '𝑡 ≔ (𝑡₁ + 𝑡₂)', or '𝑡 ≔ (𝑡₁ ⋅ 𝑡₂)', where '𝑡₁' and '𝑡₂' have length less than 'n'. Since '𝑤' does not contain '𝑥', we can use psubsuccv-P6 806. Using '𝑡₁*' for '𝑢₁', psubsuccv-P6 806 says that if... '[𝑤 / 𝑥]𝑎 = 𝑡₁ ↔ 𝑎 = 𝑡₁*)', then '[𝑤 / 𝑥]𝑏 =s‘𝑡₁ ↔ 𝑏 =s‘(𝑡₁*) = (s‘𝑡₁)*'. For addition case, we use psubaddv-P6 808. Using '𝑡₁*' for '𝑢₁' and '𝑡₂*' for '𝑢₂', psubaddv-P6 808 says that if... '[𝑤 / 𝑥]𝑎 = 𝑡₁ ↔ 𝑎 = 𝑡₁*)' and '[𝑤 / 𝑥]𝑏 = 𝑡₂ ↔ 𝑏 = 𝑡₂*)', then '[𝑤 / 𝑥]𝑐 = (𝑡₁ + 𝑡₂) ↔ 𝑐 = (𝑡₁*+ 𝑡₂*) = (𝑡₁ ⋅ 𝑡₂)*'. Similarly, inspecting psubmultv-P6 810 shows that if... '[𝑤 / 𝑥]𝑎 = 𝑡₁ ↔ 𝑎 = 𝑡₁*)' and '[𝑤 / 𝑥]𝑏 = 𝑡₂ ↔ 𝑏 = 𝑡₂*)', then '[𝑤 / 𝑥]𝑐 = (𝑡₁ ⋅ 𝑡₂) ↔ 𝑐 = (𝑡₁*⋅ 𝑡₂*) = (𝑡₁ ⋅ 𝑡₂)*'. Since '𝑡₁' and '𝑡₂' have length less than 'n', the hypotheses are fulfilled. Therefore, if for every term (not containing '𝑥'), '𝑠', of length less than 'n'... '([𝑤 / 𝑥]𝑎 = 𝑠 ↔ 𝑎 = 𝑠*)', then for any term (not containing '𝑥') of length 'n'... '([𝑤 / 𝑥]𝑏 = 𝑡 ↔ 𝑏 = 𝑡*)'. By the induction principle, '([𝑤 / 𝑥]𝑎 = 𝑡 ↔ 𝑎 = 𝑡*)' holds for every term '𝑡' (so long as it doesn't contain '𝑥'). To deal with terms that are allowed to contain '𝑥', we can use psubcomp-P6 767. psubcomp-P6 767 says that a single substitution for a term containing '𝑥' is the same as two substitutions with an intermediate dummy variable. Since the intermediate dummy variable is required to be distinct, we have two substitutions for which we can apply the previous argument. It's trivial to see that if a single substitution leads to the desired equivalency, then so will two substitutions applied in succession. We are now finished with case 1. Note that the proofs of psubsuccv-P6 806, psubaddv-P6 808, and psubmultv-P6 810 only rely on the substitution axioms for functions ( ax-L9 ) which apply to any kind of function. They have nothing to do with any non-logical axioms or definitions used to describe the exact nature of the functions appearing in the lemmas. Therefore any arbitrary type of function will have its own lemma similar to psubaddv-P6 808, which when inspected will show that equivalence to the desired form is preserved while combining terms as function arguments. Now that we have dealt with case 1, cases 2 through 5 are fairly trivial. Case 2 follows from psubneg-P6 788, case 3 follows from psubim-P6 791, case 4 follows from psuball1-P6 793, and case 5 follows from psuball2-P6 798. This concludes the proof that '([𝑤 / 𝑥]𝜑 ↔ (𝑤 / 𝑥)𝜑)' for any WFF. QED
Theorem	psubleq-P6 783	Proper Substitution is Bound to Logical Equivalence.
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓)
Theorem	psubnfr-P6 784	Proper Substitution Applied to ENF Variable. If '𝑥' is effectively not free in '𝜑', then replacing '𝑥' with some '𝑡' through proper substitution has no effect on '𝜑'.
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜑)
Theorem	psubnfr-P6.VR 785*	Variable Restricted Form of psubnfr-P6 784. '𝑥' cannot occur in '𝜑'.
⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜑)
Theorem	psubthm-P6 786	Proper Substitution Applied to a Theorem.
⊢ 𝜑    ⇒   ⊢ [𝑡 / 𝑥]𝜑
Theorem	psubneg-P6-L1 787	Lemma for psubneg-P6 788. [Auxiliary lemma - not displayed.]
Theorem	psubneg-P6 788	Proper Substitution Over Negation.
⊢ ([𝑡 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑡 / 𝑥]𝜑)
Theorem	psubim-P6-L1 789	Lemma for psubim-P6 791. [Auxiliary lemma - not displayed.]
Theorem	psubim-P6-L2 790	Lemma for psubim-P6 791. [Auxiliary lemma - not displayed.]
Theorem	psubim-P6 791	Proper Substitution Over Implication.
⊢ ([𝑡 / 𝑥](𝜑 → 𝜓) ↔ ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓))
Theorem	psuband-P6 792	Proper Substitution Over Conjunction.
⊢ ([𝑡 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑡 / 𝑥]𝜑 ∧ [𝑡 / 𝑥]𝜓))
Theorem	psuball1-P6 793	Proper Substitution Over Universal Quantifier (same variable).
⊢ ([𝑡 / 𝑥]∀𝑥𝜑 ↔ ∀𝑥𝜑)
Theorem	psubex1-P6 794	Proper Substitution Over Existential Quantifier (same variable).
⊢ ([𝑡 / 𝑥]∃𝑥𝜑 ↔ ∃𝑥𝜑)
Theorem	psuball2v-P6-L1 795*	Lemma for psuball2v-P6 796. [Auxiliary lemma - not displayed.]
Theorem	psuball2v-P6 796*	Proper Substitution Over Universal Quantifier (different variable - restriction on '𝑡'). '𝑦' cannot occur in '𝑡'.
⊢ ([𝑡 / 𝑥]∀𝑦𝜑 ↔ ∀𝑦[𝑡 / 𝑥]𝜑)
Theorem	psubex2v-P6 797*	Proper Substitution Over Existential Quantifier (different variable - restriction on '𝑡'). '𝑦' cannot occur in '𝑡'.
⊢ ([𝑡 / 𝑥]∃𝑦𝜑 ↔ ∃𝑦[𝑡 / 𝑥]𝜑)
Theorem	psuball2-P6 798*	Proper Substitution Over Universal Quantifier (different variable - non-freeness condition). '𝑧' cannot occur in '𝑡'.
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ ([𝑡 / 𝑥]∀𝑦𝜑 ↔ ∀𝑧[𝑡 / 𝑥][𝑧 / 𝑦]𝜑)
Theorem	psubex2-P6 799*	Proper Substitution Over Existential Quantifier (different variable - non-freeness condition). '𝑧' cannot occur in '𝑡'.
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ ([𝑡 / 𝑥]∃𝑦𝜑 ↔ ∃𝑧[𝑡 / 𝑥][𝑧 / 𝑦]𝜑)
7.6.5.1  Proper Substitution Applied to Atomic Formulae.
Theorem	psubspliteq-P6 800*	Apply Proper Substitution to Split Equlity. '𝑎' is distinct from all other variables.
⊢ ([𝑤 / 𝑥] 𝑡 = 𝑢 ↔ ∃𝑎([𝑤 / 𝑥] 𝑎 = 𝑡 ∧ [𝑤 / 𝑥] 𝑎 = 𝑢))