Suffix d for theorems not in "deduction form"

[Alexander van der Vekens]

By our conventions,

"A theorem is in "deduction form" (or is a "deduction") if it
       has one or more $e hypotheses, and the hypotheses and the conclusion are
       implications that share the same antecedent.  More precisely, the
       conclusion is an implication with a wff variable as the antecedent
       (usually ` ph `), and every hypothesis ($e statement) is either: ..."

There are, however, some theorems of the form `ph -> xxx ` which have a label ending with "d", but are no "deductions" because they have no hypotheses, e.g.

~eqidd, ~biidd, ~exmidd, ~fvexd

These theorems are only convenience theorems saving an ~a1i in the proofs(for example, ~eqidd is used 1441 times), but have no significant meaning, because they always say "something true follows from anything".

Is it justified that such theorems have suffix "d" although they are no deductions? With a lot of good will, one can say that there is an implicit hypothesis `ph -> T. ` (which is always true, see ~a1tru) which would make these theorems deductions. Or would it be better to use a different suffix or a complete different naming convention for such theorems?

[Benoit]

I had noticed this too, and was thinking of the suffix "k" (for "weaKening" and because ax-1 is often called "axiom K").

It currently has the suffix "d" because it works together with the genuine deductions to implement Mario Carneiro's algorithm related to the deduction theorem (his slides are on the metamath website).  But I think having another suffix makes things clearer (beginning with ~idk).

In other words, you have the two notions of "associated deduction" and "associated weakening": if

xxx : PHI_1 & ... & PHI_n => PHI

is a scheme (with n=0 corresponding to "no hypotheses"), then the associated deduction is

xxxd: ( phi -> PHI_1 ) & ... & ( phi -> PHI_n ) => ( phi -> PHI )

and the associated weakening is

xxxk: PHI_1 & ... & PHI_n => ( phi -> PHI )

In predicate calculus, there may be minor variations to deal with uses of ax-gen (using either DV conditions or non-freeness or related idioms), and variations concerning "definitional hypotheses" which may lack the antecedent.

Benoît

[Benoit]

Correction: the associated deduction is not what I wrote, but is as follows:

if

  xxx : PHI_1 & ... & PHI_n => ( PHI -> PSI )

is a scheme, then the associated deduction is

  xxxd: PHI_1 & ... & PHI_n & ( phi -> PHI ) => ( phi -> PSI )

where phi does not occur in the PHI_i's or PHI or PSI.

Benoît

[Jim Kingdon]

Using "d" for these makes sense to me.

If I want to try to be formal about it, I could say the below definition could read "zero or more $e hypotheses". But my reasoning is not primarily a formal one, it is more that using these feels like using a deduction theorem. They often satisfy hypotheses of other deduction theorems, they are parallel to non-deduction theorems (e.g. 1re vs 1red), when writing a proof I get to pick the antecedent, etc.

Is there a particular problem we need to solve? Like do we have cases where the name we want is already taken? I do feel like adding finer and finer distinctions does add a level of cognitive burden so each one should pull its weight.

[Benoit]

Jim: indeed, maybe versions related to Mario's algorithm for the deduction theorem should all be labeled xxxd, whether they have zero or more hypotheses.  But the suffix "d" is still overloaded: in my previous post and its correction, I gave two incompatible conventions of xxxd which are used in set.mm (e.g., mpd for the first and a1d for the second).  But then, both a1d and bj-a1k could pretend to be "the deduction associated with ax-1".  Similarly for mpd versus mp1i with respect to ax-mp.  Why in one case choose one convention and in another the other convention ?  For clarity, the two versions of "associated deduction" could be better distinguished, both by terminology and by systematic suffixing of a label.

Benoît

[Norman Megill]

On Sunday, November 28, 2021 at 1:23:01 PM UTC-5 Benoit wrote:

Jim: indeed, maybe versions related to Mario's algorithm for the deduction theorem should all be labeled xxxd, whether they have zero or more hypotheses. 

I agree with this, and I think we should change ~conventions to say  "zero or more $e hypotheses" as Jim suggested. Using a 'd' suffix for a1i applied to a theorem has been a defacto convention for a long time and in many places, they are frequently used in Mario-style deductions, and I think people are used to it.
 

But the suffix "d" is still overloaded: in my previous post and its correction, I gave two incompatible conventions of xxxd which are used in set.mm (e.g., mpd for the first and a1d for the second).  But then, both a1d and bj-a1k could pretend to be "the deduction associated with ax-1".  Similarly for mpd versus mp1i with respect to ax-mp.  Why in one case choose one convention and in another the other convention ?  For clarity, the two versions of "associated deduction" could be better distinguished, both by terminology and by systematic suffixing of a label.

 I think this kind of conflict is very rare. The only one I could find with a quick search is a1d vs. bj-a1k.

a1d follows the pattern of adding an antecedent to the hypothesis and conclusion of the corresponding a1i. The "a1" comes from the name of the inference form. A 0-hypothesis *d doesn't have a corresponding inference form, so we usually take the original theorem name and append a "d" suffix, e.g. fvex -> fvexd; following this pattern, bj-a1k would be named ax-1d, but since we reserve "ax-" for axioms, it could be called ax1d.

I don't see a conflict with mpd vs. mp1i. The first hypothesis of mp1i doesn't have a "ph" antecendent, so it doesn't qualify as a "pure" deduction form.  Maybe I'm misunderstanding what you mean.

