I think Jim and Norm are right, so I will adapt the ~conventions
accordingly, and add a sentence about the special case "zero hypotheses".
On Monday, November 29, 2021 at 4:59:50 AM UTC+1 Norman Megill wrote:
> On Sunday, November 28, 2021 at 1:23:01 PM UTC-5 Benoit wrote:
>
>> Jim: indeed,
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
I would be happy to see this idea explored in a mathbox. Even if we don't
import it and change our "official" FOL= axiom system on the MPE home page
(which is the result of a lot of fine tuning over many years and admittedly
somewhat biased by my personal preferences), it can still exist as an
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
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
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
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
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
