Deduction Form and Natural Deduction
|
|
Metamath Proof Explorer Deduction Form and Natural Deduction |
|
| Mirrors > Home > MPE Home > Deductions | ||
| Contents of this page |
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] |
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.
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).
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:
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).
As mentioned earlier, the 𝜑 → prefix can be used to support natural deduction. To understand that, let's first briefly examine natural deduction.
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:
There are many variations in ND systems. [Indrzejczak] page 32 believes that two kinds of variations are especially important:
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.
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.
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.
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.
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.
| This page was last updated on 4-Jul-2020.
Copyright terms: Public domain |
W3C HTML validation [external] |