BTW many deductions such as alimd have the hypothesis "|- F/ x ph" where ph is the common antecedent, but this is equivalent to "|- ( ph -> F/ x ph )" by nf5di. So we could say it still qualifies as a "pure" deduction form where we use "|- F/ x ph" rather than "|- ( ph -> F/ x ph )" for brevity.

Norm

 

Benoît

[Alexander van der Vekens]

I think Jim and Norm are right, so I will adapt the ~conventions accordingly, and add a sentence  about the special case "zero hypotheses".

[Mario Carneiro]

Late to the party, but I agree with Norm & Jim: Deductions can have 0 hypotheses, and while there is a naming conflict between whether the xxxd theorem is the result of "deductionizing" (add "ph ->" to all hyps and conclusion) the corresponding xxx or xxxi theorem, this is a rare situation. You could say that we have two operations: "make inference form" which converts |- ( A /\ B /\ C -> D ) to |- A & |- B & |- C => |- D, and "make deduction form" which adds "ph ->" to everything as mentioned. Usually when we have all three versions of a theorem, xxxi is the inference form of xxx, and xxxd is the deduction form of xxxi. In Benoit's example of bj-a1k, this is the deduction form of ax-1, skipping the a1i intermediary step.

The inference form operation is a no-op when the original theorem has no hypotheses, so you only have two forms for a theorem like fvex / fvexd. But the deduction form operation is not idempotent, you could always apply it multiple times and get everything under multiple layers of "ph -> ps -> ...", and we try to curry those iterated implications so that we can think of the deduction form operation as "effectively idempotent". Similarly, in the case where we have a theorem like ( A /\ B -> C ) we don't directly want to deductionize this because it yields an iterated implication |- ph -> ( A /\ B -> C ), and bj-a1k is an example of this. (There are some cases of deduction form theorems that retain some hypotheses in the conclusion; they are usually written as |- ( ( ph /\ A /\ B ) -> C ) though.)

If you are hankering for a naming convention for deductionized "theorem form" theorems, I would suggest dusting off the *t naming convention for theorems as a base for the deduction suffix, to form "a1td".

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3d3cf16d-3f83-453c-a5b1-9614e8093de6n%40googlegroups.com.

[David A. Wheeler]

Replying to myself - section 3.9.3 of the Metamath book defines
"closed form", "deduction form", and "inference form". See below.

If we change deduction form to say "zero or more hypotheses" then
the categories are no longer exclusive.

If we change the definition of "deduction form" so that it has zero or more hypotheses,
then I think we ALSO need to change the definition of "closed form"
so it's "no hypotheses and its conclusion is NOT in the form ph -> ..."
(or some wording to that effect). That way, the categories are
mutually exclusive & cover all options.

--- David A. Wheeler



==== From section 3.9.3 ====


• closed form: A kind of assertion (theorem) with no hypotheses.
Typically its label has no special suffix. An example is unss, which
states: `((A ⊆C ∧B ⊆C) ↔(A ∪B) ⊆C)
• deduction form: A kind of assertion with one or more hypotheses
where the conclusion is an implication with a wff variable as the
antecedent (usually φ), and every hypothesis ($e statement) is either
(1) an implication with the same antecedent as the conclusion or (2) a
definition. 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
↔); class variable definitions are more common. 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 (φ). If an assertion is
in deduction form, and other forms are also available, then we suffix
its label with “d.” An example is unssd, which states12: `(φ →A ⊆
C) & `(φ →B ⊆C) ⇒ `(φ →(A ∪B) ⊆C)
• inference form: A kind of assertion with one or more hypotheses
that is not in deduction form (e.g., there is no common antecedent).
If an assertion is in inference form, and other forms are also available,
then we suffix its label with “i.” An example is unssi, which states:
`A ⊆C & `B ⊆C ⇒ `(A ∪B) ⊆C

[David A. Wheeler]

> On Nov 29, 2021, at 3:57 AM, Mario Carneiro <di....@gmail.com> wrote:
>
> Late to the party, but I agree with Norm & Jim: Deductions can have 0 hypotheses, and while there is a naming conflict between whether the xxxd theorem is the result of "deductionizing" (add "ph ->" to all hyps and conclusion) the corresponding xxx or xxxi theorem, this is a rare situation.

Also late to the party. An alternative would be to keep the definition of "deduction form" & let the "d" suffix also be used in these other cases.

Before changing the definition of "deduction form" it'd be good to figure out how to rewrite metamath book section 3.9.3 (deduction form)
and the corresponding HTML files on deduction. They all lean heavily into the "one or more" definition.
I'm saying we can't change that, just that we'd need to rewrite those sections to be consistent, and that may be trickier than
it first appears.

--- David A. Wheeler

[David A. Wheeler]

If we're expanding the definition of "deduction form", can we also
allow hypotheses that directly state not-freeness in addition to ( ph -> ...) and definitions?
It'd be one less thing to convert. If there's a reason NOT to do that, let me know.

If we do accept that, a first-cut detailed definition below (tweaking the book's text).

--- David A. Wheeler

=====


• deduction form: A kind of assertion with zero or more hypotheses

where the conclusion is an implication with a wff variable as the
antecedent (usually φ), and every hypothesis ($e statement) is

(1) an implication with the same antecedent as the conclusion, or (2) a
definition, or (3) a direct statement of not-freeness.

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
↔); class variable definitions are more common. In practice, a proof

in deduction form will often contain many steps that are implications

where the antecedent is either that wff variable (normally φ) or is a
conjunction (...∧...) including that wff variable (φ). If an assertion is
in deduction form, and other forms are also available, then we suffix
its label with “d.” An example is unssd, which states12: `(φ →A ⊆
C) & `(φ →B ⊆C) ⇒ `(φ →(A ∪B) ⊆C)

