mmtheorems17 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17500 176 17501-17600 177 17601-17700 178 17701-17800 179 17801-17900 180 17901-18000 181 18001-18100 182 18101-18200 183 18201-18300 184 18301-18400 185 18401-18500 186 18501-18600 187 18601-18700 188 18701-18800 189 18801-18900 190 18901-19000 191 19001-19100 192 19101-19200 193 19201-19300 194 19301-19400 195 19401-19465

Type

Label

Description

Statement

Theorem

simplbi2comOLD 1601

Obsolete version of simplbi2com 1600.

|- (ph <-> (ps /\ ch))   =>   |- (ch -> (ps -> ph))

Theorem

ee1111 1602

Non-virtual deduction form of e1111 17662. (Contributed by Alan Sare, 18-Mar-2012.). The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The completed Virtual Deduction Proof (not shown) was minimized. The minimized proof is shown.

h1::	|- (ph -> ps)
h2::	|- (ph -> ch)
h3::	|- (ph -> th)
h4::	|- (ph -> ta)
h5::	|- (ps -> (ch -> (th -> (ta -> et))))
6:1,5:	|- (ph -> (ch -> (th -> (ta -> et))))
7:6:	|- (ch -> (ph -> (th -> (ta -> et))))
8:2,7:	|- (ph -> (ph -> (th -> (ta -> et))))
9:8:	|- (ph -> (th -> (ta -> et)))
10:9:	|- (th -> (ph -> (ta -> et)))
11:3,10:	|- (ph -> (ph -> (ta -> et)))
12:11:	|- (ph -> (ta -> et))
13:12:	|- (ta -> (ph -> et))
14:4,13:	|- (ph -> (ph -> et))
qed:14:	|- (ph -> et)

|- (ph -> ps)   &   |- (ph -> ch)   &   |- (ph -> th)   &   |- (ph -> ta)   &   |- (ps -> (ch -> (th -> (ta -> et))))   =>   |- (ph -> et)

Theorem

pm2.43bgbi 1603

Logical equivalence of a 2-left-nested implication and a 1-left-nested implicated when two antecedents of the former implication are identical. (Contributed by Alan Sare, 18-Mar-2012.). The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The completed Virtual Deduction Proof (not shown) was minimized. The minimized proof is shown.

1::	|- ((ph -> (ps -> (ph -> ch))) -> (ph -> (ph -> (ps -> ch))))
2::	|- ((ph -> (ph -> (ps -> ch))) -> (ph -> (ps -> ch)))
3:1,2:	|- ((ph -> (ps -> (ph -> ch))) -> (ph -> (ps -> ch)))
4::	|- ((ph -> (ps -> ch)) -> (ps -> (ph -> ch)))
5:3,4:	|- ((ph -> (ps -> (ph -> ch))) -> (ps -> (ph -> ch)))
6::	|- ((ps -> (ph -> ch)) -> (ph -> (ps -> (ph -> ch))))
qed:5,6:	|- ((ph -> (ps -> (ph -> ch))) <-> (ps -> (ph -> ch)))

|- ((ph -> (ps -> (ph -> ch))) <-> (ps -> (ph -> ch)))

Theorem

pm2.43cbi 1604

Logical equivalence of a 3-left-nested implication and a 2-left-nested implicated when two antecedents of the former implication are identical. (Contributed by Alan Sare, 18-Mar-2012.). The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The completed Virtual Deduction Proof (not shown) was minimized. The minimized proof is shown.

1::	|- ((ph -> (ps -> (ch -> (ph -> th))) ) -> (ph -> (ps -> (ph -> (ch -> th)))))
2::	|- ((ph -> (ps -> (ph -> (ch -> th))) ) -> (ps -> (ph -> (ch -> th))))
3:1,2:	|- ((ph -> (ps -> (ch -> (ph -> th))) ) -> (ps -> (ph -> (ch -> th))))
4::	|- ((ps -> (ph -> (ch -> th))) -> (ps -> (ch -> (ph -> th))))
5:3,4:	|- ((ph -> (ps -> (ch -> (ph -> th))) ) -> (ps -> (ch -> (ph -> th))))
6::	|- ((ps -> (ch -> (ph -> th))) -> (ph -> (ps -> (ch -> (ph -> th)))))
qed:5,6:	|- ((ph -> (ps -> (ch -> (ph -> th))) ) <-> (ps -> (ch -> (ph -> th))))

|- ((ph -> (ps -> (ch -> (ph -> th)))) <-> (ps -> (ch -> (ph -> th))))

Theorem

ee233 1605

Non-virtual deduction form of e233 17727. (Contributed by Alan Sare, 18-Mar-2012.) The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The completed Virtual Deduction Proof (not shown) was minimized. The minimized proof is shown.

