Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  equidK Unicode version

Theorem equidK 28235
Description: (Theorems equidK 28235 through ax12dgen4K 28280 are part of a study of our non-Tarski predicate calculus axiom schemes. We are using this theorem as a placeholder to describe this study.)

The orginal axiom schemes of Tarski's predicate calculus are ax-5 1533, ax-8 1623, ax-9v 1632, ax-13 1625, ax-14 1626, and ax-17 1628 (see http://us.metamath.org/mpegif/mmset.html#compare) and are shown as axiom schemes B4 through B8 in [KalishMontague] p. 81. These are shown to be logically complete by Theorem 1 of [KalishMontague] p. 85.

The axiom system of set.mm includes the additional axiom schemes ax-6 1534, ax-7 1535, ax-11 1624, and ax-12 1633, which are not part of Tarski's axiom schemes. They are used (and we conjecture are required) to make our system "metalogically complete" i.e. able to prove directly all possible schemes with wff and set metavariables, bundled or not, whose object-language instances are valid. (ax-11 1624 has been proved to be required; see http://us.metamath.org/award2003.html#9a. Metalogical independence of the other three are open problems.)

(There are additional predicate calculus axiom schemes included in set.mm such as ax-4 1692, but they can all be proved as theorems from the above.)

Terminology: Two set (individual) metavariables are "bundled" in an axiom or theorem scheme when there is no distinct variable constraint ($d) imposed on them. (The term "bundled" is due to Raph Levien.) For example, the  x and  y in ax-9 1684 are bundled, but they are not in ax-9v 1632. We also say that a scheme is bundled when it has at least one pair of bundled set metavariables. If distinct variable conditions are added to all set metavariable pairs in a bundled scheme, we call that the "principal" instance of the bundled scheme. For example, ax-9v 1632 is the principal instance of ax-9 1684. Whenever a common variable is substituted for two or more bundled variables in an axiom or theorem scheme, we call the substitution instance "degenerate". For example, the instance  -.  A. x -.  x  =  x of ax-9 1684 is degenerate. An advantage of bundling is ease of use since there are fewer distinct variable restrictions ($d) to be concerned with. There is also a small economy in being able to state principal and degenerate instances simultaneously. A disadvantage is that bundling may present difficulties in translations to other proof languages, which typically lack the concept (in part because their variables often represent the variables of the object language rather than metavariables ranging over them).

Because Tarski's axiom schemes are logically complete, they can be used to prove any object-language instance of ax-6 1534, ax-7 1535, ax-11 1624, and ax-12 1633. "Translating" this to Metamath, it means that Tarksi's axioms can prove any substitution instance of ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633 in which (1) there are no wff metavariables and (2) all set metavariables are mutually distinct i.e. are not bundled. In effect this is mimicking the object language by pretending that each set metavariable is an object-language variable. (There may also be specific instances with wff metavariables and/or bundling that are directly provable from Tarski's axiom schemes, but it isn't guaranteed. Whether all of them are possible is part of the still open metalogical independence problem for our additional axiom schemes.)

It can be useful to see how this can be done, both to show that our additional schemes are valid metatheorems of Tarski's system and to be able to translate object language instances of our proofs into proofs that would work with a system using only Tarski's original schemes. In addition, it may (or may not) provide insight into the conjectured metalogical independence of our additional schemes.

Past work showed that instances of ax-11o 1941 meeting condition (1) can be proved without invoking that axiom scheme (see comments in ax-11 1624). However, it was somewhat awkward to use, involving an inductive argument with auxiliary theorems ax11eq 2109, ax11el 2110, ax11indn 2112, ax11indi 2113, and ax11inda 2117. It also used axiom schemes other than Tarski's.

The new theorem schemes ax6wK 28265, ax7wK 28268, ax11wK 28273, and ax12wK 28276 are derived using only Tarski's axiom schemes, showing that Tarski's schemes can be used to derive all substitution instances of ax-6 1534, ax-7 1535, ax-11 1624, and ax-12 1633 meeting conditions (1) and (2). (The "K" suffix stands for Kalish/Montague, whose paper was a source for some of the proofs. I may change these names in the future since our practice has been to reserve upper case for special cases such as the ALT or OLD suffixes.) Each hypothesis of ax6wK 28265, ax7wK 28268, and ax11wK 28273 is of the form  ( x  =  y  ->  ( ph  <->  ps ) ) where  ps is an auxiliary or "dummy" wff metavariable in which  x doesn't occur. We can show by induction on formula length that the hypotheses can be eliminated in all cases meeting conditions (1) and (2). The example ax11wdemoK 28275 illustrates the techniques (equality theorems and bound variable renaming) used to achieve this.

We also show the degenerate instances for axioms with bundled variables in ax7dgenK 28270, ax11dgenK 28274, ax12dgen1K 28277, ax12dgen2K 28278, ax12dgen3K 28279, and ax12dgen4K 28280. (Their proofs are trivial but we include them to be thorough.) Combining the principal and degenerate cases outside of Metamath, we show that the bundled schemes ax-6 1534, ax-7 1535, ax-11 1624, and ax-12 1633 are schemes of Tarski's system, meaning that all object language instances they generate are theorems of Tarski's system.

It is interesting that Tarski's system bundles set metavariables in ax-8 1623, ax-13 1625, and ax-14 1626; indeed, a degenerate instance of ax-8 1623 appears to be indispensable for the proof of equidK 28235. Perhaps his general philosophy was that bundling is acceptable for free variables. But he also used the bundled scheme ax-9 1684 in an older system, so it seems the main purpose of his later ax-9v 1632 was just to show that the weaker unbundled form is sufficient rather than an aesthetic objection to bundled free and bound variables.

The case of ax-4 1692 is curious: originally an axiom of Tarski's system, it was proved redundant by Lemma 9 of [KalishMontague] p. 86. However, the proof is by induction on formula length, and the compact scheme form  A. x ph  ->  ph apparently cannot be proved directly from Tarski's other axioms. The best we can do seems to be ax4wK 28252, again requiring substitution instances of  ph that meet conditions (1) and (2) above. Note that our direct proof ax4 1691 requires ax-11 1624, which is not part of Tarski's system.

(End of study description.)

Identity law for equality. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Lemma 2 of [KalishMontague] p. 85. (Contributed by NM, 9-Apr-2017.)

Assertion
Ref Expression
equidK  |-  x  =  x

Proof of Theorem equidK
StepHypRef Expression
1 ax-9v 1632 . . 3  |-  -.  A. y  -.  y  =  x
2 ax-8 1623 . . . . . 6  |-  ( y  =  x  ->  (
y  =  x  ->  x  =  x )
)
32pm2.43i 45 . . . . 5  |-  ( y  =  x  ->  x  =  x )
43con3i 129 . . . 4  |-  ( -.  x  =  x  ->  -.  y  =  x
)
54alimi 1546 . . 3  |-  ( A. y  -.  x  =  x  ->  A. y  -.  y  =  x )
61, 5mto 169 . 2  |-  -.  A. y  -.  x  =  x
7 ax-17 1628 . 2  |-  ( -.  x  =  x  ->  A. y  -.  x  =  x )
86, 7mt3 173 1  |-  x  =  x
Colors of variables: wff set class
Syntax hints:   -. wn 5   A.wal 1532
This theorem is referenced by:  equcomiK  28236  ax9dgenK  28257  ax12dgen1K  28277  ax12dgen3K  28279  ax12dgen4K  28280
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-8 1623  ax-17 1628  ax-9v 1632
  Copyright terms: Public domain W3C validator