• closed form: A kind of assertion (theorem) with no hypotheses
that is not in deduction form (e.g., it's not in the form ( φ → ...)).

Typically its label has no special suffix. An example is unss, which
states: `((A ⊆C ∧B ⊆C) ↔(A ∪B) ⊆C)

• inference form: A kind of assertion with one or more hypotheses
that is not in deduction form (e.g., there is no common antecedent).
If an assertion is in inference form, and other forms are also available,

then we suffix its label with “i.” The deduction form is often the inference
form with common antecedents added if both are present.

[Benoit]

As for the questions raised by David: in my opinion, the best term to refer to hypotheses-free theorems is "hypotheses-free theorem", or "theorem with no hypotheses" (in other words, no special term is needed; you can add that it is also called a "closed form" theorem, and in a footnote, mention that within propositional calculus, it is sometimes called a tautology or simply a theorem, as opposed to an inference; however, it is more convenient for us to use "theorem" also when there are hypotheses).  Then, I would say that a scheme is an inference (resp. a deduction), if it is an inference (resp. a deduction) associated with a (not necessarily true) scheme.  This brings us back to the original question.

To summarize, let me denote a scheme by PHI => PSI where PHI actually abbreviates PHI_1 & ... & PHI_n, with n=0 corresponding to "no hypotheses".  Also, I suppose that "phi" does not occur in those, and I do not deal with DV conditions (we'll deal with ways to express non-freeness later).  Starting from a scheme
  xxx: PHI => PSI
consider the two constructions:
  xxxA: ( phi -> PHI ) => ( phi -> PSI )
  xxxk: PHI => ( phi -> PSI )  [examples: mp1i; bj-a1k; idd; etc. see first two posts of this thread for several examples]
Starting from the scheme
  yyy: PHI => ( PSI -> CHI )
consider the two additional constructions:
  yyyi: PHI & PSI => CHI [the inference associated with yyy]
  yyyB: PHI & ( phi -> PSI ) => ( phi -> CHI )

Note that yyyBi is roughly yyyi, so it is only a small abuse of language to say that "yyyBi is the inference associated with yyy".

Currently in set.mm, both the A and the B constructions are called alternatively "the deduction associated with" and both use the label suffix "d" (e.g. a1d versus mpd).  As Mario mentioned, if n=0, then yyyiA == yyyB, so they are closely related (and also xxxA == xxxk when n=0).  But this is not anymore the case when there are hypotheses.

I am not proposing a solution, here.  Only summarizing the "problem".  Maybe it's not even a big problem and people are content with it, but maybe also these varying conventions are a bit puzzling.  I have no definitive opinion yet.

Benoît

[Mario Carneiro]

On Mon, Nov 29, 2021 at 3:43 PM Benoit <benoit...@gmail.com> wrote:

As for the questions raised by David: in my opinion, the best term to refer to hypotheses-free theorems is "hypotheses-free theorem", or "theorem with no hypotheses" (in other words, no special term is needed; you can add that it is also called a "closed form" theorem, and in a footnote, mention that within propositional calculus, it is sometimes called a tautology or simply a theorem, as opposed to an inference; however, it is more convenient for us to use "theorem" also when there are hypotheses).  Then, I would say that a scheme is an inference (resp. a deduction), if it is an inference (resp. a deduction) associated with a (not necessarily true) scheme.  This brings us back to the original question.

To summarize, let me denote a scheme by PHI => PSI where PHI actually abbreviates PHI_1 & ... & PHI_n, with n=0 corresponding to "no hypotheses".  Also, I suppose that "phi" does not occur in those, and I do not deal with DV conditions (we'll deal with ways to express non-freeness later).  Starting from a scheme
  xxx: PHI => PSI
consider the two constructions:
  xxxA: ( phi -> PHI ) => ( phi -> PSI )
  xxxk: PHI => ( phi -> PSI )  [examples: mp1i; bj-a1k; idd; etc. see first two posts of this thread for several examples]
Starting from the scheme
  yyy: PHI => ( PSI -> CHI )
consider the two additional constructions:
  yyyi: PHI & PSI => CHI [the inference associated with yyy]
  yyyB: PHI & ( phi -> PSI ) => ( phi -> CHI )

Note that yyyBi is roughly yyyi, so it is only a small abuse of language to say that "yyyBi is the inference associated with yyy".

Currently in set.mm, both the A and the B constructions are called alternatively "the deduction associated with" and both use the label suffix "d" (e.g. a1d versus mpd).  As Mario mentioned, if n=0, then yyyiA == yyyB, so they are closely related (and also xxxA == xxxk when n=0).  But this is not anymore the case when there are hypotheses.

I would opt to call only the xxxA operation "deduction form". The yyyB operation is only putting the phi on some of the hypotheses, which is occasionally useful (and can be applied to an arbitrary subset of the hypotheses, so it's not a uniquely defined operation) but not very common. We can add another operation, the "closed form" operation, like so:

From the scheme

xxx: PHI => PSI

we derive

xxxt: |- ( PHI -> PSI )

Then xxxt always has 0 hypotheses, and xxxti == xxx if PSI is not an implication. For a regular theorem xxx in inference form with all three variants, we have xxx == xxxti as the inference form, xxxt as the closed form, and xxxA as the deduction form. For a non-implication theorem with zero hypotheses, we have xxx == xxxt == xxxi as the closed form and xxxA as the deduction form.

On Mon, Nov 29, 2021 at 10:30 AM David A. Wheeler <dwhe...@dwheeler.com> wrote:

Replying to myself - section 3.9.3 of the Metamath book defines
"closed form", "deduction form", and "inference form". See below.

If we change deduction form to say "zero or more hypotheses" then
the categories are no longer exclusive.

I think this is not really the right way to look at it. They aren't categories that are meant to be exclusive, they are operations that can be applied to a theorem statement with various relations between them, like Benoit has shown. However, it is convenient for discussion purposes to name a statement after the operation that produced it, even if this isn't uniquely defined in some cases.

If you want a way to pick out deduction form theorems from others, the obvious definition is the image of the deduction form operation (Benoit's xxxA operation). Stated another way, a deduction form theorem is one such that all (0 or more) hypotheses and the conclusion have the form "ph -> A" for the same wff metavariable "ph". This overlaps with "closed form" if you define it as a theorem with zero hypotheses, but I would say that anything in the intersection should be considered in deduction form, not closed form, and we can rationalize this by saying that a closed form theorem should not have any wff metavariable assumptions. fvexd is not in closed form because it has a useless metavariable hypothesis.

 

If we change the definition of "deduction form" so that it has zero or more hypotheses,
then I think we ALSO need to change the definition of "closed form"
so it's "no hypotheses and its conclusion is NOT in the form ph -> ..."
(or some wording to that effect). That way, the categories are
mutually exclusive & cover all options.

The categories are also not exhaustive. I would say that a theorem in inference form should not have an implication as the conclusion, or else it would not be in the image of the inference form operation (Benoit's yyyi operation). But then A |- ( B -> C ) is neither closed form nor inference form (and obviously not deduction form), and that's okay. We're highlighting a particular structure of theorem that composes well, exactly because not all theorems compose so nicely, and there are theorems that don't fit any of the categories. (Plus, this is a very formalistic categorization, and it doesn't fully explain all theorems you can find "in the wild". For instance, ~pntlema is definitely written in "deduction style" but it does not fit the rigid definition given here because some hypotheses don't have a "ph ->" on them, and some hypotheses are conjunctions. It's certainly possible to extend the definition to accomodate this but at some point it turns into formal descriptive linguistics and I don't think that this is necessarily helpful for someone trying to learn the conventions.)

 

• closed form: A kind of assertion (theorem) with no hypotheses.

Typically its label has no special suffix. An example is unss, which
states: `((A ⊆C ∧B ⊆C) ↔(A ∪B) ⊆C)

• deduction form: A kind of assertion with one or more hypotheses

where the conclusion is an implication with a wff variable as the

antecedent (usually φ), and every hypothesis ($e statement) is either

(1) an implication with the same antecedent as the conclusion or (2) a

definition. 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
↔); class variable definitions are more common. 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 (φ). If an assertion is
in deduction form, and other forms are also available, then we suffix
its label with “d.” An example is unssd, which states12: `(φ →A ⊆
C) & `(φ →B ⊆C) ⇒ `(φ →(A ∪B) ⊆C)

• inference form: A kind of assertion with one or more hypotheses
that is not in deduction form (e.g., there is no common antecedent).
If an assertion is in inference form, and other forms are also available,

then we suffix its label with “i.” An example is unssi, which states:

`A ⊆C & `B ⊆C ⇒ `(A ∪B) ⊆C

