How to start with verifying a formal proof programmatically?

Question

I heard the terms "theorem provers" and "proof assistants" tossed around before (which I assumed to be the same up until a couple seconds ago), and also of Coq, Idris, Agda, TLA+ (don't know which aforementioned camps they belong to), but are completely clueless where I should begin to verify a formal proof programmatically that I just came up with.

For context, I started out with Shawn Hedman's "A First Course in Logic: An Introduction to Model Theory, Proof Theory, Computatibility, and Complexity" to learn the very basics. When I got to "Proof by Contradiction" derivation rule, I tried to derive the conclusion from the premises as an exercise, but I got there via a different path, and want to make sure that the steps are sound.

So what language / tool should I dive into first to verify the formal proofs below? Or am I totally misguided and there's something fundamental that I'm missing?

For example, this is from the book:

Premises: 𝓕 ∪ {F } ⊢ G
                  𝓕 ∪ {F } ⊢ ¬G
Conclusion: 𝓕 ⊢ ¬F

Line	Statement	Justification
1	𝓕 ∪ {F} ⊢ G	Premise
2	𝓕 ∪ {¬G} ⊢ ¬F	Contrapositive applied to 1
3	𝓕 ∪ {F} ⊢ ¬G	Premise
4	𝓕 ∪ {¬¬G} ⊢ ¬F	Contrapositive applied to 3
5	𝓕 ⊢ ¬F	Proof by cases applied to 2 and 4

and this is the route I took (which I'm pretty sure is wrong):

Line	Statement	Justification
1	𝓕 ∪ {F} ⊢ ¬G	Premise
2	𝓕 ∪ {F} ⊢ (¬G v ¬F)	V-introduction applied to 1
3	𝓕 ∪ {F} ⊢ (G → ¬F)	→-definition applied to 2
4	𝓕 ∪ {F} ⊢ G	Premise
5	𝓕 ∪ {F} ⊢ ¬F	→-elimination applied to 3 and 4
6	𝓕 ∪ {¬F} ⊢ ¬F	assumption
7	𝓕 ⊢ ¬F	Proof by cases applied to 5 and 6

Again, I'm not asking to you to tell me if my solution is good or bad, but a learning path on how I can check my work going forward. Thank you!

---

update (7/19/2023): I guess this CS stack exchange thread, Introduction into first order logic verification, answers my question, but I'm not far enough into my studies to decide.

Answer 1

In my opinion, it is quite difficult to answer your question because it is very broad. However, I'll try point out several facts that might help you choose a course of action. I will cite the proof assistants (PAs) I know or have been working with.

You correctly stated that mechanical theorem provers (MTPs) are proof assistants (PAs), and probably suspected that they are suitable to their own specific fields. In fact, this is the core of the argumentation: there are many proof assistants, and, depending on their purpose, they can turn out to be suitable for proving a theorem (or not; sometimes they can get very awkward at that).

You mentioned Coq and Agda, and, to the best of my knowledge, these are suitable in the context of mathematical theorem proving. That is, theorem proving oriented towards pure math or logic. On the other hand, Prototype Verification System (PVS) is suitable to verify theorems that represent software safety conditions.¹

There are three parameters that help understand the affinity of a PA w.r.t. theorem proving:

1. the logic employed,
2. its mathematical library, and
3. degree of automation.

1. The logic employed

You should choose a tool that supports an appropriate logic. That is, one that allows you to construct the kind of proofs you want. For instance, Coq uses intuitionistic higher-order logic, and such power allows to prove theorems that are out of grasp of PAs simply employing higher-order logic. If you are willing to prove simple properties using first-order logic only, this is not a parameter you should worry about.

2. The mathematical library

It is easy to see that proving everything from scratch would require years of work, so consequently, the PA providing a heterogeneous library will make it easier to prove facts of interest. This is especially true when you are proving abstract facts, requiring sophisticated theories. Coq is an example of PA having a rather slim standard library; I recall having problems proving simple facts involving bits and sets of objects. The same problem did not arise when I used PVS.

3. Degree of automation

In general, a proof's purpose is to show that a fact holds and explain why it is the case. In this sense, PAs like Twelf and Coq are very useful, because the proof is carried out by the human prover with the help of the computer, and the result is very informative. In contrast, software safety conditions (correctness proofs) are mathematically shallow, and don't tend to shed light on the problem at hand; in general, they are more interested in knowing whether the program is correct, rather than unfolding several tens of repetitive steps. In most cases, such proofs unfold for hundreds of steps, and very few cases are interesting...

---

Depending on the type of proof you want to get, you need to choose the proper tool. For example, PVS would prove your example automatically using automated decision strategies, but the proof itself would be of no value. On the other hand, Coq would force you to carry out every single step, providing a complete yet meticulous proof.

Last but not least, comes the proof system used by the PA. Coq and many other PAs employ natural deduction, a proof system that I do not enjoy much myself. PVS on the other hand employs sequent calculus, a much simpler and clearer proof system, if you ask me.

I my opinion, you should first figure out, what you want to prove and, most importantly, why. Answering this question will allow you to avoid using PAs that are totally out of scope or that will make you dislike mechanical TP.