Computational consequences of Friedman's (unprovable) Upper Shift Fixed Point theorem?
I don't know of any consequences of this particular theorem, but normalization proofs of lambda calculi like the calculus of inductive constructions rely on large cardinal axioms -- even though the set of lambda-terms is as countable as you could want.

I think the best way to understand the computational significance of set-theoretic axioms asserting the existence of large cardinals is to think of set theory as a way of phrasing the theory of graphs. That is, a model of a set is a collection of elements equipped with a binary relation used to interpret membership. Then, the axioms of set theory tell you properties of the membership relation, including how you can form new sets from old. In particular, the axiom of foundation means that the membership relation is well-founded (ie, it has no infinite descending chains). This well-foundedness in turn means that if you can line up the execution states of a program with the transitive membership of the elements of a set, then you have a termination proof.

So an assertion that a "big" set exists has a computational payoff as a claim that a certain class of loops in a general recursive programming language terminate. This interpretation works uniformly, all the way from the plain old axiom of infinity (which justifies natural number iteration) all the way up to large cardinal axioms.

Are these axioms true? Well, if the axiom is false you can find a program in one of these classes which doesn't terminate. But if it's true, we will never be sure, thanks to the Halting theorem. Everything from natural number induction on is a matter of scientific induction, which may always be falsified by experiment -- Edward Nelson has famously hoped to prove exponentiation is a partial function!