$( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#* Introduction Metamath source file for a natural deduction based logic #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#* nat.mm - $Revision: 1.12.2.4 $ - $Date: 2006/07/05 10:21:26 $ This file (specifically, the version of this file with the above date) is placed in the public domain per the Creative Commons Public Domain Dedication. http://creativecommons.org/licenses/publicdomain/ Many theorems are borrowed from Megill's set.mm. When a theorem is in this case, it is marked by a '(#05)' or by '(#06)' which means that the theorem has been borrowed from set.mm v. 6-Jun-2005 or v. 22-Jan-2006. When the name of the theorem is different it is indicated. When a theorem has not been borrowed from set.mm an underscore is appended to its front. In the rest of this file a ??? means I have a doubt, whatever the doubt can be: a doubt about a logic concept, the english language, a fact... Anybody giving me some relief about any of these doubts will be welcome. This file is a work in progress. I prefer to give it now in case it can be useful. But it can be widely improved. This file is the work of an amateur. It can be not completely sound (I know... the wording seems strange but it means exactly what I mean). For a completely sound piece of work see set.mm Natural deduction was invented by Gentzen in the 30's (cf. Gentzen, Untersuchungen uber das logische Schliessen (Mathematische Zeitschrift 39, pp. 176-210, 405-431 1934-5)). His aim was to give a logic system where propositional and predicate calculus proofs would be easier to make than in previously designed systems (cf. for example D.Hilbert, W.Ackermann. Grundzuge der theoretischen Logik. Berlin (Springer), 1928). To achieve this goal Gentzen uses a list of hypotheses (called context in this file). Our system is not exactly the system designed by Gentzen but it can be considered as a descendant of it. A descendant of the Hilbert system is obviously the system described by Norman Megill in set.mm To understand exactly how Gentzen derived his own system from the Hilbert's system I recommend the reading of ` Introduction to metamathematics ` by Kleene chapter V (In fact I'm not sure in this chapter Kleene tries to derive Gentzen's system from Hilbert's one but it can really be read that way. In ` nat.mm ` every formula has the following form : ` # G |- ph `. ` # ` has no particular meaning. It is mandatory in metamath to begin formula with a constant and it is the only purpose of this symbol. ` G ` is the context. ` ph ` is the formula we want to prove and '|-' signals a derivation. Then ` # G |- ph ` should be read: from the hypotheses in G we can derive ph. In a certain way in Hilbert's system we make proof about propositions and in Gentzen's we make proof about derivations. The system described below has been inspired by slides by Christoph Benzmuller called from 'Natural Deduction to Sequent Calculus and back'. It can be found there: http://www.ags.uni-sb.de/~chris/papers/2002-pisa.pdf In this set of slides, the relationship between various forms of natural deduction, and between natural deduction and sequent calculus (another logic system designed by Gentzen) is exposed. Some reasons explaining why Gentzen's systems are theoritically important are also described. In particular I borrow to Benzmuller's slides the way to represent the list of hypotheses by a context appended to the left of a formula. Benzmuller himself had used, among other sources, a paper by Franck Pfenning called ` Automated theorem proving `. http://www.cs.cmu.edu/~fp/courses/atp/handouts.html All the axioms concerning propositional calculus, predicate calculus, equality come from this paper. However the system described by Pfenning is not rich enough to work with in metamath. En effet ??? it presupposes substitutions are realized at a metalogical level (i. e. by an independant device). In metamath such a device doesn't exist. Thus we must add axioms to make our system able to deal with substitution simply by handling axioms and inferences belonging to the system ). To achieve metalogical completeness I simply added 'set.mm' axioms (thanks to a suggestion by Norman Megill). O'cat suggests me to add an empty context. This is a great idea: see ax-con for more explanation. In his paper Pfenning asks some variables are new. However he doesn't describe what he means by 'new'. This proviso ( this is the technical name of that sort of requirement ) can be a $d statement. Or it can simply mean there is no free occurence of the variable. Norman Megill urged me to interpret 'new' as meaning distinct (i.e. using a $d statement), because it is easier to make a parallel between proofs in nat.mm and in set.mm this way. I have tried to realize a natural deduction system with a $d x G $. statement as its proviso. And I found it very difficult to be used. If anybody wants to know what pain and sorrow mean in logic I agree to send him/her this attempt. Realizing this sort of proviso is too much for my humble strenght, I replaced them with a 'bound x G' proviso. This is much more comfortable. Note: [ terminology ] In this file we call axiom a rule which has no proof. We call theorem a rule which has a proof. When a rule has one hypothesis or more we call it a rule of inference. When it has no hypothesis we simply call it an axiom or a theorem. A synonym for hypothesis is premisse. A formula or a statement is any group of symbols that respect the rules of syntax. The last statement of a rule of inference is its conclusion. In a ` # G |- ph ` statement any formula in G is called an hypothesis, ph is called a conclusion. We are aware that our terms are higly overloaded and correspond to various reality. In ` Introduction to metamathematics ` Kleene uses a more precise dictionary. However we think these overloadings can be used quite naturally and correspond to the structure of ` metamath ` itself and to the the usual use of these terms. Note: [ Scheme ] We use the term axiom for brievity sake but we should say 'scheme of axiom' to speak correctly. Note: [ Importation ] When we import a theorem from set.mm we can use several strategy. The simplest one consists in adding a '# bound x G' hypothesis (it is useless in propositional calculus but it may be mandatory in predicate calculus). As an alternative we can prefer binding the hypotheses. In that case we can remove the '# bound x G' hypothesis. The third way for importing theorems is to transform a set.mm theorem into a closed form. To do that simply turn the hypotheses into antecedents. ph & ps => ch is changed into ( ph -> ( ps -> ch ) ). You can have to quantify the hypothesis if you have a predicate calculus theorem. In that case the closed form will be ( A. x ph -> ( A. x ps -> ch ) ) . Note: [ Syntax of this file ] In the first column there must always be a space in order that nat.mm looks nice on the wiki. Note: Here is a plan of the system. 1 -- Natural deduction propositional calculus axioms are introduced. 1.1 -- I proved back set.mm propositional calculus axioms 'set.mm' propositional calculus axioms have been slightly transformed. I appended G in front of them. According to ax-con I can do this. This shows my own system is complete regarding propositional calculus. 2 -- Natural deduction predicate calculus axioms are introduced. 2.1 -- These are ax-ui, ax-ue, ax-ee, ax-ei, ax-eq. 2.2 -- When Pfenning asked that a variable should be 'new' I've translated it by 'bound'. 3.2.1 According to me, 'new' in ax-ui means the variable must be bound in all the statements in G. 3.2.2 According to me 'new' in ax-ee means the variable must be bound in all the staments in G and in ps (but not in ps since in this case the inference would be meaningless). 2.3 -- Pfenning's system supposes variable substitution is managed at a metalogical level. Since in metamath we can't do that I added axioms. 3 -- I added axioms to decide if a variable is bound in a formula. 4.1 These axioms are in some way independant from the rest of the system. On the contrary theorems about bound variables in set.mm are completely integre to the system. 4.1.1 The reason why I add axioms about bound variables is that I don't want to use the $d statement and therefore I need a device to emulate the 'new' proviso used by Pfenning. This device is the set of axioms about binding. 4 -- I added an axiom to manage substitution. 4.1 This is fs. 5 -- I added an axiom to manage equality. 5.1 This axiom is equsb1 5.1.1 I don't know if we must add to axiom. I have added it because it was difficult for me to prove it. But perhaps it will reveal itself to be redundant. 6 -- There remains some axioms that can't be proved. 6.1 These axioms are setax-10, setax-11, setax-12 and setax-16. 7 -- I added a meta property about context. 7.1 This is called ax-con. 7.2 This inference rule allows me to remove unnecessary provisos. 7.3 It is a justification of the reason why I can import closed form theorems from set.mm. Bibliography ------------ Bibliographical references are made by bracketing an identifer in a theorem's comment, such as [RussellWhitehead]. BourbakiTe : N. Bourbaki. Elements de mathematique. Theorie des ensembles. Chapitre 1 a 4. Nouveau tirage. Masson. Paris Milan Barcelone Mexico. 1990. $) $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#* Propositional calculus #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#* $) $( In metamath the first character of a statement must be a constant. Megill uses '|-' for this purpose. However in a natural deduction system the turnstile is normally used to separate the context from the statement. I will use then # instead of '|-' as the first character of a statement $) $c # $. $( beginning of a statement $) $c , $. $( coma (used to separate hypothesis in a context) $) $c [] $. $( empty context $) $c |- $. $( read 'the following sequence is provable from the previous list of hypotheses (called a context)' $) $c [ $. $( beginning of the context $) $c ] $. $( end of the context $) $c ( $. $( opening parenthesis (used by infix operator) $) $c ) $. $( closing parenthesis (used by infix operator) $) $c -> $. $( read 'implies' $) $c <-> $. $( read 'if and only if' $) $c -. $. $( read 'not' $) $c /\ $. $( read 'and' $) $c \/ $. $( read 'or' $) $c Abs $. $( read 'absurd' $) $c con $. $( read 'the following sequence is a context' $) $c wff $. $( read 'the following sequence is a well-formed formula' $) $( context variable $) $v G $. cong $f con G $. $( propositional variables $) $v ph $. $( Greek phi $) $v ps $. $( Greek psi $) $v ch $. $( Greek chi $) $v th $. $( Greek theta $) $v ta $. $( Greek tau $) $( The propositional variable 'phi' is a well-formed formula $) wph $f wff ph $. $( The propositional variable 'psi' is a well-formed formula $) wps $f wff ps $. $( The propositional variable 'chi' is a well-formed formula $) wch $f wff ch $. $( The propositional variable 'theta' is a well-formed formula $) wth $f wff th $. $( The propositional variable 'tau' is a well-formed formula $) wta $f wff ta $. $( Recursively defines context. If G is a context and ph is a wff then [ G , ph ] is a context. $) conr $a con [ G , ph ] $. $( The empty context is a context. $) cone $a con [] $. $( Recursively defines well formed formula $) $( if ph is a wff, -. ph is a wff. $) wn $a wff -. ph $. $( If ph and ps are wffs, ( ph -> ps ) is a wff. $) wi $a wff ( ph -> ps ) $. $( If ph and ps are wffs, ( ph <-> ps ) is a wff. $) wb $a wff ( ph <-> ps ) $. $( If ph and ps are wffs, ( ph /\ ps ) is a wff. $) wa $a wff ( ph /\ ps ) $. $( If ph and ps are wffs, ( ph \/ ps ) is a wff. $) wo $a wff ( ph \/ ps ) $. $( 'Abs' (absurdity) is a wff. $) wabs $a wff Abs $. $( Mmj2 type. These 4 statements are only used by mmj2. They have no logical meaning. mmj2 uses a strict grammatical parser. To use such a parser one needs to know which rule is the first one. This is the aim of these four rules. If one wants to work with metamath only one can remove them without danger. $) $c LSTYP $. $v lstyp $. wlstyp $f LSTYP lstyp $. $( G |- ph is the top rule used by Mmj2 $) lstyp1 $a LSTYP G |- ph $. $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Axioms =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) ${ ax-con.1 $e # [] |- ph $. $( This axiom means that if a statement can be derived from an empty context, it can be derived from any context. It's a sort of ax-we axiom but with an undefined number of hypotheses. ( Since this axiom is a sort of extension of ax-we I think we could prove it as a meta theorem. That's the reason why I called it a meta axiom. ) This meta axioms explains why we can import closed form theorem from set.mm into nat.mm. By closed form I mean $p statement without $e hypotheses. But we can't import inferences as easily. (??? example) This meta axiom has another function: it is used to prevent a 'bound x G' proviso in theorems without hypotheses ($e statement): see for instance eqcom. $) ax-con $a # G |- ph $. $} $( [ big bang ] Contrary to the system describes in 'set.mm' in a natural deduction system all the operators are introduced in one step. It is a bit confusing and it prevents from achieving the beautiful architecture of 'set.mm' where the axioms only deal with '-.' and '->', the other operators being defined with these two operators only. However we will hold out for the traditional way of defining natural deduction axioms. $) $( The only axiom of the natural deduction. $) ax-hyp $a # [ G , ph ] |- ph $. ${ ax-we.1 $e # G |- ph $. $( Hypothesis weakening. $) ax-we $a # [ G , ps ] |- ph $. $} ${ ax-ii.1 $e # [ G , ph ] |- ps $. $( Implication introduction. It is the deduction theorem that is embedded here. In the context of a Hilbert system this theorem is a meta theorem. In the context of natural deduction it is an axiom. $) ax-ii $a # G |- ( ph -> ps ) $. $} ${ ax-ie.1 $e # G |- ph $. ax-ie.2 $e # G |- ( ph -> ps ) $. $( Implication elimination. $) ax-ie $a # G |- ps $. $} ${ ax-ai.1 $e # G |- ph $. ax-ai.2 $e # G |- ps $. $( And introduction. $) ax-ai $a # G |- ( ph /\ ps ) $. $} ${ ax-are.1 $e # G |- ( ph /\ ps ) $. $( And elimination ( right argument remains ). $) ax-are $a # G |- ps $. $} ${ ax-ale.1 $e # G |- ( ph /\ ps ) $. $( And elimination ( left argument remains ). $) ax-ale $a # G |- ph $. $} ${ ax-oli.1 $e # G |- ph $. $( Or introduction ( ph is the left argument ). $) ax-oli $a # G |- ( ph \/ ps ) $. $} ${ ax-ori.1 $e # G |- ps $. $( Or introduction ( ps is the right argument ). $) ax-ori $a # G |- ( ph \/ ps ) $. $} ${ ax-oe.1 $e # G |- ( ph \/ ps ) $. ax-oe.2 $e # [ G , ph ] |- ch $. ax-oe.3 $e # [ G , ps ] |- ch $. $( Or elimination. $) ax-oe $a # G |- ch $. $} ${ ax-ni.1 $e # [ G , ph ] |- Abs $. $( Not introduction. $) ax-ni $a # G |- -. ph $. $} ${ ax-ne.1 $e # G |- ph $. ax-ne.2 $e # G |- -. ph $. $( Not elimination. $) ax-ne $a # G |- Abs $. $} ${ ax-cl.1 $e # [ G , -. ph ] |- Abs $. $( contra ( classical logic ). See axin for intuitionistic logic. $) ax-cl $a # G |- ph $. $} $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Structural properties =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( Structural properties ( = theorems to manage the context ). All the theorems about context can be proved with the axioms dealing with simple implications. The reason for that equivalence is that the usual interpretation of [ [ [] , ph ] , ps ] |- ch is ( ( ph /\ ps ) -> ch ) which is equivalent to ( ph -> ( ps -> ch ) ) ( see ~ impexp ) . $) ${ cut.1 $e # G |- ph $. cut.2 $e # [ G , ph ] |- ps $. $( A hypothesis can be removed if you prove it is a theorem. $) cut $p # G |- ps $= ( ax-ii ax-ie ) ABCDABCEFG $. $( [1-Oct-05] $) $} ${ int2.1 $e # [ [ G , ph ] , ps ] |- ch $. $( Introduction of two hypotheses. $) int2 $p # G |- ( ph -> ( ps -> ch ) ) $= ( wi conr ax-ii ) ABCDFABGCDEHH $. $( [?] $) $( [1-Oct-05] $) $} ${ elim2.1 $e # G |- ( ph -> ( ps -> ch ) ) $. $( Elimination of two antecedents. Adding a hypothesis to the context or an antecedent to a statement are equivalent in some way. $) elim2 $p # [ [ G , ph ] , ps ] |- ch $= ( conr ax-hyp wi ax-we ax-ie ) ABFZCFZCDKCGLBCDHZKBCABGIKBMHZCANBEIIJJ $. $( [?] $) $( [1-Oct-05] $) $} ${ exch.1 $e # [ [ G , ph ] , ps ] |- ch $. $( Exchange: any two hypotheses can be swapped. $) exch $p # [ [ G , ps ] , ph ] |- ch $= ( conr ax-hyp ax-we wi int2 ax-ie ) ACFZBFZCDLCBACGHMBCDIZLBGLBNIZBAOCABC DEJHHKK $. $( [?] $) $( [1-Oct-05] $) $} ${ cont.1 $e # [ [ G , ph ] , ph ] |- ps $. $( Contraction: we can remove a duplicated hypothesis. $) cont $p # [ G , ph ] |- ps $= ( conr ax-hyp ax-ii ax-ie ) ABEZBCABFIBCDGH $. $( [?] $) $( [1-Oct-05] $) $} ${ weak2.1 $e # G |- ph $. $( Two weakenings. $) weak2 $p # [ [ G , ps ] , ch ] |- ph $= ( conr ax-we ) ACFBDABCEGG $. $( [?] $) $( [15-May-06] $) $} $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Intuitionism =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) ${ axin.1 $e # G |- Abs $. $( To have an intuitionistic propositional + predicate calculus system ax-cl should be replaced by axin. The other axioms should remain untouched. However to work with an intuitionistic system you will have to be cautious. Not all the definitions traditional in a classic system are allowed. For instance we could not have defined ' E. x ph 'as ' -. A. x -. ph '. $) axin $p # G |- ph $= ( wabs wn ax-we ax-cl ) ABADBECFG $. $( [?] $) $( [15-Oct-05] $) $} $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- set.mm axioms for propositional calculus proved back =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( We can see that only ax-ii, ax-ie, ax-cl, ax-ne, ax-we and ax-hyp are needed to prove setax-1, setax-2, setax-3 and setax-mp. So the other axioms in our natural deduction system could be removed and the other connectors could be introduced by defining them. However in natural deduction it is traditional to use axioms and not definitions to introduce the propositional calculus connectors. $) $( If ph is true, we can append any wff on its left. $) setax-1 $p # G |- ( ph -> ( ps -> ph ) ) $= ( wi conr ax-hyp ax-we ax-ii ) ABCBDABEZCBIBCABFGHH $. $( [?] $) $( [29-Dec-05] $) $( A sort of distributivity of implication on itself. $) setax-2 $p # G |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) $= ( wi conr ax-hyp ax-we ax-ie ax-ii ) ABCDEZEZBCEZBDEZEALFZMNOMFZBDPBFZCDQBC PBGZPMBOMGHIQBKRPLBOLMALGHHIIJJJ $. $( [?] $) $( [29-Dec-05] $) $( Contraposition. $) setax-3 $p # G |- ( ( -. ph -> -. ps ) -> ( ps -> ph ) ) $= ( wn wi conr ax-hyp ax-we ax-ie ax-ne ax-cl ax-ii ) ABDZCDZEZCBEAOFZCBPCFZB QMFZCQCMPCGHRMNQMGQOMPOCAOGHHIJKLL $. $( [?] $) $( [29-Dec-05] $) ${ min $e # G |- ph $. maj $e # G |- ( ph -> ps ) $. $( Modus ponens is simply anoter name for ax-ie $) setax-mp $p # G |- ps $= ( ax-ie ) ABCDEF $. $( [?] $) $( [29-Dec-05] $) $} $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Implication =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) ${ a1i.1 $e # G |- ph $. $( We can always add an antecedent to a theorem. Analogue to ~ ax-we . Should be compared with ~ ax-ii as well since in a certain way it is the opposite. (#05). $) a1i $p # G |- ( ps -> ph ) $= ( ax-we ax-ii ) ACBABCDEF $. $( [?] $) $( [15-Nov-05] $) $} $( I normally don't add 'deductions' (cf. 'set.mm' a1d for an instance of what Megill calls a deduction) because the deduction theorem is one of the 'natural deduction' axioms and 'deductions' in set.mm are due to the absence of the deduction theorem. $) ${ $( Premise for ~ a2i . $) a2i.1 $e # G |- ( ph -> ( ps -> ch ) ) $. $( Inference derived from axiom ~ setax-2 . (#05) $) a2i $p # G |- ( ( ph -> ps ) -> ( ph -> ch ) ) $= ( wi conr ax-hyp ax-we ax-ie ax-ii ) ABCFZBDFALGZBDMBGZCDNBCMBHZMLBALHIJN BCDFZOMBPFZBAQLEIIJJKK $. $( [?] $) $( [1-Jul-05] $) $} ${ $( First of 2 premises for ~ syl . $) syl.1 $e # G |- ( ph -> ps ) $. $( Second of 2 premises for ~ syl . $) syl.2 $e # G |- ( ps -> ch ) $. $( Syllogisme. Megill uses this word to call this theorem. However a syllogism in the normal language is something else. (#05) $) syl $p # G |- ( ph -> ch ) $= ( conr ax-hyp wi ax-we ax-ie ax-ii ) ABDABGZCDMBCABHABCIBEJKACDIBFJKL $. $( [?] $) $( [14-Nov-05] $) $} ${ $( Premise for ~ com12 . $) com12.1 $e # G |- ( ph -> ( ps -> ch ) ) $. $( Inference that swaps (commutes) antecedents in an implication. $) com12 $p # G |- ( ps -> ( ph -> ch ) ) $= ( wi conr ax-hyp ax-we weak2 ax-ie ax-ii ) ACBDFACGZBDMBGZCDMCBACHINBCDFZ MBHABOFCBEJKKLL $. $( [?] $) $( [15-May-06] $) $} ${ imim2i.1 $e # G |- ( ph -> ps ) $. $( Inference adding common antecedents to an implication. $) imim2i $p # G |- ( ( ch -> ph ) -> ( ch -> ps ) ) $= ( wi conr ax-hyp ax-we ax-ie ax-ii ) ADBFZDCFALGZDCMDGZBCNDBMDHMLDALHIJMB CFZDAOLEIIJKK $. $( [?] $) $( [16-Nov-05] $) $} ${ imim1i.1 $e # G |- ( ph -> ps ) $. $( Inference adding common consequents to an implication, thereby interchanging the original antecedent and consequent. $) imim1i $p # G |- ( ( ps -> ch ) -> ( ph -> ch ) ) $= ( wi conr wn ax-hyp ax-we ax-ie ax-ne ax-cl ax-ii ) ACDFZBDFAOGZBDPBGZDQD HZGZDSCDSBCQBRPBIJQBCFZRPTBATOEJJJKQORPOBAOIJJKQRILMNN $. $( [?] $) $( [16-Nov-05] $) $} ${ imim12i.1 $e # G |- ( ph -> ps ) $. imim12i.2 $e # G |- ( ch -> th ) $. $( Inference joining two implications. $) imim12i $p # G |- ( ( ps -> ch ) -> ( ph -> th ) ) $= ( wi conr ax-hyp ax-we ax-ie ax-ii ) ACDHZBEHANIZBEOBIZDEPCDPBCOBJOBCHZBA QNFKKLONBANJKLODEHZBARNGKKLMM $. $( [?] $) $( [15-Nov-05] $) $} ${ 3syl.1 $e # G |- ( ph -> ps ) $. 3syl.2 $e # G |- ( ps -> ch ) $. 3syl.3 $e # G |- ( ch -> th ) $. $( Inference chaining two syllogisms. (#05) $) 3syl $p # G |- ( ph -> th ) $= ( conr ax-hyp wi ax-we ax-ie ax-ii ) ABEABIZDEOCDOBCABJABCKBFLMACDKBGLMAD EKBHLMN $. $( [?] $) $( [21-Nov-05] $) $} ${ syl5.1 $e # G |- ( ph -> ( ps -> ch ) ) $. syl5.2 $e # G |- ( th -> ps ) $. $( A syllogism rule of inference. The second premise is used to replace the second antecedent of the first premise. This sort of rule can be considered as a precursor of biimplication replacing rules like rembi4b. It can be used when only the implication holds but not the biimplication. (#05) $) syl5 $p # G |- ( ph -> ( th -> ch ) ) $= ( wi conr ax-we ax-hyp ax-ie syl ax-ii ) ABEDHABIZECDAECHBGJOBCDHZABKABPH BFJLMN $. $( [?] $) $( [21-Nov-05] $) $} ${ syl6.1 $e # G |- ( ph -> ( ps -> ch ) ) $. syl6.2 $e # G |- ( ch -> th ) $. $( A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (#05) $) syl6 $p # G |- ( ph -> ( ps -> th ) ) $= ( wi conr ax-hyp ax-we ax-ie syl ax-ii ) ABCEHABIZCDEOBCDHZABJABPHBFKLADE HBGKMN $. $( [?] $) $( [21-Nov-05] $) $} ${ syl7.1 $e # G |- ( ph -> ( ps -> ( ch -> th ) ) ) $. syl7.2 $e # G |- ( ta -> ch ) $. $( A syllogism rule of inference. The second premise is used to replace the third antecedent of the first premise. $) syl7 $p # G |- ( ph -> ( ps -> ( ta -> th ) ) ) $= ( wi conr ax-hyp ax-we ax-ie syl5 ax-ii ) ABCFEIIABJZCDEFPBCDEIIZABKABQIB GLMAFDIBHLNO $. $( [?] $) $( [21-Nov-05] $) $} ${ syl8.1 $e # G |- ( ph -> ( ps -> ( ch -> th ) ) ) $. syl8.2 $e # G |- ( th -> ta ) $. $( A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. $) syl8 $p # G |- ( ph -> ( ps -> ( ch -> ta ) ) ) $= ( wi conr ax-hyp ax-we ax-ie syl6 ax-ii ) ABCDFIIABJZCDEFPBCDEIIZABKABQIB GLMAEFIBHLNO $. $( [?] $) $( [21-Nov-05] $) $} $( imim1d not added. $) $( syld not added. $) $( imim2d not added. $) $( imim12d not added. $) $( Swap antecedents. Compare with ~ exch . (#06) $) pm2.04 $p # G |- ( ( ph -> ( ps -> ch ) ) -> ( ps -> ( ph -> ch ) ) ) $= ( wi conr ax-hyp com12 ax-ii ) ABCDEEZCBDEEAJFBCDAJGHI $. $( [?] $) $( [27-Jun-2006] $) $( com23 not added. $) ${ mpi.1 $e # G |- ps $. mpi.2 $e # G |- ( ph -> ( ps -> ch ) ) $. $( A nested modus ponens inference. Compare with ~ax-we . (#06) $) mpi $p # G |- ( ph -> ch ) $= ( conr ax-we wi ax-hyp ax-ie ax-ii ) ABDABGZCDACBEHMBCDIZABJABNIBFHKKL $. $( [?] $) $( [27-Jun-2006] $) $} ${ mpii.1 $e # G |- ch $. mpii.2 $e # G |- ( ph -> ( ps -> ( ch -> th ) ) ) $. $( A doubly nested modus ponens inference. (#06) $) mpii $p # G |- ( ph -> ( ps -> th ) ) $= ( wi conr ax-we ax-hyp ax-ie mpi ax-ii ) ABCEHABIZCDEADBFJOBCDEHHZABKABPH BGJLMN $. $( [?] $) $( [27-Jun-2006] $) $} $( mpd not added. $) $( syl5d not added. $) $( syl6d not added. $) ${ syl9.1 $e # G |- ( ph -> ( ps -> ch ) ) $. syl9.2 $e # G |- ( th -> ( ch -> ta ) ) $. $( A nested syllogism inference with different antecedents. (#06) $) syl9 $p # G |- ( ph -> ( th -> ( ps -> ta ) ) ) $= ( wi conr ax-hyp ax-we ax-ie ax-ii ) ABECFIZIABJZEOPEJZCFQCJZDFRCDQCKQCDI ZCPSEPBSABKABSIBGLMLLMQDFIZCQETPEKPETIZEAUABHLLMLMNNN $. $( [?] $) $( [27-Jun-2006] $) $} ${ syl9r.1 $e # G |- ( ph -> ( ps -> ch ) ) $. syl9r.2 $e # G |- ( th -> ( ch -> ta ) ) $. $( A nested syllogism inference with different antecedents. (#06) $) syl9r $p # G |- ( th -> ( ph -> ( ps -> ta ) ) ) $= ( wi conr ax-hyp ax-we ax-ie ax-ii ) AEBCFIZIAEJZBOPBJZCFQCJZDFRCDQCKRBCD IZQBCPBKLQBSIZCPTBATEGLLLMMREDFIZQECPEBAEKLLQEUAIZCPUBBAUBEHLLLMMNNN $. $( [?] $) $( [27-Jun-2006] $) $} $( Identity. Analogue to ~ ax-hyp . (#05) $) id $p # G |- ( ph -> ph ) $= ( ax-hyp ax-ii ) ABBABCD $. $( [?] $) $( [20-Oct-05] $) $( idd not added. $) $( Absorption of redundant antecedent. Also called the "Contraction" or "Hilbert" axiom. (#06) $) pm2.43 $p # G |- ( ( ph -> ( ph -> ps ) ) -> ( ph -> ps ) ) $= ( wi conr ax-hyp ax-we ax-ie ax-ii ) ABBCDZDZJAKEZBCLBEZBCLBFZMBJNLKBAKFGHH II $. $( [?] $) $( [27-Jun-2006] $) ${ pm2.43i.1 $e # G |- ( ph -> ( ph -> ps ) ) $. $( Inference absorbing redundant antecedent. (#06) $) pm2.43i $p # G |- ( ph -> ps ) $= ( wi pm2.43 ax-ie ) ABBCEZEHDABCFG $. $( [?] $) $( [27-Jun-2006] $) $} $( pm2.43d not added. $) ${ pm2.86i.1 $e # G |- ( ( ph -> ps ) -> ( ph -> ch ) ) $. $( Consequents can be joined. (#06) $) pm2.86i $p # G |- ( ph -> ( ps -> ch ) ) $= ( conr ax-hyp ax-we wi a1i weak2 ax-ie int2 ) ABCDABFZCFZBDNBCABGHOBCIZBD IZOCBNCGJAPQIBCEKLLM $. $( [?] $) $( [27-Jun-2006] $) $} $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Biimplication =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( Biimplication definition. I could have added axioms to manage the biimplication operator since some natural deduction systems add them. I have prefered to give a definition of the biimplication definition. This is set.mm definition for biimplication except that I have replaced '-. ( ph -> -. ps )' by the /\ operator. (#05) $) df-bi $a # G |- ( ( ( ph <-> ps ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) ) /\ ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ( ph <-> ps ) ) ) $. $( Biimplication turned into a simple implication. $) bi1 $p # G |- ( ( ph <-> ps ) -> ( ph -> ps ) ) $= ( wb wi conr wa ax-hyp df-bi ax-ale ax-we ax-ie ax-ii ) ABCDZBCEZANFZOCBEZP NOQGZANHANREZNASRNEABCIJKLJM $. $( [30-Jun-06] $) $( [17-Jun-05] $) $( Biimplication transformed into a simple implication. $) bi2 $p # G |- ( ( ph <-> ps ) -> ( ps -> ph ) ) $= ( wb wi conr wa ax-hyp df-bi ax-we ax-ale ax-ie ax-are ax-ii ) ABCDZCBEZAOF ZBCEZPQORPGZAOHQOSEZSOEZATUAGOABCIJKLMN $. $( [18-Jun-05] $) $( [18-Jun-05] $) ${ biimp.1 $e # G |- ( ph <-> ps ) $. $( Biimplication trnasormed into a simple implication (inference). $) biimp $p # G |- ( ph -> ps ) $= ( wb wi bi1 ax-ie ) ABCEBCFDABCGH $. $( [28-Feb-06] $) $( [28-Feb-06] $) $} ${ biimpr.1 $e # G |- ( ph <-> ps ) $. $( Biimplication transformed into a simple implication (inference). $) biimpr $p # G |- ( ps -> ph ) $= ( wb wi bi2 ax-ie ) ABCECBFDABCGH $. $( [28-Feb-06] $) $( [28-Feb-06] $) $} $( biimpd is not included $) $( biimprd is not included $) $( biimpcd is not included $) $( biimpd is not included $) ${ impbi.1 $e # G |- ( ph -> ps ) $. impbi.2 $e # G |- ( ps -> ph ) $. $( Simple implications transformed into a biimplication. $) impbi $p # G |- ( ph <-> ps ) $= ( wi wa wb ax-ai df-bi ax-are ax-ie ) ABCFZCBFZGZBCHZAMNDEIAPOFOPFABCJKL $. $( [?] $) $( [18-Jun-05] $) $} ${ bicomi.1 $e # G |- ( ph <-> ps ) $. $( Biimplication is reflexive. $) bicomi $p # G |- ( ps <-> ph ) $= ( wb wi bi2 ax-ie bi1 impbi ) ACBABCEZCBFDABCGHAKBCFDABCIHJ $. $( [?] $) $( [18-Jun-05] $) $} ${ mpbi.1 $e # G |- ( ph <-> ps ) $. mpbi.2 $e # G |- ph $. $( rembi* theorems make it easy to replace any definiens by its definiendum and vice versa. $) mpbi $p # G |- ps $= ( wb wi bi1 ax-ie ) ABCEABCFBCGDABCHII $. $( [?] $) $( [1-Jul-05] $) $} ${ mpbir.1 $e # G |- ( ph <-> ps ) $. mpbir.2 $e # G |- ps $. $( rembi* theorems make it easy to replace any definiens by its definiendum and vice versa. $) mpbir $p # G |- ph $= ( wb wi bi2 ax-ie ) ACBEABCFCBGDABCHII $. $( [?] $) $( [1-Jul-05] $) $} ${ sylbir.1 $e # G |- ( ph <-> ps ) $. sylbir.2 $e # G |- ( ph -> ch ) $. $( rembi* theorems make it easy to replace any definiens by its definiendum and vice versa. $) sylbir $p # G |- ( ps -> ch ) $= ( conr wb ax-we ax-hyp mpbir wi ax-ie ax-ii ) ACDACGZBDOBCABCHCEIACJKABDL CFIMN $. $( [?] $) $( [1-Jul-05] $) $} ${ sylbi.1 $e # G |- ( ph <-> ps ) $. sylbi.2 $e # G |- ( ps -> ch ) $. $( rembi* theorems make it easy to replace any definiens by its definiendum and vice versa. $) sylbi $p # G |- ( ph -> ch ) $= ( bicomi sylbir ) ACBDABCEGFH $. $( [?] $) $( [1-Jul-05] $) $} ${ sylib.1 $e # G |- ( ph <-> ps ) $. sylib.2 $e # G |- ( ch -> ph ) $. $( rembi* theorems make it easy to replace any definiens by its definiendum and vice versa. $) sylib $p # G |- ( ch -> ps ) $= ( biimp syl ) ADBCFABCEGH $. $( [?] $) $( [1-Jul-05] $) $} ${ sylibr.1 $e # G |- ( ph <-> ps ) $. sylibr.2 $e # G |- ( ch -> ps ) $. $( rembi* theorems make it easy to replace any definiens by its definiendum and vice versa. $) sylibr $p # G |- ( ch -> ph ) $= ( bicomi sylib ) ACBDABCEGFH $. $( [?] $) $( [1-Jul-05] $) $} ${ syl5ibr.1 $e # G |- ( ph <-> ps ) $. syl5ibr.2 $e # G |- ( ch -> ( ph -> th ) ) $. $( rembi* theorems make it easy to replace any definiens by its definiendum and vice versa. $) syl5ibr $p # G |- ( ch -> ( ps -> th ) ) $= ( wi conr wb ax-we ax-hyp ax-ie sylbir ax-ii ) ADCEHADIZBCEABCJDFKPDBEHZA DLADQHDGKMNO $. $( [?] $) $( [1-Jul-05] $) $} ${ syl6ib.1 $e # G |- ( ph <-> ps ) $. syl6ib.2 $e # G |- ( ch -> ( th -> ph ) ) $. $( rembi* theorems make it easy to replace any definiens by its definiendum and vice versa. $) syl6ib $p # G |- ( ch -> ( th -> ps ) ) $= ( wi conr wb ax-we ax-hyp ax-ie sylib ax-ii ) ADECHADIZBCEABCJDFKPDEBHZAD LADQHDGKMNO $. $( [?] $) $( [1-Jul-05] $) $} ${ remphyp.1 $e # G |- ( ph <-> ps ) $. remphyp.2 $e # [ G , ph ] |- ch $. $( A hypothesis is replaced by its definiens. $) remphyp $p # [ G , ps ] |- ch $= ( conr ax-hyp wi ax-ii sylbir ax-we ax-ie ) ACGCDACHACDICABCDEABDFJKLM $. $( [?] $) $( [31-Dec-05] $) $} ${ 3imtr4.1 $e # G |- ( ph -> ps ) $. 3imtr4.2 $e # G |- ( ch <-> ph ) $. 3imtr4.3 $e # G |- ( th <-> ps ) $. $( A mixed syllogism inference, useful for applying a definition to both sides of an implication. (#05) $) 3imtr4 $p # G |- ( ch -> th ) $= ( bicomi sylib sylbir ) ABDEADBGIACEBAECHIFJK $. $( [?] $) $( [12-Nov-05] $) $} ${ bitr.1 $e # G |- ( ph <-> ps ) $. bitr.2 $e # G |- ( ps <-> ch ) $. $( Biimplications is transitive. Replacement of the second member of a biimplication. $) bitr $p # G |- ( ph <-> ch ) $= ( conr wb ax-we ax-hyp wi bi1 ax-ie mpbi ax-ii mpbir impbi ) ABDABDABGZCD ACDHZBFIRBCABJABCKZBABCHZTEABCLMIMNOADBADGZBCAUADEIUBCDASDFIADJPPOQ $. $( [?] $) $( [30-Dec-05] $) $} ${ bitr2.1 $e # G |- ( ph <-> ps ) $. bitr2.2 $e # G |- ( ph <-> ch ) $. $( Replacement of the first member of a biimplication. $) bitr2 $p # G |- ( ch <-> ps ) $= ( bicomi bitr ) ACDACBDABCEGFHG $. $( [?] $) $( [1-Jan-06] $) $} ${ imbi2i.1 $e # G |- ( ph <-> ps ) $. $( We can add the same antecedent to both sides of a biimplication. $) imbi2i $p # G |- ( ( ch -> ph ) <-> ( ch -> ps ) ) $= ( wi biimp imim2i biimpr impbi ) ADBFDCFABCDABCEGHACBDABCEIHJ $. $} $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Not =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( Not definition. $) dfnot $p # G |- ( -. ph <-> ( ph -> Abs ) ) $= ( wn wabs wi conr ax-hyp ax-we ax-ne ax-ii ax-ie ax-ni impbi ) ABCZBDEZANOA NFZBDPBFBPBGPNBANGHIJJAONAOFZBQBFBDQBGQOBAOGHKLJM $. $( [?] $) $( [15-Aug-05] $) ${ a3i.1 $e # G |- ( -. ph -> -. ps ) $. $( An item of the contraposition species. $) a3i $p # G |- ( ps -> ph ) $= ( conr wn ax-hyp wi ax-we ax-ie ax-ne ax-ni ax-cl ax-ii ) ACBACEZBOBFZEZC FZQPROPGOPRHZPASCDIIJQRQRECQCROCPACGIIQRGKLKMN $. $( [?] $) $( [3-0ct-05] $) $} ${ con3i.1 $e # G |- ( ph -> ps ) $. $( An item of the contraposition species. $) con3i $p # G |- ( -. ps -> -. ph ) $= ( wn conr ax-hyp wi ax-we ax-ie ax-ne ax-ni ax-ii ) ACEZBEANFZBOBFZCPBCOB GOBCHZBAQNDIIJONBANGIKLM $. $( [?] $) $( [20-Oct-05] $) $} ${ dsl.1 $e # G |- ph $. dsl.2 $e # G |- -. ph $. $( Duns Scotus law. $) dsl $p # G |- ps $= ( ax-ne axin ) ACABDEFG $. $( [?] $) $( [15-Aug-05] $) $} $( A theorem of the Duns Scotus law species. We can as well see this theorem as a variant of setaxin-1 when the first antecedent is a negation. $) pm2.21 $p # G |- ( -. ph -> ( ph -> ps ) ) $= ( wn wi conr ax-hyp ax-we dsl ax-ii ) ABDZBCEAKFZBCLBFBCLBGLKBAKGHIJJ $. $( [?] $) $( [22-Nov-05] $) $( A theorem of the Duns Scotus law species. $) pm2.21b $p # [ [ G , -. ph ] , ph ] |- ps $= ( wn conr ax-hyp ax-we dsl ) ABDZEZBEBCJBFJIBAIFGH $. $( [?] $) $( [22-Nov-05] $) ${ pm2.21i.1 $e # G |- -. ph $. $( A contradiction implies anything. $) pm2.21i $p # G |- ( ph -> ps ) $= ( conr ax-hyp wn ax-we dsl ax-ii ) ABCABEBCABFABGBDHIJ $. $( [?] $) $( [29-Nov-05] $) $} $( Proof by contradiction. Note: the 'not' operator is a sort of reverser. Without 'not' we can only prove theorems with a right to left implication priority [ ( ph -> ( ps -> ch ) ) ]. With 'not' we can consider left to right implication priority [ ( ( ph -> ps ) -> ch ) ]. $) pm2.18 $p # G |- ( ( -. ph -> ph ) -> ph ) $= ( wn wi conr ax-hyp ax-we ax-ie ax-ne ax-cl ax-ii ) ABCZBDZBAMEZBNLEZBOLBNL FZNMLAMFGHPIJK $. $( [?] $) $( [29-Nov-05] $) $( Double negation (#05) $) dn $p # G |- ( -. -. ph <-> ph ) $= ( wn conr ax-hyp ax-we ax-ne ax-cl ax-ii ax-ni impbi ) ABCZCZBAMBAMDZBNLDLN LENMLAMEFGHIABMABDZLOLDBOBLABEFOLEGJIK $. $( [?] $) $( [13-Aug-05] $) $( Contraposition $) ctpt $p # G |- ( ( -. ph -> -. ps ) <-> ( ps -> ph ) ) $= ( wn wi setax-3 conr ax-hyp weak2 ax-ie ax-we ax-ne ax-ni int2 impbi ) ABDZ CDZECBEZABCFARPQARGZPGZCTCGZBUACBTCHSRPCARHIJTPCSPHKLMNO $. $( [?] $) $( [13-Aug-05] $) ${ con2.1 $e # G |- ( ph -> -. ps ) $. $( In these theorems about contraposition, I use double negation and ctpt. (#05) $) con2 $p # G |- ( ps -> -. ph ) $= ( wn wi ctpt dn bicomi sylbir mpbi ) ABEZEZCEZFCLFALCGABMNAMBABHIDJK $. $( [?] $) $( [29-Aug-05] $) $} ${ a2in.1 $e # G |- ( ph -> -. ps ) $. $( A sort of modus tollens. $) a2in $p # G |- ( ( ph -> ps ) -> -. ph ) $= ( wabs wi wn dfnot bicomi sylib a2i ) ABEFZBGZBCFAMLABHIABCEACGCEFBACHDJK J $. $( [?] $) $( [15-Aug-05] $) $} ${ pm3.26im.1 $e # G |- -. ( ph -> -. ps ) $. $( Simplification. In fact it is ~ ax-ale in disguise (#05) $) pm3.26im $p # G |- ph $= ( wn conr wi ax-hyp ax-we ax-ne axin ax-ii ax-cl ) ABABEZFZBCEZGZOBPOBFZP RBOBHONBANHIJKLAQENDIJM $. $( [?] $) $( [19-Aug-05] $) $} ${ pm2.51.1 $e # G |- -. ( ph -> ps ) $. $( (#05) $) pm2.51 $p # G |- ( ph -> -. ps ) $= ( wn conr wi ax-hyp ax-we ax-ii ax-ne ax-ni ) ABCEABFZCMCFZBCGZNBCNCBMCHI JMOEZCAPBDIIKLJ $. $( [?] $) $( [29-Aug-05] $) $} ${ pm2.5.1 $e # G |- -. ( ph -> ps ) $. $( (#05) $) pm2.5 $p # G |- ( -. ph -> ps ) $= ( wn conr wi ax-hyp ax-we ax-ne axin ax-ii ) ABEZCAMFZCNBCGZNBCNBFZCPBNBH NMBAMHIJKLAOEMDIJKL $. $( [?] $) $( [22-Apr-06] $) $} ${ mto.1 $e # G |- -. ps $. mto.2 $e # G |- ( ph -> ps ) $. $( The rule of modus tollens. $) mto $p # G |- -. ph $= ( conr ax-hyp wi ax-we ax-ie wn ax-ne ax-ni ) ABABFZCNBCABGABCHBEIJACKBDI LM $. $( [?] $) $( [11-Dec-05] $) $} ${ nsyl4.1 $e # G |- ( ph -> ps ) $. nsyl4.2 $e # G |- ( -. ph -> ch ) $. $( A negated syllogism inference. $) nsyl4 $p # G |- ( -. ch -> ps ) $= ( wn conr ax-hyp wi ax-we ax-ie ax-ne ax-cl ax-ii ) ADGZCAPHZBCQBQBGZHZDS RDQRIQRDJZRATPFKKLQPRAPIKMNABCJPEKLO $. $( [?] $) $( [11-Dec-05] $) $} $( Useful for eliminating an antecedent. (#06) $) pm2.61 $p # G |- ( ( ph -> ps ) -> ( ( -. ph -> ps ) -> ps ) ) $= ( wi wn conr ax-hyp ax-we mto ax-ne ax-cl ax-ii ) ABCDZBEZCDZCDAMFZOCPOFZCQ CEZFZNSBCQRGZQMRPMOAMGHHISNCTQORPOGHIJKLL $. $( [?] $) $( [6-May-06] $) ${ pm2.61i.1 $e # G |- ( ph -> ps ) $. pm2.61i.2 $e # G |- ( -. ph -> ps ) $. $( Inference eliminating an antecedent. $) pm2.61i $p # G |- ps $= ( wn wi pm2.61 ax-ie ) ABFCGZCEABCGJCGDABCHII $. $( [?] $) $( [6-May-06] $) $} ${ negbii.1 $e # G |- ( ph <-> ps ) $. $( Negate both sides of a logical equivalence. (#05) $) negbii $p # G |- ( -. ph <-> -. ps ) $= ( wn wi ctpt wb bicomi bi1 ax-ie mpbir impbi ) ABEZCEZANOFCBFZABCGACBHPAB CDIACBJKLAONFBCFZACBGABCHQDABCJKLM $. $( [?] $) $( [4-Jan-06] $) $} ${ negbii2.1 $e # G |- ( -. ph <-> -. ps ) $. $( Remove negate from both sides of a logical equivalence. $) negbii2 $p # G |- ( ph <-> ps ) $= ( wn biimpr a3i biimp impbi ) ABCACBABEZCEZDFGABCAJKDHGI $. $( [?] $) $( [18-May-06] $) $} ${ repnot.1 $e # G |- ( ph <-> ps ) $. repnot.2 $e # G |- -. ph $. $( Replacement of a wff behing a '-.' operator $) repnot $p # G |- -. ps $= ( wn wabs wi dfnot mpbi sylbir mpbir ) ACFCGHACIABCGDABFBGHABIEJKL $. $( [?] $) $( [26-Jan-06] $) $} ${ ja.1 $e # G |- ( -. ph -> ch ) $. ja.2 $e # G |- ( ps -> ch ) $. $( Inference joining the antecedents of two premises. (#06) $) ja $p # G |- ( ( ph -> ps ) -> ch ) $= ( wi conr wn dn ax-hyp ax-we mto mpbi ax-ie ax-ne ax-cl ax-ii ) ABCGZDASH ZDTDIZHZDUBCDUBBCUBBIZIBUBBJUBUCDTUAKZTUCDGZUAAUESELLMNTSUAASKLOTCDGZUAAU FSFLLOUDPQR $. $( [?] $) $( [22-Apr-06] $) $} $( Contraposition. Theorem *4.11 of [WhiteheadRussell] p. 117. $) pm4.11 $p # G |- ( ( ph <-> ps ) <-> ( -. ph <-> -. ps ) ) $= ( wb wn conr ax-hyp negbii ax-ii ax-we weak2 mpbir ax-ne ax-cl mpbi impbi ) ABCDZBEZCEZDZAQTAQFBCAQGHIATQATFZBCUABCUABFZCUBSFZBUBBSUABGJUCRSUATBSATGZ KUBSGLMNIUACBUACFZBUERFZCUECRUACGJUFRSUATCRUDKUERGOMNIPIP $. ${ _con3bii.1 $e # G |- ( ph <-> -. ps ) $. $( An inference of the contraposition series. $) _con3bii $p # G |- ( -. ph <-> ps ) $= ( wn dn bitr negbii2 ) ABEZCAIEBCEABFDGH $. $( [?] $) $( [13-Jun-2006] $) $} $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- And =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( Conjunction can be expressed in terms of implication and not connectors. (#05) $) dfan $p # G |- ( ( ph /\ ps ) <-> -. ( ph -> -. ps ) ) $= ( wa wn wi conr ax-hyp ax-we ax-are ax-ale ax-ie ax-ne ax-ni ax-ii pm3.26im dn pm2.51 mpbi ax-ai impbi ) ABCDZBCEZFZEZAUBUEAUBGZUDUFUDGZCUGBCUFUBUDAUBHI ZJUGBUCUGBCUHKUFUDHLMNOAUEUBAUEGZBCUIBCAUEHZPZUIUCEZCUICQUIBULUKUIBUCUJRLSTO UA $. $( [?] $) $( [22-Nov-05] $) $( Negated disjunction in terms of conjunction (DeMorgan's law). (#05) $) ioran $p # G |- ( -. ( ph \/ ps ) <-> ( -. ph /\ -. ps ) ) $= ( wo wn wa conr dn ax-hyp mpbi ax-oli ax-we ax-ne ax-cl ax-ori ax-ai ax-ii ax-are axin ax-oe ax-ale impbi ) ABCDZEZBEZCEZFZAUDUGAUDGZUEUFUHUEUHUEEZGZU CUJBCUJUIBUJBHUHUIIJKUHUDUIAUDIZLMNUHUFUHUFEZGZUCUMBCUMULCUMCHUHULIJOUHUDUL UKLMNPQAUGUDAUGGZUDUNUDEZGZBUPBCBUPUOUCUPUCHUNUOIJUPBIUPCGZBUQCUPCIUQUEUFUP UGCUNUGUOAUGILZLRMSTUPUEUFURUAMNQUB $. $( [?] $) $( [30-Nov-05] $) $( or can be expressed in terms of implication and not connectors. (#05) $) dfor $p # G |- ( ( ph \/ ps ) <-> ( -. ph -> ps ) ) $= ( wo wn wi conr ax-hyp ax-we dsl ax-oe ax-ii wa ioran mpbi ax-ale ax-ie ax-are ax-ne ax-cl impbi ) ABCDZBEZCFZAUBUDAUBGZUCCUEUCGZBCCUEUBUCAUBHIUFBG BCUFBHUFUCBUEUCHIJUFCHKLLAUDUBAUDGZUBUGUBEZGZCUIUCCUIUCCEZUIUHUCUJMUIBCNUGU HHOZPUGUDUHAUDHIQUIUCUJUKRSTLUA $. $( [?] $) $( [30-Nov-05] $) ${ jca.1 $e # G |- ( ph -> ps ) $. jca.2 $e # G |- ( ph -> ch ) $. $( Join consequents with 'and'. (#05) $) jca $p # G |- ( ph -> ( ps /\ ch ) ) $= ( wa conr ax-hyp wi ax-we ax-ie ax-ai ax-ii ) ABCDGABHZCDOBCABIZABCJBEKLO BDPABDJBFKLMN $. $( [?] $) $( [4-Jan-06] $) $} ${ jcai.1 $e # G |- ( ph -> ps ) $. jcai.2 $e # G |- ( ph -> ( ps -> ch ) ) $. $( Deduction replacing implication with conjunction. (#05) $) jcai $p # G |- ( ph -> ( ps /\ ch ) ) $= ( conr ax-hyp wi ax-we ax-ie ax-ii jca ) ABCDEABDABGZCDNBCABHZABCIBEJKNBC DIZOABPIBFJKKLM $. $( [?] $) $( [29-Jun-2006] $) $} ${ jctl.1 $e # G |- ps $. $( Inference conjoining a theorem to the left of a consequent. (#05) $) jctl $p # G |- ( ph -> ( ps /\ ph ) ) $= ( a1i id jca ) ABCBACBDEABFG $. $( [?] $) $( [29-Jun-2006] $) $} ${ jctr.1 $e # G |- ps $. $( Inference conjoining a theorem to the right of a consequent. (#05) $) jctr $p # G |- ( ph -> ( ph /\ ps ) ) $= ( id a1i jca ) ABBCABEACBDFG $. $( [?] $) $( [29-Jun-2006] $) $} ${ jctil.1 $e # G |- ( ph -> ps ) $. jctil.2 $e # G |- ch $. $( Inference conjoining a theorem to left of consequent in an implication. (#05) $) jctil $p # G |- ( ph -> ( ch /\ ps ) ) $= ( a1i jca ) ABDCADBFGEH $. $( [?] $) $( [29-Jun-2006] $) $} ${ jctir.1 $e # G |- ( ph -> ps ) $. jctir.2 $e # G |- ch $. $( Inference conjoining a theorem to right of consequent in an implication. (#05) $) jctir $p # G |- ( ph -> ( ps /\ ch ) ) $= ( a1i jca ) ABCDEADBFGH $. $( [?] $) $( [29-Jun-2006] $) $} ${ ancli.1 $e # G |- ( ph -> ps ) $. $( Deduction conjoining antecedent to left of consequent. (#05) $) ancli $p # G |- ( ph -> ( ph /\ ps ) ) $= ( wa conr ax-hyp wi ax-we ax-ie ax-ai ax-ii ) ABBCEABFZBCABGZMBCNABCHBDIJ KL $. $} ${ _con2bi.1 $e # G |- ( ph <-> ps ) $. _con2bi.2 $e # G |- ( ch <-> ta ) $. $( Conjunction of both sides of a biimplication. $) _con2bi $p # G |- ( ( ph /\ ch ) <-> ( ps /\ ta ) ) $= ( wa conr wb ax-we ax-hyp ax-ale mpbi ax-are ax-ai ax-ii mpbir impbi ) AB DHZCEHZATUAATIZCEUBBCABCJZTFKUBBDATLZMNUBDEADEJZTGKUBBDUDONPQAUATAUAIZBDU FBCAUCUAFKUFCEAUALZMRUFDEAUEUAGKUFCEUGORPQS $. $} $( Conjunction in terms of disjunction (DeMorgan's law). (#05) $) anor $p # G |- ( ( ph /\ ps ) <-> -. ( -. ph \/ -. ps ) ) $= ( wn wo wa ioran dn _con2bi bitr bicomi ) ABDZCDZEDZBCFZANLDZMDZFOALMGAPBQC ABHACHIJK $. $( Negated conjunction in terms of disjunction (DeMorgan's law). (#05) $) ianor $p # G |- ( -. ( ph /\ ps ) <-> ( -. ph \/ -. ps ) ) $= ( wa wn wo anor _con3bii ) ABCDBECEFABCGH $. $( ioran see above $) $( Disjunction in terms of conjunction (DeMorgan's law). (#05) $) oran $p # G |- ( ( ph \/ ps ) <-> -. ( -. ph /\ -. ps ) ) $= ( wn wa wo ioran bicomi _con3bii ) ABDCDEZDBCFZAJKAKDJABCGHIH $. $( Elimination of a conjunct. (#05) $) pm3.26 $p # G |- ( ( ph /\ ps ) -> ph ) $= ( wa conr ax-hyp ax-ale ax-ii ) ABCDZBAIEBCAIFGH $. ${ pm3.26d.1 $e # G |- ( ph -> ( ps /\ ch ) ) $. $( Elimination of a conjunct. (#05) $) pm3.26d $p # G |- ( ph -> ps ) $= ( conr wa ax-hyp wi ax-we ax-ie ax-ale ax-ii ) ABCABFZCDNBCDGZABHABOIBEJK LM $. $( [?] $) $( [23-Jun-05] $) $} $( Elimination of a conjunct. (#05) $) pm3.27 $p # G |- ( ( ph /\ ps ) -> ps ) $= ( wa conr ax-hyp ax-are ax-ii ) ABCDZCAIEBCAIFGH $. $( pm3.27d not added. $) ${ anim12i.1 $e # G |- ( ph -> ps ) $. anim12i.2 $e # G |- ( ch -> th ) $. $( Conjoin antecedents and consequents of two premises. (#05) $) anim12i $p # G |- ( ( ph /\ ch ) -> ( ps /\ th ) ) $= ( wa conr ax-hyp ax-ale wi ax-we ax-ie ax-are ax-ai ax-ii ) ABDHZCEHARIZC ESBCSBDARJZKABCLRFMNSDESBDTOADELRGMNPQ $. $( [?] $) $( [12-Nov-05] $) $} ${ anim1i.1 $e # G |- ( ph -> ps ) $. $( Introduce conjunct to both sides of an implication. (#05) $) anim1i $p # G |- ( ( ph /\ ch ) -> ( ps /\ ch ) ) $= ( id anim12i ) ABCDDEADFG $. $( [?] $) $( [1-Jan-06] $) $( Introduce conjunct to both sides of an implication. (#05) $) anim2i $p # G |- ( ( ch /\ ph ) -> ( ch /\ ps ) ) $= ( id anim12i ) ADDBCADFEG $. $( [?] $) $( [1-Jan-06] $) $} ${ _hypsp.1 $e # [ G , ( ph /\ ps ) ] |- ch $. $( A 'and' hypothesis is splitted. $) _hypsp $p # [ [ G , ph ] , ps ] |- ch $= ( conr wa ax-hyp ax-we ax-ai wi ax-ii ax-ie ) ABFZCFZBCGZDOBCNBCABHINCHJN PDKZCAQBAPDELIIM $. $( [?] $) $( [15-Nov-05] $) $} ${ _hypunif.1 $e # [ [ G , ph ] , ps ] |- ch $. $( Two hypothesis are unified with a ' /\ '. $) _hypunif $p # [ G , ( ph /\ ps ) ] |- ch $= ( wa conr ax-hyp ax-ale wi ax-are exch ax-ii ax-we ax-ie ) ABCFZGZBDQBCAP HZIQCBDJZQBCRKACSJPACSACGBDABCDELMMNOO $. $( [?] $) $( [31-Dec-05] $) $} ${ imp.1 $e # G |- ( ph -> ( ps -> ch ) ) $. $( Importation inference. (#05) $) imp $p # G |- ( ( ph /\ ps ) -> ch ) $= ( wa conr ax-hyp wi ax-we ax-ie _hypunif ax-ii ) ABCFDABCDABGZCGZCDNCHOBC DIZNBCABHJNBPIZCAQBEJJKKLM $. $} $( Syllogisme with and. $) pm3.33 $p # G |- ( ( ( ph -> ps ) /\ ( ps -> ch ) ) -> ( ph -> ch ) ) $= ( ) ? $. ${ exp.1 $e # G |- ( ( ph /\ ps ) -> ch ) $. $( Exportation inference. (#05) $) exp $p # G |- ( ph -> ( ps -> ch ) ) $= ( wi conr wa ax-hyp ax-we ax-ie _hypsp ax-ii ) ABCDFABGCDABCDABCHZGNDANIA NDFNEJKLMM $. $} $( Import-export theorem. In fact "ph , ps |- ch" ( I have removed the square brackets because metamath don't like them ) can be translated in ( ( ph /\ ps ) -> ch ). This theorem says that it could as well be translated into ( ph -> ( ps -> ch ) ) (#05) $) impexp $p # G |- ( ( ( ph /\ ps ) -> ch ) <-> ( ph -> ( ps -> ch ) ) ) $= ( wa wi conr ax-hyp exp ax-ii imp impbi ) ABCEDFZBCDFFZAMNAMGBCDAMHIJANMANG BCDANHKJL $. $( exp3a not added. $) ${ adantl.1 $e # G |- ( ph -> ps ) $. $( Inference adding a conjunct to the left of an antecedent. (#05) $) adantl $p # G |- ( ( ch /\ ph ) -> ps ) $= ( wa conr ax-hyp wi ax-we ax-ie _hypunif ax-ii ) ADBFCADBCADGZBGBCNBHNBCI ZBAODEJJKLM $. $} ${ adantr.1 $e # G |- ( ph -> ps ) $. $( Inference adding a conjunct to the right of an antecedent. (#05) $) adantr $p # G |- ( ( ph /\ ch ) -> ps ) $= ( wa conr ax-hyp ax-we wi ax-ie _hypunif ax-ii ) ABDFCABDCABGZDGBCNBDABHI NBCJZDAOBEIIKLM $. $} $( Idempotent law for conjunction. (#05) $) anidm $p # G |- ( ( ph /\ ph ) <-> ph ) $= ( wa pm3.26 conr ax-hyp ax-ai ax-ii impbi ) ABBCZBABBDABJABEBBABFZKGHI $. $( Associative law for conjunction. (#05) $) anass $p # G |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) ) $= ( wa conr ax-hyp ax-we _hypunif ax-ai ax-ii impbi ) ABCEZDEZBCDEZEZANPAMDPA MFZDFZBOQBDABCBABFZBCABGHZIHRCDQCDABCCSCGZIHQDGJJIKAPNABONSCDNSCFZDFZMDUCBC UBBDTHUBCDUAHJUBDGJIIKL $. $( set.mm uses syld to demonstrate the next theorem. It really shortens the proof. That's the reason why I wonder if I shouldn't include deductions in this file. $) ${ sylan9.1 $e # G |- ( ph -> ( ps -> ch ) ) $. sylan9.2 $e # G |- ( th -> ( ch -> ta ) ) $. $( Nested syllogism inference conjoining dissimilar antecedents. $) sylan9 $p # G |- ( ( ph /\ th ) -> ( ps -> ta ) ) $= ( wa wi conr ax-hyp adantr ax-we ax-ie adantl syl ax-ii ) ABEIZCFJASKZCDF TSCDJZASLZASUAJSABUAEGMNOTSDFJZUBASUCJSAEUCBHPNOQR $. $} ${ sylan9r.1 $e # G |- ( ph -> ( ps -> ch ) ) $. sylan9r.2 $e # G |- ( th -> ( ch -> ta ) ) $. $( Nested syllogism inference conjoining dissimilar antecedents. $) sylan9r $p # G |- ( ( th /\ ph ) -> ( ps -> ta ) ) $= ( wa wi conr ax-hyp ax-we ax-ie syl _hypunif ax-ii ) AEBICFJZAEBRAEKZBKZC DFTBCDJZSBLSBUAJZBAUBEGMMNTEDFJZSEBAELMSEUCJZBAUDEHMMNOPQ $. $} $( Introduce one conjunct as an antecedent to the another. $) abai $p # G |- ( ( ph /\ ps ) <-> ( ph /\ ( ph -> ps ) ) ) $= ( wa wi conr ax-hyp ax-ale _hypunif ax-we ax-ii ax-ai ax-ie impbi ) ABCDZBB CEZDZAOQAOFZBPRBCAOGHRBCRCBABCCABFZCGIJKLKAQOAQFZBCTBPAQGHABPCSPFBCSBPABGJS PGMILKN $. ${ bi.aa $e # G |- ( ph <-> ps ) $. $( Introduce a left conjunct to both sides of a logical equivalence. $) anbi2i $p # G |- ( ( ch /\ ph ) <-> ( ch /\ ps ) ) $= ( id impbi _con2bi ) ADDBCADDADFZIGEH $. $( Introduce a right conjunct to both sides of a logical equivalence. $) anbi1i $p # G |- ( ( ph /\ ch ) <-> ( ps /\ ch ) ) $= ( id impbi _con2bi ) ABCDDEADDADFZIGH $. $} ${ bi2an.1 $e # G |- ( ph <-> ps ) $. bi2an.2 $e # G |- ( ch <-> th ) $. $( Conjoin both sides of two equivalences. $) anbi12i $p # G |- ( ( ph /\ ch ) <-> ( ps /\ th ) ) $= ( wa biimp anim12i biimpr impbi ) ABDHCEHABCDEABCFIADEGIJACBEDABCFKADEGKJ L $. $} $( A biimplication is equivalent to two implications. $) bi $p # G |- ( ( ph <-> ps ) <-> ( ( ph -> ps ) /\ ( ps -> ph ) ) ) $= ( wb wi wa conr ax-hyp bi1 ax-ie bi2 ax-ai ax-ii ax-ale ax-are impbi ) ABCD ZBCEZCBEZFZAQTAQGZRSUAQRAQHZUABCIJUAQSUBUABCKJLMATQATGZBCUCRSATHZNUCRSUDOPM P $. $( [?] $) $( [2-Jan-06] $) $( impbid not added. $) $( Commutative law for equivalence. $) bicom $p # G |- ( ( ph <-> ps ) <-> ( ps <-> ph ) ) $= ( wb conr ax-hyp bicomi ax-ii impbi ) ABCDZCBDZAJKAJEBCAJFGHAKJAKECBAKFGHI $. $( bicomd not added. $) $( bitrd not added. $) $( bitr3d not added. $) $( bitr4d not added. $) ${ syl5bb.1 $e # G |- ( ph -> ( ps <-> ch ) ) $. syl5bb.2 $e # G |- ( th <-> ps ) $. $( A syllogism inference from two biconditionals. (#06) $) syl5bb $p # G |- ( ph -> ( th <-> ch ) ) $= ( wb conr ax-hyp wi ax-we ax-ie bicomi bitr2 ax-ii ) ABEDHABIZCDEQBCDHZAB JABRKBFLMQECAECHBGLNOP $. $} ${ syl5rbb.1 $e # G |- ( ph -> ( ps <-> ch ) ) $. syl5rbb.2 $e # G |- ( th <-> ps ) $. $( A syllogism inference from two biconditionals. (#06) $) syl5rbb $p # G |- ( ph -> ( ch <-> th ) ) $= ( wb conr ax-we bicomi ax-hyp wi ax-ie bitr2 ax-ii ) ABDEHABIZCEDQECAECHB GJKQBCDHZABLABRMBFJNOP $. $} ${ syl5bbr.1 $e # G |- ( ph -> ( ps <-> ch ) ) $. syl5bbr.2 $e # G |- ( ps <-> th ) $. $( A syllogism inference from two biconditionals. (#06) $) syl5bbr $p # G |- ( ph -> ( th <-> ch ) ) $= ( wb conr ax-hyp wi ax-we ax-ie bitr2 ax-ii ) ABEDHABIZCDEPBCDHZABJABQKBF LMACEHBGLNO $. $} ${ syl6bb.1 $e # G |- ( ph -> ( ps <-> ch ) ) $. syl6bb.2 $e # G |- ( ch <-> th ) $. $( A syllogism inference from two biconditionals. (#06) $) syl6bb $p # G |- ( ph -> ( ps <-> th ) ) $= ( wb conr ax-hyp wi ax-we ax-ie bitr ax-ii ) ABCEHABIZCDEPBCDHZABJABQKBFL MADEHBGLNO $. $( [?] $) $( [8-Jul-2006] $) $} ${ syl6rbb.1 $e # G |- ( ph -> ( ps <-> ch ) ) $. syl6rbb.2 $e # G |- ( ch <-> th ) $. $( A syllogism inference from two biconditionals. (#06) $) syl6rbb $p # G |- ( ph -> ( th <-> ps ) ) $= ( wb conr ax-hyp wi ax-we syl6bb ax-ie bicomi ax-ii ) ABECHABIZCEQBCEHABJ QBCDEABCDHKBFLADEHBGLMNOP $. $( [?] $) $( [8-Jul-2006] $) $} ${ syl6bbr.1 $e # G |- ( ph -> ( ps <-> ch ) ) $. syl6bbr.2 $e # G |- ( th <-> ch ) $. $( A syllogism inference from two biconditionals. (#06) $) syl6bbr $p # G |- ( ph -> ( ps <-> th ) ) $= cong wph wps wch wth syl6bbr.1 cong wth wch syl6bbr.2 bicomi syl6bb $. $} ${ 3bitr4g.1 $e # G |- ( ph -> ( ps <-> ch ) ) $. 3bitr4g.2 $e # G |- ( th <-> ps ) $. 3bitr4g.3 $e # G |- ( ta <-> ch ) $. $( More general version of ~ 3bitr4 . Useful for converting definitions in a formula. (#06) $) 3bitr4g $p # G |- ( ph -> ( th <-> ta ) ) $= cong wph wth wch wta cong wph wps wch wth 3bitr4g.1 cong wth wps 3bitr4g.2 bicomi syl5bbr 3bitr4g.3 syl6bbr $. $} $( It was proved by Leibniz, and it evidently pleased him enough to call it 'praeclarum theorema.' (#06) $) prth $p # G |- ( ( ( ph -> ps ) /\ ( ch -> th ) ) -> ( ( ph /\ ch ) -> ( ps /\ th ) ) ) $= ( wi wa conr ax-hyp ax-we anim12i _hypunif ax-ii ) ABCFZDEFZGBDGCEGFZANOPAN HZOHBCDEQNOANIJQOIKLM $. $( [?] $) $( [8-Jul-2006] $) $( anim2d (#06) not added. $) $( Absorption of redundant internal disjunct. (#06) $) orabs $p # G |- ( ph <-> ( ( ph \/ ps ) /\ ph ) ) $= wps wo wph cong wph conr wph wps cong wph ax-hyp ax-oli cong wph ax-hyp ax-ai ax-ii cong wph wps wo wph pm3.27 impbi $. $( Distributive law for disjunction. (#06) $) ordi $p # G |- ( ( ph \/ ( ps /\ ch ) ) <-> ( ( ph \/ ps ) /\ ( ph \/ ch ) ) ) $= ? $. $( Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (#06) $) olc $p # G |- ( ph -> ( ps \/ ph ) ) $= ( wn ax-1 orrd ) ABAABCDE $. $( [30-Aug-93] (#06) $) $( Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104. (#06) $) orc $p # G |- ( ph -> ( ph \/ ps ) ) $= ( pm2.24 orrd ) AABABCD $. $( [30-Aug-93] (#06) $) $( Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell] p. 111. (#06) $) pm3.21 $p # G |- ( ph -> ( ps -> ( ps /\ ph ) ) ) $= ( wa pm3.2 com12 ) BABACBADE $. $( [5-Aug-93] (#06) $) ${ pm3.2i.1 $e # G |- ph $. pm3.2i.2 $e # G |- ps $. $( Infer conjunction of premises. (#06) $) pm3.2i $p # G |- ( ph /\ ps ) $= ( wa pm3.2 mp2 ) ABABECDABFG $. $( [5-Aug-93] (#06) $) $} $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Biimplication and 'and' operator =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) ${ symand.1 $e # G |- ( ph /\ ps ) $. $( 'and' id symmetrical $) symand $p # G |- ( ps /\ ph ) $= ( ax-are ax-ale ax-ai ) ACBABCDEABCDFG $. $( [?] $) $( [26-Jan-06] $) $} $( And is commutative. (#06) $) ancom $p # G |- ( ( ph /\ ps ) <-> ( ps /\ ph ) ) $= ( wa conr ax-hyp symand ax-ii impbi ) ABCDZCBDZAJKAJEBCAJFGHAKJAKECBAKFGHI $. ${ biandl.1 $e # G |- ( ph /\ ps ) $. biandl.2 $e # G |- ( ph <-> ch ) $. $( Replacement of the left member of a 'and'. $) biandl $p # G |- ( ch /\ ps ) $= ( ax-ale mpbi ax-are ax-ai ) ADCABDFABCEGHABCEIJ $. $( [?] $) $( [26-Jan-06] $) $} ${ biandr.1 $e # G |- ( ph /\ ps ) $. biandr.2 $e # G |- ( ps <-> ch ) $. $( Replacement of the right member of a 'and'. $) biandr $p # G |- ( ph /\ ch ) $= ( symand biandl ) ADBACBDABCEGFHG $. $( [?] $) $( [26-Jan-06] $) $} ${ cii.1 $e # G |- ( ( ph -> ps ) /\ ( ch -> ta ) ) $. $( Moving a conjunction inside both sides of an implication. $) cii $p # G |- ( ( ph /\ ch ) -> ( ps /\ ta ) ) $= ( wa conr ax-hyp ax-ale wi ax-we ax-ie ax-are ax-ai ax-ii ) ABDGZCEGAQHZC ERBCRBDAQIZJABCKZQATDEKZFJLMRDERBDSNAUAQATUAFNLMOP $. $} ${ apbi.1 $e # G |- ( ph -> ps ) $. $( Appending a proposition to both sides of an implication $) apbi $p # G |- ( ( ch /\ ph ) -> ( ch /\ ps ) ) $= ( wa conr ax-hyp ax-ale ax-are wi ax-we ax-ie ax-ai ax-ii ) ADBFZDCFAPGZD CQDBAPHZIQBCQDBRJABCKPELMNO $. $} $( Principle of identity for logical equivalence. (#05) $) pm4.2 $p # G |- ( ph <-> ph ) $= ( id impbi ) ABBABCZED $. $( [?] $) $( [15-Nov-05] $) $( When a proposition is duplicated in a and-wff we can remove one of them. (#05) $) pm4.24 $p # G |- ( ph <-> ( ph /\ ph ) ) $= ( wa wi cone id jca ax-con conr ax-hyp _hypunif ax-ii impbi ) ABBBCZABNDEBB BEBFZOGHANBABBBABIBJKLM $. $( [?] $) $( [8-May-06] $) ${ jcad.1 $e # G |- ( ph -> ( ps -> ch ) ) $. jcad.2 $e # G |- ( ph -> ( ps -> th ) ) $. $( Deduction conjoining the consequents of two implications. (#06) $) jcad $p # G |- ( ph -> ( ps -> ( ch /\ th ) ) ) $= ? $. $} $( Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (#06) $) andi $p # G |- ( ( ph /\ ( ps \/ ch ) ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) ) $= ( wn wo wa ordi ioran orbi2i ianor anbi12i 3bitr4 negbii anor oran ) ADZBCE ZDZEZDABFZDZACFZDZFZDAQFTUBESUDPBDZCDZFZEPUEEZPUFEZFSUDPUEUFGRUGPBCHIUAUHUC UIABJACJKLMAQNTUBOL $. $( [5-Aug-93] (#06) $) $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Or =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( (Mgl) $) pm4.25 $p # G |- ( ph <-> ( ph \/ ph ) ) $= ( wo conr ax-hyp ax-oli ax-ii ax-oe impbi ) ABBBCZABJABDBBABEFGAJBAJDZBBBAJ EKBEZLHGI $. $( [?] $) $( [29-Nov-05] $) $( An implication can be replaced by a disjunction. (#05) $) imor $p # G |- ( ( ph -> ps ) <-> ( -. ph \/ ps ) ) $= ( wi wn wo conr dfor dn ax-hyp mpbi ax-we ax-ie ax-ii mpbir sylbir impbi ) ABCDZBEZCFZARTARGZTSEZCDZUASCHUAUBCUAUBGZBCUDUBBUDBIUAUBJKUARUBARJLMNONATRA TGZUBBCUEBIUETUCUESCHATJKPNQ $. $( [?] $) $( [25-Dec-05] $) $( Express implication in terms of conjunction. A theorem of the 'and' definition species. (#05) $) iman $p # G |- ( ( ph -> ps ) <-> -. ( ph /\ -. ps ) ) $= ( wi wn wa conr ax-hyp ax-we dn bicomi sylib dfan mpbi ax-ne axin ax-ni ax-ii mpbir impbi ) ABCDZBCEZFZEZAUAUDAUAGZUCUEUCGZUAUEUAUCAUAHIZUFUAEUFBUB EZDZUFCUHBUFUHCUFCJKUGLUFUCUIEZUFBUBMUEUCHNOPOQRAUDUAAUDGZUHCBUKCJUKUJEUIUK UIJUKUJUKUJGZUCULUCUJULBUBMUKUJHSUKUDUJAUDHIOQNLRT $. $( [?] $) $( [25-Dec-05] $) $( Excluded middle. $) exmid $p # G |- ( ph \/ -. ph ) $= ( wn wo wi dfor id mpbir ) ABBCZDIIEABIFAIGH $. $( [?] $) $( [30-Nov-05] $) $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Abs =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( When the antecedent is absurd, any implication is true. $) antabs $p # G |- ( Abs -> ph ) $= ( wabs conr wn ax-hyp ax-we ax-cl ax-ii ) ACBACDZBJCBEACFGHI $. $( [?] $) $( [22-Apr-06] $) $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Truth =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $c Truth $. $( Truth is a well-formed formula. $) wtru $a wff Truth $. $( Truth is the opposite of Absurdity. $) df-truth $a # G |- ( Truth <-> -. Abs ) $. ${ $( Truth is always true. $) inft $p # G |- Truth $= ( wtru wabs wn df-truth ax-hyp ax-ni mpbir ) ABCDAEACACFGH $. $} $( Truth can be removed from or added to a and-wff. $) elmtrand $p # G |- ( ( ph /\ Truth ) <-> ph ) $= ( wtru wa conr ax-hyp ax-ale ax-ii inft ax-ai impbi ) ABCDZBALBALEBCALFGHAB LABEZBCABFMIJHK $. $( When Truth is an antecedent of an implication it can be remove. $) elmtrimp $p # G |- ( ( Truth -> ph ) -> ph ) $= ( wtru wi conr inft ax-hyp ax-ie ax-ii ) ACBDZBAJEZCBKFAJGHI $. $( [?] $) $( [7-May-06] $) ${ treqth.1 $e # G |- ph $. $( Any theorem is equivalent to Truth. $) treqth $p # G |- ( Truth <-> ph ) $= ( wtru ax-we ax-ii conr inft impbi ) ADBADBABDCEFABDABGHFI $. $} ${ elmthand.1 $e # G |- ph $. $( A theorem can be removed from or added to a and-wff. $) elmthand $p # G |- ( ( ps /\ ph ) <-> ps ) $= ( wa conr ax-hyp ax-ale ax-ii ax-we ax-ai impbi ) ACBEZCAMCAMFCBAMGHIACMA CFCBACGABCDJKIL $. $} ${ elmthimp.1 $e # G |- ph $. $( When a theorem is the antecedent of an implication it can be removed. $) elmthimp $p # G |- ( ( ph -> ps ) -> ps ) $= ( wi conr ax-we ax-hyp ax-ie ax-ii ) ABCEZCAKFBCABKDGAKHIJ $. $( [?] $) $( [7-May-06] $) $} $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#* Predicate calculus #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#* $) $c / $. $( read 'is replaced by' $) $c = $. $( read 'is equal to' $) $c set $. $( read 'the following sequence is a set' $) $c A. $. $( read 'for all' $) $c E. $. $( read 'there exists' $) $c bound $. $( ' bound x G ' is read ' x is bound in all the formula of G ' $) $( individual variables $) $v u $. $v v $. $v w $. $v x $. $v y $. $v z $. su $f set u $. sv $f set v $. sw $f set w $. sx $f set x $. sy $f set y $. sz $f set z $. $( ------------------------------------------------------------------------------ Syntactic rules ------------------------------------------------------------------------------ $) $( If ph is a wff, x and y are individual variables [ x / y ] ph is a wff. $) ws $a wff [ x / y ] ph $. $( If ph is a wff and x is an individual variable A. x ph is a wff. $) wu $a wff A. x ph $. $( If ph is a wff and x is an individual variable E. x ph is a wff. $) we $a wff E. x ph $. $( if x and y are individual variables, x = y is a wff. $) wq $a wff x = y $. $( Mmj2 type. This statement is only used by mmj2. $) $( bound x G is a formula. $) lstyp2 $a LSTYP bound x G $. $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Predicate calculus axioms and inference rules =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( Bondage axioms. $) ${ ax-bg.1 $e # bound x G $. ax-bg.2 $e # [] |- ( ph -> A. x ph ) $. $( To prove that a variable is bound in all the hypotheses of a context you have to prove that it is bound in each hypothesis. $) ax-bg $a # bound x [ G , ph ] $. $} $( Any variable is bound in the empty context. $) ax-voi $a # bound x [] $. $( Axioms about the quantifiers. $) ${ ax-ui.1 $e # G |- ph $. ax-ui.2 $e # bound x G $. $( Universal quantifier introduction. $) ax-ui $a # G |- A. x ph $. $} ${ ax-ue.1 $e # G |- A. x ph $. $( Universal quantifier elimination. If a statement is true for all x it is true for a special value of x. $) ax-ue $a # G |- ph $. $} ${ ax-ei.1 $e # G |- ph $. $( Universal quantifier introduction. Strangely enough there is no need that x is bound in G whereas it is mandatory in ax-ui. However if we had imported 19.8a from set.mm into nat.mm ax-ei could be proved. Consequently ax-ei is correct. $) ax-ei $a # G |- E. x ph $. $} ${ ax-ee.1 $e # G |- E. x ph $. ax-ee.2 $e # [ G , ph ] |- ps $. ax-ee.3 $e # bound x G $. ax-ee.4 $e # G |- A. x ( ps -> A. x ps ) $. $( Existential quantifier elimination. This axiom looks like \/ elimination. It is normal. Informally we can consider that E. x ph is equivalent to [ a / x ] ph \/ [ b / x ] ph \/ ..., a, b, ... being all the possible value of the variable. $) ax-ee $a # G |- ps $. $} $( Extra axioms. The following axioms are closed form theorems borrowed to set.mm. I need them to prove several axioms in 'set.mm' (called setax-* in this file). $) $( x is bound in A. x ph. $) ax-uqb $a # G |- ( A. x ph -> A. x A. x ph ) $. $( x is bound in E. x ph. $) ax-eqb $a # G |- ( E. x ph -> A. x E. x ph ) $. ${ ax-nb.1 $e # [] |- ( ph -> A. x ph ) $. $( If x is bound in ph it is bound in -. ph $) ax-nb $a # [] |- ( -. ph -> A. x -. ph ) $. $} ${ ax-bvrb.1 $e # [] |- ( ph -> A. x ph ) $. $( If x is bound in ph, it is bound in A. y ph. $) ax-bvrb $a # [] |- ( A. y ph -> A. x A. y ph ) $. $} $( The stuff specific to natural deduction finished here. Beyond the axioms are only those of set.mm $) $( Definition of the existential quantifier. (#06) $) df-ex $a # G |- ( E. x ph <-> -. A. x -. ph ) $. $( set.mm axioms proved back. It is important to be able to prove setax-* since it ensures our system is logically and metalogically complete. $) $( Closed form of ~ax-ue . (#06) $) setax-4 $p # G |- ( A. x ph -> ph ) $= ( wu conr ax-hyp ax-ue ax-ii ) ABCDZBAIEBCAIFGH $. $( [?] $) $( [5-May-06] $) $( Axiom of Quantified Implication. This axiom moves a quantifier from outside to inside an implication, quantifying ` ps `. (#06) $) setax-5 $p # G |- ( A. x ( A. x ph -> ps ) -> ( A. x ph -> A. x ps ) ) $= ( wu wi cone conr ax-hyp ax-we ax-ue ax-ie ax-voi ax-uqb ax-bg ax-ui int2 ax-con ) ABDEZCFZDEZSCDEZFFGUASUBGUAHZSHZCDUDSCUCSIUDTDUCUASGUAIJKLUCSDGUAD DMGTDNOGBDNOPQR $. $( [?] $) $( [5-May-06] $) $( Axiom of Quantified Negation. This axiom is used to manipulate negated quantifiers. (#06) $) setax-6 $p # G |- ( -. A. x -. A. x ph -> ph ) $= ( wu wn wi cone conr ax-hyp ax-voi ax-uqb ax-nb ax-bg ax-ui ax-we ax-ne ax-cl ax-ue ax-ii ax-con ) ABCDZEZCDZEZBFGUDBGUDHZBCUEUAUEUBHZUCUFUBCUEUBIU EUBCGUDCCJUCCGUBCKLMUACGBCKLMNUEUDUBGUDIOPQRST $. $( [?] $) $( [5-May-06] $) $( Quantifier commutation. (#06) $) setax-7 $p # G |- ( A. x A. y ph -> A. y A. x ph ) $= ( wu wi cone conr ax-hyp ax-ue ax-voi ax-uqb ax-bg ax-ui ax-bvrb ax-ii ax-con ) ABDEZCEZBCEZDEZFGSUAGSHZTDUBBCUBBDUBRCGSIJJGSCCKGRCLMNGSDDKRDCGBDL OMNPQ $. $( [?] $) $( [5-May-06] $) ${ setax-gen.1 $e # G |- ph $. setax-gen.2 $e # bound x G $. $( universal quantifier introduction. It's a synonym for ax-ui. (#06) $) setax-gen $p # G |- A. x ph $= ( ax-ui ) ABCDEF $. $} $( Other theorems. $) $( a4i s a synonym for ax-ue. It is not included in this file. $) ${ a4s.1 $e # G |- ( ph -> ps ) $. $( Generalization of antecedent. (#06) $) a4s $p # G |- ( A. x ph -> ps ) $= ( wu conr ax-hyp ax-ue ax-ii syl ) ABDFZBCALBALGBDALHIJEK $. $} ${ mpg.1 $e # G |- ( A. x ph -> ps ) $. mpg.2 $e # G |- ph $. mpg.3 $e # bound x G $. $( Modus ponens combined with generalization. (#06) $) mpg $p # G |- ps $= ( wu ax-ui ax-ie ) ABDHCABDFGIEJ $. $( [?] $) $( [11-May-06] $) $} ${ a5i.1 $e # G |- ( A. x ph -> ps ) $. a5i.2 $e # bound x G $. $( If x is bound in the antecedents, we can generalize the conclusion. (#06) $) a5i $p # G |- ( A. x ph -> A. x ps ) $= ( wu conr ax-hyp wi ax-we ax-ie cone ax-uqb ax-bg ax-ui ax-ii ) ABDGZCDGA RHZCDSRCARIARCJREKLARDFMBDNOPQ $. $( [?] $) $( [8-May-06] $) $} $( Abbreviated version of ~ setax-6 . (#06) $) a6e $p # G |- ( E. x A. x ph -> ph ) $= ( wu we wn df-ex setax-6 sylbi ) ABCDZCEJFCDFBAJCGABCHI $. $( [9-Apr-06] $) $( [9-Apr-06] $) ${ a7s.1 $e # G |- ( A. x A. y ph -> ps ) $. $( Swap quantifiers in an antecedent. (#06) $) a7s $p # G |- ( A. y A. x ph -> ps ) $= ( wu setax-7 syl ) ABDGEGBEGDGCABEDHFI $. $( [9-Apr-06] $) $( [9-Apr-06] $) $} $( A universal quantifier can move from outside to inside the members of an implication (#06) $) 19.20 $p # G |- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) ) $= ( wi wu cone conr ax-hyp ax-ue a4s ax-voi ax-uqb ax-bg a5i ax-ii ax-con ) ABCEZDFZBDFCDFEZEGSTGSHZBCDUABCDUARDGSIJKGSDDLGRDMNOPQ $. $( [9-Apr-06] $) $( [9-Apr-06] $) ${ 19.20i.1 $e # G |- A. x ( ph -> ps ) $. $( Inference quantifying both antecedent and consequent. Note: In set.mm the hypothesis is not quantified. But the presence of a context makes the quantification mandatory. See also ~ 19.20i2 (#06) $) 19.20i $p # G |- ( A. x ph -> A. x ps ) $= ( wi wu 19.20 ax-ie ) ABCFDGBDGCDGFEABCDHI $. $( [10-Apr-06] $) $( [10-Apr-06] $) $} ${ 19.20i2.1 $e # G |- ( ph -> ps ) $. 19.20i2.2 $e # bound x G $. $( Inference quantifying both antecedent and consequent. Note: as an alternative to quantifiying hypotheses when we import them from set.mm we can also asked that x is bound in G. See ~ 19.20i . (#06) $) 19.20i2 $p # G |- ( A. x ph -> A. x ps ) $= ( a4s a5i ) ABCDABCDEGFH $. $( [?] $) $( [11-May-06] $) $} ${ 19.20ii.1 $e # G |- A. x ( ph -> ( ps -> ch ) ) $. $( Inference quantifying antecedent, nested antecedent, and consequent. (#06) $) 19.20ii $p # G |- ( A. x ph -> ( A. x ps -> A. x ch ) ) $= ( wu wi conr ax-hyp ax-we 19.20i ax-ie ax-ii ) ABEGZCEGDEGHAOIZCDEPOCDHZE GAOJPBQEABQHEGOFKLMLN $. $( [10-Apr-06] $) $( [10-Apr-06] $) $} $( A universal quantifier can be moved from outside to inside the members of a biimplication (#06) $) 19.15 $p # G |- ( A. x ( ph <-> ps ) -> ( A. x ph <-> A. x ps ) ) $= ( wb wu wi cone conr ax-hyp ax-ue biimp ax-voi ax-uqb ax-bg ax-ui 19.20i biimpr impbi ax-ii ax-con ) ABCEZDFZBDFZCDFZEZGHUCUFHUCIZUDUEUGBCDUGBCGDUGB CUGUBDHUCJKZLHUCDDMHUBDNOZPQUGCBDUGCBGDUGBCUHRUIPQSTUA $. $( [10-Apr-06] $) $( [10-Apr-06] $) ${ albii.1 $e # G |- ( ph <-> ps ) $. albii.2 $e # bound x G $. $( Quantification of both sides of a biimplication. (#06) $) albii $p # G |- ( A. x ph <-> A. x ps ) $= ( wb wu setax-gen 19.15 ax-ie ) ABCGZDHBDHCDHGALDEFIABCDJK $. $( [?] $) $( [22-Apr-06] $) $} ${ hbth.1 $e # G |- ph $. hbth.2 $e # bound x G $. $( This inference would be wrong with the normal textbook notion of bondage. But it is true if we use ' ( ph -> A. x ph ) ' as a mean to say that ' x is bound in ph '. (#06) $) hbth $p # G |- ( ph -> A. x ph ) $= ( wu ax-ui a1i ) ABCFBABCDEGH $. $( [10-Apr-06] $) $( [10-Apr-06] $) $} $( ` x ` is not free in ` A. x ph `. In set.mm hba1 is proved. In nat.mm it's a synonym for ax-uqb. (#06) $) hba1 $p # G |- ( A. x ph -> A. x A. x ph ) $= ( ax-uqb ) ABCD $. $( [10-Apr-06] $) $( [10-Apr-06] $) ${ hb.1 $e # G |- ( ph -> A. x ph ) $. hb.2 $e # bound x G $. $( If ` x ` is not free in ` ph ` , it is not free in ` -. ph `. (#06) $) hbne $p # G |- ( -. ph -> A. x -. ph ) $= ( wu wn con3i a4s a5i setax-6 nsyl4 ) ABCFZGZCFBGZCFBANOCANOCABMDHIEJABCK L $. $( [10-Apr-06] $) $( [10-Apr-06] $) ${ hb.4 $e # bound y G $. $( If ` x ` is not free in ` ph ` , it is not free in ` A. y ph ` . (#06) $) hbal $p # G |- ( A. y ph -> A. x A. y ph ) $= ( wu conr ax-hyp wi ax-ui 19.20i ax-we ax-ie setax-7 ax-ii ) ABDHZRCHZA RIZBCHZDHZSTRUBARJARUBKRABUADABUAKDEGLMNOTBDCPOQ $. $( [14-Apr-06] $) $( [14-Apr-06] $) $} $} ${ hbex.1 $e # G |- ( ph -> A. x ph ) $. hbex.2 $e # bound x G $. hbex.3 $e # bound y G $. $( If ` x ` is not free in ` ph ` , it is not free in ` E. y ph `. (#06) $) hbex $p # G |- ( E. y ph -> A. x E. y ph ) $= ( wn wu we conr ax-hyp wi hbne setax-gen 19.20i ax-we ax-ie setax-7 ax-ii df-ex albii 3imtr4 ) ABHZDIZHZUFCIBDJZUGCIAUECAUEUECIZAUEKZUDCIZDIZ UHUIUEUKAUELAUEUKMUEAUDUJDAUDUJMDABCEFNGOPQRUIUDDCSRTFNABDUAZAUGUFCULFUBU C $. $( [14-Apr-06] $) $( [14-Apr-06] $) $} $( A lemme to prove hbim. This lemme show how to import a rule of induction from set.mm. We replace hypotheses by quantified antecedents. This way the theorem can be imported (using ~ ax-con ). We prove back the theorem as a lemme in nat.mm then we use this lemme to prove a theorem where hypotheses are newly added. We add the needed provisos. (#06) $) hbimlem $p # G |- ( A. x ( ph -> A. x ph ) -> ( A. x ( ps -> A. x ps ) -> ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ) ) $= ( wu wi cone conr wn ax-hyp ax-we ax-ue ax-voi hba1 ax-bg hbne pm2.21 ax-ui 19.20i syl setax-1 ja ax-ii ax-con ) ABBDEFZDEZCCDEZFZDEZBCFZUJDEZFZF ZFGUFUMGUFHZUIULUNUIHZBCUKUOBIZUPDEUKUOBDUOUEDUNUFUIGUFJKLUNUIDGUFDDMGUEDNO GUHDNOZPUOUPUJDUOUPUJFDUOBCQUQRSTUOCUGUKUOUHDUOUHDUOUHDUNUIJLUQRLUOCUJDUOCU JFDUOCBUAUQRSTUBUCUCUD $. $( [?] $) $( [30-Apr-06] $) ${ hbim.1 $e # G |- ( ph -> A. x ph ) $. hbim.2 $e # bound x G $. hbim.3 $e # G |- ( ps -> A. x ps ) $. $( If ` x ` is not free in ` ph ` and ` ps ` , it is not free in ` ( ph -> ps ) ` . (#06) $) hbim $p # G |- ( ( ph -> ps ) -> A. x ( ph -> ps ) ) $= ( wu wi ax-ui hbimlem ax-ie ) ACCDHIZDHZBCIZODHIZAMDGFJABBDHIZDHNPIAQDEFJ ABCDKLL $. $( [14-Apr-06] $) $( [14-Apr-06] $) $} ${ althbim.1 $e # G |- A. x ( ph -> A. x ph ) $. althbim.3 $e # G |- A. x ( ps -> A. x ps ) $. $( If ` x ` is not free in ` ph ` and ` ps ` , it is not free in ` ( ph -> ps ) ` . Here is an example of a theorem with a bound x G hypothesis ( see ~hbim ) transformed in a theorem without this hypothesis. (#06) $) althbim $p # G |- ( ( ph -> ps ) -> A. x ( ph -> ps ) ) $= ( wu wi cone hbimlem ax-con ax-ie ) ACCDGHDGZBCHZNDGHZFABBDGHDGZMOHZEAPQH IBCDJKLL $. $} ${ hbor.1 $e # G |- ( ph -> A. x ph ) $. hbor.2 $e # bound x G $. hbor.3 $e # G |- ( ps -> A. x ps ) $. $( If ` x ` is not free in ` ph ` and ` ps ` , it is not free in ` ( ph \/ ps ) ` . (#06) $) hbor $p # G |- ( ( ph \/ ps ) -> A. x ( ph \/ ps ) ) $= ( wn wi wu wo hbne hbim dfor albii 3imtr4 ) ABHZCIZRDJBCKZSDJAQCDABDEFLFG MABCNZASRDTFOP $. $( [?] $) $( [1-May-06] $) $} ${ hban.1 $e # G |- ( ph -> A. x ph ) $. hban.2 $e # bound x G $. hban.3 $e # G |- ( ps -> A. x ps ) $. $( If ` x ` is not free in ` ph ` and ` ps ` , it is not free in ` ( ph /\ ps ) ` . (#06) $) hban $p # G |- ( ( ph /\ ps ) -> A. x ( ph /\ ps ) ) $= ( wn wi wu wa hbne hbim dfan albii 3imtr4 ) ABCHZIZHZSDJBCKZTDJARDABQDEFA CDGFLMFLABCNZATSDUAFOP $. $( [?] $) $( [1-May-06] $) $} ${ hbbi.1 $e # G |- ( ph -> A. x ph ) $. hbbi.2 $e # bound x G $. hbbi.3 $e # G |- ( ps -> A. x ps ) $. $( If ` x ` is not free in ` ph ` and ` ps ` , it is not free in ` ( ph <-> ps ) ` . (#06) $) hbbi $p # G |- ( ( ph <-> ps ) -> A. x ( ph <-> ps ) ) $= ( wi wa wu wb hbim hban bi albii 3imtr4 ) ABCHZCBHZIZSDJBCKZTDJAQRDABCDEF GLFACBDGFELMABCNZATSDUAFOP $. $( [?] $) $( [1-May-06] $) $} $( ` x ` is not free in ` -. A. x ph ` . (#06) $) hbn1 $p # G |- ( -. A. x ph -> A. x -. A. x ph ) $= ( wu wn wi cone ax-uqb ax-voi hbne ax-con ) ABCDZEZMCDFGLCGBCHCIJK $. $( [?] $) $( [16-May-06] $) $( ` x ` is not free in ` E. x ph ` . ??? cf ax-eqb (#06) $) hbe1 $p # G |- ( E. x ph -> A. x E. x ph ) $= ( we wu wi cone wn hbn1 df-ex ax-voi albii 3imtr4 ax-con ) ABCDZOCEZFGBHZCE HZRCEOPGQCIGBCJZGORCSCKLMN $. $( [?] $) $( [16-May-06] $) $( A closed form of hypothesis builder ~ hbne . (#06) $) hbnt $p # G |- ( A. x ( ph -> A. x ph ) -> ( -. ph -> A. x -. ph ) ) $= ( wu wi wn cone conr ax-hyp ax-ue ax-voi ax-uqb ax-bg hbne ax-ii ax-con ) ABBCDEZCDZBFZSCDEZEGRTGRHZBCUAQCGRIJGRCCKGQCLMNOP $. $( [?] $) $( [16-May-06] $) $( If a wff is true, it is true for at least one set. (#06) $) 19.8a $p # G |- ( ph -> E. x ph ) $= ( we conr ax-hyp ax-ei ax-ii ) ABBCDABEBCABFGH $. $( [?] $) $( [5-May-06] $) $( If a wff is universally true, it is true for at least one set. (#06) $) 19.2 $p # G |- ( A. x ph -> E. x ph ) $= ( wu we conr ax-hyp ax-ue ax-ei ax-ii ) ABCDZBCEAKFZBCLBCAKGHIJ $. $( [?] $) $( [5-May-06] $) ${ 19.3r.1 $e # G |- ( ph -> A. x ph ) $. 19.3r.2 $e # bound x G $. $( A wff may be quantified with a variable not free in it. (#06) $) 19.3r $p # G |- ( ph <-> A. x ph ) $= ( wu conr ax-hyp ax-ue ax-ii impbi ) ABBCFZDALBALGBCALHIJK $. $( [?] $) $( [5-May-06] $) $} $( We can swap universal quantifiers. (#06) $) alcom $p # G |- ( A. x A. y ph <-> A. y A. x ph ) $= ( wu setax-7 impbi ) ABDECEBCEDEABCDFABDCFG $. $( [?] $) $( [5-May-06] $) $( How to get the -. symbol out from a universal quantification (or inside an existential one). (#06) $) alnex $p # G |- ( A. x -. ph <-> -. E. x ph ) $= ( wn wu we df-ex bicomi negbii dn bitr2 ) ABDCEZDZDBCFZDLAMNANMABCGHIALJK $. $( [?] $) $( [5-May-06] $) $( Definition of the universal quantifier using the existential quantifier. (#06) $) alex $p # G |- ( A. x ph <-> -. E. x -. ph ) $= ( wu wn we wb cone dn bicomi ax-voi albii alnex bitr ax-con ) ABCDZBEZCFEZG HPQEZCDRHBSCHSBHBIJCKLHQCMNO $. $( [?] $) $( [6-May-06] $) ${ 19.9r.1 $e # G |- ( ph -> A. x ph ) $. 19.9r.2 $e # bound x G $. $( If x is bound in ph, we can add or remove the existential quantifier. (#06) $) 19.9r $p # G |- ( ph <-> E. x ph ) $= ( we 19.8a wn wu alnex hbne sylib a3i impbi ) ABBCFZABCGABOABHZCIOHPABCJA BCDEKLMN $. $( [?] $) $( [17-May-06] $) $} $( A closed version of one direction of ~ 19.9r . Perhaps a way to remove a bondage proviso. ??? (#06) $) 19.9t $p # G |- ( A. x ( ph -> A. x ph ) -> ( E. x ph -> ph ) ) $= ( wu wi we cone conr ax-hyp ax-ue ax-voi ax-uqb ax-bg 19.9r bicomi biimp ax-ii ax-con ) ABBCDEZCDZBCFZBEZEGTUBGTHZUABUCBUAUCBCUCSCGTIJGTCCKGSCLMNOPQ R $. $( [?] $) $( [17-May-06] $) $( 19.9d is not included in this file because it is a ' deduction ' $) $( How to move a negation inside or ouside the scope of a quantifier. (#06) $) exnal $p # G |- ( E. x -. ph <-> -. A. x ph ) $= ( wn we wu dn bicomi alex bitr2 negbii2 ) ABDCEZBCFZDZAMNDZLDAOMAMGHABCIJK $. $( [?] $) $( [18-May-06] $) $( A way to move a universal quantifier from outside to inside an implication. Compare with ~ 19.20 . (#06) $) 19.22 $p # G |- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) ) $= ( wi wu we cone conr wn ax-hyp ax-ue con3i ax-voi ax-uqb ax-bg 19.20i2 df-ex 3imtr4 ax-ii ax-con ) ABCEZDFZBDGZCDGZEZEHUCUFHUCIZBJZDFZJCJZDFZJUDUE UGUKUIUGUJUHDUGBCUGUBDHUCKLMHUCDDNHUBDOPQMUGBDRUGCDRSTUA $. $( [?] $) $( [8-May-06] $) ${ 19.22i.1 $e # bound x G $. 19.22i.2 $e # G |- ( ph -> ps ) $. $( Both antecedent and consequent can be quantified with an exitential quantifier. (#06) $) 19.22i $p # G |- ( E. x ph -> E. x ps ) $= ( wi wu we ax-ui 19.22 ax-ie ) ABCGZDHBDICDIGAMDFEJABCDKL $. $( [?] $) $( [11-May-06] $) $} ${ bi19.22i.1 $e # G |- ( ph <-> ps ) $. bi19.22i.2 $e # bound x G $. $( Both members of a biimplication can be quantified with an exitential quantifier. (#06) $) bi19.22i $p # G |- ( E. x ph <-> E. x ps ) $= ( we biimp 19.22i biimpr impbi ) ABDGCDGABCDFABCEHIACBDFABCEJIK $. $} $( A transformation of quantifiers and logical connectives. (#06) $) alinexa $p # G |- ( A. x ( ph -> -. ps ) <-> -. E. x ( ph /\ ps ) ) $= ( wn wi wu wa we wb cone alex dfan bicomi ax-voi bi19.22i negbii bitr ax-con ) ABCEFZDGZBCHZDIZEZJKUATEZDIZEUDKTDLKUFUCKUEUBDKUBUEKBCMNDOPQRS $. $( [?] $) $( [18-May-06] $) $( A relationship between two quantifiers and negation. (#06) $) alexn $p # G |- ( A. x E. y -. ph <-> -. E. x A. y ph ) $= ( wn we wu wb cone alex ax-voi bi19.22i negbii bicomi bitr ax-con ) ABEDFZC GZBDGZCFZEZHIRQEZCFZEZUAIQCJIUAUDITUCISUBCIBDJCKLMNOP $. $( [?] $) $( [19-May-06] $) $( Existential quantifiers can be swapped. (#06) $) excomim $p # G |- ( E. x E. y ph -> E. y E. x ph ) $= ( we wi cone ax-eqb ax-voi hbex 19.9r 19.8a 19.22i sylibr ax-con ) ABDEZCEZ BCEZDEZFGSSCEQGSCGRCDGBCHCIZDIZJTKGPSCTGBRDUAGBCLMMNO $. $( Existential quantfiers can be swapped. (#06) $) excom $p # G |- ( E. x E. y ph <-> E. y E. x ph ) $= ( we wb cone excomim impbi ax-con ) ABDECEZBCEDEZFGKLGBCDHGBDCHIJ $. $( Swapping existential and universal quantifiers. This theorem holds only for one direction of the implication. The converse is a mistake sometimes made by beginners! But sometimes the converse does hold. Example of a proof where the "obvious" way doesn't work. By obvious way I mean ax-con ax-ii ax-ue ax-ee. (#06) $) 19.12 $p # G |- ( E. x A. y ph -> A. y E. x ph ) $= ( wu we wi cone ax-uqb ax-voi hbex setax-4 19.22i 19.20i2 syl ax-con ) ABDE ZCFZBCFZDEZGHRRDETHQDCHBDIDJZCJZKHRSDHQBCUBHBDLMUANOP $. $( Importation of ~ 19.16 from set.mm as a closed form. (#06) $) 19.16lem $p # G |- ( A. x ( ph -> A. x ph ) -> ( A. x ( ph <-> ps ) -> ( ph <-> A. x ps ) ) ) $= ( wu wi wb cone conr ax-hyp ax-we ax-ue biimp ax-voi ax-uqb ax-bg 19.20i2 syl 19.15 ax-ie setax-4 sylbir impbi int2 ax-con ) ABBDEZFZDEZBCGZDEZBCDEZG ZFFHUHUJULHUHIZUJIZBUKUNBUFUKUNUGDUMUHUJHUHJKLUNBCDUNBCUNUIDUMUJJZLMUMUJDHU HDDNHUGDOPHUIDOPQRUNUFUKBUNUJUFUKGUOUNBCDSTUNBDUAUBUCUDUE $. $( [?] $) $( [29-May-2006] $) ${ 19.16.1 $e # G |- ( ph -> A. x ph ) $. 19.16.2 $e # bound x G $. $( Moving a universal quantifier inside a biimplication when x is bound in one of the wffs. (#06) $) 19.16 $p # G |- ( A. x ( ph <-> ps ) -> ( ph <-> A. x ps ) ) $= ( wu wi wb ax-ui 19.16lem ax-ie ) ABBDGHZDGBCIDGBCDGIHAMDEFJABCDKL $. $} ${ 19.16alt.1 $e # G |- A. x ( ph -> A. x ph ) $. $( An alternative to ~ 19.16 with a universal quantifier quantifying the condition instead of a bondage condition. $) 19.16alt $p # G |- ( A. x ( ph <-> ps ) -> ( ph <-> A. x ps ) ) $= ( wu wi wb 19.16lem ax-ie ) ABBDFGDFBCHDFBCDFHGEABCDIJ $. $} ${ alt19.17.1 $e # G |- ( ps -> A. x ps ) $. alt19.17.2 $e # bound x G $. $( Derived from ~ 19.16 . We can prove first the version of the theorem with a bound x ph hypothesis. Then we prove the closed form. Eventually we prove the version without the bound x ph hypothesis. $) alt19.17 $p # G |- ( A. x ( ph <-> ps ) -> ( A. x ph <-> ps ) ) $= ( wb wu conr ax-hyp ax-ue bicomi cone ax-uqb ax-bg ax-ui wi 19.16 ax-we ax-ie ax-ii ) ABCGZDHZBDHZCGAUCIZCUDUECBGZDHZCUDGZUEUFDUEBCUEUBDAUCJKLAUC DFMUBDNOPAUGUHQUCACBDEFRSTLUA $. $} $( Derived from ~ 19.16 . Closed version. Compare with ~ alt19.17 and ~ 19.17 for two other versions. $) cf19.17 $p # G |- ( A. x ( ps -> A. x ps ) -> ( A. x ( ph <-> ps ) -> ( A. x ph <-> ps ) ) ) $= ( wu wi wb cone conr ax-hyp ax-ue ax-voi ax-uqb ax-bg alt19.17 ax-ii ax-con ) ACCDEFZDEZBCGDEBDECGFZFHSTHSIZBCDUARDHSJKHSDDLHRDMNOPQ $. ${ 19.17.1 $e # G |- A. x ( ps -> A. x ps ) $. $( Derived from ~ 19.16 . (#06) $) 19.17 $p # G |- ( A. x ( ph <-> ps ) -> ( A. x ph <-> ps ) ) $= ( wu wi wb cf19.17 ax-ie ) ACCDFGDFBCHDFBDFCHGEABCDIJ $. $} $( Compare with ~ 19.22 . (#06) $) 19.18 $p # G |- ( A. x ( ph <-> ps ) -> ( E. x ph <-> E. x ps ) ) $= ( wb wu we wi cone conr ax-hyp ax-ue ax-voi ax-uqb ax-bg bi19.22i ax-ii ax-con ) ABCEZDFZBDGCDGEZHITUAITJZBCDUBSDITKLITDDMISDNOPQR $. $( [?] $) $( [5-Jun-2006] $) $( Commutation of conjunction inside an existential quantifier. Compare with ~ ancom . (#06) $) exancom $p # G |- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) ) $= ( wa wb wu we cone ancom ax-voi ax-ui ax-con 19.18 ax-ie ) ABCEZCBEZFZDGZPD HQDHFASIRDIBCJDKLMAPQDNO $. ${ 19.19.1 $e # G |- A. x ( ph -> A. x ph ) $. $( A sort of ~ 19.18 when x is bound in ph. Note: In this proof I used a new trick to remove the bound x G hypothesis. (#06) $) 19.19 $p # G |- ( A. x ( ph <-> ps ) -> ( ph <-> E. x ps ) ) $= ( wu wi wb we cone conr ax-hyp ax-ue ax-we ax-voi ax-uqb ax-bg 19.9r 19.18 ax-ie bitr int2 ax-con ) ABBDFGZDFZBCHZDFZBCDIZHZGZEAUEUJGJUEUGUIJU EKZUGKZBBDIZUHULBDUKUDUGUKUDDJUELMNUKUGDJUEDDOJUDDPQJUFDPQRULUGUMUHHUKUGL ULBCDSTUAUBUCT $. $( [?] $) $( [5-Jun-2006] $) $} ${ 19.21.1 $e # G |- A. x ( ph -> A. x ph ) $. $( A theorem of the ~ 19.20 species. x is bound in the antecedent. (#06) $) 19.21 $p # G |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) ) $= ( wi wu conr ax-ue ax-we ax-hyp 19.20i syl ax-ii cone ax-uqb ax-voi ax-ui ax-con althbim setax-4 imim2i impbi ) ABCFZDGZBCDGZFZAUEUGAUEHZBBDG ZUFABUIFZUEAUJDEIJUHBCDAUEKLMNAUGUGDGUEABUFDEAUFUFDGFZDGOUKDOCDPDQZRSTAUG UDDAUGUDFZDGOUMDOUFCBOCDUAUBULRSLMUC $. $( [?] $) $( [5-Jun-2006] $) $} ${ stdpc5.1 $e # G |- A. x ( ph -> A. x ph ) $. $( A theorem of the ~ 19.20 species. An axiom of standard predicate calculus. (#06) $) stdpc5 $p # G |- ( A. x ( ph -> ps ) -> ( ph -> A. x ps ) ) $= ( wi wu 19.21 biimp ) ABCFDGBCDGFABCDEHI $. $} ${ alt19.21ai.1 $e # G |- A. x ( ph -> A. x ph ) $. alt19.21ai.2 $e # G |- A. x ( ph -> ps ) $. $( An inference of the ~19.20 species. (#06) $) alt19.21ai $p # G |- ( ph -> A. x ps ) $= ( wi wu 19.21 biimp ax-ie ) ABCGDHZBCDHGZFALMABCDEIJK $. $} ${ 19.21ai.1 $e # G |- ( ph -> A. x ph ) $. 19.21ai.2 $e # G |- ( ph -> ps ) $. 19.21ai.3 $e # bound x G $. $( An inference of the ~ 19.20 species. (#06) $) 19.21ai $p # G |- ( ph -> A. x ps ) $= ( wu wi ax-ui alt19.21ai ) ABCDABBDHIDEGJABCIDFGJK $. $} ${ 19.21bi.1 $e # G |- A. x ( ph -> A. x ps ) $. $( A universal quantifier can be removed in the consequence. Compare with ~ ax-ue . (#06) $) 19.21bi $p # G |- ( ph -> ps ) $= ( wu wi ax-ue setax-4 syl ) ABCDFZCABKGDEHACDIJ $. $} ${ 19.23.1 $e # G |- ( ps -> A. x ps ) $. 19.23.2 $e # bound x G $. $( Similar to ~ 19.22 with the additional condition that x is bound in ps. (#06) $) 19.23 $p # G |- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) $= ( wi wu we conr ax-hyp 19.22 ax-ie 19.9t ax-we cone ax-uqb ax-bg mpg syl ax-ii ax-eqb hbim 19.8a imim1i 19.21ai impbi ) ABCGZDHZBDIZCGZAUIUKAUIJZU JCDIZCULUIUJUMGAUIKULBCDLMULCCDHGZUMCGDULCDNAUNUIEOAUIDFPUHDQRSTUAAUKUHDA UJCDABDUBFEUCABUJCABDUDUEFUFUG $. $( [?] $) $( [5-Jun-2006] $) $} ${ 19.23ai.1 $e # G |- ( ps -> A. x ps ) $. 19.23ai.2 $e # G |- ( ph -> ps ) $. 19.23ai.3 $e # bound x G $. $( Adding an existential quantifier to the antecedent. (#06) $) 19.23ai $p # G |- ( E. x ph -> ps ) $= ( wi wu we ax-ui 19.23 biimp ax-ie ) ABCHZDIZBDJCHZAODFGKAPQABCDEGLMN $. $} ${ 19.23bi.1 $e # G |- ( E. x ph -> ps ) $. $( Removal of the existential quantifier in the antecedent. (#06) $) 19.23bi $p # G |- ( ph -> ps ) $= ( we 19.8a syl ) ABBDFCABDGEH $. $} $( The universal quantifier can quantify equivocally a wff-and or each member of the and-wff. (#06) $) 19.26 $p # G |- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ A. x ps ) ) $= ( wa wu wb cone conr ax-hyp ax-ue ax-ale ax-voi ax-uqb ax-bg ax-ui ax-are ax-ai ax-ii ax-we _hypunif hban impbi ax-con ) ABCEZDFZBDFZCDFZEZGHUFUIHUFU IHUFIZUGUHUJBDUJBCUJUEDHUFJKZLHUFDDMZHUEDNOZPUJCDUJBCUKQUMPRSHUIUFHUIIZUEDU NBCHUGUHBHUGIZBUHUOBDHUGJKTUAHUGUHCUOUHICDUOUHJKUARHUIDULHUGUHDHBDNULHCDNUB OPSUCUD $. ${ 19.27.1 $e # G |- ( ps -> A. x ps ) $. 19.27.2 $e # bound x G $. $( Compare with ~ 19.26 . Example of a proof where only natural deduction technics are used. Compare with the set.mm proof to feel how a natural deduction can differ from a hilbert-style proof. (#06) $) 19.27 $p # G |- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ ps ) ) $= ( wa wu conr ax-hyp ax-ue ax-ale cone ax-uqb ax-bg ax-ui ax-are ax-ai ax-ii 19.26 wi ax-we ax-ie mpbir impbi ) ABCGZDHZBDHZCGZAUGUIAUGIZUHCUJBD UJBCUJUFDAUGJKZLAUGDFMUFDNOPUJBCUKQRSAUIUGAUIIZUGUHCDHZGULBCDTULUHUMULUHC AUIJZLULCUMULUHCUNQACUMUAUIEUBUCRUDSUE $. $} ${ 19.28.1 $e # G |- ( ph -> A. x ph ) $. 19.28.2 $e # bound x G $. $( Compare with ~ 19.26 and ~ 19.27 . (#06) $) 19.28 $p # G |- ( A. x ( ph /\ ps ) <-> ( ph /\ A. x ps ) ) $= ( wa wu 19.27 ancom albii bitr2 bitr ) ABCGZDHZCDHZBGZBPGACBGZDHQOACBDEFI ARNDACBJFKLAPBJM $. $( [?] $) $( [5-Jun-2006] $) $} $( A way to move a universal and an existential operator out from a and. ( (#06) $) 19.29 $p # G |- ( ( A. x ph /\ E. x ps ) -> E. x ( ph /\ ps ) ) $= ( wu we wa wi cone wn alex _con3bii dfan bicomi ax-voi bi19.22i bitr alnex imbi2i negbii 19.20 con3i sylbir sylbi sylib ax-con ) ABDEZCDFZGZBCGZDFZHIB CJZHZDEZJZUKUIIUOUMJZDFZUKIUNUQIUMDKLIUPUJDIUJUPIBCMNDOPQIUIUGUHJZHZJZUOIUG UHMIUGULDEZHZJUTUOIVBUSIVAURUGICDRSTIUNVBIBULDUAUBUCUDUEUF $. $( [?] $) $( [13-Jun-2006] $) $( A way to move a universal and an existential operator out from a and. See ~ 19.29 . (#06) $) 19.29r $p # G |- ( ( E. x ph /\ A. x ps ) -> E. x ( ph /\ ps ) ) $= ( we wu wa wi cone ancom ax-voi bi19.22i 19.29 sylibr sylbi ax-con ) ABDEZC DFZGZBCGZDEZHISRQGZUAIQRJIUACBGZDEUBITUCDIBCJDKLICBDMNOP $. $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- The axioms for equality. =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( My first idea was adding the axioms for equality used by Pfenning. But I think now this was not a good idea because most set.mm axioms remained unproved. So I changed my mind, I removed Pfenning's axioms and I simply use set.mm ones. All that changes are for clarity sake. $) $( A sort of transitivity for equality. $) ax-8 $a # G |- ( x = y -> ( x = z -> y = z ) ) $. $( At least one thing exists. $) ax-9 $a # G |- -. A. x -. x = y $. $( If two variables are equal we can quantified a wff by one or by the other. $) ax-10 $a # G |- ( A. x x = y -> ( A. x ph -> A. y ph ) ) $. $( Variable replacement. $) ax-11 $a # G |- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) ) $. $( An equality can be quantified by a variable distinct from its two members. $) ax-12 $a # G |- ( -. A. z z = x -> ( -. A. z z = y -> ( x = y -> A. z x = y ) ) ) $. $( This is a variant of ~ ax-9 . (#06) $) ax9 $p # G |- ( A. x ( x = y -> A. x ph ) -> ph ) $= ( wq wu wi we 19.22 wn df-ex ax-9 mpbir elmthimp syl a6e ) ACDEZBCFZGCFZRCH ZBASQCHZTGTAQRCIAUATAUAQJCFJAQCKACDLMNOABCPO $. $( [?] $) $( [8-May-06] $) $( This theorem is a re-derivation of ~ ax-9 from ~ ax9 . (#06) $) ax9a $p # G |- -. A. x -. x = y $= ( wq wn wu cone wi ax9 setax-6 a3i ax-voi mpg ax-con ) ABCDZEZBFEZGOQBFZHQB GQBCIGROGPBJKBLMN $. $( [?] $) $( [11-May-06] $) $( At least one individual exists. (#06) $) a9e $p # G |- E. x x = y $= ( wq we wn wu df-ex ax-9 mpbir ) ABCDZBEKFBGFAKBHABCIJ $. $( [?] $) $( [6-May-06] $) $( Identity law for equality (reflexivity). (#06) $) equid $p # G |- x = x $= ( ) ? $. $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Substitution =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( Define proper substitution. (#06) $) df-sb $a # G |- ( [ y / x ] ph <-> ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) ) $. ${ sbimi.1 $e # G |- ( ph -> ps ) $. sbimi.2 $e # bound x G $. $( If an implication is true it remains so if we do the same substitution in both sides of the implication (#06). $) sbimi $p # G |- ( [ y / x ] ph -> [ y / x ] ps ) $= ( wq wi wa we ws a1i a2i anim2i 19.22i anim12i df-sb 3imtr4 ) ADEHZBIZTBJ ZDKZJTCIZTCJZDKZJBEDLCEDLAUAUDUCUFATBCABCITFMNAUBUEDGABCTFOPQABDERACDERS $. $( [?] $) $( [6-May-06] $) $} ${ sbbii.1 $e # G |- ( ph <-> ps ) $. sbbii.2 $e # bound x G $. $( If a biimplication is true it remains so if we do the same substitution in both sides of the biimplication (#06). $) sbbii $p # G |- ( [ y / x ] ph <-> [ y / x ] ps ) $= ( ws biimp sbimi biimpr impbi ) ABEDHCEDHABCDEABCFIGJACBDEABCFKGJL $. $( [?] $) $( [15-May-06] $) $} $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- The axioms for a binary non-logical predicate =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( Introduce a binary non-logical predicate symbol. For more explanations about these axioms see set.mm. $) $c e. $. $( Stylized epsilon $) $( 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. After we introduce ~ cv and ~ wcel in set theory, this syntax construction becomes redundant, since it can be derived with the proof "vx cv vy cv wcel". $) wel $a wff x e. y $. $( Axiom of Equality. One of the 3 non-logical predicate axioms of our predicate calculus. $) ax-13 $a # G |- ( x = y -> ( x e. z -> y e. z ) ) $. $( Axiom of Equality. One of the 3 non-logical predicate axioms of our predicate calculus. $) ax-14 $a # G |- ( x = y -> ( z e. x -> z e. y ) ) $. $( Axiom of Quantifier Introduction. One of the 3 non-logical predicate axioms of our predicate calculus. $) ax-15 $a # G |- ( -. A. z z = x -> ( -. A. z z = y -> ( x e. y -> A. z x e. y ) ) ) $. $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= The axioms of distinct variables and quantifier introduction. =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= $) ${ $d x y $. $( Axiom of Distinct Variables. $) ax-16 $a G |- ( A. x x = y -> ( ph -> A. x ph ) ) $. $} ${ $d x ph $. $( Axiom to quantify a variable over a formula in which it does not occur. Certainly the most useful axiom in set.mm. Those who don't like bound variables will like this axiom. $) ax-17 $a G |- ( ph -> A. x ph ) $. $} $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#* Zermelo-Fraenkel Set Theory #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#* $) $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- The axioms of set theory =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( Postulate the Zermelo-Fraenkel axioms plus the Axiom of Choice. For more information see set.mm. $) $v t $. $( Let ' t ' be an individual variable. $) vt $f set t $. ${ $d x y z w v u t $. $( Two sets are equals when they have the same elements. Note: why must x and y be distinct ? $) ax-ext $a # G |- ( A. z ( z e. x <-> z e. y ) -> x = y ) $. $( "Axiom of Replacement. It tells us that that the image of any set under a function is also a set". $) ax-rep $a # G |- ( A. w E. y A. z ( A. y ph -> z = y ) -> E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) ) $. $( "Axiom of Union. It states that the union of any set exists." $) ax-un $a # G |- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y ) $. $( "Axiom of power. It states that the collection of all subsets of a set is also a set". $) ax-pow $a # G |- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) $. $( "Axiom of Regularity. Every non-empty set contains a set disjoint from itself". $) ax-reg $a # G |- ( E. y y e. x -> E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) ) $. $( "Axiom of Infinity. It asserts that given a starting set ` x ` , an infinite set built from it exists". $) ax-inf $a # G |- E. y ( x e. y /\ A. z ( z e. y -> E. w ( z e. w /\ w e. y ) ) ) $. $( "Axiom of Choice. AC (in a common version given in textbooks) asserts that given a family of mutually disjoint nonempty sets, a set exists containing exactly one member from each set in the family". $) ax-ac $a # G |- E. y A. z A. w ( ( z e. w /\ w e. x ) -> E. v A. u ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) ) $. $} $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Class abstraction =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( Declare new constants used in class definition. $) $c { $. $( Left brace $) $c | $. $( Vertical bar $) $c } $. $( Right brace $) $c class $. $( Class variable type $) $v A $. $v B $. $v C $. $v D $. $v R $. $v S $. $v T $. $( A set is a class. But some classes are not sets. The dichotomy of sets and classes are used to avoid Russel's paradox (???). $) cv $a class x $. $( The class builder. $) cab $a class { x | ph } $. $( Let ' A ' be a class variable. $) cA $f class A $. $( Let ' B ' be a class variable. $) cB $f class B $. $( Let ' C ' be a class variable. $) cC $f class C $. $( Let ' D ' be a class variable. $) cD $f class D $. $( Let ' R ' be a class variable. $) cR $f class R $. $( Let ' S ' be a class variable. $) cS $f class S $. $( Let ' T ' be a class variable. $) cT $f class T $. $( Extend wff definition to include class equality. $) wceq $a wff A = B $. $( Extend wff definition to include the membership connective between classes. $) wcel $a wff A e. B $. $( Definition of class. $) df-clab $a # G |- ( x e. { y | ph } <-> [ x / y ] ph ) $. ${ $d x A $. $d x B $. $d x y z $. df-cleq.1 $e # G |- ( A. x ( x e. y <-> x e. z ) -> y = z ) $. $( Define the equality connective between classes. (#06) $) df-cleq $a # G |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $. $} $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Negated equality and membership =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( Declare new connectives. $) $c =/= $. $( Not equal to (equal sign with slash through it). $) $c e/ $. $( Not an element of (epsilon with slash through it). $) $( Extend wff notation to include inequality. $) wne $a wff A =/= B $. $( Extend wff notation to include negated membership. $) wnel $a wff A e/ B $. $( Define inequality. $) df-ne $a # G |- ( A =/= B <-> -. A = B ) $. $( Define negated membership. $) df-nel $a # G |- ( A e/ B <-> -. A e. B ) $. $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Restricted quantification =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- The universal class =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $c V $. $( The universal class is a class. $) cvv $a class V $. $( Definition of the universal class. $) df-v $a # G |- V = { x | x = x } $. $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Proper substitution of classes for sets =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( Extend wff notation to include the proper substitution of a class for a set. $) wsbc $a wff [ A / x ] ph $. $( Define the proper substitution of a class for a set. $) df-sbc $a # G |- ( [ A / x ] ph <-> A e. { x | ph } ) $. $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Define basic set operations and relations =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= $) $( Declare new symbols. $) $c \ $. $( Backslash (difference) $) $c u. $. $( Cup (union) $) $c i^i $. $( Cap (intersection) $) $c (_ $. $( Subclass or subset symbol $) $c (. $. $( Proper subclass or subset symbol $) $( Extend class notation to include class difference (read: " ` A ` minus ` B ` "). $) cdif $a class ( A \ B ) $. $( Extend class notation to include union of two classes (read: " ` A ` union ` B ` "). $) cun $a class ( A u. B ) $. $( Extend class notation to include the intersection of two classes (read: " ` A ` intersect ` B ` "). $) cin $a class ( A i^i B ) $. $( Extend wff notation to include the subclass relation. This is read " ` A ` is a subclass of ` B `". $) wss $a wff A (_ B $. $( Extend wff notation with proper subclass relation. $) wpss $a wff A (. B $. ${ $d x A $. $d x B $. $( Define class difference, also called relative complement. $) df-dif $a # G |- ( A \ B ) = { x | ( x e. A /\ -. x e. B ) } $. $} ${ $d x A $. $d x B $. $( Define the union of two classes. $) df-un $a # G |- ( A u. B ) = { x | ( x e. A \/ x e. B ) } $. $( Define the intersection of two classes. $) df-in $a # G |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) } $. $} $( Define the subclass relationship. $) df-ss $a # G |- ( A (_ B <-> ( A i^i B ) = A ) $. $( Define proper subclass relationship between two classes. $) df-pss $a # G |- ( A (. B <-> ( A (_ B /\ A =/= B ) ) $. $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Subclasses and subsets =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= $) $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Proper substitution of classes for sets into classes =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- The Axiom of Replacement =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Derive the Axiom of Separation =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- The difference, union, and intersection of two classes =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- The empty set; derive the Axiom of the Empty Set =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- "Weak Deduction Theorem" for Set Theory =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Power classes and the Axiom of Power Sets =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( Declare the symbol for power class. $) $c P~ $. $( Calligraphic P $) $( Extend class notation to include power class. $) cpw $a class P~ A $. ${ $d x A $. $( Define power class. $) df-pw $a # G |- P~ A = { x | x (_ A } $. $} $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Unordered and ordered pairs; derive the Axiom of Pairing =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( Declare new symbols needed. $) $c <. $. $( Bracket (the period distinguishes it from 'less than') $) $c >. $. $( Bracket (the period distinguishes it from 'greater than') $) $( Extend class notation to include singleton. $) csn $a class { A } $. $( Extend class notation to include unordered pair. $) cpr $a class { A , B } $. $( Extend class notation to include ordered pair. $) cop $a class <. A , B >. $. ${ $d x A $. $( Define the singleton of a class. $) df-sn $a # G |- { A } = { x | x = A } $. $} $( Define unordered pair of classes. $) df-pr $a # G |- { A , B } = ( { A } u. { B } ) $. $( Extend class notation to include unordered triplet. $) ctp $a class { A , B , C } $. $( Define unordered triple of classes. $) df-tp $a # G |- { A , B , C } = ( { A , B } u. { C } ) $. $( Kuratowski's ordered pair definition. $) df-op $a # G |- <. A , B >. = { { A } , { A , B } } $. $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Power class and union, intersection =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- The union of a class and the Axiom of Union =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- The intersection of a class =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Indexed union and intersection =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Transitive classes =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Binary relations, ordering, and founded relations =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- $) $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# Appendix: Typesetting definitions for the tokens in this file #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# $) $( $t /* Page title, home page link */ htmltitle "Natural deduction theorems within metamath"; htmlhome '<A HREF="nat.html"><FONT SIZE=-2 FACE=sans-serif>' + '<IMG SRC="Gentzen.gif" BORDER=0 ALT=' + '"Home" HEIGHT=32 WIDTH=32 ALIGN=MIDDLE>' + 'Home</FONT></A>'; /* Optional file where bibliographic references are kept */ /* If specified, e.g. "mmset.html", Metamath will hyperlink all strings of the form "[rrr]" (where "rrr" has no whitespace) to "mmset.html#rrr" */ /* A warning will be given if the file "mmset.html" with the bibliographical references is not present. It is read in order to check correctness of the references. */ htmlbibliography "mmnat.html"; /* Variable color key at the bottom of each proof table */ htmlvarcolor '<FONT COLOR="#0000FF">wff</FONT> ' + '<FONT COLOR="#FF0000">set</FONT> ' + '<FONT COLOR="#CC33CC">class</FONT>'; /* GIF and Unicode HTML directories - these are used for the GIF version to crosslink to the Unicode version and vice-versa */ htmldir "../mpegif/"; althtmldir "../mpeuni/"; /* Symbol definitions */ htmldef "#" as "<IMG SRC='_diese.gif' WIDTH=10 HEIGHT=19 ALT='#' ALIGN=TOP> "; htmldef "bound" as "<IMG SRC='_bound.gif' WIDTH=38 HEIGHT=19 ALT='bound' ALIGN=TOP> "; htmldef "set" as "<IMG SRC='_set.gif' WIDTH=20 HEIGHT=19 ALT='set' ALIGN=TOP> "; htmldef "con" as '<FONT COLOR="#808080">con </FONT>'; htmldef "wff" as "<IMG SRC='_wff.gif' WIDTH=24 HEIGHT=19 ALT='wff' ALIGN=TOP> "; htmldef "class" as "<IMG SRC='_class.gif' WIDTH=32 HEIGHT=19 ALT='class' ALIGN=TOP> "; htmldef "G" as "<IMG SRC='_cg.gif' WIDTH=12 HEIGHT=19 ALT='G' ALIGN=TOP>"; htmldef "[]" as '[] '; htmldef "|-" as "<IMG SRC='_vdash.gif' WIDTH=12 HEIGHT=19 ALT='|-' ALIGN=TOP> "; htmldef "," as "<IMG SRC='comma.gif' WIDTH=4 HEIGHT=19 ALT=',' ALIGN=TOP> "; htmldef "(" as "<IMG SRC='lp.gif' WIDTH=5 HEIGHT=19 ALT='(' ALIGN=TOP>"; htmldef ")" as "<IMG SRC='rp.gif' WIDTH=5 HEIGHT=19 ALT=')' ALIGN=TOP>"; htmldef "->" as " <IMG SRC='to.gif' WIDTH=15 HEIGHT=19 ALT='->' ALIGN=TOP> "; htmldef "Abs" as "<IMG SRC='_abs.gif' WIDTH=24 HEIGHT=19 ALT='Abs' ALIGN=TOP> "; htmldef "-." as "<IMG SRC='lnot.gif' WIDTH=10 HEIGHT=19 ALT='-.' ALIGN=TOP> "; htmldef "<->" as " <IMG SRC='leftrightarrow.gif' WIDTH=15 HEIGHT=19 " + "ALT='<->' ALIGN=TOP> "; htmldef "\/" as " <IMG SRC='vee.gif' WIDTH=11 HEIGHT=19 ALT='\/' ALIGN=TOP> "; htmldef "/\" as " <IMG SRC='wedge.gif' WIDTH=11 HEIGHT=19 ALT='/\' ALIGN=TOP> "; htmldef "A." as "<IMG SRC='forall.gif' WIDTH=10 HEIGHT=19 ALT='A.' ALIGN=TOP>"; htmldef "E." as "<IMG SRC='exists.gif' WIDTH=9 HEIGHT=19 ALT='E.' ALIGN=TOP>"; htmldef "e." as " <IMG SRC='in.gif' WIDTH=10 HEIGHT=19 ALT='e.' ALIGN=TOP> "; htmldef "=" as " <IMG SRC='eq.gif' WIDTH=12 HEIGHT=19 ALT='=' ALIGN=TOP> "; htmldef "[" as "<IMG SRC='lbrack.gif' WIDTH=5 HEIGHT=19 ALT='[' ALIGN=TOP>"; htmldef "/" as " <IMG SRC='solidus.gif' WIDTH=6 HEIGHT=19 ALT='/' ALIGN=TOP> "; htmldef "]" as "<IMG SRC='rbrack.gif' WIDTH=5 HEIGHT=19 ALT=']' ALIGN=TOP>"; htmldef "{" as "<IMG SRC='lbrace.gif' WIDTH=6 HEIGHT=19 ALT='{' ALIGN=TOP>"; htmldef "|" as " <IMG SRC='vert.gif' WIDTH=3 HEIGHT=19 ALT='|' ALIGN=TOP> "; htmldef "}" as "<IMG SRC='rbrace.gif' WIDTH=6 HEIGHT=19 ALT='}' ALIGN=TOP>"; htmldef "Truth" as "<IMG SRC='_truth.gif' WIDTH=29 HEIGHT=19 ALT='Abs' ALIGN=TOP> "; htmldef "LSTYP" as "<IMG SRC='_lstyp.gif' WIDTH=29 HEIGHT=19 ALT='lstyp' ALIGN=TOP> "; htmldef "ph" as "<IMG SRC='_varphi.gif' WIDTH=11 HEIGHT=19 ALT='ph' ALIGN=TOP>"; htmldef "ps" as "<IMG SRC='_psi.gif' WIDTH=12 HEIGHT=19 ALT='ps' ALIGN=TOP>"; htmldef "ch" as "<IMG SRC='_chi.gif' WIDTH=12 HEIGHT=19 ALT='ch' ALIGN=TOP>"; htmldef "th" as "<IMG SRC='_theta.gif' WIDTH=8 HEIGHT=19 ALT='th' ALIGN=TOP>"; htmldef "ta" as "<IMG SRC='_tau.gif' WIDTH=10 HEIGHT=19 ALT='ta' ALIGN=TOP> "; htmldef "t" as "<IMG SRC='_t.gif' WIDTH=9 HEIGHT=19 ALT='t' ALIGN=TOP>"; htmldef "u" as "<IMG SRC='_u.gif' WIDTH=9 HEIGHT=19 ALT='u' ALIGN=TOP>"; htmldef "v" as "<IMG SRC='_v.gif' WIDTH=9 HEIGHT=19 ALT='v' ALIGN=TOP>"; htmldef "w" as "<IMG SRC='_w.gif' WIDTH=12 HEIGHT=19 ALT='w' ALIGN=TOP>"; htmldef "x" as "<IMG SRC='_x.gif' WIDTH=10 HEIGHT=19 ALT='x' ALIGN=TOP>"; htmldef "y" as "<IMG SRC='_y.gif' WIDTH=9 HEIGHT=19 ALT='y' ALIGN=TOP>"; htmldef "z" as "<IMG SRC='_z.gif' WIDTH=9 HEIGHT=19 ALT='z' ALIGN=TOP>"; htmldef "A" as "<IMG SRC='_ca.gif' WIDTH=11 HEIGHT=19 ALT='A' ALIGN=TOP>"; htmldef "B" as "<IMG SRC='_cb.gif' WIDTH=12 HEIGHT=19 ALT='B' ALIGN=TOP>"; htmldef "C" as "<IMG SRC='_cc.gif' WIDTH=12 HEIGHT=19 ALT='C' ALIGN=TOP>"; htmldef "D" as "<IMG SRC='_cd.gif' WIDTH=12 HEIGHT=19 ALT='D' ALIGN=TOP>"; htmldef "R" as "<IMG SRC='_cr.gif' WIDTH=12 HEIGHT=19 ALT='R' ALIGN=TOP>"; htmldef "S" as "<IMG SRC='_cs.gif' WIDTH=11 HEIGHT=19 ALT='S' ALIGN=TOP>"; htmldef "T" as "<IMG SRC='_ct.gif' WIDTH=12 HEIGHT=19 ALT='T' ALIGN=TOP>"; htmldef "=/=" as " <IMG SRC='ne.gif' WIDTH=12 HEIGHT=19 ALT='=/=' ALIGN=TOP> "; htmldef "e/" as " <IMG SRC='notin.gif' WIDTH=10 HEIGHT=19 ALT='e/' ALIGN=TOP> "; htmldef "V" as "<IMG SRC='cv.gif' WIDTH=12 HEIGHT=19 ALT='V' ALIGN=TOP>"; htmldef "\" as " <IMG SRC='setminus.gif' WIDTH=8 HEIGHT=19 ALT='\' ALIGN=TOP> "; htmldef "u." as " <IMG SRC='cup.gif' WIDTH=10 HEIGHT=19 ALT='u.' ALIGN=TOP> "; htmldef "i^i" as " <IMG SRC='cap.gif' WIDTH=10 HEIGHT=19 ALT='i^i' ALIGN=TOP> "; htmldef "(_" as " <IMG SRC='subseteq.gif' WIDTH=12 HEIGHT=19 ALT='(_' ALIGN=TOP> "; htmldef "(." as " <IMG SRC='subset.gif' WIDTH=12 HEIGHT=19 ALT='(.' ALIGN=TOP> "; htmldef "P~" as "<IMG SRC='scrp.gif' WIDTH=16 HEIGHT=19 ALT='P~' ALIGN=TOP>"; htmldef "<." as "<IMG SRC='langle.gif' WIDTH=4 HEIGHT=19 ALT='<.' ALIGN=TOP>"; htmldef ">." as "<IMG SRC='rangle.gif' WIDTH=4 HEIGHT=19 ALT='>.' ALIGN=TOP>"; /* These are alternate HTML definitions for the Unicode font version of the web site */ althtmldef "#" as "# "; althtmldef "bound" as 'bound '; althtmldef "Abs" as "Abs "; althtmldef "con" as "con "; althtmldef "G" as "G "; althtmldef "," as ", "; althtmldef "(" as "( "; althtmldef ")" as ") "; althtmldef "->" as ' -> '; althtmldef "-." as '-. '; althtmldef "wff" as '<FONT COLOR="#808080">wff </FONT> '; althtmldef "|-" as '<FONT COLOR="#808080">|- </FONT> '; althtmldef "ph" as ' <FONT COLOR="#0000FF"><I>ph</I></FONT> '; althtmldef "ps" as '<FONT COLOR="#0000FF"><I>ps</I></FONT> '; althtmldef "ch" as '<FONT COLOR="#0000FF"><I>ch</I></FONT> '; althtmldef "th" as '<FONT COLOR="#0000FF"><I>th</I></FONT> '; althtmldef "ta" as '<FONT COLOR="#0000FF"><I>ta</I></FONT> '; althtmldef "<->" as ' ↔ '; althtmldef "\/" as ' ⋁ ' ; /* was ∨ */ althtmldef "/\" as ' ⋀ '; /* was ∧ which is circle in WinXP Pro */ althtmldef "A." as 'A. '; althtmldef "set" as '<FONT COLOR="#808080">set </FONT> '; althtmldef "x" as ' <I><FONT COLOR="#FF0000">x </FONT></I> '; althtmldef "y" as ' <I><FONT COLOR="#FF0000">y </FONT></I> '; althtmldef "z" as '<I><FONT COLOR="#FF0000">z </FONT></I> '; althtmldef "w" as '<I><FONT COLOR="#FF0000">w </FONT></I> '; althtmldef "v" as '<I><FONT COLOR="#FF0000">v </FONT></I> '; althtmldef "E." as 'E. '; althtmldef "=" as ' = '; althtmldef "[" as ' [ '; althtmldef "/" as ' / '; althtmldef "]" as ' ] '; althtmldef "u" as '<I><FONT COLOR="#FF0000">u </FONT></I> '; althtmldef "[]" as '[] '; althtmldef "A" as 'A '; althtmldef "B" as 'B '; althtmldef "C" as 'C '; althtmldef "D" as 'D '; althtmldef "R" as 'R '; althtmldef "S" as 'S '; althtmldef "T" as 'T '; althtmldef "e." as 'e. '; althtmldef "t" as 't '; althtmldef "{" as '{ '; althtmldef "|" as '| '; althtmldef "}" as '} '; althtmldef "Truth" as 'Truth '; althtmldef "LSTYP" as 'LSTYP '; althtmldef "lstyp" as 'lstyp '; althtmldef "class" as 'class '; althtmldef "=/=" as ' ≠ '; althtmldef "e/" as ' ∉ '; althtmldef "V" as '<I>V</I>'; althtmldef "(_" as ' ⊆ '; /* ⫅ */ althtmldef "(." as ' ⊂ '; althtmldef "\" as ' ∖ '; /* ∖ */ althtmldef "u." as ' ∪ '; althtmldef "i^i" as ' ∩ '; althtmldef "P~" as '℘'; althtmldef "<." as '〈'; althtmldef ">." as '〉'; /* These are definitions for latex */ latexdef "#" as "#"; latexdef "," as ","; latexdef "[]" as "[]"; latexdef "|-" as "\vdash"; latexdef "[" as "["; latexdef "]" as "]"; latexdef "(" as "("; latexdef ")" as ")"; latexdef "->" as "\rightarrow"; latexdef "<->" as "\leftrightarrow"; latexdef "-." as "\lnot"; latexdef "\/" as "\vee"; latexdef "/\" as "\wedge"; latexdef "Abs" as "\bot"; latexdef "con" as "{\rm con}"; latexdef "wff" as "{\rm wff}"; latexdef "G" as "G"; latexdef "ph" as "\varphi"; latexdef "ps" as "\psi"; latexdef "ch" as "\chi"; latexdef "th" as "\theta"; latexdef "ta" as "\tau"; latexdef "LSTYP" as "{\rm LSTYP}"; latexdef "lstyp" as "{\rm lstyp}"; latexdef "Truth" as "\bot"; latexdef "/" as "/"; latexdef "=" as "\="; latexdef "set" as "{\rm set}"; latexdef "A." as "\forall"; latexdef "E." as "\exists"; latexdef "e." as "\in"; latexdef "x" as "x"; latexdef "y" as "y"; latexdef "z" as "z"; latexdef "w" as "w"; latexdef "v" as "v"; latexdef "u" as "u"; latexdef "t" as "t"; latexdef "{" as "\{"; latexdef "|" as "|"; latexdef "}" as "\}"; latexdef "class" as "{\rm class}"; latexdef "A" as "A"; latexdef "B" as "B"; latexdef "C" as "C"; latexdef "D" as "D"; latexdef "R" as "R"; latexdef "S" as "S"; latexdef "T" as "T"; latexdef "bound" as "bound"; latexdef "=/=" as "\ne"; latexdef "e/" as "\notin"; latexdef "V" as "V"; latexdef "G" as "G"; latexdef "(_" as "\subseteq"; latexdef "(." as "\subset"; latexdef "\" as "\setminus"; latexdef "u." as "\cup"; latexdef "i^i" as "\cap"; latexdef "P~" as "{\cal P}"; latexdef "<." as "\langle"; latexdef ">." as "\rangle"; /* End of typesetting definition section */ $)
Predicate axioms have no substitution operator any longer. I think the system fully works now. Several propositional and pure predicate theorems have been added. Set theory axioms have been added as well. All the code mandatory to generate html pages has been added. I have gif images (you can ask me them). Last but not least I have begun to fix the mistakes in the commentaries.
In the future however I think I will replace set theory by another theory (like peano arithmetic) because it is a bit stupid to try to add all set.mm set theory theorems. However I intend to add all the propositional and predicate theorems in set.mm ( at least those of 1993 ). This way it will be able to do interesting things with nat.mm.
Another thing that can be tried would be to implement intuitionistic logic in nat.mm ( few modifications to do, at least for the logic axioms [ but certainly many problems with the definitions in set theory ] ). This way we could have a full intuitionistic system. But I guess it's too difficult for me.
– 28-Jul-2006 frl