Is there little more advanced alternative of "DC Proof"? (it's a proof assistant)

Question

So far I inspected several proof assistant:

1.DC Proof. The closest to my ideal yet still not exactly what I want (although I still have some hope that maybe I'm missing something). I'm glad that it can handle propositional logic, predicate logic and set theory (for example, it can prove non-existence of the universal set, while it's impossiblee to make such proof in "Proof Designer"), yet it seems to miss some logical rules of replacement and interference. For example, commutativity and associativity of some logical opreators, constructive dilemma, destructive dilemma, hypothetical syllogism, disjunctive syllogism, exportation, modus tollens, absorption, modus ponendo tollens. I guess at the end it's possible to finish a proof without all it, but they make it easier (at the least for me). Plus "Undo" command allows to take only one step back.

2.Coq. I suppose that this monstruosity can do everything that I can ever thinking of, but this is just too cool for me. In short, I don't feel to be educated enough to even start learning how to use it.

3.Proof Designer. Can be useful, but seems like it's suffering from overspecialization. It's created for set theory and doing logical proofs in it is perversion with big letter P.

4.Minlog. As far as I understand, this proof assistant uses so-called "minimal logic". In other words, not only I need to learn new kind of logic, but this logic is less powerfull? Sorry buddy, but you're out.

Answer 1

I think that better alternative for DC Proof (and to even far more advanced proof assistants, like Coq) is method of structured proofs described in the following pappers:

https://www.microsoft.com/en-us/research/publication/write-21st-century-proof/

https://www.microsoft.com/en-us/research/publication/how-to-write-a-proof/

I came to such conclusion after playing around with DC Proof. The reasons are following:

1.There are always limits to expressiveness of languages of proof assistants. For example, in DC Proof you can't directly apply constructive dilemma, although you can deduce that such logical construction is valid for given statements, but it's tedious.But even if DC Proof could do it, it would still be hard, for example, to formalize geometrical proofs from school course of geometry. In the end it means that either proof is impossible (like you can't prove that the Universal set doesn't exist in "Proof Designer" because you're forbidden from even mentioning the Universal set) or a proof becomes more complicated.

2.I want to do my proofs purely for myself, in order to better understand given theorem/lemma. So if some things are just TOO obvious for me it would be waste of time to formally explain in all details why it must be true. Although there is danger of overconfidence, but I think that it's possible to find the right balance between reasonable confidence and always describing in all details what and why is true. Strict formalization wouldn't allow such shortcuts.

Answer 2

I have just confirmed that the following are derivable in the latest version of DC Proof 2.0 (released 2019-09-14) available free at my homepage:

• commutativity and associativity of AND (&) and OR (|)
• constructive dilemma
• destructive dilemma
• hypothetical syllogism
• disjunctive syllogism
• exportation
• modus tollens
• absorption
• modus ponendo tollens

To use a theorem derived in another proof, I use the Axiom Rule to insert that theorem at the beginning of a new proof. I also use it to introduce definitions. An axiom introduced by the user in this way (as opposed a built-in axiom) differs from a Premise only in that it cannot be discharged, and that it must be inserted at the beginning of a proof before any Premise is introduced.