7
$\begingroup$

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

$\endgroup$
  • 2
    $\begingroup$ At least some of the mysteries you've encountered would be dispelled if you treated syntax properly (by having terms and formulas appear in variable contexts), and you paid attention between meta-syntax and object-level syntax. Computer scientists have done this sort of thing, but you simply will have to get used to more structure than is available with ad-hoc techniues such as Gödel numberings. If that's acceptable, I can give some references. $\endgroup$ – Andrej Bauer Mar 18 at 19:14
  • 2
    $\begingroup$ Would your co-relations include things like set-comprehension, where $\{x:\phi(x)\}$ is a term produced from a formula $\phi(x)$? If so, then probably you'd also include things like $\lambda$-abstraction and Hilbert's $\epsilon$ operator. $\endgroup$ – Andreas Blass Mar 18 at 19:21
  • 1
    $\begingroup$ @AndrejBauer Yes please, that's more than acceptable! (And I think I'm already thinking along those lines, but laboriously and inefficiently.) $\endgroup$ – Noah Schweber Mar 18 at 19:25
  • 1
    $\begingroup$ @AndreasBlass Yes, I would also consider those examples. But while there's an extensive literature about those specific examples, I don't know of anything about the general situation. $\endgroup$ – Noah Schweber Mar 18 at 19:25
  • 1
    $\begingroup$ @GerhardPaseman Nope, co-relations should be able to act on formulas involving co-relations. And yes, they can have arities as per relations. $\endgroup$ – Noah Schweber Mar 18 at 19:26
8
$\begingroup$

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.

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

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$
$\endgroup$
  • $\begingroup$ Thank you very much! The first (non-extensional) approach is what I'm interested in; I've edited to make that clear. If you don't mind, I'm going to hold off on accepting this answer for a bit, in case other answers appear. $\endgroup$ – Noah Schweber Mar 18 at 20:56
  • $\begingroup$ The sources you've linked to are quite interesting, but I'm not seeing anything like a development of classical model theory there - e.g. that the resulting logic is compact and has the Lowenheim-Skolem property (this is easy to show for at least one version). Do you know of a more "model theoretic" source on the topic? $\endgroup$ – Noah Schweber Mar 19 at 19:42
  • $\begingroup$ Hmm, not really. Probably some first-order logicians would consider this entire conversation a triviality, because it's "just Gödel numbering", and in a sense they'd be correct. Maybe you're looking for basics of higher-order syntax, i.e., how to organize datatypes that properly deal with syntax, including free and bound variables? $\endgroup$ – Andrej Bauer Mar 19 at 22:07
  • $\begingroup$ I supplemented my answer with (hopefully) enough information to show how to apply the standard techniques from meta-programming and computer-sciency treatment of syntax. $\endgroup$ – Andrej Bauer Mar 19 at 22:41
  • $\begingroup$ Thank you very much again, and sorry for the late acceptance - I wanted to take some time to see if I could find any more "classical-model-theory-flavored" stuff. (I may wind up writing something up along these lines, at least expositorily.) $\endgroup$ – Noah Schweber Apr 19 at 23:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.