(Higher order) logic/type theory/category theory like (meta-)grammar/language/machine?

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.
• Similarly, this can be narrowed to intuitionistic propositional logic/simply typed lambda calculus/Cartesian closed categories due to the Curry-Howard-Lambek correspondence

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.

• If my tags are wrong, or if other tags need added (since this is a pretty broad subject matter I'm referring to), please feel free to add them. (I could only add 5 initially, and I'm not quite sure that's enough for this question.) Also, I'm not a math major, I'm a software developer who enjoys some occasional highly-theoretical mathematics, so I'm still learning as I go. (This also means I didn't necessarily get all the formal education to know all this by heart.) Feb 4, 2018 at 14:59
• This sounds like computational trinitarianism, if you want a Google target. Feb 4, 2018 at 21:46
• Okay. I found that in one of the links, but I wasn't sure how much I could find on Google. Also, my question is geared more towards relating it to formal language theory, as they seem "isomorphic" to one another at a certain level of abstraction. (I know that's not technically correct, but you probably get my analogy.) Feb 5, 2018 at 5:48
• Higher-order logic has nothing to do with higher category theory. Instead, higher order logic corresponds to topos theory.
– user14972
Feb 13, 2018 at 22:43

I am not entirely sure I have completely understood your question but I will try to give me 2 cents.

It is true that you can regard logics and type theories as some sort of grammars. The elements of the languages generated by these grammars are called judgments: they will be logical judgments in case you are dealing with logics and they will be typing judgements or equality-judgments in case your dealing with type theories.

The relation between logics and type theories is different from the one between grammars and languages: logics do not generate type theories, they are both grammars.

The Curry-Howard theorem establishes an isomorphism between the grammar intuitionistic propositional calculus and the grammar simply typed lambda calculus and between their languages ... though more exactly this isomorphism regards just the typing rules/judgment of simply typed lambda calculus.

Similarly there are generalizations of Curry Howard isomorphism between other logics and type theories. Again these isomorphisms relate the grammars-logics with the grammar type theories.

About the semantics: usually abstract machines are a way to provide an operational semantics for a language. Category theory provides a semantics for logics and type theories, but it is a denotational semantics which differs for the operational ones.

• @Hibou57 I would dare to say that Curry (or Howard, I don't remember who came first) said that. That is because in classical propositional logic you have the law of the middle excluded which via Curry Howard should be trasported to an inhabitant of the sum type $(A \rightarrow \bot) + A$ that cannot be build in simply typed lambda calculus. May 9, 2020 at 13:56