3
$\begingroup$

I have 3 premises

A. ∀x: S(x) → ¬∃y: K(y, x)
B. ∃x: ∃y: K(x, y)
C. ∃x: ¬S(x)

I'm trying to prove

(A ∧ B) → C

So I do the proof and eventually get the conclusion

((∀x: S(x) → ¬∃y: K(y, x)) ∧ (∃x: ∃y: K(x, y))) →  (∃x: ¬S(x))

Which I know is (A ∧ B) → C, but in a formal proof I can't just replace the individual propositions in the above statement with A, B, and C in order to get the conclusion I desire right?

So, I'm unsure of whether I have to start with the premises:

A ↔ ∀x: S(x) → ¬∃y: K(y, x)
B ↔ ∃x: ∃y: K(x, y)
C ↔ ∃x: ¬S(x)

In order to derive (A ∧ B) → C ? Or if I can just replace swap in the corresponding A, B, and C and get the conclusion.

Also, if I do have to start with a premise like: A ↔ ∀x: S(x) → ¬∃y: K(y, x) am I allowed to separate the ∀x: S(x) → ¬∃y: K(y, x) part that I need and work on it?

$\endgroup$
  • $\begingroup$ What are you allowed to use to prove a formula? $\endgroup$ – Taroccoesbrocco Sep 26 '19 at 21:19
  • $\begingroup$ @Taroccoesbrocco I don't quite understand what you're asking. $\endgroup$ – Jeffrey D Sep 26 '19 at 21:30
  • $\begingroup$ @Taroccoesbrocco In normal math I know I could just say A = (x + 2), B = (x + 3), then when I get to (x+2) + (x+3) I could write A + B. But this is a formal proof, and I'm not certain if it's allowed. $\endgroup$ – Jeffrey D Sep 26 '19 at 21:31
5
$\begingroup$

They are using the letters $A,B,C$ to represent entire propositions (including their respective quantifiers) and give you an idea of the form of the statement they want you to prove. You proved exactly what they asked you to prove. You may substitute the letters $A,B,C$ into your conclusion, if you wish, but it is not necessary. Again, I believe they were using the letters to give you an idea of what to prove. Nice work!

| cite | improve this answer | |
$\endgroup$
1
$\begingroup$

If $A$, $B$ and $C$ are premises, then one can derive $(A\land B)\to C$ as follows:

enter image description here

Notice that one only needs $C$ as a premise. So something else is going on here.

As RyRy the Fly Guy suggested they may want you to take as premises the first two statements and derive the third statement from those two. Here is how such a proof might look:

enter image description here


Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.