MPI-INF/SWS Research Reports 1991-2021
2. Number - All Departments
MPI-I-93-227
A theory and its metatheory in FS 0
Matthews, Seán
June 1993, 22 pages.
.Status: available - back from printing
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.
-
MPI-I-93-227.pdf
; Article:
- Attachement: MPI-I-93-227.dvi (89 KBytes); MPI-I-93-227.pdf (132 KBytes)
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1993-227
BibTeX@TECHREPORT{Matthews93,
AUTHOR = {Matthews, Se{\'a}n},
TITLE = {A theory and its metatheory in FS 0},
TYPE = {Research Report},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
NUMBER = {MPI-I-93-227},
MONTH = {June},
YEAR = {1993},
ISSN = {0946-011X},
}