To put your argument "into PRA" in the natural way, what one would
probably do would be first to write in PRA a proof-checker for FOL and
then simply check for a specific, given proof object, that, say, ZF |-
Freiling's-Axiom -> ~CH. The traditional function of PRA is not to
carry the mathematics but to carry the metamathematics (the proof
theory), including to check concrete proof objects.
Historically clouding the issue is the fact that in recent years, some
people such as Harvey Friedman have shown, to the surprise of many,
that one actually can use PRA for powerful "higher level" mathematics
not just for a fragment of elementary number theory. (This involves
coming up with unusual ways to represent higher level things.) See,
for example, the appendices to the second edition of Takeuti's book
Proof Theory. But I don't believe anyone argues that PRA is the right
theory in which to explore questions about uncountable cardinals.
But this newly recognized power of PRA is not the purpose for which
PRA was invented by Skolem or advocated by Hilbert-Bernays for
metamathematics. PRA is very similar to the theories behind Skolem's
arithmetic, Goodstein's recursive arithmetic, and your logics for
Lisp: a simple logic for such very finite things as arithmetic and
symbol manipulation. And a logic that almost everyone believes. E.g,
in Goodstein's case (his book Recursive Number Theory), if I recall
correctly, the only rules of inference are (a) permitting the
definition of recursive functions, (b) inferring that two recursive
functions that satisfy the same defining equations are equal
everywhere, (c) instantiation, and (d) substitution of equals for
equals.
So your proposed "exercise" is about as odd as someone proposing the
same exercise for a Lisp-logic instead of PRA after reading one of
your early 60's papers such as "Towards a Mathematical Science of
Computation" or "A Basis for a Mathematical Theory of Computation".
By the way, if one does a good job in defining PRA in the style of an
nice applicative programming language with good data structures,
including lists and symbols, then reading the concrete proof object
might actually be a real pleasure and easy for many to follow.
Especially if the proof-checker includes obviously correct but
powerful decision procedures for fragments of FOL, e.g., as in Ed
Nelson's checker qed, so that the proof object is not too long or too
tedious.
Bob