# Help with a Predicate Logic homework proof

I have a Predicate Logic argument I need to translate into the symbolism of predicate logic first and then I need to construct a proof in CP.

The argument is "Some wars are just. No war of aggression is just. Therefore, there are wars that are not wars of aggression. (Wx = x is a war, Jx = x is just, Ax = x is a war of aggression)."

I think I have it translated right, however, I am lost on how to construct the proof into CP.

This is how I have translated it (∃x) (Wx • Jx), (x) (Ax → ~Jx) ∴ (∃x) (Wx • ~Ax)

I need help with the CP proof. Any help would be very much appreciated!

I am also only allowed to use implicational rules like, MP, MT, HS, DS, CD, Simp, Conj, and Add. Equivalence rules such as DN, Com, As, DeM, Cont, Dist, Ex, Re, ME, MI. As well as QN, UI, EG, EI, UG.

• I would consider separating Ax into Wx and 'x is aggressive'. This way, you've got wars that are just and wars that are aggressive as two disjunct classes of wars Oct 16, 2019 at 22:02
• Thank you Philip. I will defiantly make those changes. Oct 16, 2019 at 22:51

Your translations are okay, but as Philip Klöcking♦ suggests, it would be better to use Ax to only mean x is of aggression, so that "x is a war of aggression" is represented: Wx • Ax and so forth.

Thus the proof becomes easy, so I'll just start you off.

1.|  (∃x) (Wx • Jx)        Premise
2.|_ (Ɐx) (Wx • Ax → ~Jx)  Premise
3.|[c]|_ Wc • Jc           Assumption (of Witness c ; aka Existential Instantiation)
4.|   |  Wc                • Elimination (aka Simplification)
5.|   |  Jc                • Elimination (aka Simplification)
6.|   |  Wc • Ac → ~Jc     Ɐ Elimination (aka Universal Instantiation)
7.|   |   |_ Ac            Assumption
:   :   :  ...
:   :
|  (∃x) (Wx • ~Ax)
• Thank you so much for your help Graham! Oct 17, 2019 at 1:15