Metamath Proof Explorer Home Metamath Proof Explorer
Deduction Form and Natural Deduction
 
Mirrors  >  Home  >  MPE Home  >  Deductions

Contents of this page
  • Introduction to deduction
  • Current approach to deductions
  • Conversion
  • Special cases
  • Introduction to natural deduction
  • Natural deduction in the Metamath Proof Explorer (MPE)
  • Other Approaches to Natural Deduction in Metamath
  • When to use deduction form instead
  • Strengths of the current approach
  • Definitions in deduction form
  • Natural deduction rules
  • A Theorem fine is Deduction,
    For it allows work-reduction:
    To show "A implies B",
    Assume A and prove B;
    Quite often a simpler production.

    --Stefan Bilaniuk
    A Problem Course in Mathematical Logic, 2003 [external]


    Introduction to deduction     A deduction (also called an inference) is a kind of statement that needs some hypotheses to be true in order for its conclusion to be true. A theorem, on the other hand, has no hypotheses (or all its hypotheses are definitions). Informally we often call both of them theorems, but on this page we will stick to the strict definition.

    When being rigorous, it is surprisingly complicated to convert some deduction in the form 𝜎 𝜏 into some theorem in the form (𝜎𝜏). The deduction says, "if we can prove 𝜎 then we can prove 𝜏," which is in some sense weaker than saying " 𝜎 implies 𝜏." In particular, there is no axiom of logic that permits us to directly obtain the theorem given the deduction. The conversion of a deduction to a theorem does not even hold in general for quantum propositional calculus, which is a weak subset of classical propositional calculus. It has been shown that adding the Standard Deduction Theorem to quantum propositional calculus turns it into classical propositional calculus!

    This is in contrast to going the other way; if we have the theorem, it is easy to recover the deduction using modus ponens ax-mp. An example of this is the derivation of the inference simpli from the theorem simpl. More details about conversions are covered below.

    In traditional logic books, this is often resolved using a metatheorem called the Deduction Theorem (discovered independently by Herbrand and Tarski around 1930). The deduction theorem, aka the standard deduction theorem, provides an algorithm for constructing a proof of a theorem from the proof of its corresponding deduction. See, for example, Margaris, First Order Mathematical Logic, p. 56. To construct a proof for a theorem, the deduction theorem's algorithm looks at each step in the proof of the original deduction and rewrites the step with several steps wherein the hypothesis is eliminated and becomes an antecedent. Ordinary mathematical proofs invoke this algorithm when converting a deduction into a theorem.

    However, in practice, no one actually carries out this conversion algorithm in ordinary mathematics. Instead, mathematicians often stop once they believe the conversion algorithm could be done. This sharply contrasts with Metamath's philosophical goal, which is to show all proofs directly from the axiom system in its database, and not skip steps or rely on higher-level metatheorems derived outside of that axiom system.

    Metamath is capable of converting a hypothesis into an antecedent. We have found that in many cases only a weakened form of the deduction theorem is necessary, called the weak deduction theorem (dedth and its variants). The weak deduction theorem is often easier to use when it is necessary to use some version of the deduction theorem in the Metamath Proof Explorer (MPE). Earlier versions of MPE applied the deduction theorem, or a weakened form of it, in a number of situations. For more information about using the deduction theorem and the weak deduction theorem, including more details of why this can be complicated, see the deduction theorem page.

    Today, the deduction theorem (including the weak variant of it) is rarely used in MPE when creating new proofs. That is because we have found much easier ways to achieve the same result. The rest of this page explains these easier ways.


    Current approach to deductions     Current MPE conventions encourage using forms that are easier to deal with directly.

    In general there is a preference today for writing assertions in "deduction form" instead of writing a proof that would require use of the deduction theorem. Applying this approach is called "deduction style". The power of deduction form in Metamath was originally identified by Mario Carneiro.

    An assertion is in deduction form if the conclusion is an implication with a wff variable as the antecedent (usually 𝜑), and every MPE hypothesis ($e statement) is either a definition or is also an implication with the same wff variable as the antecedent (usually 𝜑). A definition can be for a class variable (this is a class variable followed by "=") or a wff variable (this is a wff variable followed by ); in practice definitions (if used) are for class variables. In practice, a proof in deduction form will also contain many steps that are implications where the antecedent is either that wff variable (normally 𝜑) or is a conjunction (......) including that wff variable (𝜑).

    For example, lhop (L'Hopital's rule) is in deduction form, because its conclusion and most of its MPE hypotheses are implications with 𝜑 as the antecent. It has one MPE hypothesis that is not an implication, but that hypothesis is a definition of a class variable - which is also allowed in deduction form. Later, in the section on Definitions in deduction form, we'll explain why definitions are allowed in deduction form.

    In deduction form the antecedent (e.g., 𝜑) mimics the context handled in the deduction theorem.

    Sometimes we have assertions in multiple forms; here are the forms and the conventions for their labels (names) when multiple forms are present:

    You can compare these forms by comparing pm2.43 (closed form), pm2.43i (inference form), and pm2.43d (deduction form).


    Conversion     Once you have an assertion in deduction form, you can easily convert it to inference form or closed form:

    As noted earlier, we can also easily convert any assertion T in closed form to its related assertion Ti in inference form by applying ax-mp. The challenge, when working formally, can sometimes occur when converting some arbitrary assertion T in inference form into a related assertion Td in deduction form.

    An assertion in deduction form that has a hypothesis can be easily converted so that the hypothesis becomes an implication. More formally, given an assertion THM in deduction form with hypothesis $e (𝜑𝜓) and a conclusion (𝜑𝜒) we can easily turn THM into the assertion (𝜑 → (𝜓𝜒)). Another way to say this is that we can easily convert the THM (𝜑𝜓) ⇒ (𝜑𝜒) into (𝜑 → (𝜓𝜒)), where 𝜓 and 𝜒 are any proposition. Here the process to do that:

    1. Use simpr to trivially prove that ((𝜑𝜓) → 𝜓).
    2. Use THM and the previous step to prove ((𝜑𝜓) → 𝜒). Note that in this use, (𝜑𝜓) is substituting for 𝜑 of the THM's hypothesis, enabling us to deduce this result from the first step.
    3. Use ex and the previous step to prove (𝜑 → (𝜓𝜒)).

    Note that converting an assertion in deduction form into an implication in deduction form is different from the general case of converting an inference form into an implication. In the general case that would require the deduction theorem or some variant like the weak deduction theorem.

    The deduction form antecedent can also be used to represent the context necessary to support natural deduction systems. For example, if the antecedent is a conjunction, the other terms can represent the temporary assumptions that are sometimes used in natural deduction. Below we provide an introduction to natural deduction, and then discussion how natural deduction is implemented in Metamath set.mm (and iset.mm).


    Special cases     There are some types of hypotheses where we usually do not use a 𝜑 antecedent in a theorem's deduction form. Although this may weaken the theorem slightly, omitting this antecedent where it is not normally needed can make proofs using the theorem slightly shorter by not having to apply a1i in order to match its hypotheses. Here they are, along with a discussion of possible methods to strengthen the deduction form with 𝜑 on one of these hypotheses if needed.
    1. Existence (sethood) hypothesis, e.g., a $e of the form 𝐴 ∈ V. To add 𝜑 if desired, first turn the 𝐴 ∈ V into an antecedent using vtoclg and friends as in e.g. unisng, then convert from this (semi-)closed form back to deduction form.
    2. Not-free-in hypothesis, e.g., a $e of the form 𝑥𝜓 or 𝑥𝐴. It is very rare that you really need something of the form 𝜑 → Ⅎ𝑥𝜓 instead in set.mm, because of the 𝐴𝑉, 𝐵𝑉 assumptions that are needed in order to substitute a variable for a class. (You can substitute a wff for a variable, if the universe has at least two elements; for example you can use ∅ ∈ 𝑥 as a substitute for variable 𝜑, where we take 𝑥 to be the set {𝑦 ∈ 1𝑜𝜑}.) The special case where 𝜓 is 𝜑 is given by nfdi.
      It is possible to prove the not-free theorem for a term constructor given the equality theorem, provided you can substitute the terms for variables. Mario demonstrates this in nfnlem of peano.mm1, as follows. Suppose we have a constructor "foo (𝐴, 𝐵)" and we want to prove (𝐴𝑉𝐵𝑉𝑥𝐴𝑥𝐵) → 𝑥 foo (𝐴, 𝐵). We can let 𝑦 = 𝐴 and 𝑧 = 𝐵 be new dummies, then 𝑥 foo (𝐴, 𝐵) ↔ 𝑥 foo (𝑦, 𝑧), but the latter is true by nfv. The 𝑥𝐴 and 𝐵 theorems come up when we want to prove (𝑦 = 𝐴𝑧 = 𝐵) → (𝑥 foo (𝑦, 𝑧) ↔ 𝑥 foo (𝐴, 𝐵)); the nf equality step here requires that the context be free from 𝑥, so you need a special version of the theorem so that this can be given as a hypothesis. In the worst case, the theorem may have to be reproved back through a number of previous theorems. We do have many "nf*d" theorems that will assist this. In practice this is practically never needed.
    3. Definitional hypothesis, e.g., a $e of the form (𝜓 ↔ (𝜒𝜃)) or 𝐴 = (𝐵 + 𝐶). To prepend 𝜑, eliminate the original hypothesis with biid or eqid, then rewrite the proof where the steps are simplified with the new 𝜑 prefix form of the definitional hypotheses. See Mario's discussion about this.
    4. Implicit substitution hypothesis, e.g., a $e of the form (𝑥 = 𝑦 → (𝜑𝜓)) or (𝑥 = 𝑦𝐴 = 𝐵). To prepend 𝜑, convert the theorem to explicit substitution form, then convert back to implicit substitution form. This can be somewhat tedious, but at least it can be done in principle. See fsumshftd for an example, as discussed in the mailing list.
      This conversion is considerably less tedious if 𝐴 and 𝐵 are closed terms already, i.e., you are applying the theorem in some context rather than just trying to prove fsumshftd itself (which doesn't know what 𝐴 and 𝐵 are). For instance, if you want to prove Σ𝑥 ∈ (1...3)((𝑥 + 1)↑2) = Σ𝑦 ∈ (2...4)(𝑦↑2) by shifting the left sum to the right, you first apply fsumshft without any funny business in the substitution to prove Σ𝑥 ∈ (1...3)((𝑥 + 1)↑2) = Σ𝑦 ∈ (2...4)(((𝑦 − 1) + 1)↑2), then use sumeq2dv and equality theorems to prove (((𝑦 − 1) + 1)↑2) = (𝑦↑2) in the current context.

    As mentioned earlier, the 𝜑 prefix can be used to support natural deduction. To understand that, let's first briefly examine natural deduction.


    Introduction to Natural Deduction     Natural deduction is a widely-taught approach to logic. Those unfamiliar with natural deduction, or logic more generally, may find [Laboreo] to be a useful gentle introduction (with many examples). More detailed information is available from sources such as [Pfenning] and [Indrzejczak] (especially chapter 2). What follows here is a very brief summary.

    Natural deduction (ND) systems, as such, were originally introduced in 1934 by two logicians working independently: Jaśkowski and Gentzen. ND systems are supposed to reconstruct, in a formally proper way, traditional ways of mathematical reasoning (such as conditional proof, indirect proof, and proof by cases). As reconstructions they were naturally influenced by previous work, and many specific ND systems and notations have been developed since their original work.

    [Indrzejczak] pages 31-32 suggests that any natural deductive system must satisfy at least these three criteria:

    1. "There are some means for entering assumptions into a proof and also for eliminating them. Usually it requires some bookkeeping devices for indicating the scope of an assumption, and showing that a part of a proof depending on eliminated assumption is discharged.
    2. There are no (or, at least, very limited set of) axioms, because their role is taken over by the set of primitive rules for introduction and elimination of logical constants which means that elementary inferences instead of formulae are taken as primitive.
    3. [A genuine] ND system admits a lot of freedom in proof construction and possibility of applying several proof search strategies, like conditional proof, proof by cases, proof by reductio ad absurdum etc."

    There are many variations in ND systems. [Indrzejczak] page 32 believes that two kinds of variations are especially important:

    1. The kind of basic items (data structures) on which inference rules are defined. These notes of a proof tree "may be formulae (F-systems), sequents (S-systems), sets of formulae (generalized clauses) or other structured data (e.g. formulae with labels)".
    2. The overall format of proof representation, which are generally "trees (tree- or Gentzen-format or T-system...) or sequences (linear- or Jaśkowski format or L-system...)."
    The various Jaśkowski systems for creating a linear system of proof are popular. Many different graphic devices have been added to show groupings; a "simplified account, where each assumption is entered with the vertical line which continues until this subproof is in force, is due to Fitch, whereas [the] popular system of Copi applies bracketing to closed subproofs" ([Indrzejczak] page 42).


    Natural Deduction in the Metamath Proof Explorer (MPE)     MPE is fundamentally a Hilbert-style system. That is, MPE is based on a larger number of axioms (compared to natural deduction systems), a very small set of rules of inference (modus ponens), and the context is not changed by the rules of inference in the middle of a proof. That said, MPE proofs can be developed using the natural deduction (ND) approach as originally developed by Jaśkowski and Gentzen.

    The most common and recommended approach for applying ND in MPE is to use deduction form and apply the MPE proven assertions that are equivalent to ND rules. For example, MPE's jca is equivalent to ND rule I (and-insertion). See MPE equivalents of typical natural deduction (ND) rules for a list of equivalences. This approach for applying an ND approach within MPE relies on Metamath's wff metavariables in an essential way, and is described in more detail in the presentation "Natural Deductions in the Metamath Proof Language" by Mario Carneiro, 2014.

    In this style many steps are an implication, whose antecedent mimics the context (Γ) of most ND systems. To add an assumption, simply add it to the implication antecedent (typically using simpr), and use that new antecedent for all later claims in the same scope. If you wish to use an assertion in an ND hypothesis scope that is outside the current ND hypothesis scope, modify the assertion so that the ND hypothesis assumption is added to its antecedent (typically using adantr). Most proof steps will be proved using rules that have hypotheses and results of the form 𝜑 ...

    This is most easily understood by looking at some examples. For an annotated example where some traditional ND rules are directly applied in MPE, see ex-natded5.2, ex-natded5.3, ex-natded5.5, ex-natded5.7, ex-natded5.8, ex-natded5.13, ex-natded9.20, and ex-natded9.26.

    Only using specific natural deduction rules directly can lead to very long proofs, for exactly the same reason that only using axioms directly in Hilbert-style proofs can lead to long proofs. If the goal is short and clear proofs, then it is better to reuse already-proven proven assertions in deduction form than to start from scratch each time. For example, observe that proof ex-natded5.8 - which is a line-for-line translation of directly using only common ND rules - is much longer than ex-natded5.8-2 (which directly reuses other proven statements) and ex-natded5.2i (which doesn't worry about context). Similarly, ex-natded5.3 is longer than ex-natded5.3-2 and ex-natded5.3i. Here are a few examples of proven assertions that can be useful for proofs in deduction form:

    In some cases the metamath.exe "minimize_with" proof command can significantly shorten a proof if the original only uses the equivalent of basic ND inference rules. In practice, the simplest and clearest approach to creating a proof depends on what is to be proved.


    Other Approaches to Natural Deduction in Metamath     The text above describes the most common ways to implement natural deducation approaches in metamath and MPE. However, there are alternative approaches for using natural deduction in metamath.

    Alan Sare worked on an alternative within MPE, called virtual deduction. Much more information is available at wvd1, and an example is at iunconlem2vd [retrieved 11-Apr-2018] used to generate iunconlem2. This approach essentially replaces the outermost implication arrow with a different symbol    ▶   . Alan Sare believed this change made it easier to visualize proofs, while others disagree. The completeusersproof tool is available which supports this alternative approach.

    Frédéric Liné has developed a different metamath-based system to support natural deduction system called natural deduction [retrieved 24-Aug-2018]. He reports that his system was inspired by a slide show, "From Natural Deduction to Sequent Calculus (and back)". Practically this system is equivalent to Mario Carneiro's work.


    When to use deduction form instead    

    The deduction theorem (including the weak deduction theorem) isn't used routinely in the Metamath Proof Explorer (set.mm) today, since the alternatives are usually better. However, it can be useful to understand cases where deduction form, and the weak deduction theorem in particular, might provide an advantage.

    As a hypothetical example, suppose we have developed a theory such as complex numbers where all variable-type assumptions such as 𝐴 ∈ ℂ are stated as $e hypotheses like this:

    $e 𝐴 ∈ ℂ
    $e 𝐵 ∈ ℂ
    ----------------
    $p (𝐴 + 𝐵) = (𝐵 + 𝐴)

    The proofs of such pure inferences are usually shorter than those of other methods. Proving the closed theorem form often requires extra steps to manipulate the order of the antecedents, and the deduction form adds a small overhead to each step.

    Suppose that after a chain of 100 such inferences, we discover that we need a closed form, where the hypotheses become antecedents, for the last theorem in the chain. One reason for needing a closed form is to be able to use e.g. rexlimiv to add an existential quantifier such as 𝑥 ∈ ℂ𝜑..., which can be done only if 𝑥 ∈ ℂ is an antecedent.

    Our choices are (1) restate and reprove all 100 previous inferences as closed theorems, (2) restate and reprove all 100 theorems in natural deduction form (with 𝜑 prefixed to hypotheses and conclusion), or (3) use the weak deduction theorem to convert the last theorem in the chain to closed form. In this case, the weak deduction theorem will result in a smaller overall file size than the other methods, and it will also be far easier to implement since we only have to add 1 theorem rather than rewrite and reprove 100 theorems.

    In the early days of set.mm, many complex number theorems were available only in inference form, which motivated the development of the weak deduction theorem. Eventually, though, most complex number inferences became needed in deduction (or closed) form, and the space-saving advantage of the weak deduction theorem diminished. In particular, as the use of Mario's natural deduction method became common, the number of proofs using dedth decreased, e.g., from 232 in 2013 to 85 uses in August 2018.


    Strengths of the current approach    

    As far as we know there is nothing in the literature like either the weak deduction theorem or Mario Carneiro's natural deduction method (Mario Carneiro's method is presented in "Natural Deductions in the Metamath Proof Language" by Mario Carneiro, 2014). In order to transform a hypothesis into an antecedent, the literature's standard "Deduction Theorem" requires metalogic outside of the notions provided by the axiom system. We instead generally prefer to use Mario Carneiro's natural deduction method, then use the weak deduction theorem in cases where that is difficult to apply, and only then use the full standard deduction theorem as a last resort.

    The weak deduction theorem does not require any additional metalogic but converts an inference directly into a closed form theorem, with a rigorous proof that uses only the axiom system. Unlike the standard Deduction Theorem, there is no implicit external justification that we have to trust in order to use it.

    Mario's natural deduction method also does not require any new metalogical notions. It avoids the Deduction Theorem's metalogic by prefixing the hypotheses and conclusion of every would-be inference with a universal antecedent, "ph ->", from the very start.

    We think it is impressive and satisfying that we can do so much in a practical sense without stepping outside of our Hilbert-style axiom system. Of course our axiomatization, which is in the form of schemes, contains a metalogic of its own that we exploit. But this metalogic is relatively simple, and for our Deduction Theorem alternatives, we primarily use just the direct substitution of expressions for metavariables.


    Definitions in deduction form     At this point it's probably useful to explain in more detail why definitions do not require an antecedent in deduction form.

    The actual purpose of the 𝜑 antecedent is to introduce a hypothesis that may not always be satisfiable without some assumptions (and the exact nature of those assumptions is not known inside the theorem, so the generic 𝜑 is used). If we are dealing with a true abbreviation, just a short way to write some symbols, then a definition "D = ..." hypothesis will either be satisfied by a similar hypothesis, or by theorem eqid, which will force the substitution of "..." for "D" in the rest of the theorem. Since in any case, the hypothesis can be discharged with no assumptions, the " 𝜑" is not necessary.

    Sometimes, we wish to discharge these hypotheses with something that isn't just an abbreviation. For example, if 𝐽 ∈ (TopOn‘𝑋), then 𝑋 is the base set of the topology 𝐽, so 𝑋 = 𝐽 (toponuni), but since 𝑋 = 𝐽 is not always true in this situation, we can't prove it without the hypothesis 𝐽 ∈ (TopOn‘𝑋). What you have to do here, if you want to use a theorem that has the hypothesis 𝑋 = 𝐽 (to prove some statement P(X)), is use eqid anyway, producing a proof of P(U. J), then use (𝜑𝑋 = J ) and equality theorems to get (𝜑 ( P(X) P(U. J) ) ), then use the proof of |- P(U. J) to yield (𝜑 P(X) ). An example of this procedure is the derivation of ishaus2 (which has X = U. J given the context) from ishaus (which assumes X = U. J with no context).

    The above procedure is always possible to do, but it is not always convenient since many steps may be needed for the equality proof. In cases where we specifically intend to discharge the assumption with something other than eqid, we sometimes add ph -> to the equalities as well. A common example of this is in structure builder theorems, where we want to use a self-referential expression for the left hand side. For example, we might define a group by:

    $e (𝜑𝐵 = my-base-set )
    $e (𝜑+ = my-group-op(B) )
    mygroupval $p (𝜑 MyGroup = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩})

    Suppose that my-base-set is a complicated expression, and my-group-op(B) has a lot of references to B, so the fully expanded my-group-op(my-base-set) is really big, and we don't want to use it too many times. In the same context, we then prove:

    $e (𝜑𝐵 = my-base-set )
    $e (𝜑+ = my-group-op(B) )
    mygroupbaslem $p (𝜑 → (Base‘ MyGroup ) = my-base-set )
    mygroupaddlem $p (𝜑 → (+g MyGroup ) = my-group-op(B) )

    and now we can bootstrap the whole thing:

    mygroupbas $p (𝜑 → (Base‘ MyGroup ) = my-base-set ) $=
    1::eqid (𝜑 my-base-set = my-base-set )
    2::eqid (𝜑 my-group-op = my-group-op(my-base-set) )
    qed:1,2:mygroupbaslem (𝜑 → (Base‘ MyGroup ) = my-base-set )

    mygroupadd $p (𝜑 → (+g MyGroup ) = my-base-set ) $=
    1::mygroupbas (𝜑 → (Base‘ MyGroup ) = my-base-set )
    2::eqid (𝜑 my-group-op((Base‘ MyGroup )) = my-group-op((Base‘ MyGroup )))
    qed:1,2:mygroupbaslem (𝜑 → (+g MyGroup ) = my-group-op((Base‘ MyGroup )))

    Note that the contained references of my-group-op are now referencing ( Base ` MyGroup ), which makes this "definition" of a component of MyGroup self-referential. But that was the goal, and we have mygroupbas so we can expand it as necessary. A more elaborate version of this idea is done in prdsval, with prdsbas, prdsplusg, prdsmulr, etc pulling off components and bootstrapping using the previous theorems.

    Finally, there are a few places where (𝜑𝑋 =... ) definitions are used by convention, specifically grppropd and other *propd theorems, and isgrpd and other is*d theorems for structures.

    As a rule of thumb: Use X = ... abbreviations unless you need to use a non-identity abbreviation for X later.


    Natural Deduction Rules     For more information see natded, which shows typical natural deduction rules and their metamath equivalents.
      This page was last updated on 4-Jul-2020.
    Copyright terms: Public domain
    W3C HTML validation [external]