Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange
Join us in building a kind, collaborative learning community via our updated Code of Conduct.

a natural deduction proof environment in Fitch-style calculus for giving and checking first-order proofs (per Wikipedia)

3
votes
4answers
720 views

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 ...
2
votes
3answers
73 views

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

The only way I could think of to do this problem is reductio, but since the two biconditional terms are not contradictory, I am pretty stuck.
3
votes
2answers
358 views

LPL ( language proof and logic) - FITCH - 14.12

what's wrong with the last line in my proof? i can't understand the error on line 21 i wrote the important line of the proof : 18 - ∀z (Cube(z) → (z = c ∨ z = f)) 19 - ∃y (Cube(c) ∧ Cube(y) ∧ c ≠ ...
3
votes
4answers
172 views

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

Construct a proof for the argument: S → (R ∨ P), P → (¬R → Q) ∴ S → (Q ∨ R) I have gotten to the point in the illustration, but I am unable to figure out where to go from here. I get tricked up on ...
1
vote
4answers
100 views

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

I am wondering if I have completed this proof properly. I don't think I have it right. It's tricky! Conclusion: ¬∃x∀y[E(x,y) ↔ ¬E(y,y)] ¬¬∃x∀y[E(x,y) ↔ ¬E(y,y)] ∃x∀y[E(x,y) ↔ ¬E(y,y)] ¬E,1 ...
-1
votes
1answer
943 views

fitch proof chapter 13 exercise 13.49 [closed]

Does anyone know how to solve 13.49 ∃x P(x) ∀x ∀y ((P(x) ∧ P(y)) → x = y) = ∃x (P(x) ∧ ∀y (P(y) → y = x)) and 13.50 ∃x (P(x) ∧ ∀y (P(y) → y = x)) = ∀x ∀y ((P(x) ∧ P(y)) → x = y) I have big ...
3
votes
1answer
319 views

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 ∨...
2
votes
2answers
125 views

I am stuck on how to prove the contradiction of R(b,a) can anybody help me?

Here are some well-known properties of dyadic (2-place) relations: ∀xR(x, x) (Reflexivity) ∀x¬R(x, x) (Irreflexivity) ∀x∀y(R(x, y) → R(y, x)) (Symmetry) ∀x∀y(R(x, y) → ¬R(y, x)) (Asymmetry) ∀x∀y∀...
5
votes
4answers
341 views

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, ...
4
votes
2answers
198 views

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) ...
3
votes
2answers
1k views

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 ...
0
votes
1answer
823 views

Fitch Proof - Logic LPL 13.11

I am currently doing questions for my course from LPL Chapter 13.11. I have posted the screenshot of what I am trying to do. I am quite stuck and I can not think of a way to get to ~Tet(a). Any hint ...
5
votes
3answers
410 views

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). http://imgur.com/a/nzYCU All I need to do to complete the proof is show that P <-> Q and P -> ~Q is a contradiction (the ...
1
vote
3answers
1k views

Fitch Formal Logic Help 6.26

6.26 Premise: A v (B ^C) Premise: ~B v ~C v D Goal: A v D Prove it formally without using DeMorgan's Law.
1
vote
1answer
1k views

Logic – Deduction in Tarski's World (Fitch/LPL 13.36)

I am working on proving the following question: | ∀x [Dodec(x) → LeftOf(x, a)] | ∀x [Tet(x) → RightOf(x, a)] |––– | ∀x [SameCol(x, a) → Cube(x)] The question has the following rules: […] give a ...
3
votes
2answers
966 views

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 ...
2
votes
4answers
3k views

Conditional disjunction equivalence proof using FItch

Prove P v Q ⇔ ¬Q → P So far I have the obvious things... 1. P v Q _ | 2. ¬Q | _ | 3. | 4. | 5. | 6. | 7. | 8. P 9. ¬Q → P → Intro 2-8 I think the problem here is that I do not ...