User:IssaRice/Logical inductor construction

Notes from the Logical Induction paper as I walk through the construction of LIA in section 5.

Lemma 5.1.1 (Fixed Point Lemma)

"Observe that $\mathcal{V}\text{'}$ is equal to the natural inclusion of the finite-dimensional cube $[0,1{]}^{{{\mathcal{S}}^{\prime }}^{\prime }}$ in the space of all valuations $\mathcal{V}=[0,1{]}^{\mathcal{S}}$." -- I think what this is saying is that since $\mathcal{S}\text{'}\subset \mathcal{S}$, we can think of $[0,1{]}^{{{\mathcal{S}}^{\prime }}^{\prime }}$ as being sort of a subset of $[0,1{]}^{\mathcal{S}}$. Except it's not strictly speaking a subset, since the functions in $[0,1{]}^{{{\mathcal{S}}^{\prime }}^{\prime }}$ and $[0,1{]}^{\mathcal{S}}$ have different domains. How can we make it a subset? The "natural" way to do this is to set everything outside of $\mathcal{S}\text{'}$ to zero. But that's exactly what $\mathcal{V}\text{'}=\{\mathbb{V}\in [0,1{]}^{\mathcal{S}}:\mathbb{V}(\varphi )=0\text{ whenever }\varphi \notin {{\mathcal{S}}^{\prime }}^{\prime }\}$ is. One thing I'm still not sure about is the "finite-dimensional" part; doesn't having $[0,1]$ make the cube infinite-dimensional?

"the compact, convex space $\mathcal{V}\text{'}$" -- this intuitively makes sense, since $\mathcal{V}\text{'}$ basically "looks like" a cube. But I'm not sure how to verify this.

The following is used in the Fixed Point Lemma (5.1.1):

Writing the $n$-strategy as

$T_n=\sum _{j=1}^k{\xi }_j{\varphi }_j-\sum _{j=1}^k{\xi }_j\underset{j}{\overset{*n}{\varphi }}$

we have

$\mathbb{V}(T_n({\mathbb{P}}_{\le n-1},\mathbb{V}))=\sum _{j=1}^k{\xi }_j({\mathbb{P}}_{\le n-1},\mathbb{V})\cdot \mathbb{V}({\varphi }_j)-\sum _{j=1}^k{\xi }_j({\mathbb{P}}_{\le n-1},\mathbb{V})\cdot \underset{j}{\overset{*n}{\varphi }}({\mathbb{P}}_{\le n-1},\mathbb{V})$

But $\underset{j}{\overset{*n}{\varphi }}({\mathbb{P}}_{\le n-1},\mathbb{V})=\mathbb{V}({\varphi }_j)$ so the two sums cancel to obtain $0$.

See also

• https://machinelearning.subwiki.org/wiki/User:IssaRice/Logical_induction_notation