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

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

Type	Label	Description
Statement
PART 1  Chapter 0: Primitives
1.1  Definition of Term
Syntax	term-obj 1	If '𝑥' is an object variable, then '𝑥' is a term.
term 𝑥
Syntax	term_zero 2	The constant '0' is a term.
term 0
Syntax	term_succ 3	If '𝑡' is a term, then 's‘𝑡' is a term.
term s‘𝑡
Syntax	term-add 4	If '𝑡' and '𝑢' are terms, then '𝑡 + 𝑢' is a term.
term (𝑡 + 𝑢)
Syntax	term-mult 5	If '𝑡' and '𝑢' are terms, then '𝑡 ⋅ 𝑢' is a term.
term (𝑡 ⋅ 𝑢)
1.2  Definition of WFF
Syntax	wff-equals 6	If '𝑡' and '𝑢' are terms, then '𝑡 = 𝑢' is a well formed formula.
wff 𝑡 = 𝑢
Syntax	wff-elemof 7	If '𝑡' and '𝑢' are terms, then '𝑡 ∈ 𝑢' is a well formed formula.
wff 𝑡 ∈ 𝑢
Syntax	wff-forall 8	If '𝑥' is a object variable and '𝜑' is a well formed formula, then '∀𝑥𝜑' is a well formed formula.
wff ∀𝑥𝜑
Syntax	wff-neg 9	If '𝜑' is well formed formula, then '¬ 𝜑' is a well formed formula.
wff ¬ 𝜑
Syntax	wff-imp 10	If '𝜑' and '𝜓' are well formed formulas, then '(𝜑 → 𝜓)' is a well formed formula.
wff (𝜑 → 𝜓)
1.3  First Order Logic Axioms
1.3.1  Axioms of Propositional Calculus
Axiom	ax-L1 11	Axiom of Simplification.
⊢ (𝜑 → (𝜓 → 𝜑))
Axiom	ax-L2 12	Axiom of Frege.
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
Axiom	ax-L3 13	Axiom of Transposition.
⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))
Axiom	ax-MP 14	Rule of Modus Ponens.
⊢ 𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ 𝜓
1.3.2  Axioms of Predicate Calculus
Axiom	ax-GEN 15	Rule of Generalization.
⊢ 𝜑    ⇒   ⊢ ∀𝑥𝜑
Axiom	ax-L4 16	Axiom of Quantified Implication.
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Axiom	ax-L5 17*	Axiom of Distinctness. Note: '𝑥' cannot occur in '𝜑'.
⊢ (𝜑 → ∀𝑥𝜑)
1.3.2.1  Equality Axioms
Axiom	ax-L6 18*	Axiom of Existence. Note: '𝑥' cannot occur in '𝑡'
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑡
Axiom	ax-L7 19	Axiom of Equality.
⊢ (𝑡 = 𝑢 → (𝑡 = 𝑤 → 𝑢 = 𝑤))
1.3.3  Substitution Axioms.
1.3.3.1  Primitive Predicate Substitution Axioms.
Axiom	ax-L8-inl 20	Left '∈' substitution.
⊢ (𝑡 = 𝑢 → (𝑡 ∈ 𝑤 → 𝑢 ∈ 𝑤))
Axiom	ax-L8-inr 21	Right '∈' substitution.
⊢ (𝑡 = 𝑢 → (𝑤 ∈ 𝑡 → 𝑤 ∈ 𝑢))
1.3.3.2  Primitive Function Substitution Axioms.
Axiom	ax-L9-succ 22	Successor substitution.
⊢ (𝑡 = 𝑢 → s‘𝑡 = s‘𝑢)
Axiom	ax-L9-addl 23	Left '+' substitution.
⊢ (𝑡 = 𝑢 → (𝑡 + 𝑤) = (𝑢 + 𝑤))
Axiom	ax-L9-addr 24	Right '+' substitution.
⊢ (𝑡 = 𝑢 → (𝑤 + 𝑡) = (𝑤 + 𝑢))
Axiom	ax-L9-multl 25	Left '⋅' substitution.
⊢ (𝑡 = 𝑢 → (𝑡 ⋅ 𝑤) = (𝑢 ⋅ 𝑤))
Axiom	ax-L9-multr 26	Right '⋅' substitution.
⊢ (𝑡 = 𝑢 → (𝑤 ⋅ 𝑡) = (𝑤 ⋅ 𝑢))
1.3.4  Scheme Completion Axioms.
Axiom	ax-L10 27	Non-freeness of Negated Bound Variable.
⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
Axiom	ax-L11 28*	Quantifier Commutation.
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Axiom	ax-L12 29*	Variable Substitution. Note: '𝑥' cannot occur in '𝑡'.
⊢ (𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
PART 2  Chapter 1: Propositional Calculus (Primitive Connectives)
2.1  Logical Implication
2.1.1  Some Simple Proofs. SH = Separate Hypothesis.
Theorem	axL1.SH 30	Inference from ax-L1 11.
⊢ 𝜑    ⇒   ⊢ (𝜓 → 𝜑)
Theorem	axL2.SH 31	Inference from ax-L2 12.
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))
Theorem	axL3.SH 32	Inference from ax-L3 13.
⊢ (¬ 𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜓 → 𝜑)
2.1.2  Some Derived Inferences.
Theorem	mae-P1.1 33	Middle Antecedent Elimination Inference.
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ 𝜓    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	syl-P1.2 34	Syllogism Inference.
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	dsyl-P1.3 35	Double Syllogism Inference.
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜒 → 𝜗)    ⇒   ⊢ (𝜑 → 𝜗)
2.1.3  First Closed Form Theorems.
Theorem	id-P1.4 36	Implication Identity.
⊢ (𝜑 → 𝜑)
Theorem	rae-P1.5 37	Redundant Antecedent Elimination.
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓))
Theorem	rae-P1.5.SH 38	Inference from rae-P1.5 37.
⊢ (𝜑 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → 𝜓)
2.1.4  Proof Recipes.
Theorem	rcp-FR1 39	Frege Axiom with One Antecedent.
⊢ ((𝛾₁ → (𝜑 → 𝜓)) → ((𝛾₁ → 𝜑) → (𝛾₁ → 𝜓)))
Theorem	rcp-FR1.SH 40	Inference from rcp-FR1 39.
⊢ (𝛾₁ → (𝜑 → 𝜓))    ⇒   ⊢ ((𝛾₁ → 𝜑) → (𝛾₁ → 𝜓))
Theorem	rcp-FR2 41	Frege Axiom with Two Antecedents.
⊢ ((𝛾₂ → (𝛾₁ → (𝜑 → 𝜓))) → ((𝛾₂ → (𝛾₁ → 𝜑)) → (𝛾₂ → (𝛾₁ → 𝜓))))
Theorem	rcp-FR2.SH 42	Inference from rcp-FR2 41.
⊢ (𝛾₂ → (𝛾₁ → (𝜑 → 𝜓)))    ⇒   ⊢ ((𝛾₂ → (𝛾₁ → 𝜑)) → (𝛾₂ → (𝛾₁ → 𝜓)))
Theorem	rcp-FR3 43	Frege Axiom with 3 Antecedents.
⊢ ((𝛾₃ → (𝛾₂ → (𝛾₁ → (𝜑 → 𝜓)))) → ((𝛾₃ → (𝛾₂ → (𝛾₁ → 𝜑))) → (𝛾₃ → (𝛾₂ → (𝛾₁ → 𝜓)))))
Theorem	rcp-FR3.SH 44	Inference from rcp-FR3 43.
⊢ (𝛾₃ → (𝛾₂ → (𝛾₁ → (𝜑 → 𝜓))))    ⇒   ⊢ ((𝛾₃ → (𝛾₂ → (𝛾₁ → 𝜑))) → (𝛾₃ → (𝛾₂ → (𝛾₁ → 𝜓))))
2.1.4.1  Application of Proof Recipes. AC = Add Context.
Theorem	axL1.AC.SH 45	Deductive Form of ax-L1 11.
⊢ (𝛾 → 𝜑)    ⇒   ⊢ (𝛾 → (𝜓 → 𝜑))
Theorem	axL2.AC.SH 46	Deductive Form of ax-L2 12.
⊢ (𝛾 → (𝜑 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝛾 → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
Theorem	axL3.AC.SH 47	Deductive Form of ax-L3 13.
⊢ (𝛾 → (¬ 𝜑 → ¬ 𝜓))    ⇒   ⊢ (𝛾 → (𝜓 → 𝜑))
2.1.5  More Implication Theorems.
Theorem	imcomm-P1.6 48	Commutation of Antecedents.
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))
Theorem	imcomm-P1.6.SH 49	Inference from imcomm-P1.6 48.
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜓 → (𝜑 → 𝜒))
Theorem	imcomm-P1.6.AC.SH 50	Deductive Form of imcomm-P1.6 48
⊢ (𝛾 → (𝜑 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝛾 → (𝜓 → (𝜑 → 𝜒)))
Theorem	imsubr-P1.7a 51	Implication Substitution (right). The other related rule is imsubl-P1.7b 54.
⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜑) → (𝜒 → 𝜓)))
Theorem	imsubr-P1.7a.SH 52	Inference from imsubr-P1.7a 51.
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 → 𝜑) → (𝜒 → 𝜓))
Theorem	imsubr-P1.7a.AC.SH 53	Deductive Form of imsubr-P1.7a 51.
⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → ((𝜒 → 𝜑) → (𝜒 → 𝜓)))
Theorem	imsubl-P1.7b 54	Implication Substitution (left). The other related rule is imsubr-P1.7a 51.
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
Theorem	imsubl-P1.7b.SH 55	Inference from imsubl-P1.7b 54.
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜓 → 𝜒) → (𝜑 → 𝜒))
Theorem	imsubl-P1.7b.AC.SH 56	Deductive Form of imsubl-P1.7b 54.
⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
Theorem	mpt-P1.8 57	Closed Form of Modus Ponens.
⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
Theorem	mpt-P1.8.AC.2SH 58	Deductive Form of mpt-P1.8 57.
⊢ (𝛾 → 𝜑)    &   ⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	mpt-P1.8.2AC.2SH 59	Another Deductive Form of mpt-P1.8 57.
⊢ (𝛾₁ → (𝛾₂ → 𝜑))    &   ⊢ (𝛾₁ → (𝛾₂ → (𝜑 → 𝜓)))    ⇒   ⊢ (𝛾₁ → (𝛾₂ → 𝜓))
Theorem	mpt-P1.8.3AC.2SH 60	Another Deductive Form of mpt-P1.8 57.
⊢ (𝛾₁ → (𝛾₂ → (𝛾₃ → 𝜑)))    &   ⊢ (𝛾₁ → (𝛾₂ → (𝛾₃ → (𝜑 → 𝜓))))    ⇒   ⊢ (𝛾₁ → (𝛾₂ → (𝛾₃ → 𝜓)))
Theorem	sylt-P1.9 61	Closed Form of Syllogism.
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
Theorem	sylt-P1.9.AC.2SH 62	Deductive Form of sylt-P1.9 61.
⊢ (𝛾 → (𝜑 → 𝜓))    &   ⊢ (𝛾 → (𝜓 → 𝜒))    ⇒   ⊢ (𝛾 → (𝜑 → 𝜒))
Theorem	sylt-P1.9.2AC.2SH 63	Another Deductive Form of sylt-P1.9 61.
⊢ (𝛾₁ → (𝛾₂ → (𝜑 → 𝜓)))    &   ⊢ (𝛾₁ → (𝛾₂ → (𝜓 → 𝜒)))    ⇒   ⊢ (𝛾₁ → (𝛾₂ → (𝜑 → 𝜒)))
Theorem	maet-P1.10 64	Closed Form of Middle Antecedent Elimination.
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))
2.2  Logical Negation
2.2.1  Basic Negation Laws.
Theorem	poe-P1.11a 65	Principle of Explosion A. A contradiction implies anything. The other form is poe-P1.11b 66.
⊢ (¬ 𝜑 → (𝜑 → 𝜓))
Theorem	poe-P1.11b 66	Principle of Explosion B. A contradiction implies anything. The other form is poe-P1.11a 65.
⊢ (𝜑 → (¬ 𝜑 → 𝜓))
Theorem	poe-P1.11b.AC.2SH 67	Deductive Form of poe-P1.11b 66.
⊢ (𝛾 → 𝜑)    &   ⊢ (𝛾 → ¬ 𝜑)    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	clav-P1.12 68	Clavious's Law. The other form is nclav-P1.14 73.
⊢ ((¬ 𝜑 → 𝜑) → 𝜑)
Theorem	clav-P1.12.AC.SH 69	Deductive Form of clav-P1.12 68.
⊢ (𝛾 → (¬ 𝜑 → 𝜑))    ⇒   ⊢ (𝛾 → 𝜑)
Theorem	clav-P1.12.2AC.SH 70	Another Deductive Form of clav-P1.12 68.
⊢ (𝛾₁ → (𝛾₂ → (¬ 𝜑 → 𝜑)))    ⇒   ⊢ (𝛾₁ → (𝛾₂ → 𝜑))
Theorem	dneg-P1.13a 71	Double Negation Law A. The other related law is dneg-P1.13b 72.
⊢ (¬ ¬ 𝜑 → 𝜑)
Theorem	dneg-P1.13b 72	Double Negation Law B. The other related law is dneg-P1.13a 71.
⊢ (𝜑 → ¬ ¬ 𝜑)
Theorem	nclav-P1.14 73	Negated Clavius's Law. This is the negated form of clav-P1.12 68.
⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑)
Theorem	clav-P1.14.AC.SH 74	Deductive Form of nclav-P1.14 73.
⊢ (𝛾 → (𝜑 → ¬ 𝜑))    ⇒   ⊢ (𝛾 → ¬ 𝜑)
Theorem	nclav-P1.14.2AC.SH 75	Another Deductive Form of nclav-P1.14 73.
⊢ (𝛾₁ → (𝛾₂ → (𝜑 → ¬ 𝜑)))    ⇒   ⊢ (𝛾₁ → (𝛾₂ → ¬ 𝜑))
2.2.2  Transposition Laws.
Theorem	trnsp-P1.15a 76	Transposition Variant A.
⊢ ((𝜑 → ¬ 𝜓) → (𝜓 → ¬ 𝜑))
Theorem	trnsp-P1.15a.SH 77	Inference from trnsp-P1.15a 76.
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜓 → ¬ 𝜑)
Theorem	trnsp-P1.15b 78	Transposition Variant B.
⊢ ((¬ 𝜑 → 𝜓) → (¬ 𝜓 → 𝜑))
Theorem	trnsp-P1.15b.AC.SH 79	Deductive Form of trnsp-P1.15b 78.
⊢ (𝛾 → (¬ 𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (¬ 𝜓 → 𝜑))
Theorem	trnsp-P1.15c 80	Transposition Variant C.
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))
Theorem	trnsp-P1.15c.SH 81	Inference from trnsp-P1.15c 80.
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (¬ 𝜓 → ¬ 𝜑)
Theorem	trnsp-P1.15c.AC.SH 82	Deductive Form of trnsp-P1.15c 80
⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (¬ 𝜓 → ¬ 𝜑))
Theorem	trnsp-P1.15d 83	Transposition Variant D.
⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))
Theorem	trnsp-P1.15d.AC.SH 84	Deductive Form of trnsp-P1.15d 83.
⊢ (𝛾 → (¬ 𝜑 → ¬ 𝜓))    ⇒   ⊢ (𝛾 → (𝜓 → 𝜑))
Theorem	trnsp-P1.15d.2AC.SH 85	Another Deductive Form of trnsp-P1.15d 83.
⊢ (𝛾₁ → (𝛾₂ → (¬ 𝜑 → ¬ 𝜓)))    ⇒   ⊢ (𝛾₁ → (𝛾₂ → (𝜓 → 𝜑)))
2.2.3  Classical Arguments.
Theorem	pfbycont-P1.16 86	Proof by Contradiction.
⊢ ((𝜑 → 𝜓) → ((𝜑 → ¬ 𝜓) → ¬ 𝜑))
Theorem	pfbycont-P1.16.AC.2SH 87	Deductive Form of pfbycont-P1.16 86.
⊢ (𝛾 → (𝜑 → 𝜓))    &   ⊢ (𝛾 → (𝜑 → ¬ 𝜓))    ⇒   ⊢ (𝛾 → ¬ 𝜑)
Theorem	pfbycase-P1.17 88	Proof by Cases.
⊢ ((𝜑 → 𝜓) → ((¬ 𝜑 → 𝜓) → 𝜓))
Theorem	pfbycase-P1.17.2SH 89	Inference from pfbycase-P1.17 88
⊢ (𝜑 → 𝜓)    &   ⊢ (¬ 𝜑 → 𝜓)    ⇒   ⊢ 𝜓
Theorem	pfbycase-P1.17.AC.2SH 90	Deductive Form of pfbycase-P1.17 88.
⊢ (𝛾 → (𝜑 → 𝜓))    &   ⊢ (𝛾 → (¬ 𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → 𝜓)
PART 3  Chapter 2: Propositional Calculus (Defined Connectives)
3.1  Development. To more easily understand the theorems below, let 'conj(𝜑, 𝜓)' be an abbreviation for '¬ (𝜑 → ¬ 𝜓)'. This is the conjunction of the WFFs '𝜑' and '𝜓'. This will later be defined using the '∧' (and) symbol.
Theorem	import-L2.1a 91	Importation Lemma.
⊢ ((𝜑 → (𝜓 → 𝜒)) → (¬ (𝜑 → ¬ 𝜓) → 𝜒))
Theorem	import-L2.1a.SH 92	Inference from import-L2.1a 91.
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜒)
Theorem	export-L2.1b 93	Exportation Lemma.
⊢ ((¬ (𝜑 → ¬ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒)))
Theorem	export-L2.1b.SH 94	Inference from export-L2.1b 93.
⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	simpl-L2.2a 95	Left Simplification Lemma.
⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜑)
Theorem	simpl-L2.2a.SH 96	Inference from simpl-L2.2a 95.
⊢ ¬ (𝜑 → ¬ 𝜓)    ⇒   ⊢ 𝜑
Theorem	simpr-L2.2b 97	Right Simplification Lemma.
⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜓)
Theorem	simpr-L2.2b.SH 98	Inference from simpr-L2.2b 97.
⊢ ¬ (𝜑 → ¬ 𝜓)    ⇒   ⊢ 𝜓
Theorem	cmb-L2.3 99	Combining Lemma.
⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
Theorem	cmb-L2.3.2SH 100	Inference from cmb-L2.3 99.
⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ ¬ (𝜑 → ¬ 𝜓)