h1::	|- (ph -> (ps -> ch))
h2::	|- (ph -> (ps -> (th -> ta)))
h3::	|- (ph -> (ps -> (th -> et)))
h4::	|- (ch -> (ta -> (et -> ze)))
5:1,4:	|- (ph -> (ps -> (ta -> (et -> ze))) )
6:5:	|- (ta -> (ph -> (ps -> (et -> ze))) )
7:2,6:	|- (ph -> (ps -> (th -> (ph -> (ps -> (et -> ze))))))
8:7:	|- (ps -> (th -> (ph -> (ps -> (et -> ze)))))
9:8:	|- (th -> (ph -> (ps -> (et -> ze))) )
10:9:	|- (ph -> (ps -> (th -> (et -> ze))) )
11:10:	|- (et -> (ph -> (ps -> (th -> ze))) )
12:3,11:	|- (ph -> (ps -> (th -> (ph -> (ps -> (th -> ze))))))
13:12:	|- (ps -> (th -> (ph -> (ps -> (th -> ze)))))
14:13:	|- (th -> (ph -> (ps -> (th -> ze))) )
qed:14:	|- (ph -> (ps -> (th -> ze)))

|- (ph -> (ps -> ch))   &   |- (ph -> (ps -> (th -> ta)))   &   |- (ph -> (ps -> (th -> et)))   &   |- (ch -> (ta -> (et -> ze)))   =>   |- (ph -> (ps -> (th -> ze)))

Theorem

imbi12 1606

Implication form of imbi12i 376. imbi12 1606 is imbi12VD 17792 without virtual deductions and was automatically derived from imbi12VD 17792 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.)

|- ((ph <-> ps) -> ((ch <-> th) -> ((ph -> ch) <-> (ps -> th))))

Theorem

imbi13 1607

Join three logical equivalences to form equivalence of implications. imbi13 1607 is imbi13VD 17793 without virtual deductions and was automatically derived from imbi13VD 17793 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.)

|- ((ph <-> ps) -> ((ch <-> th) -> ((ta <-> et) -> ((ph -> (ch -> ta)) <-> (ps -> (th -> et))))))

Theorem

ee21 1608

e21 17693 without virtual deductions.

|- (ph -> (ps -> ch))   &   |- (ph -> th)   &   |- (ch -> (th -> ta))   =>   |- (ph -> (ps -> ta))

Theorem

ee33 1609

Non-virtual deduction form of e33 17697. (Contributed by Alan Sare, 18-Mar-2012.). The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The completed Virtual Deduction Proof (not shown) was minimized. The minimized proof is shown.

h1::	|- (ph -> (ps -> (ch -> th)))
h2::	|- (ph -> (ps -> (ch -> ta)))
h3::	|- (th -> (ta -> et))
4:1,3:	|- (ph -> (ps -> (ch -> (ta -> et))))
5:4:	|- (ta -> (ph -> (ps -> (ch -> et))))
6:2,5:	|- (ph -> (ps -> (ch -> (ph -> (ps -> (ch -> et))))))
7:6:	|- (ps -> (ch -> (ph -> (ps -> (ch -> et)))))
8:7:	|- (ch -> (ph -> (ps -> (ch -> et))))
qed:8:	|- (ph -> (ps -> (ch -> et)))

|- (ph -> (ps -> (ch -> th)))   &   |- (ph -> (ps -> (ch -> ta)))   &   |- (th -> (ta -> et))   =>   |- (ph -> (ps -> (ch -> et)))

Theorem

ee10 1610

e10 17682 without virtual deductions.

|- (ph -> ps)   &   |- ch   &   |- (ps -> (ch -> th))   =>   |- (ph -> th)

Theorem

iin1 1611

in1 17573 without virtual deductions.

|- (ph -> ps)   =>   |- (ph -> ps)

Theorem

ee02 1612

e02 17685 without virtual deductions.

|- ph   &   |- (ps -> (ch -> th))   &   |- (ph -> (th -> ta))   =>   |- (ps -> (ch -> ta))

Predicate calculus axiomatization

The axioms of predicate calculus

Syntax

wal 1613

Extend wff definition to include the universal quantifier ('for all'). A.xph is read "ph (phi) is true for all x." Typically, in its final application ph would be replaced with a wff containing a (free) occurrence of the variable x, for example x = y. In a universe with a finite number of objects, "for all" is equivalent to a big conjunction (AND) with one wff for each possible case of x. When the universe is infinite (as with set theory), such a propositional-calculus equivalent is not possible because an infinitely long formula has no meaning, but conceptually the idea is the same.

wff A.xph

Syntax

cv 1614

This syntax construction states that a variable x, which has been declared to be a set variable by $f statement vx, is also a class expression. This can be justified informally as follows. We know that the class builder {y | y e. x} is a class by cab 2157. Since (when y is distinct from x) we have x = {y | y e. x} by cvjust 2165, we can argue that that the syntax "class x " can be viewed as an abbreviation for "class {y | y e. x}". See the discussion under the definition of class in [Jech] p. 4 showing that "Every set can be considered to be a class."

