Do you have any references for the kind of paraconsistent type theory that you mention here?

@TimothyChow From what I've seen, I agree with you that this sort of mathematics hasn't been studied at nearly the level required to prove such a theorem, but "nobody has any idea", I don't think is a very good way to surmise the situation. In particular, for set theory developed over a certain paraconsistent logic, Cantor's theorem is unprovable. See "What is wrong with Cantor's diagonal argument?" by Ross Brady and Penelope Rush. So, if one developed enough of reverse mathematics in such a context, one could I think meaningfully ask this question.

@wojowu He's probably refering to Gentzen's proof. I really don't like the term "finitism", as I think at face value you could interpret that a number of different ways, but I think at least under one interpretation it would be reasonable to call Gentzen's proof "finitist" (Though this is not the sense in which Hilbert used the term).

@RobertBryant I'm curious to know exactly what kind of higher order functions you can make $\mathcal{A}$-differentiable (in a properly constructed algebra). Specifically, I'd like to know if there are non-commutative algebras where any convergent power series is $\mathcal{A}$-differentiable, or is that only possible in the commutative case? If not, what can we say about power series $\mathcal{A}$-differentiability$ in terms of the structure of the left-annihilator of the commutator ideal?