2 ms·
I think that transporting proofs "for free" is of less interest since we're talking about formal, and so mechanised, proofs [1], but the matter of writing proof
by pron 4y ago
I think that transporting proofs "for free" is of less interest since we're talking about formal, and so mechanised, proofs [1], but the matter of writing proofs more naturally could definitely be a selling point. Can you point to some examples of that?
[1]: A computer can formally apply meta-logical transformations as a proof tactic, too. Why not put that into the logic if it can be done formally? To keep it simpler and easier for practitioners to learn. (Some systems, like TLA+, allow you to specify and prove higher order theorems that aren't expressible as formulas in the logic; so while you might not be able to express the general notion of an isomorphism in this way, you can express a theorem that can then be used by the proof assistant to transfer proofs based on isomorphisms with respect to some specific number of operators with some specific arities)
- pron 4y agoP.S. Come to think of it, there's another aspect I don't understand. The validity of a theorem depends only on the assumptions used in the proof (so, for example, if I have a formal set theory proof that depends only on group axioms, then it applies to all groups). That is not a property that is usually expressible in the the logic -- it's a property of the proof theory of the logic -- but it is nevertheless true. Not being a logician, I'm not interested in writing proofs about my logic's proof theory, I don't need to define new proof rules as I don't develop new logics, and my logic's proof assistant is free to rely on theorems about the logic's proof theory. What do I, as a practitioner, gain by making the proof theory part of the logic?