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

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

Type	Label	Description
Statement
9.1.3  Quantifier Removal / Swapping Laws.
Theorem	qremall-P8 1101	Universal Quantifier Removal (non-freeness condition). †
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥𝜑 ↔ 𝜑)
Theorem	qremall-P8.VR 1102*	qremall-P8 1101 with variable restriction. † '𝑥' cannot occur in '𝜑'.
⊢ (∀𝑥𝜑 ↔ 𝜑)
Theorem	qremex-P8 1103	Existential Quantifier Removal (non-freeness condition). †
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 ↔ 𝜑)
Theorem	qremex-P8.VR 1104*	qremex-P8 1103 with variable restriction. † '𝑥' cannot occur in '𝜑'
⊢ (∃𝑥𝜑 ↔ 𝜑)
Theorem	qswap-P8 1105	Swap Quantifiers (non-freeness condition). †
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 ↔ ∀𝑥𝜑)
Theorem	qswap-P8.VR 1106*	qswap-P8 1105 with variable restriction. † '𝑥' cannot occur in '𝜑'.
⊢ (∃𝑥𝜑 ↔ ∀𝑥𝜑)
9.1.4  Other Effective Non-Freeness Properties.
Theorem	nfrthm-P8 1107	Every Variable is ENF in a Theorem. † This is the restatement of a previously proven result. Do not use in proofs. Use nfrthm-P7 926 instead.
⊢ 𝜑    ⇒   ⊢ Ⅎ𝑥𝜑
Theorem	nfrcond-P8 1108	ENF in Antecedent ⇒ Conditionally Not Free in Consequent. † This is actually a generalization of nfrthm-P8 1107.
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → 𝜑)    ⇒   ⊢ (𝛾 → Ⅎ𝑥𝜑)
Theorem	nfrcond-P8.VR 1109*	nfrcond-P8 1108 with variable restriction. † '𝑥' cannot occur in '𝛾'.
⊢ (𝛾 → 𝜑)    ⇒   ⊢ (𝛾 → Ⅎ𝑥𝜑)
Theorem	nfrnegconv-P8 1110	Converse of ndnfrneg-P7.2 827. This statement is not deducible with intuitionist logic.
⊢ (𝛾 → Ⅎ𝑥 ¬ 𝜑)    ⇒   ⊢ (𝛾 → Ⅎ𝑥𝜑)
Theorem	nfrnegconv-P8.RC 1111	Inference Form of nfrnegconv-P8 1110. This statement is not deducible with intuitionist logic.
⊢ Ⅎ𝑥 ¬ 𝜑    ⇒   ⊢ Ⅎ𝑥𝜑
Theorem	nfrnegconv-P8.CL 1112	Closed Form of nfrnegconv-P8 1110. This statement is not deducible with intuitionist logic.
⊢ (Ⅎ𝑥 ¬ 𝜑 → Ⅎ𝑥𝜑)
Theorem	nfrnegbi-P8 1113	Biconditional Combining ndnfrneg-P7.2 827 and nfrnegconv-P8 1110. This statement is not deducible with intuitionist logic.
⊢ (Ⅎ𝑥 ¬ 𝜑 ↔ Ⅎ𝑥𝜑)
9.1.5  Define Effective Non-Freeness Within a Term.
9.1.5.1  Syntax Definition.
Syntax	wff-nfreet 1114	Extend WFF definition to include the effective non-freeness in a term predicate 'Ⅎt𝑥'.
wff Ⅎt𝑥 𝑡
9.1.5.2  Justification Theorem.
Theorem	nfreetjust-P8 1115*	Justification Theorem for df-nfreet-D8.1 1116. † '𝑦' and '𝑧' are distinct from all other variables.
⊢ (∀𝑦Ⅎ𝑥 𝑦 = 𝑡 ↔ ∀𝑧Ⅎ𝑥 𝑧 = 𝑡)
9.1.5.3  Formal Definition.
Definition	df-nfreet-D8.1 1116*	Definition of Effictive Non-Freeness in a Term, 'Ⅎt𝑥 𝑡'. '𝑦' is distinct from all other variables.
⊢ (Ⅎt𝑥 𝑡 ↔ ∀𝑦Ⅎ𝑥 𝑦 = 𝑡)
9.1.6  Effective Non-Freeness Over Atomic Terms.
Theorem	nfrzero-P8 1117	Any variable '𝑥' is ENF in a constant term. †
⊢ Ⅎt𝑥 0
Theorem	nfrvar-P8 1118*	Any variable '𝑥' is ENF in term consisting of some variable, '𝑦', that is different from '𝑥'. †
⊢ Ⅎt𝑥 𝑦
9.1.7  Effective Non-Freeness Over Functional Terms.
Theorem	nfrsucc-P8 1119	If '𝑥' is ENF in a term '𝑡', then '𝑥' is also ENF in its successor, 's‘𝑡'. †
⊢ Ⅎt𝑥 𝑡    ⇒   ⊢ Ⅎt𝑥 s‘𝑡
Theorem	nfradd-P8 1120	If '𝑥' is ENF in the terms '𝑡₁' and '𝑡₂', then '𝑥' is ENF in the sum term, '(𝑡₁ + 𝑡₂)'. †
⊢ Ⅎt𝑥 𝑡₁    &   ⊢ Ⅎt𝑥 𝑡₂    ⇒   ⊢ Ⅎt𝑥(𝑡₁ + 𝑡₂)
Theorem	nfrmult-P8 1121	If '𝑥' is ENF in the terms '𝑡₁' and '𝑡₂', then '𝑥' is ENF in the product term, '(𝑡₁ ⋅ 𝑡₂)'. †
⊢ Ⅎt𝑥 𝑡₁    &   ⊢ Ⅎt𝑥 𝑡₂    ⇒   ⊢ Ⅎt𝑥(𝑡₁ ⋅ 𝑡₂)
9.2  More Quantifier Laws.
9.2.1  Quantifier Collection Laws.
9.2.1.1  Implication.
Theorem	qcallimr-P8 1122	Quantifier Collection Law: Universal Quantifier Right on Implication. †
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ((𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓))
Theorem	qceximr-P8 1123	Quantifier Collection Law: Existential Quantifier Right on Implication.
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ((𝜑 → ∃𝑥𝜓) ↔ ∃𝑥(𝜑 → 𝜓))
Theorem	qcalliml-P8 1124	Quantifier Collection Law: Universal Quantifier Left on Implication.
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ ((∀𝑥𝜑 → 𝜓) ↔ ∃𝑥(𝜑 → 𝜓))
Theorem	qceximl-P8 1125	Quantifier Collection Law: Existential Quantifier Left on Implication. †
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ ((∃𝑥𝜑 → 𝜓) ↔ ∀𝑥(𝜑 → 𝜓))

< Previous  Wrap >