Vwwxrf

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 $(mathbbN;+,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 $underlinen$ the Godel number of the sentence "$underlinen=underlinen$" is $3n$. Then is $forall x(G(x=x)=underline17)$ true, or is $forall x(G(x=x)=underline3cdot 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.)

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. 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.

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 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.

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.

If I understand you correctly, you might like what Feferman and Jager call BON, the basic theory of operations and numbers, based on one of Beeson's theories. See "Systems of explicit mathematics with non-constructive $mu$ operator", APAL 65 (1993), 243-263, or here.

In this theory all the definable functions are given by terms. Functions may have partial domains, and the symbol $fxdownarrow$ indicates that $fx$ is defined. There is a term $mu$ of the form
$$mu:(N rightarrow N) rightarrow N$$
meaning "the minimum $x$ with $fx=0$, if it exists" -- and you might reasonably call this a co-relation.

The result is a theory for which, as shown in the last result of the paper:
$$BON(mu)+(FMLA!-!Ind_N)equiv P!A_Omega^w equiv widehatID_1
equiv (Pi_infty^0-CA)_<epsilon_0$$