For a simple graph $X=(V,E)$, $X^\perp$ is the complementary simple graph on the same vertex set. For example if $V=\{0,1,2\}$ and $E=\{\{0,1\}\}$ then
$X^\perp = (V, \{\{0,2\},\{1,2\}\}$.

For simple graphs $X_i=(V_i,E_i)$, the graph $X_0\oplus X_1$
is just the disjoint union.
However, $X_0\text{ & }X_1$ is $(X_0^\perp\oplus X_1^\perp)^\perp$ which, if you think about it, is like $X_0\oplus X_1$ but now with edges connecting any vertex in $V_0$ to any vertex in $V_1$. This somehow represents the idea that whereas in $X_0\oplus X_1$ the two statements $X_0,X_1$ are contradictory (you either teach calculus or linear algebra; both options don’t exist!) in $X_0\text{ & }X_1$ you can still choose, so that the world as it is now doesn’t contradict either one (both options exist). In general, an edge between two vertices indicates a compatibility or coherence between the two corresponding statements.

Then $X_0\otimes X_1$ is simply the graph product and $X_0\text{ ⅋ }X_1$ represents “or” on the product vertex set $V_0\times V_1$.

A proposition is a closed subspace of a inner product space, $A\subseteq V$. (Assume $V=\mathbb R^3$.)
The negation is the orthogonal subspace $A^\perp\subseteq \mathbb R^3$.
The product $A_0\otimes A_1$ and the sum $A_0\oplus A_1$ of $A_i\subseteq V_i$ are then subspaces of $V_0\otimes V_1\cong \mathbb R^9$ (tensor product) and $V_0\oplus V_1\cong \mathbb R^6$ (direct sum a.k.a. direct product), respectively.

Then $A_0\text{ ⅋ } A_1$ is $(A_0^\perp \otimes A_1^\perp)^\perp$, another subspace of $V_0\otimes V_1$, and $A_0\text{ & }A_1$ is $(A_0^\perp \oplus A_1^\perp)^\perp$.

For example, let $A_0$ be the $xy$-plane and $A_1$ be the $z$-axis.
Then $A_0\otimes A_1$ has a basis $\mid e\rangle\mid e’\rangle$ where $\mid e\rangle$ is $(x,y,0)$ and $\mid e’\rangle$ is $(0,0,z)$.
Basically the basis vectors are
$$(1,0,0)(0,0,1); (0,1,0)(0,0,1)$$
So the dimension is $2\times 1=2$.

But $A_0\oplus A_1$ has basis vectors $e$ and $e’$ as above so the dimension is $2+1=3$. Basically the basis vectors are
$$(1,0,0,\, 0,0,0), (0,1,0,\, 0,0,0), (0,0,0,\, 0,0,1).$$

To figure out $A_0\text{ ⅋ } A_1$,
let us first observe that $A_0^\perp=A_1$ and $A_1^\perp=A_0$ in this example.
So $A_0\text{ ⅋ } A_1$ is the orthogonal complement of the subspace with basis
$$(0,0,1)(1,0,0); (0,0,1)(0,1,0)$$
hence it has dimension 7 and basis
$$(0,0,1)(0,0,1); (0,1,0)e; (1,0,0)e$$
where $e\in\{001,010,100\}$.

The only problem with this is that it seems like $A_0\text{ & }A_1$
is simply $A_0 \oplus A_1$. We can remedy that using pushouts.
Let
$$(A_0,V_0)\oplus (A_1,V_1) = (A_0\times \{0\}, V_0\times W) \times_W (A_1\times \{0\}, V_1\times W)$$
where $\times_W$ means amalgamation over $W$. Then
$$(A_0,V_0)\text{ & } (A_1,V_1) = (A_0\times W, V_0\times W) \times_W (A_1\times W, V_1\times W)$$

Some notes on Girard’s “Linear logic: its syntax and semantics”.

Let $M$ be the set of multisets of literals in the variables $p,q$, with the twist that $q$ is “reusable” so that
$(q,n)$ for any positive number $n$ is just $q$.

For example $\{(p,5),(\overline p,3),q\}\in M$.
Equip $M$ with a commutative monoid operation, namely “multiset sum” with the relation $q+q=q$. Thus $\emptyset$ is a neutral element, $s+\emptyset=s$, but the idempotents $s$ (satisfying $s+s=s$) include
$\emptyset$, $\{q\}$, $\{\overline q\}$, $\{q, \overline q\}$.

For example
$$\{(p,5),(\overline p,3),q\} + \{(p,1),q\} = \{(p,6),(\overline p,3),q\}$$

Let $\bot\subseteq M$ be the set of valid sequents, for example $\{(p,1),(\overline p,2),q\} \in \bot$ and $\{q,\overline q\}\in\bot$.

Let $X \multimap Y = \{ m \mid \forall n \in X, m + n \in Y\}$.
Let $X^\perp = X \multimap \bot$ which is therefore the set of all sequents $m$ such that for all sequents $n$ in $X$,
$m + n$ is valid. So for example $\{\overline p\} \in \{p\}^\perp$.

We further define:
$$X\otimes Y=\{m + n\mid m\in X, n\in Y\}$$

$$X\text{ ⅋ }Y = (X^\perp\otimes Y^\perp)^\perp$$

$$X\oplus Y = (X \cup Y)^{\perp\perp}$$

$$X \text{ & } Y = X \cap Y$$
(If $X=\{\{p\},\{q\}\}$ and $Y=\{\{q\},\{r\}\}$ then this is $\{\{q\}\}$, which means $X\text{ & }Y$ represents the ability to choose among $X$ or $Y$)

$0 = \emptyset^{\perp\perp}$. Note that $\emptyset^\perp=M$ and $M^\perp = \bot$ so $0 = \bot$, it seems.

$\top = M$

$1=\{\emptyset\}^{\perp\perp}$. Note that $\{\emptyset\}^\perp = (\{\emptyset\}\multimap \bot) = \bot$.
(The sequents such that for all sequents in $\{\emptyset\}$, the union is valid… are just the valid sequents.)
And then $1=\bot^\perp = (\bot\multimap\bot)$ consists of all sequents $m$ such that for all valid sequents $n$,
$m + n$ is valid… in other words, all sequents.

$I$ is the set of idempotents, i.e., multisets $s$ with $s + s = s$.

$$!X = (X\cap I)^{\perp\perp}$$

$$?X = (X^\perp\cap I)^\perp$$

For example, if $X=\{\{(p,3),q\}\}$ then $s\in X^\perp$ iff $s$ is a superset of one of the following: $\{\overline q\}$, $\{(\overline p,1)\}$.
And $X^\perp \cap I = \{\{\overline q\},\{\overline q, q\}\}$.
Finally, $?X$ is then anything that contains $\{(p,1),(\overline p,1)\}$ (“contains” in the sense of dominating the numbers occurring) or $\{q\}$.

On the other hand, if $X=\{\{(p,3)\},\{q\}\}$ then $s\in X^\perp$ iff
$s$ is a superset of *both* of $\{\overline q\}$, $\{(\overline p,1)\}$.

Throughout these considerations we kind of notice that for $X\subseteq M$, we may assume $X$ is closed upwards.

In a monoid we always have $X\subseteq X^{\perp\perp}$ but not necessarily conversely.
So this is a kind of algebraic closure with respect to a particular set $\bot$. For example, if $M=\mathbb Z$ and $\bot=\mathbb N$ then $\{-2,3\}^{\perp\perp}=[-2,\infty)$.

—

So we see that with a perhaps naïve interpretation of Girard’s writing, $\top = 1 = M$, $\bot = 0$, and so there is not complete generality.

—

A nontrivial example of a commutative monoid with some, but not all, nonzero elements being idempotent, is $\{0,1,2\}^2$ where $2=\infty$, under addition.
Thus $2+x=2$ for all $x$. We then take $\bot=\{(2,0),(2,1),(2,2),(0,2),(1,2)\}$. A 2 in the first coordinate corresponds to $p\vee\neg p$ and a 2 in the second coordinate to $q\vee \neg q$, as two different ways of reaching a tautology. There are four idempotents, $(0,0), (0,2), (2,0), (2,2)$. There are nine elements $(0,0),(0,1),\dots,(2,2)$ and $2^9=512$ possible sets $X$. Sets of the form $X^{\perp\perp}$ are upward closed and hence there are only $9+ 9 + 1$ of them. We can consider each of the connectives above for these 19 sets.
The total number of connectives possible is then $19^{19\times 19}$.

Theorem 2.28 (The Thue word is overlap-free) in my book published by de Gruyter is also Theorem 1.3.1 in Shallit’s new book “The logical approach to automatic sequences”. It is proved in Walnut as follows:

[Walnut]$ eval test "Ei,n (n >= 1) & Aj (j<=n) => T[i+j]=T[i+j+n]";
computed ~:1 states - 11ms
computed ~:2 states - 1ms
_____
FALSE

[Walnut]$ 

Theorem 2.36 (overlap-free words have an $A_N$-deficiency bound of 1) uses Theorem 2.25, one direction of which is that overlap-free words can only contain squares whose lengths are of the form $2^a$ or $3\cdot 2^a$, $a\ge 1$. If that is true then the Thue word better only have squares of such lengths. After running:

[Walnut]$ eval thuesquare "n >= 1 & Ei Aj (j T[i+j]=T[i+j+n]";

[Walnut]$

the file

thuesquare.gv

contains some code that we further process with

brew install graphviz

(which takes a long time, and produces many error messages, but not to worry) and then from the MacOS command line,

$ dot -Tpdf thuesquare.gv > thuesquare.pdf

The PDF looks like this: We can ignoring the arrow from state 0 to state 0 because it corresponds to initial zeros in the binary representation of the length $n$. Then we accept any word of the form $10^n$ or $110^n$ which is binary representation of $2^n$ and $3\cdot 2^n$, respectively. Phew! In Lemma 2.29 it is mentioned that the Thue-Morse sequence has no infinite arithmetic progressions. An infinite arithmetic progression would be characterized by $a$ and $b$ such that $T[a*k+b]=1$ for all sufficiently large $k$. Since multiplication is not included in the Walnut language, it is not clear that we can express this. But we can express $T[2*k+b]=1$:

eval test "Ei Aj (j>=i) => T[j+j+n]=T[j+j+2+n]"; 

Indeed, Walnut reports that this cannot happen, as follows: It is easier to do it like this:

[Walnut]$ eval test "En Ei Aj (j>=i) => T[j+j+n]=T[j+j+2+n]";   
_____
FALSE

[Walnut]$

If we try to multiply two variables we get the following trouble:

[Walnut]$ eval test "En Ei Aj (j>=i) => T[k*j+n]=T[k*(j+1)+n]";
java.lang.Exception: the operator * cannot be applied to two variables
	at Automata.NumberSystem.arithmetic(NumberSystem.java:791)
	at Token.ArithmeticOperator.act(ArithmeticOperator.java:188)
	at Main.Computer.compute(Computer.java:111)
	at Main.Computer.(Computer.java:49)
	at Main.Prover.eval_def_commands(Prover.java:466)
	at Main.Prover.dispatch(Prover.java:328)
	at Main.Prover.readBuffer(Prover.java:280)
	at Main.Prover.run(Prover.java:234)
	at Main.Prover.main(Prover.java:201)
the operator * cannot be applied to two variables
	: char at 22
	: eval test "En Ei Aj (j>=i) => T[k*j+n]=T[k*(j+1)+n]";

[Walnut]$ 

But we can check arithmetic sequences with longer and longer periods:

[Walnut]$ eval test "En Ei Aj (j>=i) => T[3*j+n]=T[3*(j+1)+n]";
_____
FALSE

[Walnut]$ eval test "En Ei Aj (j>=i) => T[4*j+n]=T[4*(j+1)+n]";
_____
FALSE

[Walnut]$ 

Let us now check if the infinite Fibonacci word is overlap-free.

[Walnut]$ eval test "Ei,n (n >= 1) & Aj (j<=n) => F[i+j]=F[i+j+n]";    
_____
FALSE

[Walnut]$ 

This seems to say there are no overlaps, which is false since the Fibonacci word starts: $0, 1, 0, 0, 1, 0, 1, 0$ which has overlapping occurrences of $010$. However, on page 136 it is suggested to add ?msd_fib so let us try that:

[Walnut]$ eval test "?msd_fib Ei,n (n >= 1) & Aj (j<=n) => F[i+j]=F[i+j+n]";
____
TRUE

[Walnut]$

Indeed, it is explained on page 108 that “you may need to add a ?msd specification if your sequence is automatic for other than base 2″. Now we can check whether the infinite Tribonacci word contains any overlaps: This takes a while and surprisingly gives an error. However, making a simple change in the formula, as explained in the book, fixes the problem:

[Walnut]$ eval test "?msd_trib Ei,n (n >= 1) & Aj (j<=n) => TR[i+j]=TR[i+j+n]";
computed ~:1 states - 2ms
computed ~:2 states - 1ms
Exception in thread "main" java.lang.OutOfMemoryError: Java heap space
	at java.base/java.util.ArrayList.grow(ArrayList.java:239)
	at java.base/java.util.ArrayList.grow(ArrayList.java:244)
	at java.base/java.util.ArrayList.add(ArrayList.java:454)
	at java.base/java.util.ArrayList.add(ArrayList.java:467)
	at Automata.Automaton.subsetConstruction(Automaton.java:3477)
	at Automata.Automaton.minimize_valmari(Automaton.java:281)
	at Automata.Automaton.minimize(Automaton.java:3022)
	at Automata.Automaton.quantifyHelper(Automaton.java:845)
	at Automata.Automaton.quantify(Automaton.java:743)
	at Token.LogicalOperator.actQuantifier(LogicalOperator.java:144)
	at Token.LogicalOperator.act(LogicalOperator.java:59)
	at Main.Computer.compute(Computer.java:111)
	at Main.Computer.(Computer.java:49)
	at Main.Prover.eval_def_commands(Prover.java:466)
	at Main.Prover.dispatch(Prover.java:328)
	at Main.Prover.readBuffer(Prover.java:280)
	at Main.Prover.run(Prover.java:234)
	at Main.Prover.main(Prover.java:201)
(base) Bjrns-MacBook-Pro:bin bjoernkjos-hanssen$ java Main/Prover

[Walnut]$ eval test "?msd_trib Ei,n (n >= 1) & Aj (i <= j & j <= i+n) => TR[j]=TR[j+n]";
computed ~:1 states - 9ms
computed ~:2 states - 1ms
____
TRUE

[Walnut]$

Actually, the Tribonacci word is $0, 1, 0, 2, 0, 1, 0, 0, 1, 0, 2, 0, 1, 0, 1, 0\dots$ so finding an overlap should be trivial. The situation is explained on page 111. When we consider TR[i+j+n] the extra variable compared to TR[j+n] leads to an exponentially larger automaton being generated. Thus, this is not really the implementation of Walnut’s fault but a feature of the underlying algorithm. We can ponder which prefixes of the infinite Fibonacci word are of the form $xyxyx z uvuvu$. Arithmetically this says that we have a number $n$ (the length) and numbers $l_x, l_y>0, l_z>0, l_u, l_v>0$ such that they add up to $n$ in the right way, and all the appropriate agreements occur. This is related to automatic complexity of Fibonacci words. A simpler question is which prefixes are squares.

[Walnut]$ eval test "?msd_fib Elx (lx+lx=n & At (t F[t]=F[t+lx])";

[Walnut]$ 

This produces the following automaton which in Fibonacci representation gives the lengths of the prefixes of the infinite Fibonacci word that are squares. They are 6, 10, and in general any number of the form $F_{k+3}+F_k)$. We see here the usefulness of the Fibonacci representation, since the word is not 2-automatic. If we run the same command without ?msd_fib the result is a 1-state automaton with a self-loop labeled 0. test A VS Code extension for Walnut would be great, as editing formulas is cumbersome.

