User:Physis/Language base

Although we ofter refer to the “text” of object language as “finite sequences” over a set of “letters”, but sometimes we axiomatize this explicitly. A language base declares the set of “letters” axiomatizes sequencing operations. This mini-theory formalizes what we think of informally as as “finite sequences”. Language base talks almost nothing of the syntax of the object languege (althoght the letters may coincide with those of the object languge, but also this is not necessary): treatment of syntax must be built upon it. See the notion in ^[1], but also — with somewhat different terminology — at Tarski).

\llcorner \land \lrcorner ,\;\llcorner \lor \lrcorner ,\;\llcorner \lnot \lrcorner ,\;\llcorner \to \lrcorner ,\;\llcorner \leftrightarrow \lrcorner \in \mathbf {LogicalSymbol} _{\mathrm {namefunctor} }

For better readability, let us denote the respective singleton sequences with underlining:

\llcorner 0\lrcorner ,\;\llcorner s\lrcorner ,\;\llcorner +\lrcorner ,\;\llcorner \cdot \lrcorner \in \mathbf {NonLogicalSymbol} _{\mathrm {namefunctor} }

For better readability, let us denote the respective singleton sequences with underlining:

{\underline {\land }}\equiv \langle \llcorner \land \lrcorner \rangle ,\;{\underline {\lor }}\equiv \langle \llcorner \lor \lrcorner \rangle ,\;{\underline {\lnot }}\equiv \langle \llcorner \lnot \lrcorner \rangle ,\;{\underline {\to }}\equiv \langle \llcorner \to \lrcorner \rangle ,\;{\underline {\leftrightarrow }}\equiv \langle \llcorner \leftrightarrow \lrcorner \rangle

{\underline {0}}\equiv \langle \llcorner 0\lrcorner \rangle ,\;{\underline {s}}\equiv \langle \llcorner s\lrcorner \rangle ,\;{\underline {+}}\equiv \langle \llcorner +\lrcorner \rangle ,\;{\underline {\cdot }}\equiv \langle \llcorner \cdot \lrcorner \rangle

Axiomatizations

Now we axiomatize the notion of sequence. Well-chosen axioms provide appropriate distinctions and indentifications, unambiguity, and exclude alien objects.

Let us use $\epsilon$ to denote empty sequence. Now we have more ways to step further.

List-like

One approach uses a similar terminology as the concept of list in functional programming: we can use a : operation, making form a letter and an (already made) sequence (possibly also the empty one) a new sequence. We can begin the axiomatization like this:

\forall x^{\mathbf {Letter} }\;\forall s^{\mathbf {Letter} ^{*}}\;\;x:s\neq \epsilon

\forall x^{\mathbf {Letter} }\;\forall y^{\mathbf {Letter} }\;\forall s^{\mathbf {Letter} ^{*}}\;\forall t^{\mathbf {Letter} ^{*}}\;\;x:s=y:t\rightarrow x=y\land s=t

we can define concatenation by recursion.

Concatenation and singletons

In another approach concatenation is a primitive (mainly denoted by $\frown$ ). Also a new operaration may be introduced: singleton sequece building, let us denote it here e.g. by $\langle \dots \rangle$ . Axiomatization would begin than like this:

\forall x^{\mathbf {Letter} }\;\;\langle x\rangle \neq \epsilon

\forall x^{\mathbf {Letter} }\;\forall y\;\;\langle x\rangle =\langle y\rangle \rightarrow x=y

A specific care must be taken of concatenation:

associativity
unambiguity

must be declared by appropriate axioms.

Variants

We resorted many-sorted logic in the above things. Mybe this can be avoided. But then, each letter must be regarded as a standlone case at the axioms discussing distinctions:

{\underline {\forall }}\neq {\underline {\to }}

\vdots

Failed to parse (syntax error): {\displaystyle \0 \neq \underline s}

Alternatives

Modelling sequences

We can skip this level: we can choose a more denotational approach, and refer to sequences as directly building their set-theoretic models. E.g. somethng like where