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.

  • 3
    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
    – Philip Klöcking
    Oct 16, 2019 at 22:02
  • Thank you Philip. I will defiantly make those changes.
    – Kylie
    Oct 16, 2019 at 22:51

1 Answer 1


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!
    – Kylie
    Oct 17, 2019 at 1:15

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .