Welcome to the staging ground for new communities! Each proposal has a description in the "Descriptions" category and a body of questions and answers in "Incubator Q&A". You can ask questions (and get answers, we hope!) right away, and start new proposals.
Are you here to participate in a specific proposal? Click on the proposal tag (with the dark outline) to see only posts about that proposal and not all of the others that are in progress. Tags are at the bottom of each post.
Is there a specification meta-language for logics? Question
Is there a specification meta-language for logics? A formal language which can express, “a logic with variable symbols, unary predicates, and connectives”?
1 answer
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.
0 comment threads
1 comment thread