Questions tagged [fitch]

Frederic Brenton Fitch (1908 – 1987) was an American logician who taught at Yale. He invented the Fitch-style for natural deduction. He is also famous for the paradox of knowability. The tag may also refer to natural deduction proof environments in Fitch-style calculus for giving and checking proofs.

Filter by
Sorted by
Tagged with
6 votes
3 answers

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

It's all in the question really. I am working on a proof in Fitch for a class, but I am very much stuck. I am proving the tautology that "(P → Q) ↔ (¬P ∨ Q)", and I have already finished half of it, ...
Zenreon's user avatar
  • 61
2 votes
1 answer

Contrapositive Fitch Proof

I can't seem to figure out how to get past this step. Any suggestions?
Grace's user avatar
  • 21
4 votes
4 answers

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

I have spent about 6 hours now trying to prove this using the Fitch system and I just keep going in circles! Attached is one of the 500 attempts :) I have a feeling it's done fairly simply and ...
Vika's user avatar
  • 81
4 votes
2 answers

Fitch Proof - LPL Exercise 8.17

I am currently finding the third part of this exercise (Conditional 3) difficult to prove. I was sure that my proof was correct, but the Fitch program is saying otherwise. I am finding it ...
arileah's user avatar
  • 41
3 votes
3 answers

Prove A ∨ D from A ∨ (B ∧ C) and (¬ B ∨ ¬ C) ∨ D ( LPL Q6.26) without using --> or material implication

This is a repeated question: Language Logic and Proof Q. 6.26 Using the natural deduction rules, give a formal proof of A ∨ D from the premises A ∨ (B ∧ C) (¬ B ∨ ¬ C) ∨ D ...
Billy Bob's user avatar
  • 131
2 votes
1 answer

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

I need a formal (Fitch) first order logic proof for: ∃x ∃y (P(x) ∧ P(y) ∧ x ≠ y ∧ ∀z (P(z) → (z = x ∨ z = y))) Given ∃x ∃y (P(x) ∧ P(y) ∧ x ≠ y) ∀x ∀y ∀z ((P(x) ∧ P(y) ∧ P(z)) → (x = y ∨ x = z ∨...
BobMiller's user avatar
2 votes
2 answers

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

I'm working on an assignment and I'm stuck on this proof. I feel like I'm on the right track but I can't find the way to prove the goal. A ^ B (A ^ ~C) --> ~D A -> ~C (B ^ E) --> (C v D) ~E I ...
fitch-is-killing-me's user avatar
0 votes
1 answer

Question about proving a set that is quantificationally inconsistent in PD+ (Finished the proof but want it to be checked)

Does ∃x(Nx & ~Nx) contradiction itself? Is there an error in my proof? Thank you
Stanley's user avatar
-3 votes
1 answer

Fitch Arrow Proofs [closed]

Using the FITCH program and the FITCH derivation rules you should make a proof or derivation of C10 from P5 through P11. P5: ∀x∀y(StrongPref(x,y)→ ¬StrongPref(y,x)) P6: ∀x∀y∀z((StrongPref(x,y)∧...
George P's user avatar