非表示:
キーワード:
-
要旨:
Feferman has proposed FS0, a theory of finitary inductive systems, as
a framework theory suitable for various purposes, including reasoning
both in and about encoded theories. I look here at how practical
FS0 really is. I formalise of a sequent calculus presentation of
classical propositional logic in FS0 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.
