Is there a set-theoretic proof of Induction on the complexity of formulae?

Question

The Induction on the complexity of formulae is a theorem on the syntax of PL that states the following:

Suppose an arbitrary property holds for all atomic formulae in PL, and, if it holds for A and B, then it holds for (¬A), (A∨B), (A∧B), (A→B) and (A↔B). Then this property holds for all formulae on PL.

I've seen many intuitive and "classic" demonstrations on this theorem, but is there a purely set-theoretic proof on this theorem?

What do you mean by a "purely set theoretic proof" and what do you hope to get from it? — spaceisdarkgreen, Feb 05 '22 at 23:54
This is induction on a well-founded tree (or well-founded induction), but even simpler, because the trees are finitely branching. — Couchy, Feb 06 '22 at 02:16
Is a proof method used to prove theorems stating properties of formulas or derivations. — Mauro ALLEGRANZA, Feb 06 '22 at 08:09
See also this post as well as the post Understanding Structural Induction — Mauro ALLEGRANZA, Feb 07 '22 at 07:32

score 0 · Accepted Answer · answered Feb 06 '22 at 17:24

The well-founded induction principle says the following: If you have a well-founded relation $<$ on a set $X$ (that is there is no infinitely long decreasing chain $x_1 > x_2 > x_3 > \ldots$), then given a proposition $\phi(x)$ on $x\in X$, $$(\forall x.(\forall y < x. \phi(y))\to\phi(x))\to(\forall x.\phi(x)).$$ This can be proved in set theory.

Now in the case of a finitely branching trees, let $X$ be the set of possible trees (or terms in your case), and let $x < y$ if $x$ is a subtree (or subterm) of $y$. This relation is well-founded, and the corresponding induction principle obtained from the above is called structural-induction.

Is there a set-theoretic proof of Induction on the complexity of formulae?

1 Answers1