My question is on a seemingly-natural extension of classical logic that I've been playing around with a bit in the context of generalized recursion theory. I'm sure it's been treated extensively already, but my literature search skills have failed me.



> 
> What is a good source on what happens when we extend first-order logic *(or other logics, for that matter)* to allow "co-relations?"
> 
> 
> 


By "co-relation" I mean a syntactic object which behaves dually to a relation: rather than taking some terms and producing a formula, a co-relation should take some formulas and produce a term. The motivating example of a co-relation is of course **Godel numbering**, but there are other reasonable examples as well *(EDIT: see Andreas Blass' comment below)*.


**To clarify**: while I'm definitely interested in examples, what I'm looking for in an answer is something approaching a *general theory*, at least the basics of such - in particular, it should treat arbitrary signatures involving constants, functions, relations, and co-relations, and be able to make sense of arbitrary theories in such signatures. So an example of a specific theory involving co-relations **is not** what I'm looking for.




---


It's worth pointing out - and this may also help motivate the question - that there are real issues in setting up the semantics for logic with co-relations *(EDIT: and see Andrej Bauer's comment below)*. The most significant issue, I think, is how quantifiers can or cannot "reach into" co-predicates. Look at $(\mathbb{N};+,\cdot,G)$ where $G$ is an appropriate Godel-numbering co-relation. Suppose the Godel number of the formula "$x=x$" is $17$, and for each numeral $\underline{n}$ the Godel number of the sentence "$\underline{n}=\underline{n}$" is $3n$. Then is $\forall x(G(x=x)=\underline{17})$ true, or is $\forall x(G(x=x)=\underline{3}\cdot x)$ true? I have my own guess about the "right" way to set things up, but I wouldn't be surprised at all to learn that I'm going about things incorrectly, so I'm leaving the question fairly broad.


**FINAL EDIT**: One key aspect here is that I am in no way demanding *extensionality* - co-relations are not restricted in any way in terms of how they behave on logically equivalent (tuples of) formulas. (This is of course necessary if Godel numbering is to be an example, after all.)



Logic with "co-relations" - sources?
Let us first distinguish between two kinds of operations that "take formulas to terms":


1. We might ask for *reflection* of syntax into the theory. A typical example is a quoting operator which takes a formula and returns its Gödel number.
2. We might ask for the ability to mix formulas and terms. A typical example is the subset-forming operation $\{x \in A \mid \phi(x)\}$.


The two are quite different because the first one is quite intensional (logically equivalent formulas produce different numbers) while the second one is extensional (logically equivalent formula produce the same subset).


Reflection of syntax into theory gets interesting once we ask for it to play nicely with respect to substitution and binding. I am not too familiar with this area, you could look at how [syntax is reflected into NuPRL](http://www.nuprl.org/documents/Barzilay/NuprlHOAS_02.pdf). You might also be interested in going in the other direction, namely how to convert internal representation of syntax to formulas. This goes under the name "meta-programming", where once again I am not too familiar with the literature. I am for instance aware of Aleks Nanevski's work on [meta-programming with names and necessity](https://software.imdea.org/~aleks/papers/necessity/necessity1.pdf).


For the second part (terms that contains formulas), that's very familiar territory in higher-order logic and type theory. If terms can appear in formulas and formulas can appear in terms, then the two-level stratification of terms and formulas familiar from first-order logic becomes meaningless. It is then better to put formulas and terms on equal footing and use sorts or types to keep track of what is what. One example of such a setup is [Church's type theory](https://plato.stanford.edu/entries/type-theory-church/) where there is a special type of truth values. A more modern example is dependent type theory, especially variants of it that have a dedicated sort or universe of propositions, for instance the [Calculus of constructions](https://en.wikipedia.org/wiki/Calculus_of_constructions).


If you are interested to see how such formal systems work in practice, you can look at modern proof assistants. They all eschew the traditional first-order logic (because it is inappropriate for mathematical practice) and use one of the above mentioned formalisms instead: Isabelle/HOL uses Church-style higher-order logic, Coq uses the Inductive Calculus of Constructions, and Agda uses Martin-Löf type theory.


**Supplemental:** If you're just interested in reflecting the syntax of first-order logic into arithmetic, i.e., Gödel numberings, then you'd proceed as follows, combining standard bits about syntax and meta-programming from computer science.


First, define the [abstract syntax](https://en.wikipedia.org/wiki/Abstract_syntax) of first-order logic, including an operator $G$ which takes formulas to terms. Find some way of encoding such trees as numbers, if you feel nostalgic about 20th century logic. Consider using [de Bruijn indices](https://en.wikipedia.org/wiki/De_Bruijn_index) to avoid nasty details about bound variables.


The syntax of $G$ is *not* $G(\phi)$, as you suggested, but rather
$$G(x\_1, \ldots, x\_n \mid \phi)$$
where $x\_1, \ldots, x\_n$ is a (possibly empty) list of variables. The variables $x\_1, \ldots, x\_n$ should be encoded by $G$, while any remaining free variables appearing in $\phi$ should be considered as *interpolating* variables. It might be easiest to explain this by means of an example:


* $G(x, y \mid x + y = 7)$ is a closed term (it has no free variables), so it denotes a number which encodes the expression $x + y = 7$.
* $G(y \mid x + y = 7)$ is a term whose only free variable is $x$.
* $G( \mid x + y = 8)$ is a term whose free variables are $x$ and $y$.


We want to arrange interpolation and substitution so that they interact sensibly, i.e., we expect that
$$G(x\_1, \ldots, x\_n \mid \phi)[t\_1/y\_1, \ldots, t\_m/y\_m] =
G(x\_1, \ldots, x\_n \mid \phi[t\_1/y\_1, \ldots, t\_m/y\_m]).
$$
In words: if we first encode $\phi$ and then substitute $e\_i$'s for $y\_i$'s in the resulting term, that's equal to first substituting $e\_i$'s for $y\_i$'s in $\phi$ and then encoding. The usual provisos about free variables not getting captured apply: the free variables appearing in the terms $t\_i$ must be disjoint from $x\_1, \ldots, x\_n$, and probably the $x\_i$'s must be disjoint from $y\_j$'s. (I refuse to think about this because there are [non-pedestrian ways of dealing with bound variables](https://en.wikipedia.org/wiki/Higher-order_abstract_syntax).)


We can now sensibly answer your questions about encoding of $x = x$. The encoding of $G(x \mid x = x)$ is a particular number, say $17$. The term $G( \mid x = x)$ has one free variable and suppose it is equal to the term $3 \cdot x$. Consequently, the term $G(\mid 14= 14)$ is equal to 42. Now we see that


* $\forall x . G(x \mid x = x) = 17$ is true
* $\forall x . G(\mid x = x) = 3 \cdot x$ is true
* $\forall x . G(\mid x = x) = 17$ is false
* $G(\mid x = x) = 17$ is equivalent to $3 \cdot x = 17$


