Deduction Form and Natural Deduction - Metamath Proof Explorer

Contents of this page Introduction to deduction Current approach to deductions Introduction to natural deduction Natural deduction in the Metamath Proof Explorer (MPE) Other Approaches to Natural Deduction in Metamath 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 may 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 |- si   =>    |- ta into some theorem in the form |- (si -> ta). The deduction says, "if we can prove si then we can prove ta," which is in some sense weaker than saying "si implies ta." 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.

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 particular, there is a preference 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". An assertion is in deduction form if the conclusion is an implication with a wff variable as the antecedent (usually ph), and every MPE hypothesis ($e statement) is either a definition or is also an implication with the same wff variable as the antecedent (usually ph). 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 antedent is either that wff variable (normally ph) or is a conjunction (... /\...) including that wff variable ( ph).

For example, lhop (L'Hopital's rule) is in deduction form, because its conclusion and most of its MPE hypotheses are implications with ph 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., ph) mimics the context handled in the 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. Before we discuss how to do natural deduction in MPE, we will first explain what natural deduction is.

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 ( _G) 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 ph  ->...

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:

• ovmpt2d - value of (2-operand) operation given maps-to notation.
• fvmptd - value of (1-argument) function given maps-to notation
• breq1d, breqd, and breq2d - relations with an equality

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 has 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 believes this change makes 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 21-Dec-2016]. 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.

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 ph 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 " ph" 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 " ph" is not necessary.

Sometimes, we wish to discharge these hypotheses with something that isn't just an abbreviation. For example, if "J e. ( TopOn ` X )", then X is the base set of the topology J, so X = U. J (toponuni), but since X = U. J is not always true in this situation, we can't prove it without the hypothesis "J e. ( TopOn ` X )". What you have to do here, if you want to use a theorem that has the hypothesis "|- X = U. J" (to prove some statement |- P(X)), is use eqid anyway, producing a proof of P(U. J), then use ( ph -> X = U. J ) and equality theorems to get ( ph -> ( P(X) <-> P(U. J) ) ), then use the proof of |- P(U. J) to yield |- ( ph -> 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 |- ( ph -> B = my-base-set )
$e |- ( ph -> .+ = my-group-op(B) )
mygroupval $p |- ( ph -> MyGroup = { <. ( Base ` ndx ) ,
                   B >. , <. ( +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 |- ( ph -> B = my-base-set )
$e |- ( ph -> .+ = my-group-op(B) )
mygroupbaslem $p |- ( ph -> ( Base ` MyGroup ) = my-base-set )
mygroupaddlem $p |- ( ph -> ( +g ` MyGroup ) = my-group-op(B) )

and now we can bootstrap the whole thing:

mygroupbas $p |- ( ph -> ( Base ` MyGroup ) = my-base-set ) $=
1::eqid |- ( ph -> my-base-set = my-base-set )
2::eqid |- ( ph -> my-group-op = my-group-op(my-base-set) )
qed:1,2:mygroupbaslem |- ( ph -> ( Base ` MyGroup ) = my-base-set )

mygroupadd $p |- ( ph -> ( +g ` MyGroup ) = my-base-set ) $=
1::mygroupbas |- ( ph -> ( Base ` MyGroup ) = my-base-set )
2::eqid |- ( ph -> my-group-op( ( Base ` MyGroup ) ) = my-group-op( ( Base
           ` MyGroup ) ) )
qed:1,2:mygroupbaslem |- ( ph -> ( +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 to 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 ( ph -> X = ... ) 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.