Mathbox for Norm Megill 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > equidK  Unicode version 
Description: (Theorems equidK 27889 through ax12dgen4K 27934 are part of a study of our
nonTarski 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 ax5 1533, ax8 1623, ax9v 1632, ax13 1625, ax14 1626, and ax17 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 ax6 1534, ax7 1535, ax11 1624, and ax12 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 objectlanguage instances are valid. (ax11 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 ax4 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 and in ax9 1684 are bundled, but they are not in ax9v 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, ax9v 1632 is the principal instance of ax9 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 of ax9 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 objectlanguage instance of ax6 1534, ax7 1535, ax11 1624, and ax12 1633. "Translating" this to Metamath, it means that Tarksi's axioms can prove any substitution instance of ax6 1534, ax7 1535, ax11 1624, or ax12 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 objectlanguage 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 ax11o 1940 meeting condition (1) can be proved without invoking that axiom scheme (see comments in ax11 1624). However, it was somewhat awkward to use, involving an inductive argument with auxiliary theorems ax11eq 2105, ax11el 2106, ax11indn 2108, ax11indi 2109, and ax11inda 2113. It also used axiom schemes other than Tarski's. The new theorem schemes ax6wK 27919, ax7wK 27922, ax11wK 27927, and ax12wK 27930 are derived using only Tarski's axiom schemes, showing that Tarski's schemes can be used to derive all substitution instances of ax6 1534, ax7 1535, ax11 1624, and ax12 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 27919, ax7wK 27922, and ax11wK 27927 is of the form where is an auxiliary or "dummy" wff metavariable in which 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 27929 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 27924, ax11dgenK 27928, ax12dgen1K 27931, ax12dgen2K 27932, ax12dgen3K 27933, and ax12dgen4K 27934. (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 ax6 1534, ax7 1535, ax11 1624, and ax12 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 ax8 1623, ax13 1625, and ax14 1626; indeed, a degenerate instance of ax8 1623 appears to be indispensable for the proof of equidK 27889. Perhaps his general philosophy was that bundling is acceptable for free variables. But he also used the bundled scheme ax9 1684 in an older system, so it seems the main purpose of his later ax9v 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 ax4 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 apparently cannot be proved directly from Tarski's other axioms. The best we can do seems to be ax4wK 27906, again requiring substitution instances of that meet conditions (1) and (2) above. Note that our direct proof ax4 1691 requires ax11 1624, which is not part of Tarski's system. (End of study description.) Identity law for equality. Does not use ax6 1534, ax7 1535, ax11 1624, or ax12 1633. Lemma 2 of [KalishMontague] p. 85. (Contributed by NM, 9Apr2017.) 
Ref  Expression 

equidK 
Step  Hyp  Ref  Expression 

1  ax9v 1632  . . 3  
2  ax8 1623  . . . . . 6  
3  2  pm2.43i 45  . . . . 5 
4  3  con3i 129  . . . 4 
5  4  alimi 1546  . . 3 
6  1, 5  mto 169  . 2 
7  ax17 1628  . 2  
8  6, 7  mt3 173  1 
Colors of variables: wff set class 
Syntax hints: wn 5 wal 1532 
This theorem is referenced by: equcomiK 27890 ax9dgenK 27911 ax12dgen1K 27931 ax12dgen3K 27933 ax12dgen4K 27934 
This theorem was proved from axioms: ax1 7 ax2 8 ax3 9 axmp 10 ax5 1533 axgen 1536 ax8 1623 ax17 1628 ax9v 1632 
Copyright terms: Public domain  W3C validator 