рассуждая о законе Пирса

((P→Q)→P)→P - it's obvious in a Boolean logic, but in an Intuitionistic one, in general? Does it imply that the logic is Boolean? E.g. just try Q=⊤?

Actually, (P→⊥)→P ≡ ¬¬P.

See, ¬¬P = (P→⊥)→⊥, and, 

to prove ¬¬P ⊢ (P→⊥)→P we just check that  (P→⊥)∧((P→⊥)→⊥)⊢⊥ we use A∧(A→B)⊢B.   To prove ¬¬P ⊢ (P→⊥)→P, we check that ¬P ∧ ¬¬P ⊢ P, which is ⊥ ⊢ P.  (I had spent some stupid time investigating this law's behavior in a bunch of Grothendieck's topos logics.)