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.
F stands for 'False' or 'Contradiction'. Negation is at times defined as "this implies a contradiction".
~Pis 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
P => F by Conditional Elimination, so too may we infer
~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. Also line 1
~((p->q)+(q->p) and 4 (and later 15)
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
|_ 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.