Good day. I do not quite understand how I can get ~~p after the 11th line.
Good day. You do not necessarily require
~~p to contradict
~p, you simply need some contradiction to be derivable from assuming
~(p | ~p). Well,
(p | ~p) contradicts the assumption itself, so...
Don't reiterate on line 10. The sub-proof is complete (for your purpose) at line 9.
Line 1 |_ ~(p | ~p) Assumption
: : : as you had.
Line 9 | (p | ~p) Or Introduction 8
From here the next line is instead conditional introduction.
Line 10 ~(p | ~p) => (p | ~p) => Introduction 1-9
After this, if only you could somehow derive
~(p | ~p) => ~(p | ~p) then you may apply the Stanford Fitch system's rule of negation introduction, and finally negation elimination (which is more commonly known as double negation elimination).
Somehow… Hmmm …
Anyhow, in your other system, what we have so far should translate to something like:
U. ~(p v ~p), p |- p S1
Rv+(S1) ~(p v ~p), p |- p v ~p S2
U. ~(p v ~p), p |- ~(p v ~p) S3
R~+(S2,S3) ~(p v ~p) |- ~p S4
Rv+(S4) ~(p v ~p) |- p v ~p S5
And you can complete this in three more lines.