> On Nov 29, 2021, at 3:43 PM, Benoit <[email protected]> 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
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/262E99E7-2616-47D7-9B05-0E76B5D2300A%40dwheeler.com.
