Well, indeed I have the answer to this exercise but I don't understand some steps. From 6 to 17 are OK for me but from 2 to 5 and then when step 5 is again called in step 10 is something I don't get very well.

I mean, could you re use a formula from a conditional box from above in other one? I would never have thought that. enter image description here

  • 2-5) assumed "p to q", derived a contradiction and concluded with "not (p to q)". – Mauro ALLEGRANZA Nov 24 '19 at 9:03
  • 6-13) assumed q and derived "p to q" (this can be dona more simply by to-intro). Now this contradicts "not (p to q)" derived above in step 5) and we can conclude with p, and from it with "q to p" by to-intro. – Mauro ALLEGRANZA Nov 24 '19 at 9:06
  • Welcome to SE Philosophy! Thanks for your contribution. Please take a quick moment to take the tour or find help. You can perform searches here or seek additional clarification at the meta site. Don't forget, when someone has answered your question, you can click on the checkmark to reward the user! – J D Nov 24 '19 at 15:10

The symbol F stands for 'False' or 'Contradiction'. Negation is at times defined as "this implies a contradiction".

~P is equivalent to P => F

Your system reuses the Conditional Elimination and Introduction symbols (=>E, =>I), but the inferences are more commonly known as Negation Elimination and Introduction.

Just as we may infer F from P and P => F by Conditional Elimination, so too may we infer F from P and ~P by Negation Elimination.

|  P
|  P=>F
|  F     Conditional Elimination (=>E)

|  P
|  ~P
|  F     Negation Elimination  

Or basically: We may derive F from any two statements which contradict each other. Such as lines 5 and 10, ~(p->q) and p->q. Also line 1 ~((p->q)+(q->p) and 4 (and later 15) (p->q)+(q->p)

Likewise: Just as we may infer P => F when we can derive F under assumed P by Conditional Introduction, so similarly we may infer ~P when we can derive F under assumption of P by Negation Introduction. These are assumption discharge rules

|  |_ P    Assumption
|  |  :
|  |  F
|  P => F  Conditional Introduction (=>I)

|  |_ P    Assumption
|  |  :
|  |  F
|  ~P      Negation Introduction

Note: what your system calls RAA is more commonly known as Double Negation Elimination (DNE). (RAA is more usually where: we may infer P when we can derive F under assumption of ~P).

 1.|  |_ ~((p -> q) + (q -> p))    Assumption
 2.|  |  |_ (p -> q)               Assumption
 3.|  |  |  (p -> q) + (q -> p)    2, Disjunction Introduction
 4.|  |  |  F                      1,3 Negation Elimination 
 5.|  |  ~(p -> q)                 2-4 Negation Introduction
 6.|  |  |_ q                      Assumption
 7.|  |  |  |_ ~p                  Assumption
 8.|  |  |  |  |_ p                Assumption
 9.|  |  |  |  |  q                6 Reiteration
10.|  |  |  |  p -> q              8-9 Conditional Introduction
11.|  |  |  |  F.                  5,10 Negation Elimination
12.|  |  |  ~~p                    7-11 Negation Introduction
13.|  |  |  p                      12   Double Negation Elimination
14.|  |  q -> p                    6-13 Conditional Introduction
15.|  |  (p -> q) + (q -> p)       14 Disjunction Introduction
16.|  |  F                         1,15 Negation Elimination
17.|  ~~((p -> q) + (q -> p))      1-16 Negation Introduction
18.|  (p -> q) + (q -> p)          17 Double Negation Elimination

I mean, could you re use a formula from a conditional box from above in other one? I would never have thought that.

Yes. This is the Rule of Reiteration used on line 8. You can restate something from a lower context. Think of it as 'moving into the box', if you like.

Usually Reiteration is not needed to be explicitly used; you may just refer to statements from ancestral contexts.

Remember you cannot do the reverse. You cannot 'move out of the box'.


Assume ~ [ (p-->q) v (q -->p)].

Using DeMorgan, infer : ~ (p-->q) & ~ (q-->p)

Using &-elim, infer

(1) ~ (p-->q)

(2) ~ (q-->p)

Using ~ ( A& ~B) as a definition of material implication, and Double Negation infer

  • from (1) : p & ~Q

  • from (2) : q& ~p

Using &-intro, & commutativity and &-associativity, and finally &-elim, rearrange (p & ~q)&( q& ~p) to get the contradiction (p&~p).

Finally, using ~ intro, infer that the original assumption was false.

Double negation will then allow you to infer that the goal-statement was true.

  • Hi and thanks for replying but I am not allowed to use DeMorgan or similars. What I mean is that any further than MP, MT, &E, &I, vE, vI, ->, <->, RAA and Hyp rules are forbidden. That's why I still don't get the solution given. For me there's no point of 2-5 and from steps 7 and 8 I could get easlily a contradiction suitable for "p". Literal later used in 13 for "q->p". – daenius Nov 24 '19 at 16:18
  • @daenius.-are you allowed to use an equivalence for (X--> Y) ? – Saint James Nov 24 '19 at 22:01
  • 1
    what do you mean? "-X v Y" ? This kind of "quick" transformations or equivalences are not allowed. For example, if we use Modus Ponens (MP as above) is because we have this scenario: p, p->q, so we have q – daenius Nov 25 '19 at 8:32
  • @daenius.- This is a rather demanding logical system. How is it called? – Saint James Nov 25 '19 at 8:37
  • don't worry. I've found the solution. Indeed It was a little different from the image from above. Thanks anyway – daenius Nov 26 '19 at 17:41

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.