HomeHome Metamath Proof Explorer < Previous   Next >
Browser slow? Try the
Unicode version.

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

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-11415)
  Hilbert Space Explorer  Hilbert Space Explorer
(11416-13002)
  Users' Mathboxes  Users' Mathboxes
(13003-19465)
 

Statement List for Metamath Proof Explorer - 1601-1700 - Page 17 of 195
TypeLabelDescription
Statement
 
Theoremsimplbi2comOLD 1601 Obsolete version of simplbi2com 1600.
|- (ph <-> (ps /\ ch))   =>   |- (ch -> (ps -> ph))
 
Theoremee1111 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)
 
Theorempm2.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)))
 
Theorempm2.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))))
 
Theoremee233 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)))
 
Theoremimbi12 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))))
 
Theoremimbi13 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))))))
 
Theoremee21 1608 e21 17693 without virtual deductions.
|- (ph -> (ps -> ch))   &   |- (ph -> th)   &   |- (ch -> (th -> ta))   =>   |- (ph -> (ps -> ta))
 
Theoremee33 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)))
 
Theoremee10 1610 e10 17682 without virtual deductions.
|- (ph -> ps)   &   |- ch   &   |- (ps -> (ch -> th))   =>   |- (ph -> th)
 
Theoremiin1 1611 in1 17573 without virtual deductions.
|- (ph -> ps)   =>   |- (ph -> ps)
 
Theoremee02 1612 e02 17685 without virtual deductions.
|- ph   &   |- (ps -> (ch -> th))   &   |- (ph -> (th -> ta))   =>   |- (ps -> (ch -> ta))
 
Predicate calculus axiomatization
 
The axioms of predicate calculus
 
Syntaxwal 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
 
Syntaxcv 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
 
Syntaxwceq 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
 
Theoremweq 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
 
Syntaxwcel 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
 
Theoremwel 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
 
Axiomax-5 1619 Axiom of Quantified Implication. Axiom C4 of [Monk2] p. 105.
|- (A.x(ph -> ps) -> (A.xph -> A.xps))
 
Axiomax-6 1620 Axiom of Quantified Negation. Axiom C5-2 of [Monk2] p. 113.
|- (-. A.xph -> A.x -. A.xph)
 
Axiomax-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)
 
Axiomax-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
 
Axiomax-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))
 
Axiomax-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
 
Axiomax-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)
 
Axiomax-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)))
 
Axiomax-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)))
 
Axiomax-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))
 
Axiomax-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
 
Theoremhbequid 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)
 
Theoremequidqe 1631 equid 1795 with existential quantifier without using ax-4 1637 or ax-17 1634.
|- -. A.y -. x = x
 
Theoremequidq 1632 equid 1795 with universal quantifier without using ax-4 1637 or ax-17 1634.
|- A.y x = x
 
Theoremax4sp1 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
 
Axiomax-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)
 
Theorema17d 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
 
Theoremax4 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)
 
Axiomax-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)
 
Theoremax5o 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))
 
Axiomax-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))
 
Theoremax5 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))
 
Theoremax6o 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)
 
Axiomax-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)
 
Theoremax6 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
 
Syntaxwex 1644 Extend wff definition to include the existential quantifier ("there exists").
wff E.xph
 
Definitiondf-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)
 
Theorema4i 1646 Inference rule reversing generalization.
|- A.xph   =>   |- ph
 
Theoremgen2 1647 Generalization applied twice.
|- ph   =>   |- A.xA.yph
 
Theorema4s 1648 Generalization of antecedent.
|- (ph -> ps)   =>   |- (A.xph -> ps)
 
Theorema4sd 1649 Deduction generalizing antecedent.
|- (ph -> (ps -> ch))   =>   |- (ph -> (A.xps -> ch))
 
Theoremmpg 1650 Modus ponens combined with generalization.
|- (A.xph -> ps)   &   |- ph   =>   |- ps
 
Theoremmpgbi 1651 Modus ponens on biconditional combined with generalization. (The proof was shortened by Stefan Allan, 28-Oct-2008.)
|- (A.xph <-> ps)   &   |- ph   =>   |- ps
 
Theoremmpgbir 1652 Modus ponens on biconditional combined with generalization. (The proof was shortened by Stefan Allan, 28-Oct-2008.)
|- (ph <-> A.xps)   &   |- ps   =>   |- ph
 
Theorema5i 1653 Inference from ax-5o 1639.
|- (A.xph -> ps)   =>   |- (A.xph -> A.xps)
 
Theorema6e 1654 Abbreviated version of ax-6o 1642.
|- (E.xA.xph -> ph)
 
Theorema7s 1655 Swap quantifiers in an antecedent.
|- (A.xA.yph -> ps)   =>   |- (A.yA.xph -> ps)
 
Theoremalimi 1656 Inference quantifying both antecedent and consequent.
|- (ph -> ps)   =>   |- (A.xph -> A.xps)
 
Theorem2alimi 1657 Inference doubly quantifying both antecedent and consequent.
|- (ph -> ps)   =>   |- (A.xA.yph -> A.xA.yps)
 
Theoremalim 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))
 
Theoremal2imi 1659 Inference quantifying antecedent, nested antecedent, and consequent.
|- (ph -> (ps -> ch))   =>   |- (A.xph -> (A.xps -> A.xch))
 
Theoremalanimi 1660 Variant of al2imi 1659 with conjunctive antecedent. (Contributed by Andrew Salmon, 8-Jun-2011.)
|- ((ph /\ ps) -> ch)   =>   |- ((A.xph /\ A.xps) -> A.xch)
 
Theoremalimd 1661 Deduction from Theorem 19.20 of [Margaris] p. 90.
|- (ph -> A.xph)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (A.xps -> A.xch))
 
Theoremalbi 1662 Theorem 19.15 of [Margaris] p. 90.
|- (A.x(ph <-> ps) -> (A.xph <-> A.xps))
 
Theorem19.21ai 1663 Inference from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> A.xph)   &   |- (ph -> ps)   =>   |- (ph -> A.xps)
 
Theoremalbii 1664 Inference adding universal quantifier to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (A.xph <-> A.xps)
 
Theorem2albii 1665 Inference adding 2 universal quantifiers to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (A.xA.yph <-> A.xA.yps)
 
Theoremhbth 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)
 
Theoremhbnt 1667 Closed theorem version of bound-variable hypothesis builder hbn 1669.
|- (A.x(ph -> A.xph) -> (-. ph -> A.x -. ph))
 
Theoremhba1 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)
 
Theoremhbn 1669 If x is not free in ph, it is not free in -. ph.
|- (ph -> A.xph)   =>   |- (-. ph -> A.x -. ph)
 
Theoremhbal 1670 If x is not free in ph, it is not free in A.yph.
|- (ph -> A.xph)   =>   |- (A.yph -> A.xA.yph)
 
Theoremhbex 1671 If x is not free in ph, it is not free in E.yph.
|- (ph -> A.xph)   =>   |- (E.yph -> A.xE.yph)
 
Theoremhbim 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))
 
Theoremhbor 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))
 
Theoremhban 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))
 
Theoremhbbi 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))
 
Theoremhb3or 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))
 
Theoremhb3an 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))
 
Theoremhba2 1678 Lemma 24 of [Monk2] p. 114.
|- (A.yA.xph -> A.xA.yA.xph)
 
Theoremhbia1 1679 Lemma 23 of [Monk2] p. 114.
|- ((A.xph -> A.xps) -> A.x(A.xph -> A.xps))
 
Theoremhbn1 1680 x is not free in -. A.xph.
|- (-. A.xph -> A.x -. A.xph)
 
Theoremhbe1 1681 x is not free in E.xph.
|- (E.xph -> A.xE.xph)
 
Theoremax46 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)
 
Theoremax46to4 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)
 
Theoremax46to6 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)
 
Theoremax67 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)
 
Theoremax67to6 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)
 
Theoremax67to7 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)
 
Theoremax467 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)
 
Theoremax467to4 1689 Re-derivation of ax-4 1637 from ax467 1688. Only propositional calculus is used by the re-derivation.
|- (A.xph -> ph)
 
Theoremax467to6 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)
 
Theoremax467to7 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)
 
Theoremmodal-5 1692 The analog in our "pure" predicate calculus of axiom 5 of modal logic S5.
|- (-. A.x -. ph -> A.x -. A.x -. ph)
 
Theoremmodal-b 1693 The analog in our "pure" predicate calculus of the Brouwer axiom (B) of modal logic S5.
|- (ph -> A.x -. A.x -. ph)
 
Theorem19.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)
 
Theorem19.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)
 
Theorem19.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)
 
Theoremalcom 1697 Theorem 19.5 of [Margaris] p. 89.
|- (A.xA.yph <-> A.yA.xph)
 
Theoremalnex 1698 Theorem 19.7 of [Margaris] p. 89.
|- (A.x -. ph <-> -. E.xph)
 
Theoremalex 1699 Theorem 19.6 of [Margaris] p. 89.
|- (A.xph <-> -. E.x -. ph)
 
Theorem19.9t 1700 A closed version of one direction of 19.9 1701.
|- (A.x(ph -> A.xph) -> (E.xph -> ph))

MPE Home   Contents Copyright terms: Public domain < Previous  Next >