Is there a specification meta-language for logics? Question

There are many depending on what your goals are.

First, pretty much any foundational system will let you do this via encoding. It is a tedious but straightforward exercise to encode the syntax of (typical) logics and their proof theories into PA (Peano Arithmetic), say, or even PRA (Primitive Recursive Arithmetic). Similarly, for encoding the syntax and semantics into ZFC or some other set theory. Type theory, like MLTT (Martin-Löf Type Theory), could be used as well. If your goal is to build and study logics on an existing mathematical foundation, then these would be the usual approaches. PRA is typically what someone would use if they're trying to limit foundational assumptions. There are definitely weaker systems than PRA that one could consider, but it starts getting pretty inconvenient at that point.

In a very different direction, you have things like Metamath. To over-simplify a bit, Metamath takes the view of proof as, essentially, string rewriting. Basically, you provide rewrite rules of the form: given this sequence of strings with meta-variables (which could be encoded as a single string), produce this string with meta-variables. Every substitution instance for the meta-variables is then a string rewrite rule. A "proof" ("derivation" would be a better term) simply specifies which rewrite rules to apply. Going slightly beyond pure string rewriting, Metamath has a notion that some symbols are "variables", and you can assert that a rewrite rule can't be applied unless two "variables" are distinct. This allows a rule like $y = z; \forall x.P(x, y) \leadsto \forall x.P(x, z)$ to be written but to disallow the invalid case where $z$ is $x$ from some outer scope. Metamath has no notion of formula or quantifier or connective. These are all concepts that must be defined with rewrite rules.

In a somewhat intermediate place are logical frameworks like Twelf. These are relatively weak dependent type theories that are explicitly aimed at specifying other, often more powerful, logics and type theories. Whereas Metamath takes the view of providing the absolute most basic "symbol manipulation" tools to formulate mathematics, logical frameworks take the view that there is a lot of common "meta-structure" when formulating logics that can be handled once and for all. This includes things like capture-avoiding substitution and hypothetical judgements. Systems like Natural Deduction tend to have pretty direct encodings into logical frameworks.

There isn't any universally accepted "standard" language for formulating logics. (Even if you used ZFC, the encoding will require many ad-hoc choices.) Gentzen's rule notation, as often seen in presentations of Natural Deduction or Sequent calculus, in combination with a kind of "abstract" BNF is fairly common, but this isn't standardized or universal either.

posted about 9 hours ago

CC BY-SA 4.0

Derek Elkins‭

1 2 0