A Theory and its Metatheory in FS 0
Seán Matthews · 1994
Abstract Feferman, in the previous chapter, has proposed FS, a theory of finitary inductive systems, as a framework theory that allows a user to reason both in and about an encoded theory. I look here at how practical FS really is. To this end I formalise a sequent calculus presentation of classical propositional logic, and show this can be used for work in both the theory and the metatheory. The latter is illustrated with a discussion of a proof of Gentzen’s Hauptsatz.