Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: mathematics

Topic: proving things: induction

David Egolf (Apr 03 2023 at 15:34):

In the spirit of some recent threads, I have been attempting to write a proof for an exercise in "A Mathematical Introduction to Logic" by Enderton, and I was hoping for some feedback on the proof structure I would like to use. I'm also hoping this thread can be of interest to other people hoping to learn how to prove things.

In this exercise, I find myself wanting to use a form of induction a bit more general than what I've used before, and I'm not sure if it's valid.

The exercise in question states:
"Let α be a wff; let c be the number of places at which binary connective symbols (∧, ∨, →, ↔) occur in α; let s be the number of places at which sentence symbols occur in α. (For example, if α is (A → (¬ A)) then c = 1 and s = 2.) Show by using the induction principle that s = c + 1."

Here a "wff" refers to a "well-formed formula", which is created in one of the following ways:

• Every "sentence symbol" (namely, one of: A1, A2, A3,....) is a wff
• If $\alpha$ and $\beta$ are wffs, then so are (¬ α), (α ∧ β), (α ∨ β), (α → β),
  and (α ↔ β). We call these ways of making new wffs from old ones "formula-building operations".
  Every wff is constructed from sentence symbols by application of a finite number of formula-building operations.

Now, the usual form of an induction argument I'm familiar with goes roughly like this:

• Form a statement that depends on a natural number, $P(n)$
• Show that the statement holds for the smallest natural number of interest $s$
• Show that if the statement holds for $n$, it holds for $n+1$
• Conclude that $P(n)$ holds for all natural numbers greater than or equal to $s$

However, the induction I'd like to do in this case has a bit of a different structure:

• Show that all wffs formed from 0 formula-building operations satisfy s = c+1.
• Show that applying any formula-building operation to wffs satisfying s = c+1 yields a wff that satisfies s = c+1
• Conclude that all wffs satisfy s = c+1, since all wffs are made from a finite number of formula-building operations

The second step described here (a sort of inductive step) is straightforward to carry out. What I'm more concerned with here is the basic structure of the attempted proof involved. It feels like I'm trying to generalize the idea from normal induction where we make use of repeated applications of "add one" to generate all natural numbers of interest. Is there a more general form of induction where we talk about using a collection of operations which together generate all the objects of interest, from a set of "base case" objects?

That is, is the following argument structure valid?

• We have a statement $P(x)$ which depends on $x \in X$. We want to show $P(x)$ is true for all $x \in X$.
• Begin by showing $P(x)$ is true for all $x \in Y$, with $Y \subseteq X$.
• Introduce a number of operations $b_1, b_2, \dots$ of potentially varying arity $N_i$ that "generate" $X$ from $Y$. That is, given any element $x$ of $X$, by applying our operations a finite number of times starting with elements in $Y$, we can produce the specified element $x$
• Show that, for each $i$, the output of $b_i: X^{N_i} \to X$ always satisfies $P$, provided that each of the $N_i$ input elements satisfy $P$
• Conclude that $P(x)$ is true for each $x \in X$

Any thoughts around this topic are welcome!

Ryan Wisnesky (Apr 03 2023 at 15:47):

The structure of a proof based on induction over the natural numbers should always be the same: first, you write a predicate over Nat, say P, and then show that P(0) holds, and then that P(n) implies P(n+1) (or P(m) for all m <= n implies P(n), for strong induction). Is it possible you are trying to do induction over the syntax of wffs, where you first write a predicate over wffs, say, Q, and then show that Q holds of all atomic propositions, and then that Q(x*y) holds assuming Q(x) and Q(y), hold for each connective *. It's also possible to do induction over proofs of wffs, any many things besides. In any case I'd encourage you to write the inductive hypothesis explicitly.

Ralph Sarkis (Apr 03 2023 at 15:49):

I would call this more general form of induction structural induction.

John Baez (Apr 03 2023 at 15:55):

It feels like I'm trying to generalize the idea from normal induction where we make use of repeated applications of "add one" to generate all natural numbers of interest. Is there a more general form of induction where we talk about using a collection of operations which together generate all the objects of interest, from a set of "base case" objects?

Yes, the Wikipedia article on "structural induction" discusses this kind of induction. Near the end they get into the technical details of when and why structural induction works. The set of structures you're doing induction on need to form a 'well-founded partial order'.

John Baez (Apr 03 2023 at 15:58):

