I missed this class on formal proofs and apparently the professor is not going over it any longer. I'm stuck on this current question in the textbook and I'm unsure on what the procedures are to solve a question of this sort. I have provided the slide where the rules are given but I have no clue how to implement these rules into this question. Not even sure how the steps to giving a formal proof even look like as the slides provided to me are not very descriptive. I would truly appreciate some help here. Thanks
[Math] Formal Proof – Propositional Logic
logic
Related Solutions
It looks like what you're concerned about here is how to choose between, specifically, proof systems for classical first-order logic, with examples being Hilbert systems, natural deduction or sequent calculus, all in various variants.
You're not speaking about how to choose between classical first-order logic and, for example intuitionistic logic, nor about how to choose a foundational theory to reason about with your logic (such as ZFC or NF set theory, or perhaps PA for formal number theory).
We can then answer your second question quickly: Yes, all of the proof systems for classical first-order logic are equivalent to each other. Otherwise they wouldn't be proof systems for classical first-order logic! Namely, a proof system for classical first order logic has to prove exactly those entailments that are logically valid according to the usual model-theoretic semantics of first-order logic.
Generally it is fairly easy to prove that two of these systems are equivalent. You can rewrite a proof in one of them to a proof in another by working piece for piece -- each axiom or inference rule in each of the systems corresponds to a small piece of reasoning that we can see once and for all that a given other system can express. Translating a proof piece for piece generally won't produce an elegant proof in the target system, but it certainly will be a valid proof.
Now for the first question, which has two answers.
The first is, you choose the system that makes what you want to do easy. Some properties of proofs are particularly easy to express in sequent calculus. Hilbert systems have long and unwieldy proofs but a relatively small and short definition of what a good proof is, which makes them useful for settings where you need such a formalization. Natural deduction is relatively close to how working mathematicians actually write proofs, at least compared to the other styles.
Which of these properties you put the most weight on depends on what you want to actually do with your formal proofs. And asking that question in the first place presupposes that you are going to do something with them other than write them down and hope you'll get bragging rights from doing so. This assumption is often not true.
This leads us to the second, real, answer: As a working mathematician you don't choose a proof system to work in at all. Unless you are specifically a mathematical logician and do mathematics about logic, you won't be in the business of producing formal proofs at all.
Actual mathematical proofs are written in English (or another comparable natural language, of course) -- not as formal sequences of symbols in a proof system. What is allowed in such a proof is something you'll supposedly get an intuition for as a byproduct of your study of mathematics. That's how everybody did it before formal logic was invented in the decades around 1900, and they achieved, by and large, a pretty good consensus about what is a convincing proof step and what is not. It is to a large degree how everybody still does it.
This informal agreement of which proofs are convincing or not comes first. The rules of formal logic are an attempt to reproduce the informal consensus in the shape of precise, checkable rules. They're remarkably successful at that, but it's still just a map, not the actual territory of mathematical thought.
Best Answer
For a) :
1) $(A \lor B) \land \lnot C$ --- premise
2) $\lnot C \to (D \land \lnot A)$ --- premise
3) $B \to (A \lor E)$ --- premise
4) $A \lor B$ --- from 1) by $\land$-elimination
5) $\lnot C$ --- from 1) by $\land$-elimination
6) $D \land \lnot A$ --- from 2) and 5) by $\to$-elimination
7) $\lnot A$ --- from 6) by $\land$-elimination
8) $A$ --- assumed [a]
9) $A \lor E$ --- from 8) by $\lor$-introduction
10) $B$ --- assumed [b]
11) $A \lor E$ --- from 10) and 3) by $\to$-elimination
12) $A \lor E$ --- from 4), 8)-9) and 10)-11) by $\lor$-elimination, discharging temporary assumptions [a] and [b]
13) $\lnot E$ --- assumed [c]
14) $A$ --- assumed [d]
15) $\bot$ --- contradiction : from 7) and 14) by $\bot$-introduction
16) $E$ --- assumed [e]
17) $\bot$ --- contradiction : from 13) and 16) by $\bot$-introduction
18) $\bot$ --- from 12), 13)-14) and 15)-16) by $\lor$-elimination, discharging temporary assumptions [d] and [e]
19) $E$ --- from 13) and 18) by RAA, discharging temporary assumption [c]
Note
In order to complete the proof, we need the rules for $\bot$ (as in the link referred into the above comment) :
and :
For b) :
1) $(A \to F) \land (F \to D)$ --- premise
2) $((M \lor H) \lor C) \to A$ --- premise
3) $\lnot (M \lor H) \land C$ --- premise
4) $A \to F$ --- from 1) by $\land$-elimination
5) $F \to D$ --- from 1) by $\land$-elimination
6) $C$ --- from 3) by $\land$-elimination
7) $(M \lor H) \lor C$ --- from 6) by $\lor$-introduction
8) $A$ --- from 7) and 2) by $\rightarrow$-elimination
9) $F$ --- from 8) and 4) by $\rightarrow$-elimination