On 08/06/2025 15:52, Mario Carneiro wrote: As I explain in the talk, you don't actually need depth > 1 since you can use conjunction instead. That's exactly the reason why this whole setup works pragmatically and doesn't require an infinite list of axioms. Instead of stacking things up as
ph -> a -> b -> c -> p, ph -> a -> b -> c -> q |- ph -> a -> b -> c -> (p /\ q) if you use ph /\ a /\ b /\ c -> p, ph /\ a /\ b /\ c -> q |- ph /\ a /\ b /\ c -> (p /\ q) then this is just a substitution instance of jca again. You use imp/ex in order to push and pop assumptions to the context but otherwise you never have to worry about larger depths. Ah, I missed the generality part. I only found the talk after I already completed my converter and didn't follow carefully. So the idea is to limit oneself to a certain flat kind of natural deduction proofs that can simulate deeper blocks via conjunction rules, to then be able to simulate those proofs with fewer translation rules. And this became a standard approach which people are satisfied with, so that nobody really needs a broader support for natural deduction. At least it makes sense to me now! Thierry Arnoux schrieb am Sonntag, 8. Juni 2025 um 17:59:55 UTC+2: > 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. I am under the impression that this post comes from a similar place as mine.. If the theorems around https://us.metamath.org/mpeuni/natded.html (which I've also seen before) are really meant as general tools for natural deduction based proof design, the page should probably mention this immediately (and then link to corresponding tutorials)? -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion visit https://groups.google.com/d/msgid/metamath/70607ea8-9542-4c73-8eb1-f05a297b41d9n%40googlegroups.com.
