Skip to main content
5 votes

Given p ⇒ q and m ⇒ p ∨ q, use the Fitch System to prove m ⇒ q

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 ...
virmaior's user avatar
  • 24.7k
4 votes

In Fitch, how does one prove "(P → Q)" from the premise "(¬P ∨ Q)"?

You are right : the correct way is to use Proof by cases (aka: Disjunction elimination): 1) Q --- assumed for the proof by cases [a-1] 2) P → Q --- from 1) by Conditional introduction 3) ¬P --- ...
Mauro ALLEGRANZA's user avatar
4 votes

Given p ⇒ q and m ⇒ p ∨ q, use the Fitch System to prove m ⇒ q

This is how I ended up solving it:
Vika's user avatar
  • 81
4 votes

How to prove : (( P → Q ) ∨ ( Q → R )) by natural deduction

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 ...
E...'s user avatar
  • 6,556
4 votes
Accepted

Symbolic Logic - Quantifier Proof (w/ Conditionals)

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(...
Mauro ALLEGRANZA's user avatar
4 votes
Accepted

How to Prove P(a) → ∀x(P(x) ∨ ¬(x = a)) using Natural Deduction

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 ...
Adam Sharpe's user avatar
  • 3,844
3 votes

Language Logic Proof Question: ¬∃x∀y[E(x,y) ↔ ¬E(y,y)]

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" ...
Frank Hubeny's user avatar
  • 19.5k
3 votes
Accepted

LPL ( language proof and logic) - FITCH - 14.12

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 =...
Mauro ALLEGRANZA's user avatar
3 votes

In fitch, S → (R ∨ P), P → (¬R → Q) ∴ S → (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 ...
Bram28's user avatar
  • 2,719
3 votes

In fitch, S → (R ∨ P), P → (¬R → Q) ∴ S → (Q ∨ R)

Hint 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 ...
Mauro ALLEGRANZA's user avatar
3 votes

Formal proof : predicate logic

I would do the following: 1. ∃x Cube(x) ∧ Small(d) 2. ∃x Cube(x) ∧Elim1 3. Small(d) ∧Elim1 4. | Cube(z) A 5. | Cube(z) ^ Small(d) ^Intr 3,4 6. | ∃x(Cube(x) ^ Small(d)) ∃Intr 5 ...
virmaior's user avatar
  • 24.7k
3 votes

Fitch Proof - LPL Exercise 8.17

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 B ...
virmaior's user avatar
  • 24.7k
3 votes
Accepted

Does rejecting the law of the excluded middle mean rejecting it for all propositions or only for those one cannot derive?

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 ...
Arno's user avatar
  • 978
3 votes

Fitch Proof by Contradiction help

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 ...
Graham Kemp's user avatar
  • 2,356
3 votes
Accepted

How to prove ‘∃xP(x)’ from ‘¬∀x(P(x)→Q(x))’

Resolved! I realised that I was going nowhere by assuming the opposite of what I was given as premise... I obviously had to assume the opposite of what I was trying to prove:
35308's user avatar
  • 125
3 votes

In Fitch, how does one prove “P” from the premise “(¬P ∨ Q)→P”?

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 | | : ...
Graham Kemp's user avatar
  • 2,356
3 votes

Fitch Proof Question

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) ...
Graham Kemp's user avatar
  • 2,356
3 votes
Accepted

Solving a proof in which the goal is the negation of a variable in Fitch

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. ...
Frank Hubeny's user avatar
  • 19.5k
3 votes

Why is the use of the ND rule ∃E not correct in this proof?

Existential Elimination requires that the witness (a) does not occur in the conclusion or in any undischarged assumptions. At those points, you have an undischarged assumption that includes a on line ...
Graham Kemp's user avatar
  • 2,356
2 votes

In Fitch, how does one prove "(P → Q)" from the premise "(¬P ∨ Q)"?

Since you seek to prove that a disjunction entails a conditional, therefore your strategy ought be to: use disjunction elimination and, in each case, conditional introduction, if you can. |_ ~p v q ...
Graham Kemp's user avatar
  • 2,356
2 votes

In Fitch, how does one prove "(P → Q)" from the premise "(¬P ∨ Q)"?

Using the Fitch-style natural deduction proof editor and checker I can write the following proof: Line 1 contains the premise. Since we ultimately want upon assuming "P" to get "Q", I assume "P" on ...
Frank Hubeny's user avatar
  • 19.5k
2 votes

prove: ∃x ∃y (Cube(x) ∧ Cube(y) ∧ x ≠ y ∧ ∀z (Cube(z) → (z = x ∨ z = y)))

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). Assume: [A] P(z) and unpack the first ...
Mauro ALLEGRANZA's user avatar
2 votes

How do I apply existential elimination to the following Fitch proof?

Here is a shorter proof than the one provided in an answer: https://philosophy.stackexchange.com/a/42928/29944 It is similar to the first 9 lines of this proof, but proceeds with universal ...
Frank Hubeny's user avatar
  • 19.5k
2 votes

How do I apply existential elimination to the following Fitch proof?

I have added what I think is a solution in Fitch Any comments would be appreciated. My attempt seems much longer than the Stanford Proof (8.3), which talks about "the power of free variables". I ...
Patrick Browne's user avatar
2 votes

Given p ⇒ q and m ⇒ p ∨ q, use the Fitch System to prove m ⇒ q

m => p|q So either m => q and it's done, either m => p, and since p => q, m => q. Given that and the fact that you know how to make a Fitch System (I don't exactly) you can do it easily. basically, ...
Sianurh's user avatar
  • 29
2 votes

Prove ¬∃x ∀y (E(x, y) ↔ ¬E(y, y)) given no premises

E(x,y) <-> ¬ E(y,y) is clearly false if x and y are the same, because then the statement becomes E(x,x) <-> ¬ E(x,x). Whatever we choose for x, E(x,y) <-> ¬ E(y,y) is not true for all y, ...
gnasher729's user avatar
  • 5,630
2 votes

Prove ¬∃x ∀y (E(x, y) ↔ ¬E(y, y)) given no premises

Smells like Russell's Paradox ... Anyway, yes, you totally had the right idea: proof by contradiction! And the two conditionals will contradict as long as you instantiate them with the same constant ...
Bram28's user avatar
  • 2,719
2 votes

Given p ⇒ q and m ⇒ p ∨ q, use the Fitch System to prove m ⇒ q

You already know p → q. You just need to deduce q → q, enabling you to eliminate the disjunction to conclude q as desired. As: p ˅ q, p → q, q → q Ͱ q 1.| p → q : premise 2.|_ m → (p ˅ q) : ...
Graham Kemp's user avatar
  • 2,356

Only top scored, non community-wiki answers of a minimum length are eligible