3 ms·
How proofs work is pretty simple, and you don't need types to do natural deduction. As usual, types only complicate the picture. Here is a more straightforward
by auggierose 1y ago
How proofs work is pretty simple, and you don't need types to do natural deduction. As usual, types only complicate the picture. Here is a more straightforward and natural way to treat natural deduction: http://abstractionlogic.com http://abstractionlogic.com .
- runeblaze 1y agosure of course one does not need types to do natural deduction… if you throw what you showed me to your average maths undergrad in the US they will get confused — I truly don’t see how proofs are simple
- auggierose 1y agoIt is a matter of presentation and what people are used to. In particular, in abstraction logic, in the simplest (and most general!) case, you only have these proof rules: Axiom, Assume, AddAnte, BindAnte, FreeAnte, InferAnte. If we just focus on this case, we can choose simpler names for these rules: Axiom, Assume, Add, Bind, Free, Infer. That's it. That is all there is to proof.