On 08/06/2025 15:52, Mario Carneiro wrote:
On Sat, Jun 7, 2025 at 8:20 PM [email protected]
<[email protected]> wrote:
In particular, I noticed that Mario Carneiro gave a talk
<https://us.metamath.org/other.html#natded> on "*Natural Deduction
in the Metamath Proof Language*", but it doesn't seem to have
gained much traction; at least I do not see many theorems in
Metamath that would be crucial to apply proof design based on
natural deduction.
To the contrary, I would say that the idea behind that talk was quite
influential on set.mm <http://set.mm>; writing large theorems in
"deduction style" basically became the default, replacing the more
limited usage of inference style + weak deduction theorem as well as
"theorem style" closed inferences which do a lot of context
manipulation. Personally I consider writing deduction proofs in
metamath / set.mm <http://set.mm> to be basically a solved problem.
This was also my first reaction.
As far as I'm concerned, virtually all of my recent additions are
deduction style.
Here is a discussion which basically calls for even more deduction from
theorems: https://github.com/metamath/set.mm/issues/3990, with some
strong support.
A quick look at changes-set.mm will show that recently, we've been
moving a lot of deduction style proofs to the main part of set.mm (those
with labels ending in `d`)
BR,
_
Thierry
--
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 visit
https://groups.google.com/d/msgid/metamath/286aace6-9d3c-47be-b646-d62c9ceb0296%40gmx.net.
