Formal proof of "Law of ecxluded middle"

I wonder how to give a formal, Fitch-style, proof of P v P ..?

I am able to prove it by contradiction when I use that P & P is a tautological consequence of (P v P ) . But in order to prove this (one of the DeMorgan's laws I think?) formally I have to use the law of excluded middle itself...

I also know how to show these tautologies with truth tables, but an exercise explicitly ask for a formal proof of P v P .

All help is appreciated :)

A shorter proof of the formal law of the excluded middle

A shorter way to construct a proof here comes as to use a rule of single-negation elimination instead of double-negation elimination... "From a sub-derivation which starts with Np and derives a contradiction, we may immediately infer p." Jaskowski, one of the founders of natural deduction, and whose proof boxes lead to Fitch-style proofs, used this rule instead of double-negation elimination. But, I digress. In prefix notation a proof can go:

0 | NApNp hypothesis

1 || Np hypothesis

2 || ApNp 2 alternation introduction

3 || KApNpNApNp 3, 1 conjunction introduction

4 | p 2-4 negation elimination

5 | ApNp 5 alternation-introduction

6 | KApNpNApNp 6, 1 conjunction introduction

7 ApNp 1-7 negation elimination

This does hold in *some* non-classical logics, and works as a proof in any non-classical logic where the rules of inference here used here work out as sound. If you want to consider all non-classical logics at once, this formal law neither holds nor does not hold.