Item

Abstract

Feferman has proposed a system, FS_0, as an alternative framework for \u000Aencoding logics and also for reasoning about those encodings. We have \u000Aimplemented a version of this framework and performed experiments that show \u000Athat it is practical. Specifically, we describe a formalisation of predicate \u000Acalculus and the development of an admissible rule that manipulates formulae \u000Awith bound variables. This application will be of interest to researchers \u000Aworking with frameworks that use mechanisms based on substitution in the lambda \u000Acalculus to implement variable binding and substitution in the declared logic \u000Adirectly. We suggest that meta‐theoretic reasoning, even for a theory using \u000Abound variables, is not as difficult as is often supposed, and leads to more \u000Apowerful ways of reasoning about the encoded theory.