Elementary Logic in Linear Space

Let $\mathcal{A}[\bar{y}]$ denote the set of all atomic formula (i.e., a predicate applied to a tuple of variables) involving the free variables $\bar{y}$. Let $\mathcal{B}[\bar{y}]$ denote the subset of $\mathcal{A}[\bar{y}]$ that mentions the last element of $\bar{y}$ at least once. Let

be the set where an element is a conjunction of every $\phi_{i}$ or its negation where $(\pm)^{0}\phi\triangleq\lnot\phi$, and $(\pm)^{1}\phi\triangleq\phi$.

The set of attributive constituents $\Gamma^{(r)}[\bar{y}]$ with free variables $\bar{y}$ is defined by induction on quantifier rank $r$.

In the base case,

Intuitively, a rank $0$ attributive constituent with free variables $\bar{y}=y_{1},\dots,y_{k}$ describes how the individual $y_{k}$ relates to the other individuals $y_{1},\dots,y_{k-1}$ via all the atomic formula in the language.

In the inductive case,

The notation $(\exists^{E}z)$ indicates an exclusive interpretation of quantification so that $z$ is distinct from all other variables in scope. For example, $(\exists^{E}z)\phi[\bar{y};z]\triangleq(\exists z)z\neq y_{1}\land\dots\land z\neq y_{k}\land\phi[\bar{y};z]$ where $x\neq y$ is shorthand for $\lnot(x=y)$. Intuitively, a rank $r$ constituent with free variables $\bar{y}$ describes (1) how $y_{k}$ is related to each $y_{1},\dots,y_{k-1}$ where $\bar{y}=y_{1},\dots,y_{k}$ and (2) for every possible smaller description (i.e., a rank $r-1$ attributive constituents), whether or not an additional individual $z$ exists that is related to the other individuals $\bar{y}$ recursively via that description.

The set of rank $r$ constituents $\Delta^{(r)}[\bar{y}]$ with free variables $\bar{y}$ is defined using attributive constituents as

Thus a rank $r$ constituent with free variables $\bar{y};z$ completes the description of a rank $r$ attributive constituent by additionally describing how each term in $\bar{y}$ is related to one another. Thus we can think of a constituent as describing a possible kind of “logical world”.

Some constituents will be unsatisfiable, and hence, describe possibilities that are impossible. The satisfiable constituents, on the other hand, describe logically possible worlds.

As a reminder, a (real-valued) vector space $(V,+,\cdot)$ is a set $V$ along with vector addition $+:V\times V\rightarrow V$ and scalar multiplication $\cdot:\mathbb{R}\times V\rightarrow V$ satisfying the vector space axioms. We define a vector space for sentences of quantifier rank $r$ by defining the set and the two operations.

The vector space spans all rank $r$ first-order sentences.

As a reminder, every sentence of rank $s\leq r$ is equivalent to some sentence of rank $r$. Thus this vector space expresses all first-order sentences up to rank $r$.

The number of attributive constituents of rank $r$ can be computed recursively as

where $|\Gamma^{(0)}[\bar{y}]|$, is combinatorial in the number of base predicates in $\bar{y}$. The number of constituents of rank $r$ is then

where $|\Delta^{(0)}[\bar{y}]|$ is combinatorial in the number of base predicates in $\bar{y}$. Consequently, the first-order vector space has a super-exponential number of dimensions as a function of quantifier rank $r$. Thus the vector space has astronomic dimension. Later in Section 7, we will see how models of a theory can be used to approximately span the theory.

We can define an inner product between two vectors in the standard way:

It is a routine exercise to check that this is an inner product. As usual, two vector are orthogonal if their inner product is $0$.

The converse does not hold because there can be multiple inconsistent constituents at some quantifier rank $r$. In other words, there are multiple ways to express falsehood in this standard basis so we may have two unsatisfiable sentences that have an inner product of $0$. Note that if we remove all inconsistent constituents of rank $r$ from the basis, then we end up with a basis of $r$-isomorphism types (e.g., see (Libkin, 2004)). In this case, falsehood is represented by $\vec{0}$.

Let $\mathcal{E}$ be an enumeration $\mathcal{L}^{(r)}$ that spans it, i.e., every first-order sentence of rank $r$ can be written as a disjunction of elements from $\mathcal{E}$. Given an enumeration of $\mathcal{L}^{(r)}$, we can construct an enumeration that spans it as $\lnot\phi^{(r)}_{1},\phi^{(r)}_{1},\lnot\phi^{(r)}_{1}\land\lnot\phi^{(r)}_{2},\lnot\phi^{(r)}_{1}\land\phi^{(r)}_{2},\phi^{(r)}_{1}\land\lnot\phi^{(r)}_{2},\phi^{(r)}_{1}\land\phi^{(r)}_{2},\dots$.

