Let $GL$ be the provability logic containing the axioms $K := \Box (\varphi\to \psi)\to (\Box \varphi\to \Box \psi)$ and $L := \Box(\Box \varphi \to \varphi)\to \Box \varphi$, along with the necessitation rule (from $\varphi$, infer $\Box\varphi$).
Let $\Box^n\varphi$ be the iteration of $n$-many boxes before $\varphi$ (that is, $\Box^n\varphi$ is $\overbrace{\Box\dots\Box}^{n \text{ times}}\varphi$). Let $\bot$ be the false proposition.
One can show that: if $GL\not\vdash\varphi$, then there is $n$ such that $GL + \Box^n\bot \not\vdash\varphi$.
An intuitive proof goes through the completeness of $GL$ with respect with finite trees: if $GL$ does not prove $\varphi$, then there is a finite tree $T$ invalidating $\varphi$; the root of $T$ satisfies $\Box^{depth(T)+1}\bot$; so $GL + \Box^{depth(T)+1}\not\vdash\varphi$.
My question is: can we prove this proposition with a syntactical argument which avoids the completeness theorem for $GL$?
