Spread (intuitionism)

Definitions

Overview

In modern terminology, a spread is an inhabited closed set of sequences. Spreads are defined via a spread function, which performs a (decidable) "check" on finite sequences. If all the finite initial parts of an infinite sequence satisfy a spread function's "check", then we say that the infinite sequence is admissible to the spread. The notion of a spread and its spread function are interchangeable in the literature. Graph theoretically, one may think of a spread in terms of a rooted, directed tree with numerical vertex labels. A fan, also known as finitary spread, is a special type of spread. In graph terms, it is finitely branching. Finally, a dressed spread is a spread together some function acting on finite sequences.

Preliminary notation and terminology

This article uses "${\displaystyle ⟨}$" and "${\displaystyle ⟩}$" to denote the beginning resp. the end of a sequence. The sequence with no elements, the so called empty sequence, is denoted by ${\displaystyle ⟨⟩}$.

Given an infinite sequence ${\displaystyle ⟨x_1,x_2,\dots ⟩}$, we say that the finite sequence ${\displaystyle ⟨y_1,y_2,\dots ,y_i⟩}$ is an initial segment of ${\displaystyle ⟨x_1,x_2,\dots ⟩}$ if and only if ${\displaystyle x_1=y_1}$ and ${\displaystyle x_2=y_2}$ and ... and ${\displaystyle x_i=y_i}$.

Spread function

A spread function ${\displaystyle s}$ is a function on finite sequences that satisfies the following properties:

• Given any finite sequence ${\displaystyle ⟨x_1,x_2,\dots ,x_i⟩}$ either ${\displaystyle s(⟨x_1,x_2,\dots ,x_i⟩)=0}$ or ${\displaystyle s(⟨x_1,x_2,\dots ,x_i⟩)=1}$. In other words, the property being tested must be decidable via ${\displaystyle s}$.
• ${\displaystyle s(⟨⟩)=0}$.
• Given any finite sequence ${\displaystyle ⟨x_1,x_2,\dots ,x_i⟩}$ such that ${\displaystyle s(⟨x_1,x_2,\dots ,x_i⟩)=0}$, there exist some ${\displaystyle k}$ such that ${\displaystyle s(⟨x_1,x_2,\dots ,x_i,k⟩)=0}$.

Given a finite sequence, if ${\displaystyle s}$ returns 0, the sequence is admissible to the spread given through ${\displaystyle s}$, and otherwise it is inadmissible. The empty sequence is admissible and so part of every spread. Every finite sequence in the spread can be extended to another finite sequence in the spread by adding an extra element to the end of the sequence. In that way, the spread function acts as a characteristic function accepting many long finite sequences.

We also say that an infinite sequence ${\displaystyle ⟨x_1,x_2,\dots ⟩}$ is admissible to a spread defined by spread function ${\displaystyle s}$ if and only if every initial segment of ${\displaystyle ⟨x_1,x_2,\dots ⟩}$ is admissible to ${\displaystyle s}$. For example, for a predicate characterizing a law-like, unending sequence of numbers, one may validate that it is admissible with respect to some spread function.

Fan

Informally, a spread function ${\displaystyle s}$ defines a fan if, given a finite sequence admissible to the spread, there are only finitely many possible values that we can add to the end of this sequence such that our new extended finite sequence is admissible to the spread. Alternatively, we can say that there is an upper bound on the value for each element of any sequence admissible to the spread. Formally:

• A spread function ${\displaystyle s}$ defines a fan if and only if given any sequence admissible to the spread ${\displaystyle ⟨x_1,x_2,\dots ,x_i⟩}$, then there exists some ${\displaystyle k}$ such that, given any ${\displaystyle j>k}$ then ${\displaystyle s(⟨x_1,x_2,\dots ,x_i,j⟩)=1}$

So given a sequence admissible to the fan, we have only finitely many possible extensions that are also admissible to the fan, and we know the maximal element we may append to our admissible sequence such that the extension remains admissible.

Examples

Spreads

Simple examples of spreads include

• The set of sequences of even numbers
• The set of sequences of the integers 1–6
• The set of sequences of valid terminal commands.

Fans

• The set of sequences of legal chess moves
• The set of infinite binary sequences
• The set of sequences of letters

What follows are two spreads commonly used in the literature.

The universal spread (the continuum)

Given any finite sequence ${\displaystyle ⟨x_1,x_2,\dots ,x_i⟩}$, we have ${\displaystyle s(⟨x_1,x_2,\dots ,x_i⟩)=0}$. In other words, this is the spread containing all possible sequences. This spread is often used to represent the collection of all choice sequences.

The binary spread

Given any finite sequence ${\displaystyle ⟨x_1,x_2,\dots ,x_i⟩}$, if all of our elements (${\displaystyle x_1,x_2,\dots ,x_i}$) are 0 or 1 then ${\displaystyle s(⟨x_1,x_2,\dots ,x_i⟩)=0}$, otherwise ${\displaystyle s(⟨x_1,x_2,\dots ,x_i⟩)=1}$. In other words, this is the spread containing all binary sequences.

Dressed spreads

An example of a dressed spread is the spread of integers such that ${\displaystyle s(⟨x_1,x_2,\dots ,x_i⟩)=0}$ if and only if

${\displaystyle \mathrm{\forall }y.(0<y\le i)\to ((x_i=0)\vee (x_i=2\cdot x_{y-1}\pm 1))}$,

together with the function ${\displaystyle f(⟨x_1,x_2,\dots ,x_i⟩)=x_i\cdot 2^{2-i}}$. This represents the real numbers.