If you don't know what a well-founded partial order is and when you've got one, you can either 1) learn this stuff, or 2) fake it (this is probably rather common and you can probably get away with it by muttering words like "I will do structural induction on the set of wffs"), or 3) use old-fashioned induction on natural numbers, by assigning to each wff (or whatever you're doing) a natural number describing its complexity, in such a way that a wff of complexity n+1 can only be obtained in various specified ways (which you list) from a wff of complexity n.

John Baez (Apr 03 2023 at 16:02):

Also see Mike Shulman's remark on induction. "Strong" induction on natural numbers is where you get to assume $P(k)$ for all $k \le n$ in order to prove $P(n+1)$.

John Baez (Apr 03 2023 at 16:03):

(It's a good exercise to use ordinary "weak" induction on natural numbers to prove strong induction.)

Mike Shulman (Apr 03 2023 at 20:32):

Well-founded partial orders are one way to be precise about structural induction, but not the only way. For instance, your sketch:

• We have a statement $P(x)$ which depends on $x \in X$. We want to show $P(x)$ is true for all $x \in X$.
• Begin by showing $P(x)$ is true for all $x \in Y$, with $Y \subseteq X$.
• Introduce a number of operations $b_1, b_2, \dots$ of potentially varying arity $N_i$ that "generate" $X$ from $Y$. That is, given any element $x$ of $X$, by applying our operations a finite number of times starting with elements in $Y$, we can produce the specified element $x$
• Show that, for each $i$, the output of $b_i: X^{N_i} \to X$ always satisfies $P$, provided that each of the $N_i$ input elements satisfy $P$
• Conclude that $P(x)$ is true for each $x \in X$

can be justifed directly without talking about well-foundedness explicitly. Define a subset $Z$ of $X$ to be "$b$-closed" if whenever the inputs of some $b_i$ belong to $Z$, so does the output. Your assumption that $Y$ generates $X$ under $b$ means that if a $b$-closed subset contains $Y$, then it must be all of $X$. (If you like, this is by ordinary natural-number induction on the finite number of $b$-operations you have to apply to get from $Y$ to some element $x\in X$.) Your two proofs show that the set $\{x \in X \mid P(x)\}$ contains $Y$ and is $b$-closed; therefore it is all of $X$.

Mike Shulman (Apr 03 2023 at 20:33):

Another way to justify structural induction is to talk about general "inductive definitions", which categorically are [[initial]] [[algebras for an endofunctor]]. In the case of logical formulas (I dislike the term "wff" because no one ever wants to talk about an "ill-formed" formula), we are talking about the endofunctor of $\rm Set$ defined by
$F(x) = S + X + (X\times X) + (X\times X) + (X\times X) + (X\times X)$
where $S$ is the set of sentence symbols. An $F$-algebra is a set $X$ with a function $F(X) \to X$, which means that we have an interpretation of every sentence symbol as an element of $X$, together with one unary operation $X\to X$ corresponding to negation, and four binary operations $X\times X \to X$ corresponding to disjunction, conjunction, implication, and equivalence. The set $W$ of formulas is the initial such $F$-algebra, which means that its elements are "freely generated" by applying these operations formally. This is a categorical way to express that "Every wff is constructed from sentence symbols by application of a finite number of formula-building operations."

Given this definition, we can justify structural induction as follows. Suppose $P(x)$ is some property of formulas, and consider $U = \{ x\in W \mid P(x)\}$. The "base case" and "inductive steps" show that $U$ is itself an $F$-algebra such that the inclusion $U \hookrightarrow W$ is an $F$-algebra homomorphism. But $W$ is the initial $F$-algebra, so there is also an $F$-algebra homomorphism $W\to U$, and uniqueness means that the composite $W\to U \hookrightarrow W$ is the identity. Therefore, $U = W$, i.e. $P(x)$ holds for all $x\in W$.

John Baez (Apr 03 2023 at 21:17):

Jacob Zelko is just beginning his studies of pure math, learning how to prove things, so initial algebras of endofunctors may be too much for him - and definitely for the faculty who will be grading his homework!

Mike Shulman (Apr 03 2023 at 21:18):

I don't see Jacob Zelko in this thread?

David Egolf (Apr 03 2023 at 23:05):

Awesome! Looks like there's a lot of great responses here! Thanks everyone. Once I spend some time absorbing what's here in a bit more detail, I'll write up some thoughts in response.

John Baez (Apr 03 2023 at 23:36):

Okay, @Mike Shulman. I'm mixed up about people, as usual. Jakob has been looking for advice on how to prove things, and I thought this was a continuation of that. I was recently explaining the basics of first-order logic to David Egolf, like what's a "predicate", so initial algebras of endofunctors might be a bit heavy-duty for him, but what the heck.... he's resilient, he'll bounce back.

Mike Shulman (Apr 03 2023 at 23:44):

Sure, I can see that it might be heavy for some readers. But I can also imagine a reader who knows some category theory but not so much set theory or formal logic, for whom initial algebras of endofunctors might be easier to understand than well-founded partial orders. I don't know anything about David's background.

John Baez (Apr 03 2023 at 23:47):

I've been talking with him a lot here so I have detailed model of his internal state. :upside_down: But yes, even if he isn't thrilled by "induction via initial algebras" (and he actually might be), someone else will.

Mike Shulman (Apr 04 2023 at 17:33):

I just noticed that Clive Newstead's intro-to-proofs textbook infinite descent includes a section at the very end (12.2) on "inductively defined sets". It looks pretty good and pretty accessible.

David Egolf (Apr 04 2023 at 18:04):

Mike Shulman said:

I just noticed that Clive Newstead's intro-to-proofs textbook infinite descent includes a section at the very end (12.2) on "inductively defined sets". It looks pretty good and pretty accessible.

Oh, that does look good! In addition to the section you note, I am also drawn to the simple clear definition of a "predicate". (Ahh, the struggle of having access to more interesting books than the time and energy to read them!)

David Egolf (Apr 04 2023 at 20:49):

John Baez said:

3) use old-fashioned induction on natural numbers, by assigning to each wff (or whatever you're doing) a natural number describing its complexity, in such a way that a wff of complexity n+1 can only be obtained in various specified ways (which you list) from a wff of complexity n.

I thought it would be interesting to try to complete the above exercise using a few of the different approaches suggested above, starting with the "weak induction principle". The trick here is assigning a complexity natural number to wffs so that a wff complexity $n+1$ can be made in a simple way from wffs with complexity $n$.

For example, consider the wff $(A1 \vee A2) \vee A3$. This is formed by apply the $\vee$ formula-building operation to $(A1 \vee A2)$ and $A3$. Since both of these wffs are used as ingredients to make a wff with some complexity $n+1$, I'd like to assign them each complexity $n$. However, $A1 \vee A2$ seems like it should probably be assigned a higher complexity number than $A3$.

In general, it seems more natural to instead ask that we build a wff of complexity $n+1$ from formulas of complexity $n$ or less (instead of strictly those of complexity $n$). I believe that will corresponds to using strong induction, and I'll try that in a minute.

David Egolf (Apr 04 2023 at 21:18):

Here's the principle of strong induction as stated in "An Infinite Descent into Pure Mathematics":
strong induction

We set $p(n)$ to be: "A wff constructed by application of $n$ formula-building operations satisfies $s=c+1$."
$p(0)$ is: A wff constructed by application of 0 formula-building operations satisfies $s=c+1$. This is true because $s=1$ and $c=0$ for our sentence symbols, which are the only wffs formed by applying zero formula-building operations.

For arbitrary $n \geq 0$, we now assume that $p(k)$ is true for all $0 \leq k \leq n$.
We want to show that $p(n+1)$ is true under this assumption.
$p(n+1)$ is: A wff constructed by application of $n+1$ formula-building operations satisfies $s=c+1$.
Let $\gamma$ be a wff constructed by application of $n+1$ formula-building operations.
Then $\gamma$ is of one of the following forms:
(¬ α), (α ∧ β), (α ∨ β), (α → β)
where $\alpha$ and $\beta$ are wffs.
In each case, $\gamma$ is constructed from wffs constructed by application of $n$ or fewer formula-building operations.
In the first case, $\gamma = (\neg \alpha)$. We know $\alpha_s = \alpha_c + 1$ by our assumption.
(Here $\alpha_s$ denotes $s$ for the wff $\alpha$, and $\alpha_c$ denotes $c$ for $\alpha$).
So, $\gamma_s = \alpha_s$ and $\gamma_c = \alpha_c$ and $\gamma_s = \gamma_c + 1$.
In the second case $\gamma = \alpha \wedge \beta$, we know $\alpha_s = \alpha_c + 1$ and $\beta_s = \beta_c + 1$ by our assumption.
So, $\gamma_s = \alpha_s + \beta_s = \alpha_c + \beta_c + 2$ and $\gamma_c = \alpha_c + \beta_c + 1$. That gives $\gamma_s = \gamma_c + 1$ as desired.
The remaining two cases are similar to this one.
We conclude $p(n+1)$ is true for arbitrary $n \geq 0$, assuming that $p(k)$ is true for all $0 \leq k \leq n$.

By the strong induction principle, $p(n)$ is true for all $n \geq 0$.

This approach seems like it's a good match for this exercise, as we can combine wffs of varying complexity to make a wff of a given complexity.

David Egolf (Apr 04 2023 at 21:20):

Whew. Time for me to take a break now!

Jason Erbele (Apr 05 2023 at 20:05):

It is perhaps worth noting that this proof by strong induction of a statement about wffs can be turned into a proof of the statement about graphs that Jacob Zelko started the Fantastic Proofs thread with. Just substitute "path" for "wff", "vertex" for "sentence symbol", and "edge" for "connective symbol" (and ignore negation altogether).

Well, technically we also have to start at n=1 instead of n=0 to match up with the definition of path given there (though I would argue for including the degenerate path with one vertex in the set of paths).

Jacob Zelko (Apr 08 2023 at 00:14):

Hi folks! Been busy traveling and wrapping up a paper submission (:partying_face:)! Was catching up and saw my name pop up a bit! Feel free to always ping me if you want. :smile:

Regarding induction, I’m still in the process of gaining basic understanding to talk about wffs. Right now, working through Velleman and truth tables as we speak!!

David Egolf (Apr 20 2023 at 15:16):

Mike Shulman said:

Another way to justify structural induction is to talk about general "inductive definitions", which categorically are [[initial]] [[algebras for an endofunctor]]. In the case of logical formulas (I dislike the term "wff" because no one ever wants to talk about an "ill-formed" formula), we are talking about the endofunctor of $\rm Set$ defined by
$F(x) = S + X + (X\times X) + (X\times X) + (X\times X) + (X\times X)$
where $S$ is the set of sentence symbols. An $F$-algebra is a set $X$ with a function $F(X) \to X$, which means that we have an interpretation of every sentence symbol as an element of $X$, together with one unary operation $X\to X$ corresponding to negation, and four binary operations $X\times X \to X$ corresponding to disjunction, conjunction, implication, and equivalence. The set $W$ of formulas is the initial such $F$-algebra, which means that its elements are "freely generated" by applying these operations formally. This is a categorical way to express that "Every wff is constructed from sentence symbols by application of a finite number of formula-building operations."

Let me try and understand this a little. We have our endofunctor $F: \rm Set \to \rm Set$ which sends each set $X$ to the set $S + X + (X\times X) + (X\times X) + (X\times X) + (X\times X)$. Then, for a choice of $X$, a function $F(X) \to X$ defines several functions "side by side": $F_S: S \to X$, $F_{\neg}: X \to X$, $F_{\wedge}: X \times X \to X$, $F_{\vee}: X \times X \to X$, $F_{\implies}: X \times X \to X$ and an extra function (relative to the operations I discussed above) $F_\equiv: X \times X \to X$.

I think we are working towards providing data that describes how to make new logical formulas from old ones, or from sentence symbols. It's cool to see how an $F$-algebra describes a set of "building blocks", together with a collection of operations to combine them. I suppose this idea could be generalized to other categories too, with products and coproducts (?).

Now, there are lots of choices we could make for $X$. However, we want to pick $X$ in some "free" way, if I understand correctly, so that $X$ becomes a set of logical formulas. I think this corresponds to putting the symbols $S$ in $X$, and then adding a new formula for the output of each our unary and binary operators - and we require the outputs of each of these to be distinct, for distinct inputs. I guess this should yield the logical formulas we want.

David Egolf (Apr 20 2023 at 15:28):

To understand the rest, I think I'd need to try some examples with the definition of a morphism between $F$-algebras. I don't yet really understand what it means to have a morphism between two $F$-algebras. (Although I see the definition on the nlab page you linked, it will take me some absorbing/practice with the idea).

Ralph Sarkis (Apr 20 2023 at 15:33):

This is a great tutorial, but it also covers coinduction at the same time. Maybe you can try reading only Section 5.

Mike Shulman (Apr 20 2023 at 16:29):

In this case, a morphism of $F$-algebras is a function that preserves the map from $S$, the negation unary operation, and the four binary operations. That is, if $\phi:X\to Y$ is a morphism of $F$-algebras, we have $\phi(F_S^X(s)) = F_S^Y(s)$, $\phi(F_\neg^X(x)) = F_\neg^Y(\phi(x))$, $\phi(F_\wedge^X(x_1,x_2)) = F_\wedge^Y(\phi(x_1),\phi(x_2))$, etc.