Recall that the Gram-Schmidt process is a method for constructing an orthonormal basis from a set of vectors that spans the space. Applying the Gram-Schmidt process results in the following basis: $\hat{e_{1}}\triangleq\phi^{(r)}_{1},\hat{e_{2}}\triangleq\lnot\phi^{(r)}_{1}\land\phi^{(r)}_{2},\hat{e_{3}}\triangleq\lnot\phi^{(r)}_{1}\land\lnot\phi^{(r)}_{2}\land\phi^{(r)}_{3},\dots$.

We begin by recalling a basic fact about constituents and their expansion to higher quantifier rank.

Observe that a constituent can be the expansion of two distinct constituents, in which case it is necessarily unsatisfiable. In symbols, if $\delta^{(r+s)}\succ^{s}_{r}\delta^{(r)}_{1}$ and $\delta^{(r+s)}\succ^{s}_{r}\delta^{(r)}_{2}$ then $\nvDash\delta^{(r+s)}$.

Additionally, observe that the notion of expansion is consistent with logical implication. More concretely, if $\delta^{(r+s)}\succ^{s}_{r}\delta^{(r)}$ then $\vDash\delta^{(r+s)}\rightarrow\delta^{(r)}$. When $\delta^{(r+s)}$ is satisfiable, we can interpret it as extending the description of a logical possibility denoted by $\delta^{(r)}$ to account for $s$ additional individuals. In other words, $\delta^{(r+s)}$ is a higher resolution description of $\delta^{(r)}$. When $\delta^{(r+s)}$ is not satisfiable, we can interpret it as an inconsistent description obtained by extending some description (either consistent or inconsistent).

These two observations highlight a certain asymmetry between satisfiable and unsatisfiable descriptions. Whereas a satisfiable constituent is necessarily in the expansion of another unique satisfiable constituent at a given rank due to mutual exclusivity, an unsatisfiable constituent can be in the expansion of any constituent. We thus have to make a choice about how different logical impossibilities are related to one another in order to prevent two sequences that eventually describe logical impossibilities from merging into each other.

We use a syntactic criterion to aid with uniquely associating constituents with their expansions.³³3The syntactic criterion we use is one of the conditions used in the definition of trivial inconsistency (Hintikka, 1965). Trivial inconsistency is a syntactic criterion for determining whether or not a constituent is satisfiable that satisfies a completeness property (Hintikka, 1965): a constituent that is not satisfiable has a quantifier rank where all of its expansions are trivially inconsistent. The idea is to define a suitable notion for a constituent $\delta^{(r)}$ to be a prefix of another constituent $\delta^{(r+1)}$.

The notation

gives the set representation of a constituent where the notation $\langle\cdot\rangle^{\gamma^{(r-1)}[z]}_{\gamma^{(r)}}$ indicates that whether or not the formula inside is negated depends on $\gamma^{(r-1)}[z]$ and $\gamma^{(r)}$. When the quantifier rank is $0$, we have $\dagger\delta^{(0)}\triangleq\{\top\}$. The notation $\tilde{\delta}^{(r)}$ indicates that we remove the deepest layer of quantification from $\delta^{(r)}$, i.e., all formula involving the rank $r$ quantifiers.⁴⁴4We can see the effect that removing a layer of quantification has on a constituent by rewriting it to only use rank $0$ attributive constituents as $\displaystyle\delta^{(r+1)}\equiv\bigwedge_{\gamma^{(r-1)}[z_{1}]\in\Gamma^{(r)}[z_{1}]}\Big{\langle}(\exists^{E}z_{1})\gamma^{(0)}[z_{1}]\land\ldots\Big{\langle}$ $\displaystyle\bigwedge_{\gamma^{(0)}[\bar{z}_{r+1}]\in\Gamma^{(0)}[\bar{z}_{r+1}]}\Big{\langle}(\exists^{E}z_{r+1})\gamma^{(0)}[\bar{z}_{r+1}]\Big{\rangle}^{\gamma^{(1)}[\bar{z}_{r}]}_{\gamma^{(r+1)}}\ldots\Big{\rangle}^{\gamma^{(r)}[z_{1}]}_{\gamma^{(r+1)}}\,.$

We say that $\delta^{(r)}$ is a prefix of $\delta^{(r+1)}$, written $\delta^{(r)}\sqsubseteq\delta^{(r+1)}$, if $\dagger\gamma^{(r)}=\dagger\tilde{\gamma}^{(r+1)}$.

The first item ensures that every constituent is the prefix of some expansion constituent so that the resolution of its description can increased. The second and third items ensure that prefixes are compatible with logical implication. More concretely, the second ensures that satisfiable expansions have satisfiable prefixes while the third ensures that an unsatisfiable constituent is the prefix of some unsatisfiable expansion.

