Shutte's Consistency of Arithmetic

[Anton Freund]

>> I'm wondering is Shutte or anyone else has published any similar proofs.

If I understand your question correctly, then the answer is yes: This is a
fundamental method of an entire research area, namely ordinal analysis.
The following is a very good survey:

Michael Rathjen, The Realm of Ordinal Analysis
https://www1.maths.leeds.ac.uk/~rathjen/realm.pdf

>> Specifically, I'm interested in other proofs that use this same approach
>> for
>> establishing the underivability of other, more complex, formulas in S or
>> S_infinity.

Ordinal analysis is often (but not only) concerned with Pi^0_2-statements
(totality of algorithms). In addition to the survey above, you could e.g.
consult the following:

Matt Fairtlough and Stanley Wainer, Hierarchies of Provably Recursive
Functions, in: S. Buss (ed.), Handbook of Proof Theory
https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/137/

Since you are specifically asking about "more complex" formulas: The
unprovability of complex formulas (e.g. Pi^1_2-statements) can often be
established by other methods (e.g. computability theory). In my opinion,
it is one of the great achievements of ordinal analysis that it can deal
with statements of low logical complexity (i.e. Pi^0_1 and Pi^0_2).