A framework for defining logics (Q4033837)

The authors provide a meta-logic for defining logics. The meta-logic is based on a typed \(\lambda\)-calculus with dependent types. Within this logic desired logics may be encoded. Syntax is encoded using the typed lambda-calculus in a style similar to Martin-Löf's arities. This approach to higher-order abstract syntax allows one to use the lambda calculus to capture notions like variable binding and substitution in a uniform way. Rules and proofs are modeled with a new paradigm called judgment as types, where, in analogy with the propositions as types principle, judgments (such as provability or validity) are identified with the types of their proofs. This leads to a presentation of rules and proofs whereby rules are viewed as proofs of higher-order judgments and proof checking becomes type-checking. The content of the paper focuses on the LF type theory and its meta- theoretic properties (e.g., normalization, Church-Rosser, etc.), its theory of expressions (how syntax is encoded), and its theory of rules (how rules and proofs are encoded). Considerable emphasis is laid on developing a methodology for establishing the correctness of encodings. This means that a formula \(\varphi\) is provable in some theory \(T\) (the authors illustrate this with first and higher-order logic) if and only if the corresponding LF judgement has a member \(t\). Moreover each such \(t\) encodes a proof and these stand in a bijection with proofs in the theory \(T\).