TL;DR: Could you consider the relation between logic, type theory, and category theory like the relation between formal grammars (rules), formal languages (syntax), and abstract machines (semantics), and similarly, the higher order variants (of logic, etc.) as meta-equivalents (of formal grammars, etc.)?
Note: I'm not a mathematician, so most of this is self-taught. I'm a self-taught developer, so I may have missed various minor details and such. Apologies if this happened and my question wound up incomplete somehow.
I was reading up on how category theory and type theory relate, and how there's a clear duality between both of those and logic, and having some familiarity with basic formal grammar/language concepts, I started thinking of an analogy.
- Formal language theory sees languages as providing the syntax and abstract machines providing semantics. There similarly also exists a grammar, which defines the rules for building the language and for the semantics to bind to.
- Languages define the syntax, the set of strings/symbols valid within it.
- Type theory can be regarded as a formal syntactic framework for category theory, providing a set of concepts for it to work from.
- Languages can be defined based on their rules. Similarly, type theory can be defined through its logical inference rules (and generally is).
- Machines define the semantics, what each "production" does.
- Category theory can be regarded as providing a semantic framework for type theory, explaining what each concept does.
- Machines are typically defined by what they do, but the capabilities of certain classes of machines are defined by the languages they accept, with certain restrictions on their grammars. Similarly, classes of categories could be defined by the types it contains, with restrictions on which rules of logic apply. (This maps very closely to the concept of objects + morphisms.)
- Grammars define the rules applied to determine whether some set of symbols are within a language.
- Although I can't find any material explicitly stating it, it seems logic, being as rule-based as it is, fills this gap pretty well as providing a rule framework based on a syntax to define the rules.
- Grammars can "generate" languages that satisfy its rules. Similarly, logic is often used to "generate" various conclusions through their proofs, and in the case of constructive logic, is literally used to "generate" type theories and similar through strategic rule definitions.
- Higher order logic/type theory/category theory extends this to basically generate such logic/type theories/category theories, almost as templates.
- This is analogous to meta-grammars, meta-languages, and hypermachines/machines that implement machines.*
- Similarly, this can be narrowed to intuitionistic propositional logic/simply typed lambda calculus/Cartesian closed categories due to the Curry-Howard-Lambek correspondence
- This is analogous to the hierarchy of non-recursive grammars/finite languages/DAFSA
So, in a sense, if I'm correct with my reasoning,
$$ \begin{matrix} \text{(higher order) logic} \\ \text{(meta-) rules} \\ \text{(meta-) grammar} \end{matrix} \Leftrightarrow \begin{matrix} \text{(higher order) type theory} \\ \text{(meta-) syntax} \\ \text{(meta-) language} \end{matrix} \Leftrightarrow \begin{matrix} \text{(higher order) category theory} \\ \text{(meta-) semantics} \\ \text{(meta-) machine} \end{matrix} $$
?
Or am I missing something?
Also, by any chance, where could I find some authors/researchers that could help me better understand this relation?
* It'd be nice if Wikipedia actually made these remotely accessible from anywhere else short of hard-to-discover Google searches.
