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
--
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/13ef02c8-01c9-45d9-8e61-6e77cf98da82n%40googlegroups.com.