In the Thue sequence $t_0t_1t_2\dots=011010011001…$, each $t_n$ is the parity of the number of 1s in the binary representation $(n)_2$ of $n$. This leads to a 2-state DFAO (deterministic finite automaton with output) that reads $(n)_2$ and keeps track of the parity so far. This is an prototypical example of an automatic sequence. The Fibonacci word $f_0f_1f_2\dots = 01001010$ where $f_n=f_{n-1}f_{n-2}$ can be handled similarly using the Fibonacci representation of numbers. In it, we write $n$ as $a_1\cdot 1 + a_2\cdot 2 + a_3\cdot 3+a_4\cdot 5+a_5\cdot 8+\dots$ where $1,2,3,5,8,\dots$ are Fibonacci numbers and each $a_i\in\{0,1\}$. It is unique provided that no two consecutive 1s in the representation are allowed. These two examples already hint at a rich theory of automatic sequences with respect to various representation systems. Such a theory has been established in the old-fashioned manner of mathematicians over the years. Now, due to the decidability of Presburger arithmetic and some of its extensions, and a computer implementation thereof called Walnut and due to Hamoon Mousavi, researchers in the area are able to programmatically answer many research questions and verify or correct results from the literature. As a theoretical backbone for the approach, it is shown that a sequence is $k$-automatic if and only if it is first order definable in the structure $(\mathbb N, +, V_k)$, where $V_k(n)$ is the greatest power of $k$ that divides $n$. The author emphasizes that Walnut computations are not formally guaranteed to be correct; however, experience has lead to large and growing confidence in its results. As a piece of software Walnut is fairly easy to use and install. The underlying algorithm has bad worst-case complexity and this affects the use of Walnut in interesting ways. When we consider the Tribonacci word in position $i+j+n$, \texttt{TR[i+j+n]}, the three variables lead to an exponentially larger automaton being generated than if we had stuck with two, and the program crashing. Rewriting the query to use \texttt{TR[j+n]} fixes the problem, as explained in the book. Thus, this program crash is not really the implementation of Walnut’s fault but an aspect of the underlying algorithm. The topics covered include squares, palindromes, and a wide variety of notions from combinatorics on words. The book is very well-written with few errors, and many easily stated open problems. The many entertaining examples of English words exemplifying the concepts introduced can even be appreciated by non-mathematicians: for example, the word “distinguishing” is a concatenation of two equal-length words differ in only two positions.