Define a sequence of graphs as follows. Let $T_{0}\triangleq(\Delta^{(0)},\{\})$ so that the vertices are the constituents of rank $0$ and no edges. Let $T_{r+1}\triangleq T_{r}\cup(\Delta^{(r+1)},\xi^{(r+1)})$ with edges $\xi^{(r+1)}\triangleq\operatorname{edges}(r,\xi^{(r)})$ where $\operatorname{edges}$ is defined in Algorithm 1.

Recall that we can define a topology on a tree by defining a basis of open sets identified by finite initial segments of the tree.⁵⁵5For background on topology, we refer the reader to (Munkres, 2000). Let $\Psi$ be the set of paths of a refinement tree. We write $\bar{\delta}^{(r)}$ to indicate the path $(\delta^{(0)},\dots,\delta^{(r)})$ in a refinement tree. Then a basic open set has the form

where $\sqsubseteq$ indicates a prefix relation on refinement tree paths. We can think of a basic open $B_{\delta^{(r)}}$ as the description of $\delta^{(r)}$ along with all possible ways in which that description can be extended.

The inner product $\langle\cdot,\cdot\rangle$ is given by

for $f,g\in\mathbb{H}$ (i.e., $f$ and $g$ are square integrable).

Although there are an uncountable number of infinitely precise descriptions, there is a sense in which we really only have a denumerable handle on them.

This concludes the construction of a space for first-order logic. For simplicity, we will largely restrict attention to the case of fixed quantifier rank throughout the rest of the paper as it suffices to illustrate the main ideas of what a “signals in space” perspective might offer.

We use the observation that $\phi_{1}\rightarrow\phi_{2}$ is syntactic sugar for $\lnot\phi_{1}\lor\phi_{2}$ to express mp as an operator.

Analogous to how we can model the evolution of a physical system by considering the sequencing of operators that correspond to physical processes, we can model the evolution of a logical system by considering the effects of sequencing mp operators that correspond to deductive processes.

Observe that $\textbf{MP}_{\phi_{1}\rightarrow\phi_{2}}$ is a continuous operator. We can interpret this as another instantiation of the locality of computation: Any sentence that can be deduced is a sequence of local and small steps. As it turns out, $\textbf{MP}_{\phi_{1}\rightarrow\phi_{2}}$ is “entropic” in a sense that we describe next.

We begin with the observation that mp increases plausibility of a logical system.

Intuitively, the plausibility of a logical system increases because the number of possibilities we consider possible after an application of mp increases. Note that this fact does not contradict the law of conservation of plausibility. In particular, an application of mp changes the logical system under consideration which may no longer be the total system $\bm{\top}$.

We can rephrase the increase in plausibility as an increase in unnormalized entropy. Recall the unnormalized entropy of a vector $(a_{1},\dots,a_{n})$ is defined as $U(a_{1},\dots,a_{n})\triangleq\sum_{i=1}^{n}a_{i}(1-\log(a_{i}))$. Let $\bm{\phi}^{\ddagger}$ be the vector where $\langle\hat{\delta}^{(R)},\bm{\phi}\rangle=1$ whenever $\delta^{(R)}\in\operatorname{dnf}(\phi)$ and $\langle\hat{\delta}^{(R)},\bm{\phi}\rangle=\alpha$ otherwise where $\alpha>0$.

Let $\operatorname{refute}:\mathcal{L}\rightarrow\mathbf{2}$ be a function that soundly approximates the deduction relation, i.e., $\operatorname{refute}(\phi)=\top$ implies that $\nvDash\phi$. We can think of $\operatorname{refute}(\phi)$ as a resource-bound prover. Similarly, let $\operatorname{check}_{\mathcal{M}}\mathcal{L}\rightarrow\mathbf{2}$ be a function that soundly approximates a model checker, i.e., $\operatorname{check}_{\mathcal{M}}(\phi)=\top$ implies that $\mathcal{M}\vDash\phi$. As before, we can think of $\operatorname{check}_{\mathcal{M}}(\phi)$ as a resource-bound model checker.

Suppose we have sentences $\phi^{F}_{1},\dots,\phi^{F}_{N}$ that are known to be false, knowledge of models $\mathcal{M}_{1},\dots,\mathcal{M}_{M}$, and sentences $\phi_{1},\dots,\phi_{L}$ whose satisfiability is not known. We can interpret $\lnot\phi^{F}_{1},\dots,\lnot\phi^{F}_{N}$ as theorems, $\mathcal{M}_{1},\dots,\mathcal{M}_{M}$ as common examples, $\phi_{1},\dots,\phi_{L}$ as conjectures that are specific to the agent. (We will see why we include conjectures momentarily.) Let $\phi_{0}\triangleq\bigwedge_{i=1}^{N}\phi^{F}_{i}$. Let $N_{ij}\triangleq 1$ when $\operatorname{refute}(\phi_{i}\rightarrow\phi_{j})=\top$ and