(A) : For the left-to-tight direction we have :
1. P v Q
| 2. ¬Q --- assumed 
| 3. P --- assumed  for v-Elim
| 4. P --- from 3
| 5. Q --- assumed  for v-Elim
| 6. ⊥ --- from 2 and 5 by →-Elim (recall that : ¬Q is abbrev for Q → ⊥)
| 7. P --- from 6 by ⊥-Elim
| 8. P --- from 3-4 an 5-7 with 1 by v-Elim, discharging  and [...
HINT: I'll sketch the derivation. Since the theorem is a conditional, try using conditional proof/conditional-introduction by assuming P(a) and trying to derive ∀x(P(x) ∨ ¬(x = a)) from it. Here, to derive it, I would try an indirect proof by assuming the negation ¬∀x(P(x) ∨ ¬(x = a)) and trying to derive a contradiction. Use quantifier equivalence rules to ...
This must be a typo in the text book: in the case that ∀x: Tet(x) ∧ ¬Cube(x) the premises are both true (provided there is at least one x), but the conclusion obviously does not hold.
However, you can prove that the promises entail ∃x: Tet(x).
You are right : the correct way is to use proof by cases:
1) Q --- assumed for the proof by cases [a-1]
2) P → Q --- from 1) by →-intro
3) ¬P --- assumed for the proof by cases [a-2]
4) P --- assumed [b]
5) contradicition !
6) Q --- from 5)
7) P → Q --- from 6) by →-intro, discharging [b]
and it is done.
Here's a more elegant solution:
I used http://proofs.openlogicproject.org/ to do the proof.
We have M -> P v Q and we have P -> Q
this means that if we get P, we also get Q.
Also our conclusion is a conditional which means conditional introduction is a good way to get that form of conclusion.
begin by assuming M -- since this is the left side of ...
Since the argument has no premises, we must start with an assumption, either for reductio or for conditional proof. In this case, conditional proof would not work, so we have to go with reductio. So we start with:
1. | ~((P→Q)∨(Q→R)) assumption
Since we're going for reductio, we need to derive a contradiction. Since all we've got is this assumption, ...
You have to use or-elim on 1) considering two separate cases.
1st case : Dodec(x) and Large(x), from which, with 3) and assuming Small(x), derive a contradiction and then FrontOf(x,c).
2nd case Cube(x) and Small(x), from which, with 2), derive FrontOf(x,c).
I agree with your concern : the exercise is proposed before the explanation of the inference rules for the quantifiers : thus, we are not requested to use them.
The exercise asks to prove that the biconditional : ∀x Tet(b) ↔ ∃w Tet(b) is a logical truth, i.e. that
the two sides of the biconditional are logically equivalent (2nd ed : 2011, page 286).
Fitch is correct.
First, you are falling for the formal fallacy affirming the consequent in your subproof at 11-13 to generate the contradiction. Denying the antecedent looks like:
A → B
In your case ,
~Q → ~P
Second, you are discharging the subproof incorrectly. At 10, you assume Q, but at 15 you discharge as P → Q. ...
| 1) A ∨ (B ∧ C) --- premise
|_ 2) (¬ B ∨ ¬ C) ∨ D --- premise
| |_ 3) A --- assumed [a] from 1) for ∨-elim
| | 4) A ∨ D --- from 3) by ∨-intro
| |_ 5) (B ∧ C) --- assumed [b] [from 1) for ∨-elim
| | |_ 6) D --- assumed [c] from 2) for ∨-elim
| | | 7) A ∨ D --- from 6) by ∨-intro
| | /
| | |_ 8) (¬ B ∨ ¬ C) --- assumed [d] from 2) for ∨-...
Here is a proof using a Fitch-style, natural deduction proof checker.
To make well-formed sentences I had to rewrite some of the names used in the OP's example. In place of "E", I used "P", since "E" is a symbol for the existential quantifier in this proof checker. Also the notation in this proof checker is more compact. For example, "E(x,y)" became "Pxy"....
Assume S and derive R ∨ P from 1st premise.
Now two sub-proofs, for ∨-elim:
1) Assume R and derive Q ∨ R by ∨-intro, and it is done.
2) Assume P and derive ¬R → Q from 2nd premise.
Now use R ∨ ¬R (Excluded Middle) for a new ∨-elim:
2.1) Assume R and derive Q ∨ R.
2.2) Assume ¬R and derive Q from ¬R → Q and then derive Q ∨ R.
Having derived Q ∨ R ...
Like Pe I did a proof by contradiction ... and by making the assumption of ~(Q v R) earlier in the proof (and exploiting Fitch's shortcut of allowing ~ Intro to be used while getting rid of the negation of the assumption), I was able to shave off a few lines:
What to me is really interesting about this proof is that the subproof starting with R is used ...
18 - ∀z (Cube(z) → (z = c ∨ z = f))
19 - (Cube(c) ∧ Cube(y) ∧ c ≠ y) ∧ ∀z (Cube(z) → (z = c ∨ z = f)) --- from 4 and 18 by ∧-intro
20 - ∃x ∃y [(Cube(x) ∧ Cube(y) ∧ x ≠ y) ∧ ∀z (Cube(z) → (z = x ∨ z = y))] --- from 19 by ∃-intro twice
20 is derived under the two assumptions 3 and 4 made for two ∃-elim's with terms c and f. They are not present in 20; thus, ...
Rejecting the law of excluded middle is already a somewhat strong committment for constructivists - I think the generally agreed upon is only to not accept it. [If you are confused because you do not see the distinction, you are using the law of excluded middle!] This means that while one does not assume that the law of excluded middle holds, one also does ...
The rules of inference are named as they are for a reason.
When feel the need to raise a context to derive a target, determine what rule of introduction you will need to deduce the target. That will tell you what assumption you might need to raise and what conclusion you will need to derive.
When the target is a conditional, like, Indiff(a,b) → ~(...
In Fitch, how does one prove “P” from the premise “(¬P ∨ Q)→P”?
One assumes not-P and uses a Reduction To Absurdity proof.
|_ (~P v Q) -> P Premise
| |_ ~P Assumption
| | : :
| | : :
| | : :
| ~~P Negation Introduction
| P Double Negation Elimination
P → Q, R ˄ S |- ¬P → (Q ˄ R) is not syntactically valid.
An assumption of ¬P will not allow you to eliminate the conditional in P → Q to derive Q .
Is there a typo?
P → Q, R ˄ S |- P → (Q ˄ R) is valid.
1| P → Q
2|_ R ˄ S
3| R ˄E, 2
4| |_ P
5| | Q →E, 1,4
6| | Q ˄ R ˄I, 3,5
7| P → (Q ˄ R) →I, 4-6
Since one has to derive ¬E one place to start would be E as an assumption. That strategy would attempt to derive a contradiction somewhere after the assumption and then derive ¬E which is the goal.
The rest of the steps I think you are aware of. I am including the results of the proof checker. The proof checker you are using is likely different and you ...
To eliminate the disjunction, prove your conclusion (here P) for each terms of the disjunction in sub proofs. If the conclusion holds for each terms separately, then it holds for the disjunction of them too.
Alternatively, you can prove P by drawing a contradiction from not-P (then again you'll have to show that each term of the disjunction entails a ...
Here are a couple options:
If you have a double negation rule, you can turn B into ~~B. Then you can use a disjunctive syllogism rule together with (~C v ~B) to get ~C.
You can try an indirect proof, where you assume C, and then conjoin it with B to get (C & B), which yields a contradiction with line 2, entailing ~C.
The proof is going to be a big v-elim on A v (B ^ C). You could just have easily done the v-elim on (~B v ~C) v D, however. I've tried to make the notation match what's in the textbook, though I admit that it is rather atrocious. Might be worthwhile to copy it out by hand just so you can see how the scoping works for the subproofs.
1. |A v (B ^ C) ...
Use ∃-elim twice with 1st premise to get :
P(a) ∧ P(b) ∧ a ≠ b.
Use ∀-elim with 2nd premise to get :
(P(a) ∧ P(b) ∧ P(z)) → (a = b ∨ a = z ∨ b = z).
and unpack the first above to get :
and the second above to get:
¬ (a=b) → (a = z ∨ b = z)
and by modus ponens (i.e. →-elim) derive:
a = z ∨ b = z.
By →-intro (...