Inductive Structures
I sat in on a lecture mostly about inductive structures today in CMU’s 21-300 Basic Logic. I went with who we will refer to as cursed schedule guy (from the last post) and we talked with Professor Cummings afterwards; more on the contents at the end.
Also, I will be a lot more expository than the lecture was. I feel like you had to connect a lot of dots in your head in the lecture, whereas the point here is to at least provide a reference for myself to turn my brain off.
No guarantees that the details are entirely right since this is off memory and Google is really, really bad when it comes to formal logic stuff. Also I will be vague since this is a general overview.
Anyway, it’s math time!
First we establish the following:
(Finitary Function) A finitary function is just a function with a finite number of inputs.
An example of a finitary function is addition on the reals: it takes .
An example of an infinitary function (i.e. not finitary) is one that takes an infinite number of reals as input and outputs their sum; e.g. .1 Now here is where things get real tricky. Take the function that does much the same as , only it takes one (which you will note is a finite number) infinite sequence of reals. For example, , where the input of is the sequence rather than each individual element.
This seems super cursed; and are fundamentally the same and yet they are classified entirely differently for a theorem who we will see only cares about this one classification. The point is about finiteness of the number of inputs though, we don’t need the members of the input to be finite or countable or whatever.
(Inductive Structures) An inductive structure is an ordered pair where is a set and is a set of finitary functions.
This definition is very general. There is no restriction besides that every function is is finitary. itself may be infinite, uncountable, whatever. So may be. In fact, not every function in needs to even admit any member of or tuples of members of as inputs.
A standard inductive structure is . Note and are functions that take two inputs in and return an output in . For instance, . Yes, this is cursed notation, but you can think of the binary operator as a function with two inputs. And in fact, you have to when strictly considering inductive structures. Also, this inductive structure feels closed. This is a word we will define later, but takes two members of to a member of . So does . You should intuitively feel that this inductive structure feels closed-ish.
Here is a more cursed inductive structure. Let be the set of odd integers and be the set of even integers. Then let be some function from to . Then is an inductive structure, despite the fact that ’s domain does not include any member of . Cursed, isn’t it? But it still falls under the definition, even if this inductive structure does not actually do anything interesting.
Now for a bit of notation that will make it easier to refer to ’s arguments for arbitrary . The motivation for this notation is vectors, because in some sense vectors are just lists.
We denote the list , , , as . We will refer to an arbitrary element in the list as .
Now for our final definition:
(Closure) A closure under is a set such that for every function and every in the domain of such that , .
Say is a closure under . Then you can naturally construct a closed inductive structure . We won’t worry about that in this post.
The argument
Now for the theorem.
For any set and any set of finitary functions , there exists a set such that and is a closure under . Furthermore, we can find a least upper bound , meaning that there exists some such that for all satisfying the same property, .
The main difficulty is showing such a exists. The least upper bound property is pretty easy to see just from how is explicitly constructed.
Y exists
We will recursively generate a sequence . Let , and let . In other words, we look at what we get from taking with every input in , and join it to to find .
Now let . We claim works, and we show this by proving if each is in some , then must be too.
Note each by definition is in some if it is in . Because for , and there is some maximum in the list of that are in, for all . This is where we use the finitary condition, because otherwise we have no guarantee this maximal exists to begin with. And by definition, .
Y is a least upper bound
This is a standard set theory argument; we just want to show that for the we have just constructed. ( is an arbitrary closure under that is a superset of .)
We claim that if for any , we must have . We prove this via induction on .
The base case where holds true by definition ().
If , then either or there is some with all such that . This follows straight from the definition of . If then we are done. Otherwise we are done by the definition of a closure.
Finitary is a lie
A subset of our discussion with Prof. Cummings after class. This is where I don’t really know what I’m saying, which is why it is quite hand-wavy.
The finitary condition should make you feel like something is off; like it isn’t really necessary. And in fact, it isn’t if you use the right perspective. In the “ exists” section, we indexed the finite set with a countable set, namely the natural numbers. The reason we cannot let be infinite (more precisely, have the same cardinality as is because then we cannot find some maximum in of these elements in .
But what if we had a number that was guaranteed to be “bigger” than anything in ? Another source of motivation: don’t you see how the size of the indexing set is “just an infinity bigger” than the finite set ? If we index with the ordinal number , then we can find some “maximum” in that is bigger than every element in the set of size (you can treat this as here) of our finitary set. And thus, if we commit to using ordinals for indexing, we can have the number of inputs be ordinal too. And thus the finitary condition can be dropped.
Apparently all of this is legal in set theory land. They just tighten their argument up much more than I am right now.
We won’t deal with the detail of convergence here since it’s just an example. Set if the sum diverges or something to cover this hole, the function will still be infinitary. Or you can exclude divergent sequences. It doesn’t matter.↩︎