While it is tempting and perhaps occasionally useful to view cv 1614 as a "type conversion" from a set variable to a class variable, keep in mind that cv 1614 is intrinsically no different from any other class-building syntax such as cab 2157, cun 2857, or c0 3114.

(The description above applies to set theory, not predicate calculus. The purpose of introducing class x here, and not in set theory where it belongs, is to allow us to express i.e. "prove" the weq 1616 of predicate calculus from the wceq 1615 of set theory, so that we don't "overload" the = connective with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers.)

class x

Syntax

wceq 1615

Extend wff definition to include class equality.

(The purpose of introducing wff A = B here, and not in set theory where it belongs, is to allow us to express i.e. "prove" the weq 1616 of predicate calculus in terms of the wceq 1615 of set theory, so that we don't "overload" the = connective with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers. For example, some parsers - although not the Metamath program - stumble on the fact that the = in x = y could be the = of either weq 1616 or wceq 1615, although mathematically it makes no difference. The class variables A and B are introduced temporarily for the purpose of this definition but otherwise not used in predicate calculus. See df-cleq 2163 for more information on the set theory usage of wceq 1615.)

wff A = B

Theorem

weq 1616

Extend wff definition to include atomic formulas using the equality predicate.

(Instead of introducing weq 1616 as an axiomatic statement, as was done in an older version of this database, we introduce it by "proving" a special case of set theory's more general wceq 1615. This lets us avoid overloading the = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1616 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1615. Note: To see the proof steps of this syntax proof, type "show proof weq /all" in the Metamath program.)

wff x = y

Syntax

wcel 1617

Extend wff definition to include the membership connective between classes.

(The purpose of introducing wff A e. B here is to allow us to express i.e. "prove" the wel 1618 of predicate calculus in terms of the wceq 1615 of set theory, so that we don't "overload" the e. connective with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers. The class variables A and B are introduced temporarily for the purpose of this definition but otherwise not used in predicate calculus. See df-clab 2158 for more information on the set theory usage of wcel 1617.)

wff A e. B

Theorem

wel 1618

Extend wff definition to include atomic formulas with the epsilon (membership) predicate. This is read "x is an element of y," "x is a member of y," "x belongs to y," or "y contains x." Note: The phrase "y includes x " means "x is a subset of y;" to use it also for x e. y, as some authors occasionally do, is poor form and causes confusion, according to George Boolos (1992 lecture at MIT).

This syntactical construction introduces a binary non-logical predicate symbol e. (epsilon) into our predicate calculus. We will eventually use it for the membership predicate of set theory, but that is irrelevant at this point: the predicate calculus axioms for e. apply to any arbitrary binary predicate symbol. "Non-logical" means that the predicate is presumed to have additional properties beyond the realm of predicate calculus, although these additional properties are not specified by predicate calculus itself but rather by the axioms of a theory (in our case set theory) added to predicate calculus. "Binary" means that the predicate has two arguments.

(Instead of introducing wel 1618 as an axiomatic statement, as was done in an older version of this database, we introduce it by "proving" a special case of set theory's more general wcel 1617. This lets us avoid overloading the e. connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1618 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1617. Note: To see the proof steps of this syntax proof, type "show proof wel /all" in the Metamath program.)

wff x e. y

Axiom

ax-5 1619

Axiom of Quantified Implication. Axiom C4 of [Monk2] p. 105.

|- (A.x(ph -> ps) -> (A.xph -> A.xps))

Axiom

ax-6 1620

Axiom of Quantified Negation. Axiom C5-2 of [Monk2] p. 113.

|- (-. A.xph -> A.x -. A.xph)

Axiom

ax-7 1621

Axiom of Quantifier Commutation. This axiom says universal quantifiers can be swapped. One of the 4 axioms of pure predicate calculus. Axiom scheme C6' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Lemma 12 of [Monk2] p. 109 and Axiom C5-3 of [Monk2] p. 113. An alternate axiomatization could use ax467 1688 in place of ax-4 1637, ax-6o 1642, and ax-7 1621.

|- (A.xA.yph -> A.yA.xph)

Axiom

ax-gen 1622

Rule of Generalization. The postulated inference rule of pure predicate calculus. See e.g. Rule 2 of [Hamilton] p. 74. This rule says that if something is unconditionally true, then it is true for all values of a variable. For example, if we have proved x = x, we can conclude A.xx = x or even A.yx = x. Theorem a4i 1646 shows we can go the other way also: in other words we can add or remove universal quantifiers from the beginning of any theorem as required.

|- ph   =>   |- A.xph

Axiom

ax-8 1623

Axiom of Equality. One of the equality and substitution axioms of predicate calculus with equality. This is similar to, but not quite, a transitive law for equality (proved later as equtr 1801). Axiom scheme C8' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom C7 of [Monk2] p. 105.

Axioms ax-8 1623 through ax-16 1883 are the axioms having to do with equality, substitution, and logical properties of our binary predicate e. (which later in set theory will mean "is a member of"). Note that all axioms except ax-16 1883 and ax-17 1634 are still valid even when x, y, and z are replaced with the same variable because they do not have any distinct variable (Metamath's $d) restrictions. Distinct variable restrictions are required for ax-16 1883 and ax-17 1634 only.

|- (x = y -> (x = z -> y = z))

Axiom

ax-9 1624

Axiom of Existence. One of the equality and substitution axioms of predicate calculus with equality. One thing this axiom tells us is that at least one thing exists (although ax-4 1637 and possibly others also tell us that, i.e. they are not valid in the empty domain of a "free logic.") In this form (not requiring that x and y be distinct) it was used in an axiom system of Tarski (see Axiom B7' in footnote 1 of [KalishMontague] p. 81.) It is equivalent to axiom scheme C10' in [Megill] p. 448 (p. 16 of the preprint); the equivalence is established by ax9o 1791 and ax9 1793. A more convenient form of this axiom is a9e 1794, which has additional remarks.

Raph Levien proved the independence of this axiom from the others on 12-Apr-2005. See item 16 at http://us.metamath.org/award2003.html.

|- -. A.x -. x = y

Axiom

ax-10 1625

Axiom of Quantifier Substitution. One of the equality and substitution axioms of predicate calculus with equality. Appears as Lemma L12 in [Megill] p. 445 (p. 12 of the preprint).

The original version of this axiom was ax-10o 1810 ("o" for "old") and was replaced with this shorter ax-10 1625 in May 2008. The old axiom is proved from this one as theorem ax10o 1809. Conversely, this axiom is proved from ax-10o 1810 as theorem ax10 1811.

|- (A.x x = y -> A.y y = x)

Axiom

ax-11 1626

Axiom of Variable Substitution. One of the 5 equality axioms of predicate calculus. The final consequent A.x(x = y -> ph) is a way of expressing "y substituted for x in wff ph " (cf. sb6 1943). It is based on Lemma 16 of [Tarski] p. 70 and Axiom C8 of [Monk2] p. 105, from which it can be proved by cases.

The original version of this axiom was ax-11o 1893 ("o" for "old") and was replaced with this shorter ax-11 1626 in Jan. 2007. The old axiom is proved from this one as theorem ax11o 1892. Conversely, this axiom is proved from ax-11o 1893 as theorem ax11 1894.

Juha Arpiainen proved the independence of this axiom (in the form of the older axiom ax-11o 1893) from the others on 19-Jan-2006. See item 9a at http://us.metamath.org/award2003.html.

Interestingly, if the wff expression substituted for ph contains no wff variables, the resulting statement can be proved without invoking this axiom. This means that even though this axiom is metalogically independent from the others, it is not logically independent. Specifically, we can prove any wff-variable-free instance of axiom ax-11o 1893 (from which the ax-11 1626 instance follows by theorem ax11 1894.) The proof is by induction on formula length, using ax11eq 2047 and ax11el 2048 for the basis steps and ax11indn 2050, ax11indi 2051, and ax11inda 2055 for the induction steps.

See also ax11v 1941 and ax11v2 1890 for other equivalents of this axiom that (unlike this axiom) have distinct variable restrictions.

|- (x = y -> (A.yph -> A.x(x = y -> ph)))

Axiom

ax-12 1627

Axiom of Quantifier Introduction. One of the equality and substitution axioms of predicate calculus with equality. Informally, it says that whenever z is distinct from x and y, and x = y is true, then x = y quantified with z is also true. In other words, z is irrelevant to the truth of x = y. Axiom scheme C9' in [Megill] p. 448 (p. 16 of the preprint). It apparently does not otherwise appear in the literature but is easily proved from textbook predicate calculus by cases.

An open problem is whether this axiom is redundant. Note that the analogous axiom for the membership connective, ax-15 2044, has been shown to be redundant. It is also unknown whether this axiom can be replaced by a shorter formula. However, it can be derived from two slightly shorter formulas, as shown by a12study 2062.

|- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))

Axiom

ax-13 1628

Axiom of Equality. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. It substitutes equal variables into the left-hand side of the e. binary predicate. Axiom scheme C12' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Axiom B8 (p. 75) of system S2 of [Tarski] p. 77. "Non-logical" means that the predicate is not a primitive of predicate calculus proper but instead is an extension to it. "Binary" means that the predicate has two arguments. In a system of predicate calculus with equality, like ours, equality is not usually considered to be a non-logical predicate. In systems of predicate calculus without equality, it typically would be.

|- (x = y -> (x e. z -> y e. z))

Axiom

ax-14 1629

Axiom of Equality. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. It substitutes equal variables into the right-hand side of the e. binary predicate. Axiom scheme C13' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Axiom B8 (p. 75) of system S2 of [Tarski] p. 77.

|- (x = y -> (z e. x -> z e. y))

Some theorems that use neither ax-17 nor ax-4

Theorem

hbequid 1630

A more general version of hbequid2 1842 using ax-5 1619, ax-8 1623, ax-12 1627, and ax-gen 1622.

|- (x = x -> A.y x = x)

Theorem

equidqe 1631

equid 1795 with existential quantifier without using ax-4 1637 or ax-17 1634.

|- -. A.y -. x = x

Theorem

equidq 1632

equid 1795 with universal quantifier without using ax-4 1637 or ax-17 1634.

|- A.y x = x

Theorem

ax4sp1 1633

A special case of ax-4 1637 without using ax-4 1637 or ax-17 1634.

|- (A.y -. x = x -> -. x = x)

Axiom ax-17 - first use of the $d distinct variable statement

Axiom

ax-17 1634

Axiom to quantify a variable over a formula in which it does not occur. Axiom C5 in [Megill] p. 444 (p. 11 of the preprint). Also appears as Axiom B6 (p. 75) of system S2 of [Tarski] p. 77 and Axiom C5-1 of [Monk2] p. 113.

This axiom is logically redundant in the (logically complete) predicate calculus axiom system consisting of ax-gen 1622, ax-4 1637 through ax-9 1624, ax-10o 1810, and ax-12 1627 through ax-16 1883: in that system, we can derive any instance of ax-17 1634 not containing wff variables by induction on formula length, using ax17eq 1884 and ax17el 2045 for the basis together hbn 1669, hbal 1670, and hbim 1672. However, if we omit this axiom, our development would be quite inconvenient since we could work only with specific instances of wffs containing no wff variables - this axiom introduces the concept of a set variable not occurring in a wff (as opposed to just two set variables being distinct).

|- (ph -> A.xph)

Theorem

a17d 1635

ax-17 1634 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as hbeleqd 2700.

|- (ph -> (ps -> A.xps))

Derive ax-4, ax-5o, and ax-6o

Theorem

ax4 1636

Theorem showing that ax-4 1637 can be derived from ax-5 1619, ax-gen 1622, ax-8 1623, ax-9 1624, ax-11 1626, and ax-17 1634 and is therefore redundant in a system including the latter axioms. Lemma 21 of [Monk2] p. 114.

This theorem should not be referenced in any proof. Instead, we will use ax-4 1637 below so that explicit uses of ax-4 1637 can be more easily identified. In particular, this will more cleanly separate out the theorems of "pure" predicate calculus that don't involve equality or distinct variables. A beginner may wish to accept ax-4 1637 a priori, so that the proof of this theorem (ax4 1636), which involves equality as well as the distinct variable requirements of ax-17 1634, can be put off until those axioms are studied.

Note: All predicate calculus axioms introduced from this point forward are redundant. Immediately before their introduction, we prove them from earlier axioms to demonstrate their redundancy. Specifically, redundant axioms ax-4 1637, ax-5o 1639, ax-6o 1642, ax-9o 1792, ax-10o 1810, ax-11o 1893, ax-15 2044, and ax-16 1883 are proved by theorems ax4 1636, ax5o 1638, ax6o 1641, ax9o 1791, ax10o 1809, ax11o 1892, ax15 2043, and ax16 1882. We never reference those theorems directly - instead, we use the axiom version that immediately follows it - in order to better isolate the uses of the redundant axioms for easier study of subsystems containing them.

(The proof was shortened by Scott Fenton, 24-Jan-2011.)

|- (A.xph -> ph)

Axiom

ax-4 1637

Axiom of Specialization. A quantified wff implies the wff without a quantifier (i.e. an instance, or special case, of the generalized wff). In other words if something is true for all x, it is true for any specific x (that would typically occur as a free variable in the wff substituted for ph). (A free variable is one that does not occur in the scope of a quantifier: x and y are both free in x = y, but only x is free in A.yx = y.) This is one of the axioms of what we call "pure" predicate calculus (ax-4 1637 through ax-7 1621 plus rule ax-gen 1622). Axiom scheme C5' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom B5 of [Tarski] p. 67 (under his system S2, defined in the last paragraph on p. 77).

Note that the converse of this axiom does not hold in general, but a weaker inference form of the converse holds and is expressed as rule ax-gen 1622. Conditional forms of the converse are given by ax-12 1627, ax-15 2044, ax-16 1883, and ax-17 1634.

Unlike the more general textbook Axiom of Specialization, we cannot choose a variable different from x for the special case. For use, that requires the assistance of equality axioms, and we deal with it later after we introduce the definition of proper substitution - see stdpc4 1858.

An nice alternate axiomatization uses ax467 1688 and ax-5o 1639 in place of ax-4 1637, ax-5 1619, ax-6 1620, and ax-7 1621.

This axiom is redundant in the presence of certain other axioms, as shown by theorem ax4 1636. (We replaced the older ax-5o 1639 and ax-6o 1642 with newer versions ax-5 1619 and ax-6 1620 in order to prove this redundancy.)

|- (A.xph -> ph)

Theorem

ax5o 1638

Show that the original axiom ax-5o 1639 can be derived from ax-5 1619 and others. See ax5 1640 for the rederivation of ax-5 1619 from ax-5o 1639.

Part of the proof is based on the proof of Lemma 22 of [Monk2] p. 114.

This theorem should not be referenced in any proof. Instead, use ax-5o 1639 below so that uses of ax-5o 1639 can be more easily identified.

|- (A.x(A.xph -> ps) -> (A.xph -> A.xps))

Axiom

ax-5o 1639

Axiom of Quantified Implication. This axiom moves a quantifier from outside to inside an implication, quantifying ps. Notice that x must not be a free variable in the antecedent of the quantified implication, and we express this by binding ph to "protect" the axiom from a ph containing a free x. One of the 4 axioms of "pure" predicate calculus. Axiom scheme C4' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Lemma 5 of [Monk2] p. 108 and Axiom 5 of [Mendelson] p. 69.

This axiom is redundant, as shown by theorem ax5o 1638.

|- (A.x(A.xph -> ps) -> (A.xph -> A.xps))

Theorem

ax5 1640

Rederivation of axiom ax-5 1619 from the orginal version, ax-5o 1639. See ax5o 1638 for the derivation of ax-5o 1639 from ax-5 1619.

This theorem should not be referenced in any proof. Instead, use ax-5 1619 above so that uses of ax-5 1619 can be more easily identified.

Note: This is the same as theorem alim 1658 below. It is proved separately here so that it won't be dependent on the axioms used for alim 1658 (which may change in the future).

|- (A.x(ph -> ps) -> (A.xph -> A.xps))

Theorem

ax6o 1641

Show that the original axiom ax-6o 1642 can be derived from ax-6 1620 and others. See ax6 1643 for the rederivation of ax-6 1620 from ax-6o 1642.

This theorem should not be referenced in any proof. Instead, use ax-6o 1642 below so that uses of ax-6o 1642 can be more easily identified.

|- (-. A.x -. A.xph -> ph)

Axiom

ax-6o 1642

Axiom of Quantified Negation. This axiom is used to manipulate negated quantifiers. One of the 4 axioms of pure predicate calculus. Equivalent to axiom scheme C7' in [Megill] p. 448 (p. 16 of the preprint). An alternate axiomatization could use ax467 1688 in place of ax-4 1637, ax-6o 1642, and ax-7 1621.

This axiom is redundant, as shown by theorem ax6o 1641.

|- (-. A.x -. A.xph -> ph)

Theorem

ax6 1643

Rederivation of axiom ax-6 1620 from the orginal version, ax-6o 1642. See ax6o 1641 for the derivation of ax-6o 1642 from ax-6 1620.

This theorem should not be referenced in any proof. Instead, use ax-6 1620 above so that uses of ax-6 1620 can be more easily identified.

|- (-. A.xph -> A.x -. A.xph)

Predicate calculus without distinct variables

"Pure" predicate calculus ax-4, ax-5o, ax-6o, ax-gen

Syntax

wex 1644

Extend wff definition to include the existential quantifier ("there exists").

wff E.xph

Definition

df-ex 1645

Define existential quantification. E.xph means "there exists at least one set x such that ph is true." Definition of [Margaris] p. 49.

|- (E.xph <-> -. A.x -. ph)

Theorem

a4i 1646

Inference rule reversing generalization.

|- A.xph   =>   |- ph

Theorem

gen2 1647

Generalization applied twice.

|- ph   =>   |- A.xA.yph

Theorem

a4s 1648

Generalization of antecedent.

|- (ph -> ps)   =>   |- (A.xph -> ps)

Theorem

a4sd 1649

Deduction generalizing antecedent.

|- (ph -> (ps -> ch))   =>   |- (ph -> (A.xps -> ch))

Theorem

mpg 1650

Modus ponens combined with generalization.

|- (A.xph -> ps)   &   |- ph   =>   |- ps

Theorem

mpgbi 1651

Modus ponens on biconditional combined with generalization. (The proof was shortened by Stefan Allan, 28-Oct-2008.)

|- (A.xph <-> ps)   &   |- ph   =>   |- ps

Theorem

mpgbir 1652

Modus ponens on biconditional combined with generalization. (The proof was shortened by Stefan Allan, 28-Oct-2008.)

|- (ph <-> A.xps)   &   |- ps   =>   |- ph

Theorem

a5i 1653

Inference from ax-5o 1639.

|- (A.xph -> ps)   =>   |- (A.xph -> A.xps)

Theorem

a6e 1654

Abbreviated version of ax-6o 1642.

|- (E.xA.xph -> ph)

Theorem

a7s 1655

Swap quantifiers in an antecedent.

|- (A.xA.yph -> ps)   =>   |- (A.yA.xph -> ps)

Theorem

alimi 1656

Inference quantifying both antecedent and consequent.

|- (ph -> ps)   =>   |- (A.xph -> A.xps)

Theorem

2alimi 1657

Inference doubly quantifying both antecedent and consequent.

|- (ph -> ps)   =>   |- (A.xA.yph -> A.xA.yps)

Theorem

alim 1658

Theorem 19.20 of [Margaris] p. 90. (The proof was shortened by O'Cat, 30-Mar-2008.)

|- (A.x(ph -> ps) -> (A.xph -> A.xps))

Theorem

al2imi 1659

Inference quantifying antecedent, nested antecedent, and consequent.

|- (ph -> (ps -> ch))   =>   |- (A.xph -> (A.xps -> A.xch))

Theorem

alanimi 1660

Variant of al2imi 1659 with conjunctive antecedent. (Contributed by Andrew Salmon, 8-Jun-2011.)

|- ((ph /\ ps) -> ch)   =>   |- ((A.xph /\ A.xps) -> A.xch)

Theorem

alimd 1661

Deduction from Theorem 19.20 of [Margaris] p. 90.

|- (ph -> A.xph)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (A.xps -> A.xch))

Theorem

albi 1662

Theorem 19.15 of [Margaris] p. 90.

|- (A.x(ph <-> ps) -> (A.xph <-> A.xps))

Theorem

19.21ai 1663

Inference from Theorem 19.21 of [Margaris] p. 90.

|- (ph -> A.xph)   &   |- (ph -> ps)   =>   |- (ph -> A.xps)

Theorem

albii 1664

Inference adding universal quantifier to both sides of an equivalence.

|- (ph <-> ps)   =>   |- (A.xph <-> A.xps)

Theorem

2albii 1665

Inference adding 2 universal quantifiers to both sides of an equivalence.

|- (ph <-> ps)   =>   |- (A.xA.yph <-> A.xA.yps)

Theorem

hbth 1666

No variable is (effectively) free in a theorem.

This and later "hypothesis-building" lemmas, with labels starting "hb...", allow us to construct proofs of formulas of the form |- (ph -> A.xph) from smaller formulas of this form. These are useful for constructing hypotheses that state "x is (effectively) not free in ph."

|- ph   =>   |- (ph -> A.xph)

Theorem

hbnt 1667

Closed theorem version of bound-variable hypothesis builder hbn 1669.

|- (A.x(ph -> A.xph) -> (-. ph -> A.x -. ph))

Theorem

hba1 1668

x is not free in A.xph. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114.

|- (A.xph -> A.xA.xph)

Theorem

hbn 1669

If x is not free in ph, it is not free in -. ph.

|- (ph -> A.xph)   =>   |- (-. ph -> A.x -. ph)

Theorem

hbal 1670

If x is not free in ph, it is not free in A.yph.

|- (ph -> A.xph)   =>   |- (A.yph -> A.xA.yph)

Theorem

hbex 1671

If x is not free in ph, it is not free in E.yph.

|- (ph -> A.xph)   =>   |- (E.yph -> A.xE.yph)

Theorem

hbim 1672

If x is not free in ph and ps, it is not free in (ph -> ps). (The proof was shortened by O'Cat, 3-Mar-2008.)

|- (ph -> A.xph)   &   |- (ps -> A.xps)   =>   |- ((ph -> ps) -> A.x(ph -> ps))

Theorem

hbor 1673

If x is not free in ph and ps, it is not free in (ph \/ ps).

|- (ph -> A.xph)   &   |- (ps -> A.xps)   =>   |- ((ph \/ ps) -> A.x(ph \/ ps))

Theorem

hban 1674

If x is not free in ph and ps, it is not free in (ph /\ ps).

|- (ph -> A.xph)   &   |- (ps -> A.xps)   =>   |- ((ph /\ ps) -> A.x(ph /\ ps))

Theorem

hbbi 1675

If x is not free in ph and ps, it is not free in (ph <-> ps).

|- (ph -> A.xph)   &   |- (ps -> A.xps)   =>   |- ((ph <-> ps) -> A.x(ph <-> ps))

Theorem

hb3or 1676

If x is not free in ph, ps, and ch, it is not free in (ph \/ ps \/ ch).

|- (ph -> A.xph)   &   |- (ps -> A.xps)   &   |- (ch -> A.xch)   =>   |- ((ph \/ ps \/ ch) -> A.x(ph \/ ps \/ ch))

Theorem

hb3an 1677

If x is not free in ph, ps, and ch, it is not free in (ph /\ ps /\ ch).

|- (ph -> A.xph)   &   |- (ps -> A.xps)   &   |- (ch -> A.xch)   =>   |- ((ph /\ ps /\ ch) -> A.x(ph /\ ps /\ ch))

Theorem

hba2 1678

Lemma 24 of [Monk2] p. 114.

|- (A.yA.xph -> A.xA.yA.xph)

Theorem

hbia1 1679

Lemma 23 of [Monk2] p. 114.

|- ((A.xph -> A.xps) -> A.x(A.xph -> A.xps))

Theorem

hbn1 1680

x is not free in -. A.xph.

|- (-. A.xph -> A.x -. A.xph)

Theorem

hbe1 1681

x is not free in E.xph.

|- (E.xph -> A.xE.xph)

Theorem

ax46 1682

Proof of a single axiom that can replace ax-4 1637 and ax-6o 1642. See ax46to4 1683 and ax46to6 1684 for the re-derivation of those axioms. (Contributed by Scott Fenton, 12-Sep-2005.)

|- ((A.x -. A.xph -> A.xph) -> ph)

Theorem

ax46to4 1683

Re-derivation of ax-4 1637 from ax46 1682. Only propositional calculus is used for the re-derivation. (Contributed by Scott Fenton, 12-Sep-2005.)

|- (A.xph -> ph)

Theorem

ax46to6 1684

Re-derivation of ax-6o 1642 from ax46 1682. Only propositional calculus is used for the re-derivation. (Contributed by Scott Fenton, 12-Sep-2005.)

|- (-. A.x -. A.xph -> ph)

Theorem

ax67 1685

Proof of a single axiom that can replace both ax-6o 1642 and ax-7 1621. See ax67to6 1686 and ax67to7 1687 for the re-derivation of those axioms.

|- (-. A.x -. A.yA.xph -> A.yph)

Theorem

ax67to6 1686

Re-derivation of ax-6o 1642 from ax67 1685. Note that ax-6o 1642 and ax-7 1621 are not used by the re-derivation.

|- (-. A.x -. A.xph -> ph)

Theorem

ax67to7 1687

Re-derivation of ax-7 1621 from ax67 1685. Note that ax-6o 1642 and ax-7 1621 are not used by the re-derivation.

|- (A.xA.yph -> A.yA.xph)

Theorem

ax467 1688

Proof of a single axiom that can replace ax-4 1637, ax-6o 1642, and ax-7 1621 in a subsystem that includes these axioms plus ax-5o 1639 and ax-gen 1622 (and propositional calculus). See ax467to4 1689, ax467to6 1690, and ax467to7 1691 for the re-derivation of those axioms. This theorem extends the idea in Scott Fenton's ax46 1682.

|- ((A.xA.y -. A.xA.yph -> A.xph) -> ph)

Theorem

ax467to4 1689

Re-derivation of ax-4 1637 from ax467 1688. Only propositional calculus is used by the re-derivation.

|- (A.xph -> ph)

Theorem

ax467to6 1690

Re-derivation of ax-6o 1642 from ax467 1688. Note that ax-6o 1642 and ax-7 1621 are not used by the re-derivation. The use of alimi 1656 (which uses ax-4 1637) is allowed since we have already proved ax467to4 1689.

|- (-. A.x -. A.xph -> ph)

Theorem

ax467to7 1691

Re-derivation of ax-7 1621 from ax467 1688. Note that ax-6o 1642 and ax-7 1621 are not used by the re-derivation. The use of alimi 1656 (which uses ax-4 1637) is allowed since we have already proved ax467to4 1689.

|- (A.xA.yph -> A.yA.xph)

Theorem

modal-5 1692

The analog in our "pure" predicate calculus of axiom 5 of modal logic S5.

|- (-. A.x -. ph -> A.x -. A.x -. ph)

Theorem

modal-b 1693

The analog in our "pure" predicate calculus of the Brouwer axiom (B) of modal logic S5.

|- (ph -> A.x -. A.x -. ph)

Theorem

19.8a 1694

If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89.

|- (ph -> E.xph)

Theorem

19.2 1695

Theorem 19.2 of [Margaris] p. 89, generalized to use two set variables. (Contributed by O'Cat, 31-Mar-2008.)

|- (A.xph -> E.yph)

Theorem

19.3 1696

A wff may be quantified with a variable not free in it. Theorem 19.3 of [Margaris] p. 89.

|- (ph -> A.xph)   =>   |- (A.xph <-> ph)

Theorem

alcom 1697

Theorem 19.5 of [Margaris] p. 89.

|- (A.xA.yph <-> A.yA.xph)

Theorem

alnex 1698

Theorem 19.7 of [Margaris] p. 89.

|- (A.x -. ph <-> -. E.xph)

Theorem

alex 1699

Theorem 19.6 of [Margaris] p. 89.

|- (A.xph <-> -. E.x -. ph)

Theorem

19.9t 1700

A closed version of one direction of 19.9 1701.

|- (A.x(ph -> A.xph) -> (E.xph -> ph))