I think this in some sense the most general way of thinking of the Pythagorean theorem.

--that $P\lor\lnot\mathsf{Con}(T)$ is always decidable by $T$ which doesn't seem right to me. But maybe it is still true that any independent sentence about the well-foundedness of an ordinal implies $\mathsf{Con}(T)$, IDK.

Would it be wrong to suggest that the claim reduces to (1) every computable theory is ultimately "reachable" by PRA + some computable ordinal, i.e. the semantics of any program can be determined by a sufficiently complex program (2) if T models PRA and can induct along $\alpha$, then $\mathsf{PRA}+\alpha\not\models \mathsf{Con}(T)$ (3) $\mathsf{Con}(T)$ is in some sense the "minimal" statement independent of $T$? I guess the last one is the non-trivial bit -- perhaps it can be formalized in the sense of "any true sentence independent of $T$ can prove $\mathsf{Con}(T)$ but that would imply--

Ah wait, no it's fine -- your axiom 4 implies the converse of axiom 3, and preservation of binary unions leads to $A\subseteq B\Rightarrow \mathrm{cl}(A)\subseteq\mathrm{cl}(B)$.

Wait -- so in a pre-topology, it's no longer true true that "if $x$ touches $A\subset B$, then $x$ touches $B$"?

@ManfredWeis Would you recall the title of the post you meant to link to? Your link is an actively updated feed -- is it this?

Because good proofs are just a formalisation of the intuitive understanding -- rather than wasting space explaining the insights, you can just give them the proof, and an even somewhat experienced reader can re-create the details.

On PhysicsOverflow, there is a link to this paper for the same question.

This has received an answer on PhysicsOverflow if you're still interested: Classical and Quantum Chern-Simons Theory