metamath.lean

-- Rule of Modus Ponens. The postulated inference rule of propositional
-- calculus. See e.g. Rule 1 of [Hamilton] p. 73. 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. "Modus ponens" is short for "modus ponendo ponens," a Latin phrase
-- that means "the mode that by affirming affirms" - remark in [Sanford]
-- p. 39. This rule is similar to the rule of modus tollens mto 176.
--
-- Note: In some web page displays such as the Statement List, the symbols
-- "& " and "⇒ " informally indicate the relationship between the hypotheses
-- and the assertion (conclusion), abbreviating the English words "and" and
-- "implies." They are not part of the formal language. (Contributed by NM,
-- 30-Sep-1992.) 
--
-- ⊢ 𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ 𝜓
def ax_mp {φ ψ} (a : φ) (ab : φ → ψ) : ψ := ab a

-- Axiom Simp. Axiom A1 of [Margaris] p. 49. One of the 3 axioms of
-- propositional calculus. The 3 axioms are also given as Definition 2.1 of
-- [Hamilton] p. 28. This axiom is called Simp or "the principle of
-- simplification" in Principia Mathematica (Theorem *2.02 of
-- [WhiteheadRussell] p. 100) because "it enables us to pass from the joint
-- assertion of 𝜑 and 𝜓 to the assertion of 𝜑 simply." It is Proposition 1 of
-- [Frege1879] p. 26, its first axiom. (Contributed by NM, 30-Sep-1992.) 
-- ⊢ (𝜑 → (𝜓 → 𝜑))
def ax_1 {φ ψ} : φ → (ψ → φ) :=
    assume a b, a

-- Axiom Frege. Axiom A2 of [Margaris] p. 49. One of the 3 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; see Proposition 2 of [Frege1879] p. 26. It is also
-- proved as Theorem *2.77 of [WhiteheadRussell] p. 108. The other direction
-- of this axiom also turns out to be true, as demonstrated by pm5.41 364.
-- (Contributed by NM, 30-Sep-1992.) 
-- ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
def ax_2 {φ ψ χ} : (φ → ψ → χ) → (φ → ψ) → φ → χ :=
    assume abc ab a, abc a (ab a)

open classical

-- Axiom Transp. Axiom A3 of [Margaris] p. 49. One of the 3 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 (Theorem *2.17 of [WhiteheadRussell] p. 103). We will also use
-- the term "contraposition" for this principle, although the reader is
-- advised that in the field of philosophical logic, "contraposition" has a
-- different technical meaning. (Contributed by NM, 30-Sep-1992.)
-- ⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))
def ax_3 {φ ψ} : (¬φ → ¬ψ) → (ψ → φ) := by_cases
    (assume (a : φ) _ _, a)
    (assume (na : ¬φ) (nanb : ¬φ → ¬ψ) (b : ψ),
        absurd b (nanb na))

-- A double modus ponens inference. (Contributed by NM, 5-Apr-1994.)
def mp2 {φ ψ χ} (a : φ) (b : ψ) (f : φ → ψ → χ) : χ :=
    f a b

-- A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013.) 
-- ⊢ 𝜑    &   ⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ 𝜒
def mp2b {φ ψ χ} (a : φ) (ab : φ → ψ) (bc : ψ → χ) : χ :=
    bc (ab a)

-- Description: Inference derived from axiom ax-1 6. See a1d 25 for an
-- explanation of our informal use of the terms "inference" and "deduction."
-- See also the comment in syld 44. (Contributed by NM, 29-Dec-1992.)
-- ⊢ 𝜑    ⇒   ⊢ (𝜓 → 𝜑)
def a1i {φ ψ} (a : φ) : ψ → φ :=
    ax_1 a

-- Drop and replace an antecedent. (Contributed by Stefan O'Rear,
-- 29-Jan-2015.) 
-- ⊢ 𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜒 → 𝜓)
def mp1i {φ ψ χ} (a : φ) (ab : φ → ψ) : χ → ψ :=
    a1i (ax_mp a ab)