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

CC BY-SA 3.0
2018-04-09T13:45:14.083Z
2018-04-09T13:45:14.083Z
Jonathan Schuster
<p>(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.)</p>

<p>Say you have some tree of possibly infinite depth with root node $n_0$. (EDIT: the number of children per node <em>is</em> 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).</p>

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

<ul>
<li>$n \in G$, or</li>
<li>for every child node $n'$ of $n$, $P(n')$ holds.</li>
</ul>

<p><strong>To prove</strong>: $P(n_0)$ holds</p>

<p>$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.</p>

<p>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?</p>

CC BY-SA 3.0
2018-04-06T23:11:01.327Z
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.
mhum
CC BY-SA 3.0
2018-04-06T23:49:10.973Z
If you truncate the tree at the good nodes, isn't this just https://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.
David Eppstein
CC BY-SA 3.0
2018-04-09T13:44:35.613Z
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.
Jonathan Schuster
<tree><model-checking><temporal-logic>
Proving liveness-like property on an infinite tree
Jonathan Schuster
# Proving liveness-like property on an infinite tree

(Asked by: username_0 on 2018-04-06)

(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?

**Tags:** tree, model-checking, temporal-logic
> **Comments:**
> **username_1**: 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.  
> **username_2**: If you truncate the tree at the good nodes, isn't this just https://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.  
> **username_0**: 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.  

---

## 1 answers

### Answer by username_0 on 2018-04-09. Score: 0 | Accepted answer

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


---

