Vanessa Kosoy's Shortform

Vanessa Kosoy

Let's also explicitly describe 0th order and 1st order infra-Bayesian logic (although they are should be segments of higher-order).

0-th order

Syntax

Let be the set of propositional variables. We define the language $L$ :

Any $a \in A$ is also in $L$
$⊥ \in L$
$⊤ \in L$
Given $ϕ, ψ \in L$ , $ϕ \land ψ \in L$
Given $ϕ, ψ \in L$ , $ϕ \lor ψ \in L$

Notice there's no negation or implication. We define the set of judgements $J := L \times L$ . We write judgements as $ϕ ⊢ ψ$ (" $ψ$ in the context of $ϕ$ "). A theory is a subset of $J$ .

Semantics

Given $T \subseteq J$ , a model of $T$ consists of a compact Polish space $X$ and a mapping $M : L \to □ X$ . The latter is required to satisfy:

$M (⊥) = ⊥_{X}$
$M (⊤) = ⊤_{X}$
$M (ϕ \land ψ) = M (ϕ) \land M (ψ)$ . Here, we define $\land$ of infradistributions as intersection of the corresponding sets
$M (ϕ \lor ψ) = M (ϕ) \lor M (ψ)$ . Here, we define $\lor$ of infradistributions as convex hull of the corresponding sets
For any $ϕ ⊢ ψ \in T$ , $M (ϕ) ⪯ M (ψ)$

1-st order

Syntax

We define the language using the usual syntax of 1-st order logic, where the allowed operators are $\land$ , $\lor$ and the quantifiers $\forall$ and $\exists$ . Variables are labeled by types from some set $T$ . For simplicity, we assume no constants, but it is easy to introduce them. For any sequence of variables $(v_{1} \dots v_{n})$ , we denote $L_{v}$ the set of formulae whose free variables are a subset of $v_{1} \dots v_{n}$ . We define the set of judgements $J := ⋃_{v} L_{v} \times L_{v}$ .

Semantics

Given $T \subseteq J$ , a model of $T$ consists of

For every $t \in T$ , a compact Polish space $M (t)$
For every $ϕ \in L_{v}$ where $v_{1} \dots v_{n}$ have types $t_{1} \dots t_{n}$ , an element $M_{v} (ϕ)$ of $□ X_{v}$ , where $X_{v} := (\prod_{i = 1}^{n} M (t_{i}))$

It must satisfy the following:

$M_{v} (⊥) = ⊥_{X_{v}}$
$M_{v} (⊤) = ⊤_{X_{v}}$
$M_{v} (ϕ \land ψ) = M_{v} (ϕ) \land M_{v} (ψ)$
$M_{v} (ϕ \lor ψ) = M_{v} (ϕ) \lor M_{v} (ψ)$
Consider variables $u_{1} \dots u_{n}$ of types $t_{1} \dots t_{n}$ and variables $v_{1} \dots v_{m}$ of types $s_{1} \dots s_{m}$ . Consider also some $σ : {1 \dots m} \to {1 \dots n}$ s.t. $s_{i} = t_{σ i}$ . Given $ϕ \in L_{v}$ , we can form the substitution $ψ := ϕ [v_{i} = u_{σ (i)}] \in L_{u}$ . We also have a mapping $f_{σ} : X_{u} \to X_{v}$ given by $f_{σ} (x_{1} \dots x_{n}) = (x_{σ (1)} \dots x_{σ (m)})$ . We require $M_{u} (ψ) = f^{*} (M_{v} (ϕ))$
Consider variables $v_{1} \dots v_{n}$ and $i \in {1 \dots n}$ . Denote $p r : X_{v} \to X_{v ∖ v_{i}}$ the projection mapping. We require $M_{v ∖ v_{i}} (\exists v_{i} : ϕ) = {p r}_{*} (M_{v} (ϕ))$
Consider variables $v_{1} \dots v_{n}$ and $i \in {1 \dots n}$ . Denote $p r : X_{v} \to X_{v ∖ v_{i}}$ the projection mapping. We require that $p : M_{v ∖ v_{i}} (\forall v_{i} : ϕ)$ if an only if, for all $q \in Δ X_{v}$ s.t ${p r}_{*} q = p$ , $q : {p r}_{*} (M_{v} (ϕ))$
For any $ϕ ⊢ ψ \in T$ , $M_{v} (ϕ) ⪯ M_{v} (ψ)$

Vanessa Kosoy's Shortform

6

Vanessa Kosoy's Shortform

6