# Adapted mechanically from set.mm # todo: proper attribution ## redirect prop.gh kind (wff) tvar (wff ph) tvar (wff ps) tvar (wff ch) tvar (wff th) tvar (wff ta) # (_Note_: This theorem will never appear in a completed proof and can be # ignored if you are using this database to learn logic - please start # with the next statement, [[wn]].) # # This is a technical theorem to assist proof development. It provides a # temporary way to add an independent subproof to a proof under # development, for later assignment to a normal proof step. # # The Metamath program's Proof Assistant requires proofs to be developed # backwards from the conclusion with no gaps, and it has no mechanism that # lets the user to work on isolated subproofs. This theorem provides a # workaround for this limitation. It can be inserted at any point in a # proof to allow an independent subproof to be developed on the side, for # later use as part of the final proof. # # //Instructions//: (1) Assign this theorem to any unknown step in the # proof. Typically, the last unknown step is the most convenient, since # 'assign last' can be used. This step will be replicated in hypothesis # dummylink.1, from where the development of the main proof can continue. # (2) Develop the independent subproof backwards from hypothesis # dummylink.2. If desired, use a 'let' command to pre-assign the # conclusion of the independent subproof to dummylink.2. (3) After the # independent subproof is complete, use 'improve all' to assign it # automatically to an unknown step in the main proof that matches it. # (4) After the entire proof is complete, use # 'minimize */n/b/e 3syl,we?,wsb' to clean up (discard) all dummylink # references automatically. # # This theorem was originally designed to assist importing partially # completed Proof Worksheets from Mel O'Cat's mmj2 Proof Assistant GUI, # but it can also be useful on its own. Interestingly, this "theorem" - # or more precisely, inference - requires no axioms for its proof. stmt (dummylink () (ph ps) ph) term (wff (-. ph)) term (wff (-> ph ps)) ## First Axiom: Simplification ## ## One of the three axioms of propositional calculus. ## This axiom is called "the principle of simplification" in Principia Mathematica ## because "it enables us to pass from the joint assertion of φ and ψ to the assertion ## of φ simply." ## ## Propositional calculus can be thought of as asserting formulas ## that are universally "true" when their variables are replaced by any combination of ## "true" and "false." Propositional calculus was first formalized by ## Frege in 1879 and simplified by ## Lukasiewicz around 1930. ## ## ## (-> ph (-> ps ph)) ##
## stmt (ax-1 () () (-> ph (-> ps ph))) ## Second Logic Axiom: Frege ## ## Axiom Frege. One of the three axioms of propositional calculus. ## It distributes an antecedent over two consequents. This axiom was part of ## Frege's original ## system and is known as Frege in the literature. The other direction of this ## axiom also turns out to be true, as demonstrated by ## pm5.41. ## ## ## (-> (-> ph (-> ps ch)) (-> (-> ph ps) (-> ph ch))) ##
## stmt (ax-2 () () (-> (-> ph (-> ps ch)) (-> (-> ph ps) (-> ph ch)))) ## Third Logic Axiom: Contraposition ## ## One of the three axioms of propositional calculus. ## It swaps or "transposes" the order of the consequents when negation is removed. ## An informal example is that the statement "if there are no clouds in the sky, ## it is not raining" implies the statement "if it is raining, there are clouds in ## the sky." This axiom is called Transp or "the principle of transposition" in ## Principia Mathematica. We will also use the term "contraposition" for this ## principle, although note that in the field of philosophical logic, "contraposition" ## has a different technical meaning. ## ## ## (-> (-> (-. ph) (-. ps)) (-> ps ph)) ##
## stmt (ax-3 () () (-> (-> (-. ph) (-. ps)) (-> ps ph))) ## Modus Ponens Axiom ## ## Rule of Modus Ponens. The postulated inference rule of ## propositional calculus. The rule says, "if φ ## is true, and φ implies ψ, then ψ must also be true." This rule is sometimes ## called "detachment," since it detaches the minor premise from the major premise. ## ## ## ph ] ] ## (-> ph ] [ ps) ## [ [ ps ##
## stmt (ax-mp () (ph (-> ph ps)) ps) # Inference derived from axiom [[ax-1]]. See [[a1d]] for an explanation of # our informal use of the terms "inference" and "deduction." See also # the comment in [[syld]]. ## Axiom 1 Inference ## ## [ ph ## (-> ps [ ph) ##
stmt (a1i () (ph) (-> ps ph)) # Inference derived from axiom [[ax-2]]. ## Second Axiom Inference ## ## (-> ph ] (-> [ ps ] [ ch)) ## (-> (-> ph ] [ ps ] ) (-> ph [ ch)) ##
stmt (a2i () ((-> ph (-> ps ch))) (-> (-> ph ps) (-> ph ch))) # An inference version of the transitive laws for implication [[imim2]] and # [[imim1]], which Russell and Whitehead call "the principle of the # syllogism...because...the syllogism in Barbara is derived from them" # (quote after Theorem *2.06 of [bib/WhiteheadRussell] p. 101). Some authors # call this law a "hypothetical syllogism." # # (A bit of trivia: this is the most commonly referenced assertion in our # database. In second place is [[ax-mp]], followed by [[visset]], [[bitri]], # [[imp]], and [[ex]]. The Metamath program command 'show usage' shows the # number of references.) ## Syllogism ## ## (-> ph [ ps ] ] ] ) ## [ (-> ps ] [ ch ] ) ## (-> ph [ [ [ ch ] ) ##
stmt (syl () ((-> ph ps) (-> ps ch)) (-> ph ch)) # Inference that swaps (commutes) antecedents in an implication. ## Commute First and Second Antecedents ## ## (-> ph (-> ps ch)) ## (-> ps (-> ph ch)) ##
stmt (com12 () ((-> ph (-> ps ch))) (-> ps (-> ph ch))) # Deduction introducing an embedded antecedent. (The proof was revised by # Stefan Allan, 20-Mar-2006.) # # //Naming convention//: We often call a theorem a "deduction" and suffix # its label with "d" whenever the hypotheses and conclusion are each # prefixed with the same antecedent. This allows us to use the theorem in # places where (in traditional textbook formalizations) the standard # Deduction Theorem would be used; here #ph# would be replaced with a # conjunction ([[df-an]]) of the hypotheses of the would-be deduction. By # contrast, we tend to call the simpler version with no common antecedent # an "inference" and suffix its label with "i"; compare theorem [[a1i]]. # Finally, a "theorem" would be the form with no hypotheses; in this case # the "theorem" form would be the original axiom [[ax-1]]. We usually show # the theorem form without a suffix on its label (e.g. [[pm2.43]] vs. # [[pm2.43i]] vs. [[pm2.43d]]). When an inference is converted to a theorem # by eliminating an "is a set" hypothesis, we sometimes suffix the theorem # form with "g" (for "more general") as in [[uniex]] vs. [[uniexg]]. ## First Axiom Deduction ## ## [ ph ## (-> ps [ ph) ##
stmt (a1d () ((-> ph ps)) (-> ph (-> ch ps))) # Deduction distributing an embedded antecedent. ## Second Axiom Deduction ## ## (-> ph (-> ps ] (-> [ ch ] [ th))) ## (-> ph (-> (-> ps ] [ ch ] ) (-> ps [ th))) ##
stmt (a2d () ((-> ph (-> ps (-> ch th)))) (-> ph (-> (-> ps ch) (-> ps th)))) # A closed form of syllogism (see [[syl]]). Theorem *2.05 of # [bib/WhiteheadRussell] p. 100. ## Syllogism (Closed Form) stmt (imim2 () () (-> (-> ph ps) (-> (-> ch ph) (-> ch ps)))) # A closed form of syllogism (see [[syl]]). Theorem *2.06 of # [bib/WhiteheadRussell] p. 100. ## Syllogism (Closed Form) stmt (imim1 () () (-> (-> ph ps) (-> (-> ps ch) (-> ph ch)))) # Inference adding common consequents in an implication, thereby # interchanging the original antecedent and consequent. ## Syllogism stmt (imim1i () ((-> ph ps)) (-> (-> ps ch) (-> ph ch))) # Inference adding common antecedents in an implication. ## Syllogism ## ## (-> [ ph ] [ ps) ## (-> (-> ch [ ph ] ) (-> ch [ ps)) ##
stmt (imim2i () ((-> ph ps)) (-> (-> ch ph) (-> ch ps))) ## Inference joining two implications (Bridge) stmt (imim12i () ((-> ph ps) (-> ch th)) (-> (-> ps ch) (-> ph th))) ## Inference adding three nested antecedents stmt (imim3i () ((-> ph (-> ps ch))) (-> (-> th ph) (-> (-> th ps) (-> th ch)))) ## Inference chaining two syllogisms stmt (3syl () ((-> ph ps) (-> ps ch) (-> ch th)) (-> ph th)) ## A syllogism rule of inference ## ## The second premise is used to replace the second antecedent of the first premise. ## stmt (syl5 () ((-> ph (-> ps ch)) (-> th ps)) (-> ph (-> th ch))) ## A syllogism rule of inference ## ## The second premise is used to replace the consequent of the first premise. ## stmt (syl6 () ((-> ph (-> ps ch)) (-> ch th)) (-> ph (-> ps th))) ## A syllogism rule of inference ## ## The second premise is used to replace the third antecedent of the first premise. ## stmt (syl7 () ((-> ph (-> ps (-> ch th))) (-> ta ch)) (-> ph (-> ps (-> ta th)))) ## A syllogism rule of inference ## ## The second premise is used to replace the consequent of the first premise. ## stmt (syl8 () ((-> ph (-> ps (-> ch th))) (-> th ta)) (-> ph (-> ps (-> ch ta)))) ## Deduction adding nested antecedents stmt (imim2d () ((-> ph (-> ps ch))) (-> ph (-> (-> th ps) (-> th ch)))) ## Modus Ponens Deduction ## ## (-> ph [ ps ] ] ) ## (-> ph (-> [ ps ] [ ch)) ## (-> ph [ [ [ ch) ##
stmt (mpd () ((-> ph ps) (-> ph (-> ps ch))) (-> ph ch)) ## Syllogism deduction # (The proof was shortened by O'Cat, 19-Feb-2008.) stmt (syld () ((-> ph (-> ps ch)) (-> ph (-> ch th))) (-> ph (-> ps th))) ## Deduction adding nested consequents stmt (imim1d () ((-> ph (-> ps ch))) (-> ph (-> (-> ch th) (-> ps th)))) ## Deduction combining antecedents and consequents stmt (imim12d () ((-> ph (-> ps ch)) (-> ph (-> th ta))) (-> ph (-> (-> ch th) (-> ps ta)))) # Swap antecedents. Theorem *2.04 of [bib/WhiteheadRussell] p. 100. ## Commute First and Second Antecedents stmt (pm2.04 () () (-> (-> ph (-> ps ch)) (-> ps (-> ph ch)))) # Theorem *2.83 of [bib/WhiteheadRussell] p. 108. stmt (pm2.83 () () (-> (-> ph (-> ps ch)) (-> (-> ph (-> ch th)) (-> ph (-> ps th))))) ## Commute Second and Third Antecedents ## ## (-> ph (-> ps (-> ch th))) ## (-> ph (-> ch (-> ps th))) ##
stmt (com23 () ((-> ph (-> ps (-> ch th)))) (-> ph (-> ch (-> ps th)))) ## Commute First and Third Antecedents stmt (com13 () ((-> ph (-> ps (-> ch th)))) (-> ch (-> ps (-> ph th)))) ## Commute Antecedents (Rotate Left) stmt (com3l () ((-> ph (-> ps (-> ch th)))) (-> ps (-> ch (-> ph th)))) ## Commute Antecedents (Rotate Right) stmt (com3r () ((-> ph (-> ps (-> ch th)))) (-> ch (-> ph (-> ps th)))) ## Commute Third and Fourth Antecedents stmt (com34 () ((-> ph (-> ps (-> ch (-> th ta))))) (-> ph (-> ps (-> th (-> ch ta))))) ## Commute Second and Fourth Antecedents stmt (com24 () ((-> ph (-> ps (-> ch (-> th ta))))) (-> ph (-> th (-> ch (-> ps ta))))) ## Commute First and Fourth Antecedents stmt (com14 () ((-> ph (-> ps (-> ch (-> th ta))))) (-> th (-> ps (-> ch (-> ph ta))))) ## Commute Antecedents (Rotate Left) stmt (com4l () ((-> ph (-> ps (-> ch (-> th ta))))) (-> ps (-> ch (-> th (-> ph ta))))) ## Commute Antecedents (Rotate Twice) stmt (com4t () ((-> ph (-> ps (-> ch (-> th ta))))) (-> ch (-> th (-> ph (-> ps ta))))) ## Commute Antecedents (Rotate Right) stmt (com4r () ((-> ph (-> ps (-> ch (-> th ta))))) (-> th (-> ph (-> ps (-> ch ta))))) ## Introducing an embedded antecedent stmt (a1dd () ((-> ph (-> ps ch))) (-> ph (-> ps (-> th ch)))) ## Double Modus Ponens stmt (mp2 () (ph ps (-> ph (-> ps ch))) ch) # (The proof was shortened by Stefan Allan, 20-Mar-2006.) ## Modus Ponens Inference stmt (mpi () (ps (-> ph (-> ps ch))) (-> ph ch)) ## Modus Ponens Inference stmt (mpii () (ch (-> ph (-> ps (-> ch th)))) (-> ph (-> ps th))) ## Modus Ponens Deduction stmt (mpdd () ((-> ph (-> ps ch)) (-> ph (-> ps (-> ch th)))) (-> ph (-> ps th))) ## Modus Ponens Deduction stmt (mpid () ((-> ph ch) (-> ph (-> ps (-> ch th)))) (-> ph (-> ps th))) ## Modus Ponens Deduction stmt (mpdi () ((-> ps ch) (-> ph (-> ps (-> ch th)))) (-> ph (-> ps th))) ## Modus Ponens & Commute Antecedents stmt (mpcom () ((-> ps ph) (-> ph (-> ps ch))) (-> ps ch)) ## Syllogism deduction stmt (syldd () ((-> ph (-> ps (-> ch th))) (-> ph (-> ps (-> th ta)))) (-> ph (-> ps (-> ch ta)))) ## Syllogism & Commute Antecedents stmt (sylcom () ((-> ph (-> ps ch)) (-> ps (-> ch th))) (-> ph (-> ps th))) ## Syllogism & Commute Antecedents stmt (syl5com () ((-> ph (-> ps ch)) (-> th ps)) (-> th (-> ph ch))) ## Syllogism & Commute Antecedents stmt (syl6com () ((-> ph (-> ps ch)) (-> ch th)) (-> ps (-> ph th))) ## Syllogism ## Syllogism inference with common nested antecedent. stmt (syli () ((-> ps (-> ph ch)) (-> ch (-> ph th))) (-> ps (-> ph th))) ## Syllogism Deduction stmt (syl5d () ((-> ph (-> ps (-> ch th))) (-> ph (-> ta ch))) (-> ph (-> ps (-> ta th)))) ## Syllogism Deduction stmt (syl6d () ((-> ph (-> ps (-> ch th))) (-> ph (-> th ta))) (-> ph (-> ps (-> ch ta)))) ## Syllogism Deduction stmt (syl9 () ((-> ph (-> ps ch)) (-> th (-> ch ta))) (-> ph (-> th (-> ps ta)))) ## Syllogism Deduction stmt (syl9r () ((-> ph (-> ps ch)) (-> th (-> ch ta))) (-> th (-> ph (-> ps ta)))) ## Identity ## ## (-> ph ph) ##
stmt (id () () (-> ph ph)) # Principle of identity. Theorem *2.08 of [bib/WhiteheadRussell] p. 101. This # version is proved directly from the axioms for demonstration purposes. # This proof is a popular example in the literature and is identical, # step for step, to the proofs of Theorem 1 of [bib/Margaris] p. 51, # Example 2.7(a) of [bib/Hamilton] p. 31, Lemma 10.3 of [bib/BellMachover] p. 36, # and Lemma 1.8 of [bib/Mendelson] p. 36. It is also # "Our first proof" in Hirst and Hirst's //A Primer for Logic and Proof// # p. 16 (PDF p. 22) at # [[http://www.mathsci.appstate.edu/~jlh/primer/hirst.pdf]]. # For a shorter version of the proof that takes advantage of previously # proved theorems, see [[id]]. ## Identity ## ## (-> ph ph) ##
stmt (id1 () () (-> ph ph)) ## Identity stmt (idd () () (-> ph (-> ps ps))) ## Modus Ponens stmt (pm2.27 () () (-> ph (-> (-> ph ps) ps))) ## Absorb redundant antecedent stmt (pm2.43 () () (-> (-> ph (-> ph ps)) (-> ph ps))) ## Absorb redundant antecedent ## ## (-> ph [ (-> ph ps)) ## [ (-> ph ps) ##
stmt (pm2.43i () ((-> ph (-> ph ps))) (-> ph ps)) ## Absorb redundant antecedent ## ## (-> ph [ (-> ps [ (-> ps ch))) ## (-> ph [ [ (-> ps ch)) ##
stmt (pm2.43d () ((-> ph (-> ps (-> ps ch)))) (-> ph (-> ps ch))) ## Absorb redundant antecedent stmt (pm2.43a () ((-> ps (-> ph (-> ps ch)))) (-> ps (-> ph ch))) ## Absorb redundant antecedent stmt (pm2.43b () ((-> ps (-> ph (-> ps ch)))) (-> ph (-> ps ch))) ## Syllogism & Contraction stmt (sylc () ((-> ph (-> ps ch)) (-> th ph) (-> th ps)) (-> th ch)) ## Converse of ax-2 stmt (pm2.86 () () (-> (-> (-> ph ps) (-> ph ch)) (-> ph (-> ps ch)))) ## Converse of ax-2 stmt (pm2.86i () ((-> (-> ph ps) (-> ph ch))) (-> ph (-> ps ch))) # Deduction based on [[pm2.86]]. ## Converse of ax-2 stmt (pm2.86d () ((-> ph (-> (-> ps ch) (-> ps th)))) (-> ph (-> ps (-> ch th)))) # The Linearity Axiom of the infinite-valued sentential logic (L-infinity) # of Lukasiewicz. (Contributed by O'Cat, 12-Aug-2004.) ## Lukasiewicz's Linearity Axiom stmt (loolin () () (-> (-> (-> ph ps) (-> ps ph)) (-> ps ph))) # An alternate for the Linearity Axiom of the infinite-valued sentential # logic (L-infinity) of Lukasiewicz, due to Barbara Wozniakowska, //Reports # on Mathematical Logic// 10, 129-137 (1978). (Contributed by O'Cat, # 8-Aug-2004.) ## Lukasiewicz's Linearity Axiom stmt (loowoz () () (-> (-> (-> ph ps) (-> ph ch)) (-> (-> ps ph) (-> ps ch)))) # Inference rule derived from axiom [[ax-3]]. ## Third Axiom Inference stmt (con4i () ((-> (-. ph) (-. ps))) (-> ps ph)) # Deduction derived from axiom [[ax-3]]. ## Third Axiom Deduction stmt (con4d () ((-> ph (-> (-. ps) (-. ch)))) (-> ph (-> ch ps))) # From a wff and its negation, anything is true. Theorem *2.21 of # [bib/WhiteheadRussell] p. 104. Also called the Duns Scotus law. ## Contradiction Implies Anything stmt (pm2.21 () () (-> (-. ph) (-> ph ps))) # A contradiction implies anything. Inference from [[pm2.21]]. ## Contradiction Implies Anything stmt (pm2.21i () ((-. ph)) (-> ph ps)) # A contradiction implies anything. Deduction from [[pm2.21]]. ## Contradiction Implies Anything ## ## (-> ph [ (-. [ ps ] )) ## (-> ph (-> [ [ ps ] ch)) ##
stmt (con2i () ((-> ph (-. ps))) (-> ps (-. ph))) # A contraposition inference. ## Contraposition ## ## (-> ph ps ) ## (-> (-. ps) (-. ph)) ##
stmt (con3i () ((-> ph ps)) (-> (-. ps) (-. ph))) # Theorem *2.5 of [bib/WhiteheadRussell] p. 107. stmt (pm2.5 () () (-> (-. (-> ph ps)) (-> (-. ph) ps))) # Theorem *2.51 of [bib/WhiteheadRussell] p. 107. stmt (pm2.51 () () (-> (-. (-> ph ps)) (-> ph (-. ps)))) # Theorem *2.52 of [bib/WhiteheadRussell] p. 107. stmt (pm2.52 () () (-> (-. (-> ph ps)) (-> (-. ph) (-. ps)))) # Theorem *2.521 of [bib/WhiteheadRussell] p. 107. stmt (pm2.521 () () (-> (-. (-> ph ps)) (-> ps ph))) # Inference version of [[pm2.24]]. ## Contradiction Implies Anything stmt (pm2.24i () (ph) (-> (-. ph) ps)) # Deduction version of [[pm2.21]]. ## Contradiction Implies Anything stmt (pm2.24d () ((-> ph ps)) (-> ph (-> (-. ps) ch))) ## Modus Tollens ## ## [ [ [ (-. [ ps) ## (-> [ ph ] [ [ ps) ## (-. [ ph ] ) ] ] ##
stmt (mto () ((-. ps) (-> ph ps)) (-. ph)) ## Modus Tollens ## ## [ [ [ (-. [ ch) ## (-> ph (-> [ ps ] [ [ ch)) ## (-> ph (-. [ ps ] ] ] )) ##
stmt (mtoi () ((-. ch) (-> ph (-> ps ch))) (-> ph (-. ps))) ## Modus Tollens stmt (mtod () ((-> ph (-. ch)) (-> ph (-> ps ch))) (-> ph (-. ps))) # A rule similar to modus tollens. ## Modus Tollens stmt (mt2 () (ps (-> ph (-. ps))) (-. ph)) ## Modus Tollens stmt (mt2i () (ch (-> ph (-> ps (-. ch)))) (-> ph (-. ps))) ## Modus Tollens stmt (mt2d () ((-> ph ch) (-> ph (-> ps (-. ch)))) (-> ph (-. ps))) # A rule similar to modus tollens. ## Modus Tollens stmt (mt3 () ((-. ps) (-> (-. ph) ps)) ph) ## Modus Tollens stmt (mt3i () ((-. ch) (-> ph (-> (-. ps) ch))) (-> ph ps)) ## Modus Tollens stmt (mt3d () ((-> ph (-. ch)) (-> ph (-> (-. ps) ch))) (-> ph ps)) ## Modus Tollens stmt (mt4d () ((-> ph ps) (-> ph (-> (-. ch) (-. ps)))) (-> ph ch)) ## Negated Syllogism stmt (nsyl () ((-> ph (-. ps)) (-> ch ps)) (-> ph (-. ch))) ## Negated Syllogism stmt (nsyld () ((-> ph (-> ps (-. ch))) (-> ph (-> ta ch))) (-> ph (-> ps (-. ta)))) ## Negated Syllogism stmt (nsyl2 () ((-> ph (-. ps)) (-> (-. ch) ps)) (-> ph ch)) ## Negated Syllogism stmt (nsyl3 () ((-> ph (-. ps)) (-> ch ps)) (-> ch (-. ph))) ## Negated Syllogism stmt (nsyl4 () ((-> ph ps) (-> (-. ph) ch)) (-> (-. ch) ps)) ## Negated Syllogism stmt (nsyli () ((-> ph (-> ps ch)) (-> th (-. ch))) (-> ph (-> th (-. ps)))) # Theorem *3.2 of [bib/WhiteheadRussell] p. 111, expressed with primitive # connectives. (The proof was shortened by Josh Purinton, 29-Dec-2000.) ## Join antecedents stmt (pm3.2im () () (-> ph (-> ps (-. (-> ph (-. ps)))))) # Theorem 8 of [bib/Margaris] p. 60. (The proof was shortened by Josh Purinton, # 29-Dec-2000.) stmt (mth8 () () (-> ph (-> (-. ps) (-. (-> ph ps))))) # Theorem *2.61 of [bib/WhiteheadRussell] p. 107. Useful for eliminating an # antecedent. ## Proof by cases stmt (pm2.61 () () (-> (-> ph ps) (-> (-> (-. ph) ps) ps))) # Inference eliminating an antecedent. ## Proof by cases ## ## (-> ph [ ps) ## (-> (-. ph) [ ps) ## [ ps ##
stmt (biimpri () ((<-> ph ps)) (-> ps ph)) # Deduce an implication from a logical equivalence. ## Biconditional Implies Conditional ## ## (-> ph (<-> [ ps ch ] )) ## (-> ph (-> [ ps ch ] )) ##
stmt (biimpd () ((-> ph (<-> ps ch))) (-> ph (-> ps ch))) # Deduce a converse implication from a logical equivalence. ## Biconditional Implies Conditional stmt (biimprd () ((-> ph (<-> ps ch))) (-> ph (-> ch ps))) # Deduce a commuted implication from a logical equivalence. ## Biconditional Implies Conditional stmt (biimpcd () ((-> ph (<-> ps ch))) (-> ps (-> ph ch))) # Deduce a converse commuted implication from a logical equivalence. ## Biconditional Implies Conditional stmt (biimprcd () ((-> ph (<-> ps ch))) (-> ch (-> ph ps))) # Infer an equivalence from an implication and its converse. ## Bicondition from two conditionals ## ## (-> ph ps) ## (-> ps ph) ## (<-> ph ps) ##
stmt (bicomi () ((<-> ph ps)) (<-> ps ph)) # An inference from transitive law for logical equivalence. ## Transitive Property ## ## (<-> ph ] [ ps ] ] ) ## [ (<-> [ ps ] [ ch) ## (<-> ph ] [ [ [ ch) ##
stmt (bitri () ((<-> ph ps) (<-> ps ch)) (<-> ph ch)) # An inference from transitive law for logical equivalence. ## Transitive Property stmt (bitr2i () ((<-> ph ps) (<-> ps ch)) (<-> ch ph)) # An inference from transitive law for logical equivalence. ## Transitive Property ## ## (<-> ps ] [ ph ] ) ## (<-> ps ] ] [ ch) ## (<-> [ [ ph [ ch) ##
stmt (bitr3i () ((<-> ps ph) (<-> ps ch)) (<-> ph ch)) # An inference from transitive law for logical equivalence. ## Transitive Property stmt (bitr4i () ((<-> ph ps) (<-> ch ps)) (<-> ph ch)) # A chained inference from transitive law for logical equivalence. ## Transitive Property stmt (3bitri () ((<-> ph ps) (<-> ps ch) (<-> ch th)) (<-> ph th)) # A chained inference from transitive law for logical equivalence. ## Transitive Property stmt (3bitrri () ((<-> ph ps) (<-> ps ch) (<-> ch th)) (<-> th ph)) # A chained inference from transitive law for logical equivalence. ## Transitive Property stmt (3bitr2i () ((<-> ph ps) (<-> ch ps) (<-> ch th)) (<-> ph th)) # A chained inference from transitive law for logical equivalence. ## Transitive Property stmt (3bitr2ri () ((<-> ph ps) (<-> ch ps) (<-> ch th)) (<-> th ph)) # A chained inference from transitive law for logical equivalence. ## Transitive Property stmt (3bitr3i () ((<-> ph ps) (<-> ph ch) (<-> ps th)) (<-> ch th)) # A chained inference from transitive law for logical equivalence. ## Transitive Property stmt (3bitr3ri () ((<-> ph ps) (<-> ph ch) (<-> ps th)) (<-> th ch)) # A chained inference from transitive law for logical equivalence. This # inference is frequently used to apply a definition to both sides of a # logical equivalence. ## Transitive Property stmt (3bitr4i () ((<-> ph ps) (<-> ch ph) (<-> th ps)) (<-> ch th)) # A chained inference from transitive law for logical equivalence. ## Transitive Property stmt (3bitr4ri () ((<-> ph ps) (<-> ch ph) (<-> th ps)) (<-> th ch)) # Introduce an antecedent to both sides of a logical equivalence. ## Equivalence over Implication ## ## (<-> [ ph ] [ [ ps) ## (<-> (-> ch [ ph ] ) [ (-> ch [ ps)) ##
stmt (imbi2i () ((<-> ph ps)) (<-> (-> ch ph) (-> ch ps))) # Introduce a consequent to both sides of a logical equivalence. ## Equivalence over Implication ## ## (<-> ph ] ] [ ps ] ) ## (<-> (-> ph ] ch) ] (-> [ ps ] ch)) ##
stmt (imbi1i () ((<-> ph ps)) (<-> (-> ph ch) (-> ps ch))) # Negate both sides of a logical equivalence. ## Negation Both Sides ## ## (<-> [ ph ] [ ps ] ) ## (<-> (-. [ ph ] ) (-. [ ps ] )) ##
stmt (notbii () ((<-> ph ps)) (<-> (-. ph) (-. ps))) ## Join two equivalences to form equivalent implication stmt (imbi12i () ((<-> ph ps) (<-> ch th)) (<-> (-> ph ch) (-> ps th))) # An inference from a biconditional, related to modus ponens. ## Modus Ponens ## ## ph ] ] ] ## (<-> ph ] [ ps ] ) ## [ [ ps ] ##
stmt (mpbi () (ph (<-> ph ps)) ps) # An inference from a biconditional, related to modus ponens. ## Modus Ponens ## ## [ [ ps ] ## (<-> ph ] [ ps ] ) ## ph ] ] ] ##
stmt (mpbir () (ps (<-> ph ps)) ph) # An inference from a biconditional, related to modus tollens. ## Modus Tollens ## ## (-. [ ph ] ) ] ] ## (<-> [ ph ] [ [ ps) ## [ [ [ (-. [ ps) ##
stmt (mtbi () ((-. ph) (<-> ph ps)) (-. ps)) # An inference from a biconditional, related to modus tollens. ## Modus Tollens ## ## [ [ (-. [ ps) ## (<-> [ ph ] [ [ ps) ## (-. [ ph) ] ] ] ##
stmt (mtbir () ((-. ps) (<-> ph ps)) (-. ph)) # An inference from a nested biconditional, related to modus ponens. ## Modus Ponens ## ## [ ps ] ## (-> ph (<-> [ ps ] ch)) ## (-> ph [ [ ch)) ##
stmt (mpbii () (ps (-> ph (<-> ps ch))) (-> ph ch)) # An inference from a nested biconditional, related to modus ponens. ## Modus Ponens stmt (mpbiri () (ch (-> ph (<-> ps ch))) (-> ph ps)) # A deduction from a biconditional, related to modus ponens. ## Modus Ponens stmt (mpbid () ((-> ph ps) (-> ph (<-> ps ch))) (-> ph ch)) # A deduction from a biconditional, related to modus ponens. ## Modus Ponens stmt (mpbird () ((-> ph ch) (-> ph (<-> ps ch))) (-> ph ps)) # Inference rule introducing a theorem as an antecedent. ## Theorem as antecedent ## ## [ ph ] ## (<-> ps (-> [ ph ] ps)) ##
stmt (a1bi () (ph) (<-> ps (-> ph ps))) # A mixed syllogism inference from an implication and a biconditional. ## Syllogism ## ## (-> ph [ ps ] ] ] ) ## [ (<-> ps ] [ ch ] ) ## (-> ph [ [ [ ch ] ) ##
stmt (sylib () ((-> ph ps) (<-> ps ch)) (-> ph ch)) # A mixed syllogism inference from a biconditional and an implication. # Useful for substituting an antecedent with a definition. ## Syllogism ## ## (<-> ph [ ps ] ] ] ) ## [ (-> ps ] [ ch ] ) ## ( -> ph [ [ [ ch ] ) ##
stmt (sylbi () ((<-> ph ps) (-> ps ch)) (-> ph ch)) # A mixed syllogism inference from an implication and a biconditional. # Useful for substituting a consequent with a definition. ## Syllogism stmt (sylibr () ((-> ph ps) (<-> ch ps)) (-> ph ch)) # A mixed syllogism inference from a biconditional and an implication. ## Syllogism stmt (sylbir () ((<-> ps ph) (-> ps ch)) (-> ph ch)) # A syllogism deduction. ## Syllogism stmt (sylibd () ((-> ph (-> ps ch)) (-> ph (<-> ch th))) (-> ph (-> ps th))) # A syllogism deduction. ## Syllogism stmt (sylbid () ((-> ph (<-> ps ch)) (-> ph (-> ch th))) (-> ph (-> ps th))) # A syllogism deduction. ## Syllogism stmt (sylibrd () ((-> ph (-> ps ch)) (-> ph (<-> th ch))) (-> ph (-> ps th))) # A syllogism deduction. ## Syllogism stmt (sylbird () ((-> ph (<-> ch ps)) (-> ph (-> ch th))) (-> ph (-> ps th))) # A mixed syllogism inference from a nested implication and a # biconditional. Useful for substituting an embedded antecedent with a # definition. ## Syllogism stmt (syl5ib () ((-> ph (-> ps ch)) (<-> th ps)) (-> ph (-> th ch))) # A mixed syllogism inference from a nested implication and a # biconditional. ## Syllogism stmt (syl5ibr () ((-> ph (-> ps ch)) (<-> ps th)) (-> ph (-> th ch))) # A mixed syllogism inference. ## Syllogism stmt (syl5bi () ((-> ph (<-> ps ch)) (-> th ps)) (-> ph (-> th ch))) # A mixed syllogism inference. ## Syllogism stmt (syl5cbi () ((-> ph (<-> ps ch)) (-> th ps)) (-> th (-> ph ch))) # A mixed syllogism inference. ## Syllogism stmt (syl5bir () ((-> ph (<-> ps ch)) (-> th ch)) (-> ph (-> th ps))) # A mixed syllogism inference. ## Syllogism stmt (syl5cbir () ((-> ph (<-> ps ch)) (-> th ch)) (-> th (-> ph ps))) # A mixed syllogism inference from a nested implication and a # biconditional. ## Syllogism stmt (syl6ib () ((-> ph (-> ps ch)) (<-> ch th)) (-> ph (-> ps th))) # A mixed syllogism inference from a nested implication and a # biconditional. Useful for substituting an embedded consequent with a # definition. ## Syllogism stmt (syl6ibr () ((-> ph (-> ps ch)) (<-> th ch)) (-> ph (-> ps th))) # A mixed syllogism inference. ## Syllogism stmt (syl6bi () ((-> ph (<-> ps ch)) (-> ch th)) (-> ph (-> ps th))) # A mixed syllogism inference. ## Syllogism stmt (syl6bir () ((-> ph (<-> ch ps)) (-> ch th)) (-> ph (-> ps th))) # A mixed syllogism inference from a doubly nested implication and a # biconditional. ## Syllogism stmt (syl7ib () ((-> ph (-> ps (-> ch th))) (<-> ta ch)) (-> ph (-> ps (-> ta th)))) # A syllogism rule of inference. The second premise is used to replace # the consequent of the first premise. ## Syllogism stmt (syl8ib () ((-> ph (-> ps (-> ch th))) (<-> th ta)) (-> ph (-> ps (-> ch ta)))) # A mixed syllogism inference, useful for removing a definition from both # sides of an implication. ## Syllogism stmt (3imtr3i () ((-> ph ps) (<-> ph ch) (<-> ps th)) (-> ch th)) # A mixed syllogism inference, useful for applying a definition to both # sides of an implication. ## Syllogism stmt (3imtr4i () ((-> ph ps) (<-> ch ph) (<-> th ps)) (-> ch th)) # A contraposition inference. ## Contraposition stmt (con1bii () ((<-> (-. ph) ps)) (<-> (-. ps) ph)) # A contraposition inference. ## Contraposition ## ## (<-> ph (-. ps)) ## (<-> ps (-. ph)) ##
## right('Commute', '∨') stmt (orcom () () (<-> (\/ ph ps) (\/ ps ph))) # Axiom *1.4 of [bib/WhiteheadRussell] p. 96. ## Commutative Property of OR stmt (pm1.4 () () (-> (\/ ph ps) (\/ ps ph))) # Theorem *2.62 of [bib/WhiteheadRussell] p. 107. ## Unidirectional definition of OR stmt (pm2.62 () () (-> (\/ ph ps) (-> (-> ph ps) ps))) # Theorem *2.621 of [bib/WhiteheadRussell] p. 107. ## Unidirectional definition of OR stmt (pm2.621 () () (-> (-> ph ps) (-> (\/ ph ps) ps))) # Theorem *2.68 of [bib/WhiteheadRussell] p. 108. ## Unidirectional definition of OR stmt (pm2.68 () () (-> (-> (-> ph ps) ps) (\/ ph ps))) ## Denial of a Disjunct ## Elimination of disjunction by denying a disjunct. <.summary> stmt (orel1 () () (-> (-. ph) (-> (\/ ph ps) ps))) ## Denial of a Disjunct ## Elimination of disjunction by denying a disjunct. <.summary> stmt (orel2 () () (-> (-. ph) (-> (\/ ps ph) ps))) # Theorem *2.25 of [bib/WhiteheadRussell] p. 104. stmt (pm2.25 () () (\/ ph (-> (\/ ph ps) ps))) # Theorem *2.53 of [bib/WhiteheadRussell] p. 107. stmt (pm2.53 () () (-> (\/ ph ps) (-> (-. ph) ps))) # Inference adding a left disjunct to both sides of a logical # equivalence. ## Equivalence over Disjunction ## ## (<-> [ ph ] [ [ ps) ## (<-> (\/ ch [ ph ] ) [ (\/ ch [ ps)) ##
stmt (orbi2i () ((<-> ph ps)) (<-> (\/ ch ph) (\/ ch ps))) # Inference adding a right disjunct to both sides of a logical # equivalence. ## Equivalence over Disjunction ## ## (<-> ph ] ] [ ps ] ) ## (<-> (\/ ph ] ch) ] (\/ [ ps ] ch)) ##
stmt (pm3.2i () (ph ps) (/\ ph ps)) # Theorem *3.37 (Transp) of [bib/WhiteheadRussell] p. 112. stmt (pm3.37 () () (-> (-> (/\ ph ps) ch) (-> (/\ ph (-. ch)) (-. ps)))) ## Nested conjunction of antecedents stmt (pm3.43i () () (-> (-> ph ps) (-> (-> ph ch) (-> ph (/\ ps ch))))) # Deduce conjunction of the consequents of two implications ("join # consequents with 'and'"). ## Join two implications ## ## (-> ph ps ] ] ) ## (-> ph ] [ ch) ## (-> ph (/\ ps ] [ ch)) ##
stmt (jca () ((-> ph ps) (-> ph ch)) (-> ph (/\ ps ch))) ## Replace implication with conjunction stmt (jcai () ((-> ph ps) (-> ph (-> ps ch))) (-> ph (/\ ps ch))) # Inference conjoining a theorem to the left of a consequent. ## Add theorem to the left of a consequent stmt (jctl () (ps) (-> ph (/\ ps ph))) # Inference conjoining a theorem to the right of a consequent. ## Add theorem to the right of a consequent stmt (jctr () (ps) (-> ph (/\ ph ps))) ## Add theorem to the left of a consequent stmt (jctil () ((-> ph ps) ch) (-> ph (/\ ch ps))) ## Add theorem to the right of a consequent stmt (jctir () ((-> ph ps) ch) (-> ph (/\ ps ch))) ## Add antecedent stmt (ancl () () (-> (-> ph ps) (-> ph (/\ ph ps)))) ## Add antecedent stmt (ancr () () (-> (-> ph ps) (-> ph (/\ ps ph)))) # Deduction conjoining antecedent to left of consequent. ## Add Antecedent ## ## (-> ph [ [ ps) ## (-> ph [ (/\ ph [ ps)) ##
stmt (ancli () ((-> ph ps)) (-> ph (/\ ph ps))) # Deduction conjoining antecedent to right of consequent. ## Add Antecedent ## ## (-> ph [ ps ] ) ## (-> ph (/\ [ ps ] ph)) ##
stmt (adantl () ((-> ph ps)) (-> (/\ ch ph) ps)) # Inference adding a conjunct to the right of an antecedent. ## Add Conjunct ## ## (-> ph ] [ [ [ ps) ## (-> (/\ ph ] [ ch ] ) [ ps) ##
stmt (adantr () ((-> ph ps)) (-> (/\ ph ch) ps)) # Deduction adding a conjunct to the left of an antecedent. ## Add Conjunct stmt (adantld () ((-> ph (-> ps ch))) (-> ph (-> (/\ th ps) ch))) # Deduction adding a conjunct to the right of an antecedent. ## Add Conjunct stmt (adantrd () ((-> ph (-> ps ch))) (-> ph (-> (/\ ps th) ch))) # Deduction adding a conjunct to antecedent. ## Add Conjunct ## ## (-> (/\ [ ph [ ps) ch) ## (-> (/\ (/\ th [ ph) [ ps) ch) ##