Non-foundationalist foundational thinking

[jodmos.horon]

On Thursday, June 9th, 2022 at 09:10, Vaughan Pratt <pratt at cs.stanford.edu> wrote:

> There may be even better accounts of objects showing what they "really are". If there are better accounts than objects as Chu spaces I'm all ears.

I believe there is. The notion I have in mind may be approached either set theoretically or in a more category theory fashion.

The question of what is a structure may be approached as Miroslav Benda did.

Modeloids. I, Miroslav Benda, Transactions of the American Mathematical Society, Vol. 250 (Jun., 1979), pp. 47-90

"Let us take a concrete example, one which goes to the origins of mathematics. Consider collections of pebbles. Declare two such sets to be analogous just in case they are both nonempty. Hence the only distinction perceived at this level is between the empty and the nonempty. Let us assume that "pointing out a feature" means taking a pebble out of a set of pebbles (the binary operation we talked about in the beginning). Then a set consisting of one pebble is seen to be no longer equivalent to a collection of two or more pebbles. The new analogy has three equivalence classes, one consisting of the empty set, one of the collection of sets with one pebble only and the third consists of the rest. By repeating this process we distinguish more and more obtaining eventually the natural numbers by naming the equivalence classes."

This is basically a back and forth argument.

What he observed is that that back and forth arguments could be encoded by an equivalence relation ~ on n-tuples of items in a structure. 1. a ~ b implies that the tuples a and b are of the same length. 2. the truthiness of the equivalence relation is preserved under an identical permutations of indices for a and b. 3. the truthiness of the equivalence relation is preserved under an identical restriction of indices on both a and b.

It then is possible to encode, for instance, basic geometry in this context using collineation as is done in his example 1.4. As follows:

Let X be a plane. For n-uples a := (a_1,...,a_n) and b := (b_1,...,b_n) of points in the plane, we may say a ~ b if and only if for all i, j, k, (a_i, a_j and a_k are collinear iff b_1, b_j and b_k are collinear).

The data of ~ encodes the structure. (And does away with the game theoretic aspects of back and forth by encapsulating it in that equivalence relation.)

It is further shown in example 1.5 that any relational structure may be encoded as such an equivalence relation. And further on that for any such equivalence relation, it is possible to find a (non-unique) relational vocabulary which matches this equivalence relation.

The vocabulary one gets this way from ~ is not unique. But, modulo technicalities, two such relational vocabularies end up being biinterpretable.

In the end, Miroslav Benda's framework is a bit crude for various reasons, but it ends up encoding structures nicely, and independently of relational signatures. For instance, a group and its opposite group (the one obtained by interpreting x.y as y.x) are the same structure when it comes to the equivalence relation ~.

So, in the end, there is no need for a language to encode a structure. The relation ~ is enough. From that relation, it is possible to find a relational vocabulary that generates the formulas required to recover the relation. In a sense, this relational vocabulary is the data of "generators", and the axioms they satisfy (which are, modulo technicalities, h-inductive axioms in the sense of positive logic) are the "relations" between "generators". Much like in homological algebra, this amounts to a "presentation" of the Lindenbaum algebra, data from which one gets ~.

Making the construction more precise would involve categorical paraphernalia involving Chu morphisms. Which I will sketch very briefly.

For the domain S of a relational structure, one may consider the functor S: F° → Set, where F is the skeletal category of finite sets and mappings thereof, where for an arrow i: n → m, the arrow S(i): S(m) → S(n) sends (x_1, ..., x_m) to (x_i(1),...,x_i(n)).

If we consider symbolic relations of arity n as forming a set T(n), we see that an interpretation of them is given by a mapping ⫤: S(n) x T(n) → 2 yielding a binary relation or, here equivalently, a polar Galois connection. We may turn T into a functor T: F → Set by interpreting the action of i on rho in T(n) yielding i.rho in T(m) (for i an arrow n → m in F) as follows:

(i.rho)(x_1,...,x_m) is the symbolic relation rho(x_i(1),...,x_i(n)).

These mappings are related across arities as follows (for x in S(m), rho in T(n)):

x.i ⫤ rho iff x ⫤ i.rho

This is nothing else than the claim that T(i): T(n) → T(m) and S(i): S(m) → S(n) are two arrows in opposite directions forming a Chu morphism from the object ⫤: S(n) x T(n) → 2 of Chu(Set, 2) to the object ⫤: S(m) x T(m) → 2 of of Chu(Set, 2).

One may extend the above in the other direction, by considering the action of the converse i°: m → n of i: n → m as follows:

Property P for U: (x,z) in the graph of the converse S(i)°: S(n) → S(m) of S(i): S(m) → S(n) implies that (z ⫤ rho implies x in U)

{ x such that x ⫤ i°.rho } is minimal for inclusion among all sets U satisfying property P

The two lines above uniquely characterise the action of i°: m → n on rho: T(m), yielding rho: T(n). And we get a Chu correspondance instead of a Chu morphism.

It may be shown from these definitions that for an injective i: m → n, i°.rho is an existential quantification of rho, existentially quantified over all the x_k for k not in the image of i: m → n. (m and n respectively are the finite sets {1,...,m} and {1,...,n}).

In fact, one may see S and T as being a functorialised kind of Galois connections. There are closure operators on both sides, just as in usual Galois connections. On the side of T, that closure operator yields the semantic closure of a collection of symbolic relations of common arity, yielding the Lindenbaum algebra when considering the closed items. On the side of S, that closure operator yields (modulo technicalities) the closure under equivalences classes of the relation ~ axiomatised by Miroslav Benda.

These two closure operators on both sides are closely related as for usual Galois connections.

But, conceptually, to characterise a relational structure, we only need the closure operator. i.e. the ~ equivalence relation. Not the full Galois connection between syntax and semantics. Which is why Miroslav Benda's construct does encode structures without requiring any notion of syntax.

On the category theoretic side and syntactic side, this construct is quite close to what Mark Kamsma came up with in:

Kamsma, M. Type space functors and interpretations in positive logic. Arch. Math. Logic (2022)

On a more set-theoretic side and more semantic side, in classical logic and not positive logic, the equivalence relation of Miroslav Benda encodes model theoretic structure with no syntactic cruft.

To my mind, that indeed is a better notion of what a "mathematical object" really is. And it also allows glueing them, by the way.

Jodmos Horon.