The only thing I would change here is "one or more" -> "zero or more", in both deduction form and inference form. This will make inference form and closed form overlap for theorems with no hypotheses/assumptions at all, and that's okay, it meets the criteria for both.

[Benoit]

Starting from a scheme
  xxx: PHI => PSI
consider the two constructions:
  xxxA: ( phi -> PHI ) => ( phi -> PSI )
  xxxk: PHI => ( phi -> PSI )  [examples: mp1i; bj-a1k; idd; etc. see first two posts of this thread for several examples]
Starting from the scheme
  yyy: PHI => ( PSI -> CHI )
consider the two additional constructions:
  yyyi: PHI & PSI => CHI [the inference associated with yyy]
  yyyB: PHI & ( phi -> PSI ) => ( phi -> CHI )

I would opt to call only the xxxA operation "deduction form". The yyyB operation is only putting the phi on some of the hypotheses, which is occasionally useful (and can be applied to an arbitrary subset of the hypotheses, so it's not a uniquely defined operation) but not very common.

That's a detail, but yyyB is actually uniquely defined (look at the way yyyB is obtained from yyy, not from yyyi, which was the line just above it, which might explain the confusion).

Anyway, your proposal makes sense: the "deduction associated with" refers to the construction A, and also, by small abuse of language, to the construction iA when n=0 (i.e. when yyy has no hypotheses).  An example is ax-1: ph -> (ps -> ph) which gives a1i: ph => ps -> ph, and then a1id: ch -> ph => ch -> ( ps -> ph), but we label it a1d instead of a1id.  Collisions may appear when we want in set.mm the genuine A construction, and not the iA construction (which is the B construction when n=0).  This is the case of bj-a1k, which is the genuine "deduction associated with ax-1", while a1d is actually "the deduction associated with the inference associated with ax-1".  You seem to think that these cases are uncommon enough to still use this abuse of notation and terminology.  I do not have a strong opinion either way, but one has to be aware of this small abuse of notation and terminology (once settled, we'll edit the conventions accordingly).

We can add another operation, the "closed form" operation, like so:

From the scheme

xxx: PHI => PSI

we derive

xxxt: |- ( PHI -> PSI )

In my notation, PHI abbreviated PHI_1 & ... & PHI_n (but PSI and CHI are single metaformulas), so to define xxxt, I guess that you mean either the curried form (implication chain) or the uncurried form (one antecedent which is a conjunction); this is up to permutation of the PHI_i's (and association in the uncurried form), and suppose n>0, but these are minor variants.

Then xxxt always has 0 hypotheses, and xxxti == xxx if PSI is not an implication.

I do not understand why PSI being an implication makes a difference.  Maybe it's because by "xxxi", you mean the maximally iterated construction xxxi....i ?  Also, if there are n>1 hypotheses, things have to be stated a bit more precisely, but I think the intention is clear.

Benoît

[David A. Wheeler]

>
> On Mon, Nov 29, 2021 at 3:43 PM Benoit <benoit...@gmail.com> wrote:

> On Mon, Nov 29, 2021 at 10:30 AM David A. Wheeler <dwhe...@dwheeler.com> wrote:
> If we change deduction form to say "zero or more hypotheses" then
> the categories are no longer exclusive.
>

> On Nov 30, 2021, at 3:23 AM, Mario Carneiro <di....@gmail.com> wrote:
> I think this is not really the right way to look at it. They aren't categories that are meant to be exclusive, they are operations that can be applied to a theorem statement with various relations between them, like Benoit has shown. However, it is convenient for discussion purposes to name a statement after the operation that produced it, even if this isn't uniquely defined in some cases.

I *DID* intend for them to be exclusive; exclusive & complete categorizations are a lot easier to explain ;-).

I'm okay with them being non-exclusive, but then we need to expressly say so. The purpose of these categories is to help people categorize & use assertions.
More importantly, clear conventions make it easier for people to work together.

> If you want a way to pick out deduction form theorems from others, the obvious definition is the image of the deduction form operation (Benoit's xxxA operation). Stated another way, a deduction form theorem is one such that all (0 or more) hypotheses and the conclusion have the form "ph -> A" for the same wff metavariable "ph". This overlaps with "closed form" if you define it as a theorem with zero hypotheses, but I would say that anything in the intersection should be considered in deduction form, not closed form, and we can rationalize this by saying that a closed form theorem should not have any wff metavariable assumptions. fvexd is not in closed form because it has a useless metavariable hypothesis.

An overlap is fine. We can say, "These are not exclusive, because some statements with no hypotheses can be simultaneously in closed form and deduction form. By convention we typically refer to these as being in deduction form (since they are, even if they aren't exclusively in this form)."

> The categories are also not exhaustive. I would say that a theorem in inference form should not have an implication as the conclusion, or else it would not be in the image of the inference form operation (Benoit's yyyi operation). But then A |- ( B -> C ) is neither closed form nor inference form (and obviously not deduction form), and that's okay.

Under our current definitions this is clearly inference form. E.g., mmnatded.html says:
• Inference form: An assertion with hypotheses but no common antecedent is an "inference form"; it has a label suffix "i".

We can change our definitions, obviously. Why is being in the image of this yyyi operation is so important?
I'm honestly asking, I don't understand (maybe I'm missing the obvious).
To me it's helpful saying "this is in inference form", and I believe the algorithm for converting deduction form
to inference form works with *all* statements currently defined as being in inference form.
I don't see the big advantage in losing the ability to explain that.

> We're highlighting a particular structure of theorem that composes well, exactly because not all theorems compose so nicely, and there are theorems that don't fit any of the categories. (Plus, this is a very formalistic categorization, and it doesn't fully explain all theorems you can find "in the wild". For instance, ~pntlema is definitely written in "deduction style" but it does not fit the rigid definition given here because some hypotheses don't have a "ph ->" on them, and some hypotheses are conjunctions.

Huh? pntlema *does* meet the definition of "deduction form" that we've been using for many years. The current definition of "deduction form" allows hypotheses to be either (1) (ph-> ...) or (2) definitions (using = or <->). pntlema meets the current definition of deduction form, and I think it should *continue* to be considered an example of deduction form.

I also suggested expanding the definition of "deduction form" to allow a third case: not-free assertions without ( ph -> ...) statements.
We have statements such as "alrimd" that are technically not in deduction form merely because they use F/,
but are stated as being in deduction form. Let's expressly define them as being in deduction form.

> It's certainly possible to extend the definition to accomodate this but at some point it turns into formal descriptive linguistics and I don't think that this is necessarily helpful for someone trying to learn the conventions.)

Our *current* definitions allow for "definitions without a leading ph->", it's been that way for many years & it's clearly a useful construct.

I think it *is* helpful to clearly define these conventions. Clearly defining them makes it much easier for everyone to follow them. If they're too restrictive, let's identify reasonable relaxations and include them in the definitions.

I think that's particularly important for deduction form. How about this?"

• deduction form: A kind of assertion with zero or more hypotheses

where the conclusion is an implication with a wff variable as the
antecedent (usually φ), and every hypothesis ($e statement) is either

(1) an implication with the same antecedent as the conclusion, (2) a
definition, or (3) a statement of not-freeness ` F/ ` . {... existing text ...}

Are there any other relaxations for a theorem that would be sensibly
called "deduction form"? The only one I can think of is
where 1+ hypotheses are of the form:
( ( ph /\ ps ) -> ... )
Where "ph" is the common antecedent and ps are additions.
I'm not really advocating for it, I'm simply pointing out that
I think we add a few relaxations to the definition of
"deduction form" so that others who want to use the form will
easily know what they should be doing by convention.

--- David A. Wheeler

[David A. Wheeler]

> On Nov 29, 2021, at 3:43 PM, Benoit <benoit...@gmail.com> wrote:
>
> As for the questions raised by David: in my opinion, the best term to refer to hypotheses-free theorems is "hypotheses-free theorem", or "theorem with no hypotheses" (in other words, no special term is needed; you can add that it is also called a "closed form" theorem, and in a footnote, mention that within propositional calculus, it is sometimes called a tautology or simply a theorem, as opposed to an inference; however, it is more convenient for us to use "theorem" also when there are hypotheses).

It definitely gets confusing in some book sections & pages, e.g., mmnatded.html and mmededuction.html.

Currently they say:
> 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. (Informally we may call both of them theorems, but on this page we will stick to the strict definition.) An example of a deduction is the contraposition inference:

It might be easier to say something like this:

> Some theorems have one or more hypotheses; some have no hypotheses. Within propositional calculus, the term "deduction" is sometimes used for an assertion that has one or more hypotheses while "theorem" is only used for assertions with have no hypotheses. In metamath terminology, all proven assertions are termed theorems (whether they have hypotheses or not); to clearly identify a subset you can refer to "theorems without hypotheses" or "theorems with hypotheses" (the latter means "one or more hypotheses").

If with switch to "with" and "without" the other text would be easier to explain.

--- David A. Wheeler

[David A. Wheeler]

Quick addendum: We already note that we allow several cases & still call it deduction form:
http://us.metamath.org/mpeuni/mmnatded.html#special-cases

We could change the definition of "deduction form" to include them, & then note that in some
cases you could use mainly deduction form with a few special cases. It makes the definition
of "deduction form" longer, but it makes it much clearer what deduction form *is*.

--- David A. Wheeler

[Mario Carneiro]

On Tue, Nov 30, 2021 at 1:02 PM Benoit <benoit...@gmail.com> wrote:

Starting from a scheme
  xxx: PHI => PSI
consider the two constructions:
  xxxA: ( phi -> PHI ) => ( phi -> PSI )
  xxxk: PHI => ( phi -> PSI )  [examples: mp1i; bj-a1k; idd; etc. see first two posts of this thread for several examples]
Starting from the scheme
  yyy: PHI => ( PSI -> CHI )
consider the two additional constructions:
  yyyi: PHI & PSI => CHI [the inference associated with yyy]
  yyyB: PHI & ( phi -> PSI ) => ( phi -> CHI )

I would opt to call only the xxxA operation "deduction form". The yyyB operation is only putting the phi on some of the hypotheses, which is occasionally useful (and can be applied to an arbitrary subset of the hypotheses, so it's not a uniquely defined operation) but not very common.

That's a detail, but yyyB is actually uniquely defined (look at the way yyyB is obtained from yyy, not from yyyi, which was the line just above it, which might explain the confusion).

Ah yes I see that, I mean to say that I would prefer to view it as an application of the partial-A operation on yyy': PHI & PSI => CHI (where by partial-A I mean that you only put "ph ->" on some subset of the hypotheses, in this case PSI).

Anyway, your proposal makes sense: the "deduction associated with" refers to the construction A, and also, by small abuse of language, to the construction iA when n=0 (i.e. when yyy has no hypotheses).  An example is ax-1: ph -> (ps -> ph) which gives a1i: ph => ps -> ph, and then a1id: ch -> ph => ch -> ( ps -> ph), but we label it a1d instead of a1id.  Collisions may appear when we want in set.mm the genuine A construction, and not the iA construction (which is the B construction when n=0).  This is the case of bj-a1k, which is the genuine "deduction associated with ax-1", while a1d is actually "the deduction associated with the inference associated with ax-1".  You seem to think that these cases are uncommon enough to still use this abuse of notation and terminology.  I do not have a strong opinion either way, but one has to be aware of this small abuse of notation and terminology (once settled, we'll edit the conventions accordingly).

There is a reason that the case is uncommon, which is that it is explicitly discouraged to have theorems of the form ( A -> ( B -> C ) ) in deduction form (without good reason; as always, these are not hard and fast rules). For bj-a1k I'm fine with making an exception because it is (morally) in the propositional calculus section and there we allow anything at all, since you might need some crazy theorems during bootstrapping. But once things have settled down and you are doing a proof about locally compact manifolds or something you probably don't want to be using iterated implication.

 

We can add another operation, the "closed form" operation, like so:

From the scheme

xxx: PHI => PSI

we derive

xxxt: |- ( PHI -> PSI )

In my notation, PHI abbreviated PHI_1 & ... & PHI_n (but PSI and CHI are single metaformulas), so to define xxxt, I guess that you mean either the curried form (implication chain) or the uncurried form (one antecedent which is a conjunction); this is up to permutation of the PHI_i's (and association in the uncurried form), and suppose n>0, but these are minor variants.

I mean the uncurried form, probably left associated too (although df-3an makes things complicated to specify here). In the case where n = 0, we define xxxt == xxx, i.e. no implication is introduced.

 

Then xxxt always has 0 hypotheses, and xxxti == xxx if PSI is not an implication.

I do not understand why PSI being an implication makes a difference.  Maybe it's because by "xxxi", you mean the maximally iterated construction xxxi....i ?  Also, if there are n>1 hypotheses, things have to be stated a bit more precisely, but I think the intention is clear.

I am being loose with currying. Assume every implication is uncurried. Then if xxx is A |- ( B -> C ) then xxxt is |- ( ( A /\ B ) -> C ) and xxxti is A, B |- C.

On Tue, Nov 30, 2021 at 4:22 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:

> On Nov 30, 2021, at 3:23 AM, Mario Carneiro <di....@gmail.com> wrote:
> I think this is not really the right way to look at it. They aren't categories that are meant to be exclusive, they are operations that can be applied to a theorem statement with various relations between them, like Benoit has shown. However, it is convenient for discussion purposes to name a statement after the operation that produced it, even if this isn't uniquely defined in some cases.

I *DID* intend for them to be exclusive; exclusive & complete categorizations are a lot easier to explain ;-).

I'm okay with them being non-exclusive, but then we need to expressly say so. The purpose of these categories is to help people categorize & use assertions.
More importantly, clear conventions make it easier for people to work together.

The important part for naming is being able to recognize when a theorem is the deduction form counterpart of another theorem, or an inference form counterpart. For this purpose the rule is pretty clear: do lots of hypotheses and the conclusion have a wff metavariable assumption in them? Then it's deduction form. Have all the hypotheses been written as $e hyps instead of formulas before the ->? then it's inference form. Does it have a minimum of $e hypotheses and lots of hypotheses conjoined before the ->? Then it's in closed form. Is this exhaustive and handle all edge cases? Absolutely not, and that's okay.

> The categories are also not exhaustive. I would say that a theorem in inference form should not have an implication as the conclusion, or else it would not be in the image of the inference form operation (Benoit's yyyi operation). But then A |- ( B -> C ) is neither closed form nor inference form (and obviously not deduction form), and that's okay.

Under our current definitions this is clearly inference form. E.g., mmnatded.html says:
        • Inference form: An assertion with hypotheses but no common antecedent is an "inference form"; it has a label suffix "i".

We can change our definitions, obviously. Why is being in the image of this yyyi operation is so important?
I'm honestly asking, I don't understand (maybe I'm missing the obvious).
To me it's helpful saying "this is in inference form", and I believe the algorithm for converting deduction form
to inference form works with *all* statements currently defined as being in inference form.
I don't see the big advantage in losing the ability to explain that.

I would say that it is an inference, but not that it is in inference form. Indeed, I rather like having 0-ary inferences still be technically inferences, because it unifies terminology, even if we would generally refer to those as axioms or closed statements instead. Metamath generally does not distinguish between having 0 or more $e hypotheses in its architecture, unlike traditional FOL that has "axioms" and "inference rules" and never shall they meet, which I think is silly because one is clearly a special case of the other.

For "inference form" specifically, the idea is to support a proof strategy which is similar to deduction style but without the context, when you either don't need a context or can use dedth to simulate one. For example, ~strleun (like many automation lemmas) is in inference form, because the intent is to only ever have closed terms substituted for those variables, for which a context is not needed. If you put a "ph ->" on only the first hypothesis, then it would not compose properly - you can't pipe one strleun into another anymore, because it's not keeping the context empty. If the proof really required that, then it should switch to deduction form instead. Such a lemma I would call as neither inference form nor deduction form; it is violating the best practices of the form so it's nothing. It's an inference, but that's not much of a categorization because literally every $a/$t statement is an inference.

> We're highlighting a particular structure of theorem that composes well, exactly because not all theorems compose so nicely, and there are theorems that don't fit any of the categories. (Plus, this is a very formalistic categorization, and it doesn't fully explain all theorems you can find "in the wild". For instance, ~pntlema is definitely written in "deduction style" but it does not fit the rigid definition given here because some hypotheses don't have a "ph ->" on them, and some hypotheses are conjunctions.

Huh? pntlema *does* meet the definition of "deduction form" that we've been using for many years. The current definition of "deduction form" allows hypotheses to be either (1) (ph-> ...) or (2) definitions (using = or <->). pntlema meets the current definition of deduction form, and I think it should *continue* to be considered an example of deduction form.

I mean the xxxA definition given in this thread. pntlema is not in the image of that operation. Of course it is in "deduction form" in the colloquial sense, but defining what this is precisely will result in a complicated definition with lots of exceptions which is not helpful to people, that's what I keep saying.

I also suggested expanding the definition of "deduction form" to allow a third case: not-free assertions without ( ph -> ...) statements.
We have statements such as "alrimd" that are technically not in deduction form merely because they use F/,
but are stated as being in deduction form. Let's expressly define them as being in deduction form.

We also need to include deductions that include |- G Struct < M , N > as a hypothesis, and lots of other things that are intended to be proved in the empty context. If you really want to catalogue this maybe you should put the information on the definition instead of in an already over-large "conventions" page.

 

>  It's certainly possible to extend the definition to accomodate this but at some point it turns into formal descriptive linguistics and I don't think that this is necessarily helpful for someone trying to learn the conventions.)


Our *current* definitions allow for "definitions without a leading ph->", it's been that way for many years & it's clearly a useful construct.

I don't mean to exclude these from "deduction form" at all. I mean to not define "deduction form" precisely, but only at the level of a dictionary or glossary definition. That is, be comfortable with an incomplete characterization, focus on the important features. My comparison to linguistics was deliberate: mathematics is a language, and sometimes defining what words mean is hard. Lots of things come with shades of detail, and if you rush to include them all then you will get something no human can understand anymore.

 

I think it *is* helpful to clearly define these conventions. Clearly defining them makes it much easier for everyone to follow them. If they're too restrictive, let's identify reasonable relaxations and include them in the definitions.

Or, put enough weasel words in the definition that it is clear that it is not a precise definition.

I think that's particularly important for deduction form. How about this?"

• deduction form: A kind of assertion with zero or more hypotheses
where the conclusion is an implication with a wff variable as the
antecedent (usually φ), and every hypothesis ($e statement) is either
(1) an implication with the same antecedent as the conclusion, (2) a
definition, or (3) a statement of not-freeness ` F/ ` . {... existing text ...}

Are there any other relaxations for a theorem that would be sensibly
called "deduction form"? The only one I can think of is
where 1+ hypotheses are of the form:
( ( ph /\ ps ) -> ... )
Where "ph" is the common antecedent and ps are additions.
I'm not really advocating for it, I'm simply pointing out that

I think we add a few relaxations to the definition of

"deduction form" so that others who want to use the form will
easily know what they should be doing by convention.

Here are some relaxations that exist in the wild:

* Some hypotheses don't have "ph ->":
  * A e. _V

  * N e. NN

  * A = ...

* Some "A = ..." definitions *do* have "ph ->"

* Some hypotheses are conjunctions like ph -> ( A /\ B ) (pntlema is like this)

* The conclusion is ( ph /\ A /\ B ) -> C, i.e. some hypotheses are not written as $e hyps

* Hypotheses might be written as "ph -> A. x e. A ps" or "( ph /\ x e. A ) -> ps"

* There might be multiple wff metavariables, for example the conclusion is "( ph /\ ps ) -> B" and some of the hypotheses are "( ph /\ ps ) -> A" and others are "ph -> C"

What I am proposing is to *ignore this* for the purpose of a glossary definition, and instead try to capture the salient features; mmnatded can talk about the reasons for using deduction form and the tradeoffs of these various relaxations.

On Tue, Nov 30, 2021 at 4:41 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:

> On Nov 29, 2021, at 3:43 PM, Benoit <benoit...@gmail.com> wrote:
> As for the questions raised by David: in my opinion, the best term to refer to hypotheses-free theorems is "hypotheses-free theorem", or "theorem with no hypotheses" (in other words, no special term is needed; you can add that it is also called a "closed form" theorem, and in a footnote, mention that within propositional calculus, it is sometimes called a tautology or simply a theorem, as opposed to an inference; however, it is more convenient for us to use "theorem" also when there are hypotheses).

It definitely gets confusing in some book sections & pages, e.g., mmnatded.html and mmededuction.html.

Currently they say:
> 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. (Informally we may call both of them theorems, but on this page we will stick to the strict definition.) An example of a deduction is the contraposition inference:

It might be easier to say something like this:

> Some theorems have one or more hypotheses; some have no hypotheses. Within propositional calculus, the term "deduction" is sometimes used for an assertion that has one or more hypotheses while "theorem" is only used for assertions with have no hypotheses. In metamath terminology, all proven assertions are termed theorems (whether they have hypotheses or not); to clearly identify a subset you can refer to "theorems without hypotheses" or "theorems with hypotheses" (the latter means "one or more hypotheses").

In traditional parlance, a "theorem with hypotheses" would be called an "inference rule". Additionally, a "deduction" is synonymous for a proof. I don't think we need to define "deduction" at all, because our primary interest is in the "deduction theorem" and "deduction form", which are their own things.

Reading the text as it is on the page, I don't think we need to make any changes. It seems good enough for pedagogy. We don't need to be talking about all the edge cases in the very first sentence following the header "introduction to deduction".

Mario

[Alexander van der Vekens]

Unfortunately, I had no time to follow the whole discussion in detail, but I think David's proposal is acceptable:

• deduction form: A kind of assertion with zero or more hypotheses
where the conclusion is an implication with a wff variable as the
antecedent (usually φ), and every hypothesis ($e statement) is either
(1) an implication with the same antecedent as the conclusion, (2) a
definition, or (3) a statement of not-freeness ` F/ ` . {... existing text ...}

Maybe further results of this discussion can be documented on page/section http://us.metamath.org/mpeuni/mmnatded.html#special-cases. Can we insert this link also into set.mm?

Alexander