A theory and its metatheory in FS 0

Matthews, Seán

アイテム詳細

登録内容を編集ファイル形式で保存

一時保存へ追加

タグ情報を表示リリース履歴を表示詳細要約

公開

報告書

A theory and its metatheory in FS 0

MPS-Authors

/persons/resource/persons45002

Matthews, Seán
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

There are no locators available

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

フルテキスト (公開)

MPI-I-93-227.pdf
(全文テキスト（全般）), 132KB

付随資料 (公開)

There is no public supplementary material available

引用

Matthews, S.(1993). A theory and its metatheory in FS 0 (MPI-I-93-227). Saarbrücken: Max-Planck-Institut für Informatik.

引用: https://hdl.handle.net/11858/00-001M-0000-0014-B470-A

要旨

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.