1
$\begingroup$

(Context: this is a problem from the middle of my dissertation work, abstracted into a more general problem. It's related to showing that some liveness properties hold, so perhaps work from something like CTL could apply.)

Say you have some tree of possibly infinite depth with root node $n_0$. (EDIT: the number of children per node is bounded, in case that helps.) There exists a special set $G$ of "good" nodes in the tree such that for every path from $n_0$ through the tree, that path contains a node in $G$ (although that node can be at any arbitrary depth).

Now, say there is some property $P$ on nodes of the tree such that $P(n)$ holds if and only if:

  • $n \in G$, or
  • for every child node $n'$ of $n$, $P(n')$ holds.

To prove: $P(n_0)$ holds

$P$ is practically another way of saying "every path has a node in $G$", so this seems almost trivial. However, I can't seem to formally prove it. An inductive proof seems like the way to go ("I expect my children to all be in P if I'm not in $G$ myself, so $P$ should hold for me"), but what to induct on? Something like "distance until the farthest "good" node" seems natural, but I'm not sure such a bound exists.

I'm reasonably sure this statement can be proved, so how to prove it? Is there indeed a bound on the farthest "good node", and if so, what is the argument that such a bound exists?

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ Is it too naive to prove this by contradiction? If $\neg P(n_0)$, then $\exists$ child $n_1$ of $n_0$ such that $\neg P(n_1)$, $\exists$ child $n_2$ of $n_1$ such that $\neg P(n_2)$, etc... leading to a path $n_0, n_1, n_2, \ldots$ that does not contain any node in $G$. I think this avoids any Axiom of Choice issues but I'm not 100% certain. $\endgroup$
    – mhum
    Commented Apr 6, 2018 at 23:11
  • 1
    $\begingroup$ If you truncate the tree at the good nodes, isn't this just en.wikipedia.org/wiki/K%C3%B6nig%27s_lemma ? The truncated tree has no infinite paths (because they must all be truncated) and no infinite degree nodes (by assumption) so by König's infinity lemma it is a finite tree. Now in the finite tree you can use induction on the size of the subtree below each node. $\endgroup$
    – David Eppstein
    Commented Apr 6, 2018 at 23:49
  • $\begingroup$ Thank you both! I think the proof by contradiction should work for my purposes, especially since I realize now it could be helpful in my work to generalize to infinitely-branching trees (which I think that proof would support). It's good to have König's lemma too, though, as a backup in case that doesn't work out for some reason. $\endgroup$
    – Jonathan Schuster
    Commented Apr 9, 2018 at 13:44

1 Answer 1

Reset to default
0
$\begingroup$

See the comments on the question above: both a proof by contradiction and a use of König's lemma appear to suffice.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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