# Adapted mechanically from set.mm # todo: proper attribution ## redirect prop_min.ghi 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) term (wff (T)) term (wff (F)) ## Axiom of Truth ## ## T represents a true statement. In theory, we could define T as (ph -> ph) <-> T ## except Ghilbert does not accept binding wffs as variables. ## stmt (tru () () (T)) ## redirect prop.gh # 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 ## ## (-> ph [ ps ] ) ## (-> ph (<-> [ ps [ ch)) ## (-> ph [ [ ch) ##
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 (pm3.41i () ((-> ph ps)) (-> (/\ ph ch) ps)) ## Add to Antecedent ## ## (-> [ ph ps) ## (-> (/\ ch [ ph) ps) ##
stmt (pm3.42i () ((-> ph ps)) (-> (/\ ch ph) ps)) # Conjoin antecedent to left of consequent. Theorem *4.7 of # [bib/WhiteheadRussell] p. 120. ## 'Add Antecedent as consequent' stmt (anclb () () (<-> (-> ph ps) (-> ph (/\ ph ps)))) # Conjoin antecedent to right of consequent. ## 'Add Antecedent as consequent' stmt (ancrb () () (<-> (-> ph ps) (-> ph (/\ ps ph)))) # Conjunction implies implication. Theorem *3.4 of [bib/WhiteheadRussell] # p. 113. ## Conjunction implies implication stmt (pm3.4 () () (-> (/\ ph ps) (-> ph ps))) # Conjunction with implication. Compare Theorem *4.45 of # [bib/WhiteheadRussell] p. 119. ## Conjunction with implication stmt (pm4.45im () () (<-> ph (/\ ph (-> ps ph)))) # Conjoin antecedents and consequents of two premises. ## Join antecedents and consequents stmt (anim12i () ((-> ph ps) (-> ch th)) (-> (/\ ph ch) (/\ ps th))) # Introduce conjunct to both sides of an implication. ## Introduce conjunct to both sides stmt (anim1i () ((-> ph ps)) (-> (/\ ph ch) (/\ ps ch))) # Introduce conjunct to both sides of an implication. ## Introduce conjunct to both sides stmt (anim2i () ((-> ph ps)) (-> (/\ ch ph) (/\ ch ps))) # Disjoin antecedents and consequents of two premises. ## Join antecedents and consequents stmt (orim12i () ((-> ph ps) (-> ch th)) (-> (\/ ph ch) (\/ ps th))) # Introduce disjunct to both sides of an implication. ## Introduce disjunct to both sides stmt (orim1i () ((-> ph ps)) (-> (\/ ph ch) (\/ ps ch))) # Introduce disjunct to both sides of an implication. ## Introduce disjunct to both sides stmt (orim2i () ((-> ph ps)) (-> (\/ ch ph) (\/ ch ps))) # Theorem *2.3 of [bib/WhiteheadRussell] p. 104. stmt (pm2.3 () () (-> (\/ ph (\/ ps ch)) (\/ ph (\/ ch ps)))) # Disjunction of antecedents. Compare Theorem *3.44 of # [bib/WhiteheadRussell] p. 113. ## Disjunction of antecedents stmt (jao () () (-> (-> ph ps) (-> (-> ch ps) (-> (\/ ph ch) ps)))) # Inference disjoining the antecedents of two implications. ## Join two implications ## ## (-> ph ] ] ] ps) ## (-> [ [ ch ] ps) ## (-> (\/ ph ] [ ch ] ) ps) ##
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) ##
stmt (anidms () ((-> (/\ ph ph) ps)) (-> ph ps)) # Conjunction idempotence with antecedent. (Contributed by Roy F. # Longton, 8-Aug-2005.) ## Conjunction is Idempotent stmt (anidmdbi () () (<-> (-> ph (/\ ps ps)) (-> ph ps))) # Commutative law for conjunction. Theorem *4.3 of [bib/WhiteheadRussell] # p. 118. ## Commute Conjunction ## right('Commute', '∧') stmt (ancom () () (<-> (/\ ph ps) (/\ ps ph))) # Inference commuting conjunction in antecedent. //Notational convention//: # We sometimes suffix with "s" the label of an inference that manipulates # an antecedent, leaving the consequent unchanged. The "s" means that the # inference eliminates the need for a syllogism ([[syl]]) -type inference # in a proof. ## Commute Conjunction stmt (ancoms () ((-> (/\ ph ps) ch)) (-> (/\ ps ph) ch)) # Deduction commuting conjunction in antecedent. ## Commute Conjunction stmt (ancomsd () ((-> ph (-> (/\ ps ch) th))) (-> ph (-> (/\ ch ps) th))) # Theorem *3.22 of [bib/WhiteheadRussell] p. 111. ## Commute Conjunction stmt (pm3.22 () () (-> (/\ ph ps) (/\ ps ph))) # Associative law for conjunction. Theorem *4.32 of [bib/WhiteheadRussell] # p. 118. ## Associative Property ## right('Associate', 'R') left('Associate', 'L') stmt (anass () () (<-> (/\ (/\ ph ps) ch) (/\ ph (/\ ps ch)))) # Associative law for conjunction applied to antecedent (eliminates # syllogism). ## Associative Property stmt (anasss () ((-> (/\ (/\ ph ps) ch) th)) (-> (/\ ph (/\ ps ch)) th)) # Associative law for conjunction applied to antecedent (eliminates # syllogism). ## Associative Property stmt (anassrs () ((-> (/\ ph (/\ ps ch)) th)) (-> (/\ (/\ ph ps) ch) th)) # Distribution of implication with conjunction. ## Distributive Property stmt (imdistan () () (<-> (-> ph (-> ps ch)) (-> (/\ ph ps) (/\ ph ch)))) # Distribution of implication with conjunction. ## Distributive Property stmt (imdistani () ((-> ph (-> ps ch))) (-> (/\ ph ps) (/\ ph ch))) # Distribution of implication with conjunction. ## Distributive Property stmt (imdistanri () ((-> ph (-> ps ch))) (-> (/\ ps ph) (/\ ch ph))) # Distribution of implication with conjunction (deduction rule). ## Distributive Property stmt (imdistand () ((-> ph (-> ps (-> ch th)))) (-> ph (-> (/\ ps ch) (/\ ps th)))) # Theorem *5.3 of [bib/WhiteheadRussell] p. 125. ## Distributive Property stmt (pm5.3 () () (<-> (-> (/\ ph ps) ch) (-> (/\ ph ps) (/\ ph ch)))) # Theorem *5.61 of [bib/WhiteheadRussell] p. 125. ## Eliminate Disjoint stmt (pm5.61 () () (<-> (/\ (\/ ph ps) (-. ps)) (/\ ph (-. ps)))) ## Syllogism stmt (sylan () ((-> (/\ ph ps) ch) (-> th ph)) (-> (/\ th ps) ch)) ## Syllogism stmt (sylanb () ((-> (/\ ph ps) ch) (<-> th ph)) (-> (/\ th ps) ch)) ## Syllogism stmt (sylanbr () ((-> (/\ ph ps) ch) (<-> ph th)) (-> (/\ th ps) ch)) ## Syllogism stmt (sylan2 () ((-> (/\ ph ps) ch) (-> th ps)) (-> (/\ ph th) ch)) ## Syllogism stmt (sylan2b () ((-> (/\ ph ps) ch) (<-> th ps)) (-> (/\ ph th) ch)) ## Syllogism stmt (sylan2br () ((-> (/\ ph ps) ch) (<-> ps th)) (-> (/\ ph th) ch)) ## Double Syllogism stmt (syl2an () ((-> (/\ ph ps) ch) (-> th ph) (-> ta ps)) (-> (/\ th ta) ch)) ## Double Syllogism stmt (syl2anb () ((-> (/\ ph ps) ch) (<-> th ph) (<-> ta ps)) (-> (/\ th ta) ch)) ## Double Syllogism stmt (syl2anbr () ((-> (/\ ph ps) ch) (<-> ph th) (<-> ps ta)) (-> (/\ th ta) ch)) ## Syllogism stmt (syland () ((-> ph (-> (/\ ps ch) th)) (-> ph (-> ta ps))) (-> ph (-> (/\ ta ch) th))) ## Syllogism stmt (sylan2d () ((-> ph (-> (/\ ps ch) th)) (-> ph (-> ta ch))) (-> ph (-> (/\ ps ta) th))) tvar (wff et) ## Syllogism stmt (syl2and () ((-> ph (-> (/\ ps ch) th)) (-> ph (-> ta ps)) (-> ph (-> et ch))) (-> ph (-> (/\ ta et) th))) ## Syllogism stmt (sylanl1 () ((-> (/\ (/\ ph ps) ch) th) (-> ta ph)) (-> (/\ (/\ ta ps) ch) th)) ## Syllogism stmt (sylanl2 () ((-> (/\ (/\ ph ps) ch) th) (-> ta ps)) (-> (/\ (/\ ph ta) ch) th)) ## Syllogism stmt (sylanr1 () ((-> (/\ ph (/\ ps ch)) th) (-> ta ps)) (-> (/\ ph (/\ ta ch)) th)) ## Syllogism stmt (sylanr2 () ((-> (/\ ph (/\ ps ch)) th) (-> ta ch)) (-> (/\ ph (/\ ps ta)) th)) ## Syllogism stmt (sylani () ((-> ph (-> (/\ ps ch) th)) (-> ta ps)) (-> ph (-> (/\ ta ch) th))) ## Syllogism stmt (sylan2i () ((-> ph (-> (/\ ps ch) th)) (-> ta ch)) (-> ph (-> (/\ ps ta) th))) ## Syllogism stmt (syl2ani () ((-> ph (-> (/\ ps ch) th)) (-> ta ps) (-> et ch)) (-> ph (-> (/\ ta et) th))) # A syllogism deduction with conjoined antecents. ## Syllogism stmt (syldan () ((-> (/\ ph ps) ch) (-> (/\ ph ch) th)) (-> (/\ ph ps) th)) # Nested syllogism inference conjoining dissimilar antecedents. ## Syllogism stmt (sylan9 () ((-> ph (-> ps ch)) (-> th (-> ch ta))) (-> (/\ ph th) (-> ps ta))) # Nested syllogism inference conjoining dissimilar antecedents. ## Syllogism stmt (sylan9r () ((-> ph (-> ps ch)) (-> th (-> ch ta))) (-> (/\ th ph) (-> ps ta))) # Modus ponens conjoining dissimilar antecedents. ## Modus Ponens stmt (mpan9 () ((-> ph ps) (-> ch (-> ps th))) (-> (/\ ph ch) th)) # A syllogism inference combined with contraction. ## Syllogism & Contraction stmt (sylanc () ((-> (/\ ph ps) ch) (-> th ph) (-> th ps)) (-> th ch)) ## Syllogism & Contraction stmt (syl2anc () ((-> (/\ (/\ ph ps) (/\ ch th)) ta) (-> et ph) (-> et ps) (-> et ch) (-> et th)) (-> et ta)) ## Syllogism & Contraction stmt (sylancb () ((-> (/\ ph ps) ch) (<-> th ph) (<-> th ps)) (-> th ch)) ## Syllogism & Contraction stmt (sylancbr () ((-> (/\ ph ps) ch) (<-> ph th) (<-> ps th)) (-> th ch)) ## Syllogism & Commute stmt (sylancom () ((-> (/\ ph ps) ch) (-> (/\ ch ps) th)) (-> (/\ ph ps) th)) ## Eliminate Antecedent by Cases stmt (pm2.61ian () ((-> (/\ ph ps) ch) (-> (/\ (-. ph) ps) ch)) (-> ps ch)) ## Eliminate Antecedent by Cases stmt (pm2.61dan () ((-> (/\ ph ps) ch) (-> (/\ ph (-. ps)) ch)) (-> ph ch)) ## Proof by contradiction stmt (condan () ((-> (/\ ph (-. ps)) ch) (-> (/\ ph (-. ps)) (-. ch))) (-> ph ps)) # Introduce one conjunct as an antecedent to the another. ## Introduce conjunct as antecedent ## left('Simplify', '→') stmt (abai () () (<-> (/\ ph ps) (/\ ph (-> ph ps)))) # Introduce a left conjunct to both sides of a logical equivalence. ## Add conjunct to both sides ## ## (<-> [ ph ] [ [ ps) ## (<-> (/\ ch [ ph ] ) [ (/\ ch [ ps)) ##
stmt (anbi2i () ((<-> ph ps)) (<-> (/\ ch ph) (/\ ch ps))) ## Add conjunct to both sides ## Introduce a right conjunct to both sides of a logical equivalence. ## ## (<-> ph ] ] [ ps ] ) ## (<-> (/\ ph ] ch) ] (/\ [ ps ] ch)) ##
stmt (anbi1i () ((<-> ph ps)) (<-> (/\ ph ch) (/\ ps ch))) ## Conjoin both sides of two equivalences ## ## (<-> ph ] ] ] [ ps ] ] ) ## (<-> [ [ ch ] [ [ th ] ) ## (<-> (/\ ph ] [ ch ] ) (/\ [ ps [ th ] )) ##
stmt (anbi12i () ((<-> ph ps) (<-> ch th)) (<-> (/\ ph ch) (/\ ps th))) # Theorem *5.53 of [bib/WhiteheadRussell] p. 125. stmt (pm5.53 () () (<-> (-> (\/ (\/ ph ps) ch) th) (/\ (/\ (-> ph th) (-> ps th)) (-> ch th)))) # A rearrangement of conjuncts. ## Rearrangement conjunction stmt (an12 () () (<-> (/\ ph (/\ ps ch)) (/\ ps (/\ ph ch)))) # A rearrangement of conjuncts. ## Rearrangement conjunction stmt (an23 () () (<-> (/\ (/\ ph ps) ch) (/\ (/\ ph ch) ps))) # Deduction rearranging conjuncts. ## Rearrangement conjunction stmt (an1s () ((-> (/\ ph (/\ ps ch)) th)) (-> (/\ ps (/\ ph ch)) th)) # Inference commuting a nested conjunction in antecedent. ## Rearrangement conjunction stmt (ancom2s () ((-> (/\ ph (/\ ps ch)) th)) (-> (/\ ph (/\ ch ps)) th)) # Deduction rearranging conjuncts. ## Rearrangement conjunction stmt (ancom13s () ((-> (/\ ph (/\ ps ch)) th)) (-> (/\ ch (/\ ps ph)) th)) # Deduction rearranging conjuncts. ## Rearrangement conjunction stmt (an1rs () ((-> (/\ (/\ ph ps) ch) th)) (-> (/\ (/\ ph ch) ps) th)) # Inference commuting a nested conjunction in antecedent. ## Rearrangement conjunction stmt (ancom1s () ((-> (/\ (/\ ph ps) ch) th)) (-> (/\ (/\ ps ph) ch) th)) # Deduction rearranging conjuncts. ## Rearrangement conjunction stmt (ancom31s () ((-> (/\ (/\ ph ps) ch) th)) (-> (/\ (/\ ch ps) ph) th)) ## Absorb conjunct stmt (anabs1 () () (<-> (/\ (/\ ph ps) ph) (/\ ph ps))) ## Absorb conjunct stmt (anabs5 () () (<-> (/\ ph (/\ ph ps)) (/\ ph ps))) ## Absorb conjunct stmt (anabs7 () () (<-> (/\ ps (/\ ph ps)) (/\ ph ps))) ## Absorb antecedent into conjunction stmt (anabsi5 () ((-> ph (-> (/\ ph ps) ch))) (-> (/\ ph ps) ch)) ## Absorb antecedent into conjunction stmt (anabsi6 () ((-> ph (-> (/\ ps ph) ch))) (-> (/\ ph ps) ch)) ## Absorb antecedent into conjunction stmt (anabsi7 () ((-> ps (-> (/\ ph ps) ch))) (-> (/\ ph ps) ch)) ## Absorb antecedent into conjunction stmt (anabsi8 () ((-> ps (-> (/\ ps ph) ch))) (-> (/\ ph ps) ch)) ## Absorb antecedent into conjunction stmt (anabss1 () ((-> (/\ (/\ ph ps) ph) ch)) (-> (/\ ph ps) ch)) ## Absorb antecedent into conjunction stmt (anabss3 () ((-> (/\ (/\ ph ps) ps) ch)) (-> (/\ ph ps) ch)) ## Absorb antecedent into conjunction stmt (anabss4 () ((-> (/\ (/\ ps ph) ps) ch)) (-> (/\ ph ps) ch)) ## Absorb antecedent into conjunction stmt (anabss5 () ((-> (/\ ph (/\ ph ps)) ch)) (-> (/\ ph ps) ch)) ## Absorb antecedent into conjunction stmt (anabss7 () ((-> (/\ ps (/\ ph ps)) ch)) (-> (/\ ph ps) ch)) ## Absorb antecedent into conjunction stmt (anabsan () ((-> (/\ (/\ ph ph) ps) ch)) (-> (/\ ph ps) ch)) ## Absorb antecedent into conjunction stmt (anabsan2 () ((-> (/\ ph (/\ ps ps)) ch)) (-> (/\ ph ps) ch)) ## Rearrange Conjunction stmt (an4 () () (<-> (/\ (/\ ph ps) (/\ ch th)) (/\ (/\ ph ch) (/\ ps th)))) ## Rearrange Conjunction stmt (an42 () () (<-> (/\ (/\ ph ps) (/\ ch th)) (/\ (/\ ph ch) (/\ th ps)))) ## Rearrange Conjunction stmt (an4s () ((-> (/\ (/\ ph ps) (/\ ch th)) ta)) (-> (/\ (/\ ph ch) (/\ ps th)) ta)) ## Rearrange Conjunction stmt (an42s () ((-> (/\ (/\ ph ps) (/\ ch th)) ta)) (-> (/\ (/\ ph ch) (/\ th ps)) ta)) # Distribution of conjunction over conjunction. ## Distributive Property stmt (anandi () () (<-> (/\ ph (/\ ps ch)) (/\ (/\ ph ps) (/\ ph ch)))) # Distribution of conjunction over conjunction. ## Distributive Property stmt (anandir () () (<-> (/\ (/\ ph ps) ch) (/\ (/\ ph ch) (/\ ps ch)))) # Inference that undistributes conjunction in the antecedent. ## Distributive Property stmt (anandis () ((-> (/\ (/\ ph ps) (/\ ph ch)) ta)) (-> (/\ ph (/\ ps ch)) ta)) # Inference that undistributes conjunction in the antecedent. ## Distributive Property stmt (anandirs () ((-> (/\ (/\ ph ch) (/\ ps ch)) ta)) (-> (/\ (/\ ph ps) ch) ta)) # A theorem similar to the standard definition of the biconditional. # Definition of [bib/Margaris] p. 49. ## Definition of biconditional ## left('Simplify', '↔') stmt (dfbi2 () () (<-> (<-> ph ps) (/\ (-> ph ps) (-> ps ph)))) ## Definition of biconditional stmt (dfbi () () (/\ (-> (<-> ph ps) (/\ (-> ph ps) (-> ps ph))) (-> (/\ (-> ph ps) (-> ps ph)) (<-> ph ps)))) # Deduce an equivalence from two implications. ## Deduce Biconditional from two conditionals ## ## (-> ph (-> [ ps ch ] )) ## (-> ph (-> [ ch ps ] )) ## (-> ph (<-> [ ps ch ] )) ##
stmt (bibi2i () ((<-> ph ps)) (<-> (<-> ch ph) (<-> ch ps))) # Inference adding a biconditional to the right in an equivalence. ## Add biconditional to both sides of a equivalence ## ## (<-> ph ] ] [ ps ] ) ## (<-> (<-> ph ] ch) ] (<-> [ ps ] ch)) ##
stmt (mpan2 () (ps (-> (/\ ph ps) ch)) (-> ph ch)) # An inference based on modus ponens. ## Modus Ponens ## ## ph ] ] ] ] ## [ [ ps ] ] ## (-> (/\ ph ] [ ps ] ) [ ch) ## [ [ [ [ ch ##
stmt (mp2an () (ph ps (-> (/\ ph ps) ch)) ch) # An inference based on modus ponens. ## Modus Ponens stmt (mpani () (ps (-> ph (-> (/\ ps ch) th))) (-> ph (-> ch th))) # An inference based on modus ponens. ## Modus Ponens stmt (mpan2i () (ch (-> ph (-> (/\ ps ch) th))) (-> ph (-> ps th))) # An inference based on modus ponens. ## Modus Ponens stmt (mp2ani () (ps ch (-> ph (-> (/\ ps ch) th))) (-> ph th)) # A deduction based on modus ponens. ## Modus Ponens stmt (mpand () ((-> ph ps) (-> ph (-> (/\ ps ch) th))) (-> ph (-> ch th))) # A deduction based on modus ponens. ## Modus Ponens stmt (mpan2d () ((-> ph ch) (-> ph (-> (/\ ps ch) th))) (-> ph (-> ps th))) # A deduction based on modus ponens. ## Modus Ponens stmt (mp2and () ((-> ph ps) (-> ph ch) (-> ph (-> (/\ ps ch) th))) (-> ph th)) # An inference based on modus ponens. ## Modus Ponens stmt (mpdan () ((-> ph ps) (-> (/\ ph ps) ch)) (-> ph ch)) # An inference based on modus ponens with commutation of antecedents. ## Modus Ponens stmt (mpancom () ((-> ps ph) (-> (/\ ph ps) ch)) (-> ps ch)) # An inference based on modus ponens. ## Modus Ponens stmt (mpanl1 () (ph (-> (/\ (/\ ph ps) ch) th)) (-> (/\ ps ch) th)) # An inference based on modus ponens. ## Modus Ponens stmt (mpanl2 () (ps (-> (/\ (/\ ph ps) ch) th)) (-> (/\ ph ch) th)) # An inference based on modus ponens. ## Modus Ponens stmt (mpanl12 () (ph ps (-> (/\ (/\ ph ps) ch) th)) (-> ch th)) # An inference based on modus ponens. ## Modus Ponens stmt (mpanr1 () (ps (-> (/\ ph (/\ ps ch)) th)) (-> (/\ ph ch) th)) # An inference based on modus ponens. ## Modus Ponens stmt (mpanr2 () (ch (-> (/\ ph (/\ ps ch)) th)) (-> (/\ ph ps) th)) # An inference based on modus ponens. ## Modus Ponens stmt (mpanr12 () (ps ch (-> (/\ ph (/\ ps ch)) th)) (-> ph th)) # An inference based on modus ponens. ## Modus Ponens stmt (mpanlr1 () (ps (-> (/\ (/\ ph (/\ ps ch)) th) ta)) (-> (/\ (/\ ph ch) th) ta)) # Modus-tollens-like theorem. ## Modus Tollens stmt (mtt () () (-> (-. ph) (<-> (-. ps) (-> ps ph)))) # A false consequent falsifies an antecedent. ## Modus Tollens stmt (mt2bi () (ph) (<-> (-. ps) (-> ps (-. ph)))) # A deduction from a biconditional, similar to modus tollens. ## Modus Tollens stmt (mtbid () ((-> ph (-. ps)) (-> ph (<-> ps ch))) (-> ph (-. ch))) # A deduction from a biconditional, similar to modus tollens. ## Modus Tollens stmt (mtbird () ((-> ph (-. ch)) (-> ph (<-> ps ch))) (-> ph (-. ps))) # An inference from a biconditional, similar to modus tollens. ## Modus Tollens stmt (mtbii () ((-. ps) (-> ph (<-> ps ch))) (-> ph (-. ch))) # An inference from a biconditional, similar to modus tollens. ## Modus Tollens ## ## [ [ (-. [ ch) ## (-> ph (<-> ps ] [ [ ch)) ## (-> ph (-. ps ] ] ] )) ##
stmt (con4biir () ((<-> ph ps)) (<-> (-. ph) (-. ps)) ) # Reorder sylbi a bit. ## Syllogism ## ## (-> ps ] ] ] ch) ## (<-> ps ] [ ph ] ) ## (-> [ [ ph ] ch) ##
stmt (sylbi2() ((-> ps ch) (<-> ps ph)) (-> ph ch) ) # Commute the conclusion of bitr3i. ## Transitive Property ## ## (<-> ps [ [ [ ph ] ) ## (<-> ps [ ch ] ] ] ) ## [ (<-> ch ] [ ph ] ) ##
stmt (bitr3icom() ((<-> ps ph) (<-> ps ch)) (<-> ch ph) ) ## Equivalence over Disjunction ## ## (\/ ph ] ] ] ps) ## (<-> ph ] [ ch ] ) ## (\/ [ [ ch ] ps) ##
stmt (orbi1ii () ((\/ ph ps) (<-> ph ch)) (\/ ch ps) ) ## Equivalence over Disjunction ## ## (\/ ph [ ps ] ] ] ) ## (<-> [ ps ] [ ch ] ) ## (\/ ph [ [ [ ch ] ) ##
stmt (orbi2ii () ((\/ ph ps) (<-> ps ch)) (\/ ph ch) ) ## Equivalence over Conjunction ## ## (/\ ph ] ] ] ps) ## (<-> ph ] [ ch ] ) ## (\/ [ [ ch ] ps) ##
stmt (anbi1ii () ((/\ ph ps) (<-> ph ch)) (/\ ch ps) ) ## Equivalence over Conjunction ## ## (/\ ph [ ps ] ] ] ) ## (<-> [ ps ] [ ch ] ) ## (/\ ph [ [ [ ch ] ) ##
stmt (anbi2ii () ((/\ ph ps) (<-> ps ch)) (/\ ph ch) ) ## Associative Property stmt (orassi () ((\/ (\/ ph ps) ch)) (\/ ph (\/ ps ch)) ) ## Associative Property stmt (orassli () ((\/ ph (\/ ps ch))) (\/ (\/ ph ps) ch) ) ## Associative Property stmt (anassi () ((/\ (/\ ph ps) ch)) (/\ ph (/\ ps ch)) ) ## Associative Property stmt (anassli () ((/\ ph (/\ ps ch))) (/\ (/\ ph ps) ch) ) ## Associative Property stmt (biassi () ((<-> (<-> ph ps) ch)) (<-> ph (<-> ps ch)) ) ## Associative Property stmt (biassli () ((<-> ph (<-> ps ch))) (<-> (<-> ph ps) ch) ) ## Commute Conjunction ## ## (/\ ph ps) ## (/\ ps ph) ##
stmt (ancomi () ((/\ ph ps)) (/\ ps ph)) ## Commute Disjunction ## ## (\/ ph ps) ## (\/ ps ph) ##
stmt (orcomi () ((\/ ph ps)) (\/ ps ph)) ## F is false stmt (notfal () () (-. (F))) ## Remove Implies ## ## [ ph ] ## (<-> (-> [ ph ] ps) ps) ##
stmt (impRemove1 () (ph) (<-> (-> ph ps) ps)) ## Remove Implies ## ## [ ph ] ## (<-> (-> ps [ ph ] ) (T)) ##
stmt (impRemove2 () (ph) (<-> (-> ps ph) (T))) ## Remove Implies ## ## [ (-. [ ph ] ) ## (<-> (-> [ [ ph ] ps) (T)) ##
stmt (impNotRemove1 () ((-. ph)) (<-> (-> ph ps) (T))) ## Remove Equivalence ## ## [ (-. [ ph ] ) ## (<-> (-> ps [ [ ph ] ) (-. ps)) ##
stmt (impNotRemove2 () ((-. ph)) (<-> (-> ps ph) (-. ps))) ## Remove Equivalence ## ## [ ph ] ## (<-> (<-> [ ph ] ps) ps) ##
stmt (biRemove1 () (ph) (<-> (<-> ph ps) ps)) ## Remove Equivalence ## ## [ ph ] ## (<-> (<-> ps [ ph ] ) ps) ##
stmt (biRemove2 () (ph) (<-> (<-> ps ph) ps)) ## Remove Equivalence ## ## [ (-. [ ph ] ) ## (<-> (<-> ps [ [ ph ] ) (-. ps)) ##
stmt (biNotRemove2 () ((-. ph)) (<-> (<-> ps ph) (-. ps))) ## Remove Equivalence ## ## [ (-. [ ph ] ) ## (<-> (<-> [ [ ph ] ps) ps) ##
stmt (biNotRemove1 () ((-. ph)) (<-> (<-> ph ps) (-. ps))) ## Remove AND ## ## [ ph ] ## (<-> (/\ [ ph ] ps) ps) ##
stmt (anRemove1 () (ph) (<-> (/\ ph ps) ps)) ## Remove AND ## ## [ ph ] ## (<-> (/\ ps [ ph ] ) ps) ##
stmt (anRemove2 () (ph) (<-> (/\ ps ph) ps)) ## Remove AND ## ## [ (-. [ ph ] ) ## (<-> (/\ [ [ ph ] ps) (F)) ##
stmt (anNotRemove1 () ((-. ph)) (<-> (/\ ph ps) (F))) ## Remove AND ## ## [ (-. [ ph ] ) ## (<-> (/\ ps [ [ ph ] ) (F)) ##
stmt (anNotRemove2 () ((-. ph)) (<-> (/\ ps ph) (F))) ## Remove OR ## ## [ ph ] ## (<-> (\/ [ ph ] ps) (T)) ##
stmt (orRemove1 () (ph) (<-> (\/ ph ps) (T))) ## Remove OR ## ## [ ph ] ## (<-> (\/ ps [ ph ] ) (T)) ##
stmt (orRemove2 () (ph) (<-> (\/ ps ph) (T))) ## Remove OR ## ## [ (-. [ ph ] ) ## (<-> (\/ [ [ ph ] ps) ps) ##
stmt (orNotRemove1 () ((-. ph)) (<-> (\/ ph ps) ps)) ## Remove OR ## ## [ (-. [ ph ] ) ## (<-> (\/ ps [ [ ph ] ) ps) ##
stmt (orNotRemove2 () ((-. ph)) (<-> (\/ ps ph) ps)) # ax-mp with the order of the first and second hypotheses reversed. ## Modus Ponens ## ## (-> ph ] [ ps) ## ph ] ] ## [ [ ps ##
stmt (ax-mpRemove () ((-> ph ps) ph ) ps) # mto with the order of the first and second hypotheses reversed. ## Modus Tollens ## ## (-> [ ph ] [ [ ps) ## [ [ [ (-. [ ps) ## (-. [ ph ] ) ] ] ##
stmt (mtoRemove () ((-> ph ps) (-. ps)) (-. ph)) # mpbi with the order of the first and second hypotheses reversed. ## Modus Ponens ## ## (<-> ph ] [ ps ] ) ## ph ] ] ] ## [ [ ps ] ##
stmt (mpbiRemove () ((<-> ph ps) ph ) ps) # mpbir with the order of the first and second hypotheses reversed. ## Modus Ponens ## ## (<-> ph ] [ ps ] ) ## [ [ ps ] ## ph ] ] ] ##
stmt (mpbirRemove () ((<-> ph ps) ps ) ph) # mtbi with the order of the first and second hypotheses reversed. ## Modus Tollens ## ## (<-> [ ph ] [ [ ps) ## [ [ [ (-. [ ps) ## (-. [ ph ] ) ] ] ##
stmt (mtbiRemove () ((<-> ph ps) (-. ph)) (-. ps)) # mtbir with the order of the first and second hypotheses reversed. ## Modus Tollens ## ## (<-> [ ph ] [ [ ps) ## [ [ (-. [ ps) ## (-. [ ph) ] ] ] ##
stmt (mtbirRemove () ((<-> ph ps) (-. ps)) (-. ph)) ## right('Simplify', '↔') stmt (mpbi-inline () () (-> (/\ ph (<-> ph ps)) ps)) stmt (impexpi () ((-> (/\ ph ps) ch)) (-> ps (-> ph ch))) stmt (anim3 () () (-> (/\ ph (-> ps ch)) (-> ps (/\ ph ch)))) stmt (ancomd () ((-> ph (/\ ps ch))) (-> ph (/\ ch ps)))