Vanessa Kosoy's Shortform

Vanessa Kosoy

Infra-Bayesianism can be naturally understood as semantics for a certain non-classical logic. This promises an elegant synthesis between deductive/symbolic reasoning and inductive/intuitive reasoning, with several possible applications. Specifically, here we will explain how this can work for higher-order logic. There might be holes and/or redundancies in the precise definitions given here, but I'm quite confident the overall idea is sound.

We will work with homogenous ultracontributions (HUCs). will denote the space of HUCs over $X$ . Given $μ \in □ X$ , $S (μ) \subseteq Δ^{c} X$ will denote the corresponding convex set. Given $p \in Δ X$ and $μ \in □ X$ , $p : μ$ will mean $p \in S (μ)$ . Given $μ, ν \in □ X$ , $μ ⪯ ν$ will mean $S (μ) \subseteq S (ν)$ .

Syntax

Let $T^{ι}$ denote a set which we interpret as the types of individuals (we allow more than one). We then recursively define the full set of types $T$ by:

$0 \in T$ (intended meaning: the uninhabited type)
$1 \in T$ (intended meaning: the one element type)
If $α \in T^{ι}$ then $α \in T$
If $α, β \in T$ then $α + β \in T$ (intended meaning: disjoint union)
If $α, β \in T$ then $α \times β \in T$ (intended meaning: Cartesian product)
If $α \in T$ then $(α) \in T$ (intended meaning: predicates with argument of type $α$ )

For each $α, β \in T$ , there is a set $F_{α \to β}^{0}$ which we interpret as atomic terms of type $α \to β$ . We will denote $V_{α}^{0} := F_{1 \to α}^{0}$ . Among those we distinguish the logical atomic terms:

${p r}_{α β} \in F_{α \times β \to α}^{0}$
$i_{α β} \in F_{α \to α + β}^{0}$
Symbols we will not list explicitly, that correspond to the algebraic properties of $+$ and $\times$ (commutativity, associativity, distributivity and the neutrality of $0$ and $1$ ). For example, given $α, β \in T$ there is a "commutator" of type $α \times β \to β \times α$ .
$=_{α} \in V_{(α \times α)}^{0}$
${d i a g}_{α} \in F_{α \to α \times α}^{0}$
$()_{α} \in V_{((α) \times α)}^{0}$ (intended meaning: predicate evaluation)
$⊥ \in V_{(1)}^{0}$
$⊤ \in V_{(1)}^{0}$
$\lor_{α} \in F_{(α) \times (α) \to (α)}^{0}$
$\land_{α} \in F_{(α) \times (α) \to (α)}^{0}$ [EDIT: Actually this doesn't work because, except for finite sets, the resulting mapping (see semantics section) is discontinuous. There are probably ways to fix this.]
$\exists_{α β} \in F_{(α \times β) \to (β)}^{0}$
$\forall_{α β} \in F_{(α \times β) \to (β)}^{0}$ [EDIT: Actually this doesn't work because, except for finite sets, the resulting mapping (see semantics section) is discontinuous. There are probably ways to fix this.]
Assume that for each $n \in N$ there is some $D_{n} \subseteq □ [n]$ : the set of "describable" ultracontributions [EDIT: it is probably sufficient to only have the fair coin distribution in $D_{2}$ in order for it to be possible to approximate all ultracontributions on finite sets]. If $μ \in D_{n}$ then $┌ μ ┐ \in V_{(\sum_{i = 1}^{n} 1)}$

We recursively define the set of all terms $F_{α \to β}$ . We denote $V_{α} := F_{1 \to α}$ .

If $f \in F_{α \to β}^{0}$ then $f \in F_{α \to β}$
If $f_{1} \in F_{α_{1} \to β_{1}}$ and $f_{2} \in F_{α_{2} \to β_{2}}$ then $f_{1} \times f_{2} \in F_{α_{1} \times α_{2} \to β_{1} \times β_{2}}$
If $f_{1} \in F_{α_{1} \to β_{1}}$ and $f_{2} \in F_{α_{2} \to β_{2}}$ then $f_{1} + f_{2} \in F_{α_{1} + α_{2} \to β_{1} + β_{2}}$
If $f \in F_{α \to β}$ then $f^{- 1} : F_{(β) \to (α)}$
If $f \in F_{α \to β}$ and $g \in F_{β \to γ}$ then $g \circ f \in F_{α \to γ}$

Elements of $V_{(α)}$ are called formulae. Elements of $V_{(1)}$ are called sentences. A subset of $V_{(1)}$ is called a theory.

Semantics

Given $T \subseteq V_{(1)}$ , a model $M$ of $T$ is the following data. To each $α \in T$ , there must correspond some compact Polish space $M (t)$ s.t.:

$M (0) = \emptyset$
$M (1) = p t$ (the one point space)
$M (α + β) = M (α) ⊔ M (β)$
$M (α \times β) = M (α) \times M (β)$
$M ((α)) = □ M (α)$

To each $f \in F_{α \to β}$ , there must correspond a continuous mapping $M (f) : M (α) \to M (β)$ , under the following constraints:

$p r$ , $i$ , $d i a g$ and the "algebrators" have to correspond to the obvious mappings.
$M (=_{α}) = ⊤_{{d i a g}_{M (α)}}$ . Here, ${d i a g}_{X} \subseteq X \times X$ is the diagonal and $⊤_{C} \in □ X$ is the sharp ultradistribution corresponding to the closed set $C \subseteq X$ .
Consider $α \in T$ and denote $X := M (α)$ . Then, $M (()_{α}) = ⊤_{□ X} ⋉ {i d}_{□ X}$ . Here, we use the observation that the identity mapping ${i d}_{□ X}$ can be regarded as an infrakernel from $□ X$ to $X$ .
$M (⊥) = ⊥_{p t}$
$M (⊤) = ⊤_{p t}$
$S (M (\lor) (μ, ν))$ is the convex hull of $S (μ) \cup S (ν)$
$S (M (\land) (μ, ν))$ is the intersection of $S (μ) \cup S (ν)$
Consider $α, β \in T$ and denote $X := M (α)$ , $Y := M (β)$ and $p r : X \times Y \to Y$ the projection mapping. Then, $M (\exists_{α β}) (μ) = {p r}_{*} μ$ .
Consider $α, β \in T$ and denote $X := M (α)$ , $Y := M (β)$ and $p r : X \times Y \to Y$ the projection mapping. Then, $p : M (\forall_{α β}) (μ)$ iff for all $q \in Δ^{c} (X \times Y)$ , if ${p r}_{*} q = p$ then $q : μ$ .
$M (f_{1} \times f_{2}) = M (f_{1}) \times M (f_{2})$
$M (f_{1} + f_{2}) = M (f_{1}) ⊔ M (f_{2})$
$M (f^{- 1}) (μ) = M (f)^{*} (μ)$ .
$M (g \circ f) = M (g) \circ M (f)$
$M (┌ μ ┐) = μ$

Finally, for each $ϕ \in T$ , we require $M (ϕ) = ⊤_{p t}$ .

Semantic Consequence

Given $ϕ \in V_{(1)}$ , we say $M ⊨ ϕ$ when $M (ϕ) = ⊤_{p t}$ . We say $T ⊨ ϕ$ when for any model $M$ of $T$ , $M ⊨ ϕ$ . It is now interesting to ask what is the computational complexity of deciding $T ⊨ ϕ$ . [EDIT: My current best guess is co-RE]

Applications

As usual, let $A$ be a finite set of actions and $O$ be a finite set of observation. Require that for each $o \in O$ there is $σ_{o} \in T^{ι}$ which we interpret as the type of states producing observation $o$ . Denote $σ_{*} := \sum_{o \in O} σ_{o}$ (the type of all states). Moreover, require that our language has the nonlogical symbols $s_{0} \in V_{(σ_{*})}^{0}$ (the initial state) and, for each $a \in A$ , $K_{a} \in F_{σ_{*} \to (σ_{*})}^{0}$ (the transition kernel). Then, every model defines a (pseudocausal) infra-POMDP. This way we can use symbolic expressions to define infra-Bayesian RL hypotheses. It is then tempting to study the control theoretic and learning theoretic properties of those hypotheses. Moreover, it is natural to introduce a prior which weights those hypotheses by length, analogical to the Solomonoff prior. This leads to some sort of bounded infra-Bayesian algorithmic information theory and bounded infra-Bayesian analogue of AIXI.

Vanessa Kosoy's Shortform

6

Vanessa Kosoy's Shortform

6