Philosophy Stack Exchange
Philosophy Stack Exchange

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.

For information about Frederic Fitch see the Wikipedia entry "Frederic Fitch": https://en.wikipedia.org/wiki/Frederic_Fitch.

For the knowability paradox see the following:

Brogaard, Berit and Salerno, Joe, "Fitch's Paradox of Knowability", The Stanford Encyclopedia of Philosophy (Winter 2013 Edition), Edward N. Zalta (ed.), URL = https://plato.stanford.edu/archives/win2013/entries/fitch-paradox/.

There are at least two Fitch-style proof checkers and associated textbooks:

99 questions
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, but now I must prove that "(¬P ∨ Q)" implies "(P →…
Zenreon
  • 61
  • 3
5
votes
3 answers

How can I prove a contradiction follows from P <-> Q and P -> ~Q?

I am so close to solving this problem: (Language Logic and Proof 8.36). https://i.stack.imgur.com/1zMnZ.jpg All I need to do to complete the proof is show that P <-> Q and P -> ~Q is a contradiction (the problem has a similar form to this) How can…
Jerry Qu
  • 125
  • 6
4
votes
3 answers

Disjunctive Syllogism in a Fitch Style System

I'm trying to prove an argument of the form: B ~(C & B) Therefore: ~C. I can expand out ~(C & B) into ~C OR ~B, and with the premise B, it is clear that ~C is the case. However, I'm having trouble proving this using a Fitch style system.…
Sinthet
  • 163
  • 3
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 straight-forwardly but I'm not too good at understanding…
Vika
  • 81
  • 5
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 particularly difficult to understand why my citing and rule…
arileah
  • 41
  • 1
  • 2
4
votes
2 answers

Fitch style disjunction elimination

I am having difficulty in formally proving a simple argument. Consider P(x) v Q(x) not P(x) ---------- Q(x) It is easy to see that the argument is indeed valid, but I cannot seem to prove it formally. Here is one attempt: P(x) v Q(x) not…
DrDeanification
  • 321
  • 1
  • 3
  • 10
3
votes
1 answer

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

How would a formal Fitch proof look like. I am given P(a) → ∀x(P(x) ∨ ¬(x = a)) to prove using Natural Deduction of predicate logic. I am confused on how to proceed with the proof. Please advice me on how to go about with this. Thanks in advance
Moey mnm
  • 47
  • 4
3
votes
3 answers

2 simple Formal Fitch Proofs

I'm having difficulty proving these. They seem obvious, but I can't figure how to set up formal proofs for them. Could anyone give me clues on how to start them? ¬(P∧¬Q) from the premise P→Q; ¬Q→(R→P) from the premise P∨Q. Thanks
35308
  • 125
  • 1
  • 8
3
votes
2 answers

Formal proof : predicate logic

This is what I need to prove formally: 1.∃x Cube(x) ∧ Small(d) . . . . Goal :∃x (Cube(x) ∧ Small(d)) I have already tried different ways, but I still can't prove the goal. 1. ∃x Cube(x) ∧ Small(d) 2. ∃x Cube(x) ∧Eilm1 3.Small(d) …
wenwen
  • 31
  • 1
3
votes
2 answers

LPL 10.26 - Fitch - How to use ∀ Intro and ∃ Elim?

I am using LPL (Language, Proof, and Logic, commonly known as LPL) and the bundled Fitch program. I am trying to solve problem 10.26: 10.26: ∀x Tet(b) ↔ ∃w Tet(b) Looks simple enough, as the null quantification means this is just: Tet(b) ↔…
user15247
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 The LPL textbook has not yet introduced material implication or the…
Billy Bob
  • 131
  • 1
  • 2
2
votes
1 answer

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

Is there anyone who could explain to me why these errors occur? It seems to me the rule was used properly.
sannelavinia
  • 21
  • 1
2
votes
1 answer

Contrapositive Fitch Proof

I can't seem to figure out how to get past this step. Any suggestions?
Grace
  • 21
  • 1
2
votes
1 answer

Fitch Proof - Arrow's logic of preferences

I've been stumped on this one question in particular for several days now and I'm hoping to get some help on where I'm going wrong. Given the following premises: ∀x∀y(StrongPref(x,y)→…
rzy
  • 29
  • 2
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 started by ^elim for A and B, then I started a subproof…
fitch-is-killing-me
  • 41
  • 3
1
2 3 4 5 6 7