#LyX 2.3 created this file. For more info see http://www.lyx.org/
\lyxformat 544
\begin_document
\begin_header
\save_transient_properties true
\origin unavailable
\textclass article
\use_default_options true
\maintain_unincluded_children false
\language english
\language_package default
\inputencoding auto
\fontencoding global
\font_roman "default" "default"
\font_sans "default" "default"
\font_typewriter "default" "default"
\font_math "auto" "auto"
\font_default_family default
\use_non_tex_fonts false
\font_sc false
\font_osf false
\font_sf_scale 100 100
\font_tt_scale 100 100
\use_microtype false
\use_dash_ligatures true
\graphics default
\default_output_format default
\output_sync 0
\bibtex_command default
\index_command default
\paperfontsize default
\use_hyperref false
\papersize default
\use_geometry false
\use_package amsmath 1
\use_package amssymb 1
\use_package cancel 1
\use_package esint 1
\use_package mathdots 1
\use_package mathtools 1
\use_package mhchem 1
\use_package stackrel 1
\use_package stmaryrd 1
\use_package undertilde 1
\cite_engine basic
\cite_engine_type default
\use_bibtopic false
\use_indices false
\paperorientation portrait
\suppress_date false
\justification true
\use_refstyle 1
\use_minted 0
\index Index
\shortcut idx
\color #008000
\end_index
\secnumdepth 3
\tocdepth 3
\paragraph_separation indent
\paragraph_indentation default
\is_math_indent 0
\math_numbering_side default
\quotes_style english
\dynamic_quotes 0
\papercolumns 1
\papersides 1
\paperpagestyle default
\tracking_changes false
\output_changes false
\html_math_output 0
\html_css_as_file 0
\html_be_strict false
\end_header
\begin_body
\begin_layout Title
The Syntax of Axioms
\end_layout
\begin_layout Author
Linas Vepštas
\end_layout
\begin_layout Date
4 July 2025
\end_layout
\begin_layout Abstract
This text examines some practical notational and representational issues
that arise when one attempts to represent common mathematical axioms as
if they were the definition of a syntax, from which one might try to generate
a language of all syntactically valid sentences.
There are no particular problems if one sets pen to paper; the issues arise
when trying to develop software.
The representational framework explored here is that of jigsaws, as that
seems to be the most generic representation for mathematical structures,
and has a particularly appealing form for the generation and parsing of
languages.
\end_layout
\begin_layout Section
Introduction
\end_layout
\begin_layout Standard
The correspondence between syntax and language is widely understood in many
different branches of mathematics.
It is often fairly self–evident, and there are a number of different formalisms
that attempt to provide a generic description.
\end_layout
\begin_layout Standard
For example, groups are generated from their collection of generators: the
group itself is the
\begin_inset Quotes eld
\end_inset
language
\begin_inset Quotes erd
\end_inset
that is generated.
The generation itself is subject to the axioms defining a group, plus the
group presentation.
If there is no presentation, the free group is generated.
One can also think of a group as being the free group modulo it's presentation.
\end_layout
\begin_layout Standard
A more general conception of this sort arises in term algebras.
There, one has a collection of terms, say
\begin_inset Formula $\left\{ f\left(x,y,z\right),g\left(x,y\right),\cdots,h\left(x,y,z,w\right)\right\} $
\end_inset
and a collection of constants
\begin_inset Formula $\left\{ c_{1},c_{2},\cdots,c_{n}\right\} $
\end_inset
and one freely composes these to form all finite trees: this is the language
generated by the term algebra.
In model theory, one has the same idea, but also adds relations: these
are predicates
\begin_inset Formula $\left\{ r_{1}\left(x,y\right),r_{2}\left(w,x,z\right),\cdots\right\} $
\end_inset
that evaluate to crisp true–false values, and thus can be freely combined
with the conventional logical operators
\begin_inset Formula $\lnot,\wedge,\vee$
\end_inset
to form logical sentences.
The result of composing terms with predicates, and then combining these
with logical operators gives the freely generated language.
Squinting a bit, it is not hard to see that the generated objects are trees.
\end_layout
\begin_layout Standard
A related notion arises in proof theory, where one has a collection of axioms,
which are then combined with inference rules.
Combining these freely usually results in fragments of proofs; one has
a complete and valid proof if the generation terminates and results in
a single value
\begin_inset Quotes eld
\end_inset
true
\begin_inset Quotes erd
\end_inset
.
\end_layout
\begin_layout Standard
Of course, one definition of generic syntax and generic language if provided
by Chomsky, who shows how to define a collection of production rules, that,
when iterated on and freely combined, generates a language.
\end_layout
\begin_layout Standard
The above gives five distinct examples of where some collection of rules
or terms or symbols can be iterated on, multiplied, combined or composed,
with varying degrees of freedom, to generate a language.
In each specific domain, there are no particular difficulties in doing
so.
The core reason for the absence of difficulties is because humans, the
mathematicians, invent a collection of symbols that can be written on pieces
of paper, and the meaning of each symbol, and the method of combining it
with others, can be explained with words that are meaningful to the reader.
\end_layout
\begin_layout Standard
The exploration performed in this text is the construction of a generic
system for representing all these different systems in such a way that
the generation can proceed algorithmically.
This presupposes that there is some simple way of encoding these systems
in some computer–friendly, algorithm–friendly form.
There is a relatively well–known way of doing this, and it will be reviewed
next.
The bulk of this text will consist of exploring a large collection of axioms
taken from different branches of mathematics, and examining how they get
encoded.
The hope is that a programming reference can arise from this work.
\end_layout
\begin_layout Standard
The next section introduces the concept of a jigsaw, and explores how it
can be represented in a convenient computational fashion.
It is introductory in nature, providing a review.
After this follows actual examples of the representation of axioms, terms,
logical connectives, and so on, from various domains of mathematics.
\end_layout
\begin_layout Standard
This text tries to strike a balance between
\begin_inset Quotes eld
\end_inset
hurry up and go
\begin_inset Quotes erd
\end_inset
and
\begin_inset Quotes eld
\end_inset
annoying precision
\begin_inset Quotes erd
\end_inset
.
Conceptually, the
\begin_inset Quotes eld
\end_inset
big picture
\begin_inset Quotes erd
\end_inset
here is not that complicated, and can be understood at a glance.
See, for example, references x,y,z.
But, as always, the devil is in the details, and the details can be frustrating
, annoying and uncooperative.
Thus, much of this text is mired in pedantic, trivial, verbose, soporific
explanations.
Sorry about that.
I dislike writing it as much as you dislike reading it, but there seems
to be no other way.
\end_layout
\begin_layout Section
Jigsaws
\end_layout
\begin_layout Standard
The jigsaw paradigm for representing structure is relatively well–known
and wide–spread through multiple branches of mathematics, but is not so
famous as to evade a short introduction.
\end_layout
\begin_layout Standard
A reasonable starting point is the concept of a jigsaw in Link Grammar (LG).
This is a theory of natural language, and, as such, works quite well; full–feat
ured lexicons have been created for English, Russian and Thai, with smaller
dictionaries for a dozen other languages.
The lexical entries in LG are jigsaws, and parsing proceeds by selecting
jigsaws, attaching them in a valid, until all words in a sentence have
been joined, and there are no unconnected connectors remaining.
The word
\begin_inset Quotes eld
\end_inset
jigsaw
\begin_inset Quotes erd
\end_inset
is meant to be understood in a literal sense.
The figure below is from the original 1991 LG paper.
Hopefully, this diagram makes clear the intended process of parsing: one
works to connect up all the connectors.
\end_layout
\begin_layout Standard
\align center
\begin_inset Graphics
filename graphics/link-grammar.png
lyxscale 50
width 100col%
\end_inset
\end_layout
\begin_layout Standard
The goal of the following paragraphs is not so much to explain how LG works,
or even why it works, but to review how the concept of jigsaws can be represent
ed in a generic computational fashion.
This is important because this paper makes the fundamental claim that
\emph on
all of mathematics
\emph default
can be represented with jigsaws, and more: all of physical nature can be
likewise.
The main body of this text will provide many examples showing how this
can be done.
\end_layout
\begin_layout Standard
Consider the sentence
\begin_inset Quotes eld
\end_inset
He sang a song to her.
\begin_inset Quotes erd
\end_inset
The lexis will contain a jigsaw for the verb
\begin_inset Quotes eld
\end_inset
sang
\begin_inset Quotes erd
\end_inset
, and it will have connectors to the subject
\begin_inset Quotes eld
\end_inset
he
\begin_inset Quotes erd
\end_inset
, the object
\begin_inset Quotes eld
\end_inset
song
\begin_inset Quotes erd
\end_inset
and the indirect object
\begin_inset Quotes eld
\end_inset
her
\begin_inset Quotes erd
\end_inset
.
This is a transitive verb with indirect object, and is represented in the
lexis as
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
\begin_inset Box Frameless
position "t"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "100col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open
\begin_layout Plain Layout
\family sans
sang: S– & O+ & I+;
\end_layout
\end_inset
\end_layout
\begin_layout Standard
\begin_inset VSpace defskip
\end_inset
The capital letters are the connector type; the plus and minus signs are
directional indicators, indicating to the left, or to the right.
Thus, the lexical entry for
\begin_inset Quotes eld
\end_inset
he
\begin_inset Quotes erd
\end_inset
will contain a connector
\family sans
S+
\family default
, indicating that it connects to the right.
During parsing, the
\family sans
S+
\family default
and
\family sans
S
\family default
– will be joined up to form an
\family sans
S
\family default
link between the subject and the verb, completing the parse for these two
connectors.
\end_layout
\begin_layout Standard
Note that a partially–completed parse still has the form of a jigsaw, that
is, of having some shape, and having some unconnected connectors.
This compositionality means that the jigsaw pieces obey the sheaf axioms.
Sheaves are already a widely used concept in mathematics, but the relation
to jigsaws remains opaque.
\end_layout
\begin_layout Standard
The string representation `
\family sans
sang: S– & O+ & I+;
\family default
` is fine, if one's goal is to store the LG lexis in a flat file.
Using it in computer code requires creating a parser that is capable of
reading this file format, and then converting it into some other format,
for example, some layout of C or C++ or Java structures, existing in RAM,
where binary executables composed of machine code can act on these RAM
structures.
This is a tangible example of the conversion of structural representations
from one form to another: from what is held in a text file, to what is
in RAM.
The conversion of structure is meant to be homomorphic, in some sense,
and injective: the in–RAM representation is supposed to be faithful to
the file representation.
\end_layout
\begin_layout Standard
The string representation `
\family sans
sang: S– & O+ & I+;
\family default
` is fine, if one's goal is to limit oneself to working only with LG.
It is inadequate for representing typed connections in general.
Consider, for example, the C/C++ subroutine declaration `
\family sans
int func(float x);
\family default
`.
This is a forward declaration of an interface, an API, that takes a floating
point number as input, and returns an int.
This can be abstract represented as a jigsaw, having input and output connector
s, those connectors having the types `
\family sans
int
\family default
` and `
\family sans
float
\family default
`.
With some belabored effort, the prototype can be represented in LG form
as `
\family sans
func: INT– & FLT+;
\family default
` indicated the two typed but unconnected connectors, and the lexical name
`
\family sans
func
\family default
`.
Compositionality requires that the lexis also include entries such as `
\family sans
3.14159: FLT–;
\family default
` thus allowing it to be composed with the function to give `
\family sans
func(3.14159);
\family default
` or, as a partially assembled jigsaw, `
\family sans
func(3.14159): INT–;
\family default
` indicating that there is still one unconnected connector: the integer
output, meant to be connected to something: say, to `
\family sans
printf
\family default
`, for example.
\end_layout
\begin_layout Standard
This last example hopefully incites the idea that jigsaws might be widely
applicable across a broad domain of structural representation.
The specific LG lexical representation is problematic, though, so let us
look at it more carefully, to see what it really says.
\end_layout
\begin_layout Standard
The connector `
\family sans
S–
\family default
` is actually a pair: the type `
\family sans
S
\family default
`, and the directional indicator `
\family sans
–
\family default
`.
Thus, a variety of different notations suggest themselves:
\begin_inset Formula
\[
\left(S,-\right)\qquad S\times-\qquad S\otimes-\qquad\left|S\right\rangle \otimes\left|-\right\rangle
\]
\end_inset
all of which are meant to indicate an ordered pair, and the last two notations
suggesting that there is something
\begin_inset Quotes eld
\end_inset
tensorial
\begin_inset Quotes erd
\end_inset
about it.
For the present, the Cartesian product suffices.
\end_layout
\begin_layout Standard
The ampersand operator was meant to indicate that all of the connectors
are active, and must eventually be connected.
It is a list of connectors.
It is written in infix form, but a prefix form is preferable; this allows
a list to be specified.
Different programming languages specify lists in a variety of different
notations; for the present, s–expressions will be used.
S–expressions are foundational for lisp and scheme, and are readily convertible
to other syntactic forms, e.g.
python.
S–expressions also have the useful nature of being interpreted directly
as trees, and thus fit naturally with ideas of recursive computation.
Thus armed, the s–expression for `
\family sans
S– & O+ & I+
\family default
` is `
\family sans
(& (S –) (O +) (I +
\family default
))` where the leading ampersand is a type indicator: the list that follows
is of the type of being a connector list.
The full lexical entry `
\family sans
sang: S– & O+ & I+;
\family default
` becomes `
\family sans
(: sang (& (S –) (O +) (I +
\family default
)))` where the colon is again a type indicator: what follows the colon is
an lexical item, followed by a connector list.
\end_layout
\begin_layout Standard
Using colons and ampersands as type indicators is somewhat awkward, and
a slightly more verbose representation is clearer: `
\family sans
(LexicalEntryType
\begin_inset Quotes eld
\end_inset
sang
\begin_inset Quotes erd
\end_inset
(ConnectorListType (S –) (O +) (I +
\family default
)))`.
Note that this s–expression always has a type name as the first element
of the list.
This is fine, because the connector types `
\family sans
S, O, I
\family default
` are to be understood as true type–theoretical types.
The connection rules state that the `
\family sans
S
\family default
` connector can mate only with another `
\family sans
S
\family default
` connector, and no other type.
The only awkwardness here is that the list of connector types is potentially
unbounded.
A different issue is that `+` and `–` are also types, except now the connection
rules are heterosexual: `+` can only mate to `–`, and homosexual connections
are not allowed.
Using such politically florid terms reminds us that other possibilities
may be desirable.
The construction of undirected graphs asks for a mono–sexual connector,
because the edges of an undirected graph are have no orientation.
The construction of parse graphs for natural languages such as Finnish,
Turkish and Lithuanian require not one but two directional indicators:
(head,dependent) and (left,right) This is because these languages are mostly
word–order independent, and allow almost arbitrary reorderings of words
in a sentence.
Meaning is derived from the structure of the suffixes, indicating possessive,
accusative, etc.
relationships.
At any rate, the point being made here is that `+` and `–` are also types,
and one might want to entertain an expanded universe of the kinds of types
that can be used to indicate mating, and one might want to have mating
rules more complex than heterosexuality.
It is not out of place to remark that, in nature, there are fungii with
far more than two sexes, and complex mating rules for which combinations
produce viable offspring.
The genomic, transcriptomic processes for mating need only produce working
individuals; there is no law of nature demanding heterosexuality.
\end_layout
\begin_layout Standard
Armed with this understanding, the suggested s–expression encoding is then
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
\begin_inset Box Frameless
position "t"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "100col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open
\begin_layout Plain Layout
\family sans
(LexicalEntryType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ItemType
\begin_inset Quotes eld
\end_inset
sang
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ConnectorListType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
S
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
–
\begin_inset Quotes erd
\end_inset
))
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
O
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
+
\begin_inset Quotes erd
\end_inset
))
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
I
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
+
\begin_inset Quotes erd
\end_inset
))))
\end_layout
\end_inset
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
This has the property that the very first token after the open paren is
a type name.
The indentation is for convenience and readability, as s–expressions are
notoriously painful to read.
It is for this reason that python uses significant whitespace: it is to
force the programmer to indent properly, to work with the human visual
system to understand the tree structure.
The above can be trivially converted to python, merely by rearranging parenthes
is, and inserting some strategic commas.
The indentation also indicates the tree form: the more the indentation,
the further down the abstract syntax tree (AST).
\end_layout
\begin_layout Standard
The C/C++ example API declaration `
\family sans
int func(float x);
\family default
` becomes
\end_layout
\begin_layout Standard
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
\begin_inset Box Frameless
position "t"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "100col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open
\begin_layout Plain Layout
\family sans
(LexicalEntryType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ItemType
\begin_inset Quotes eld
\end_inset
func
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ConnectorListType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
int
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
output
\begin_inset Quotes erd
\end_inset
))
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
float
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
input
\begin_inset Quotes erd
\end_inset
))))
\end_layout
\end_inset
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
This is sadly quite verbose, but has several very desirable properties:
it encodes the structure of the API declaration in exactly the same form,
a jigsaw, as an LG entry for natural language, also a jigsaw.
It encodes as a typed tree, where the type of every vertex of the tree
is cleanly specified, leaving no ambiguity, and nothing implicit.
It is a string encoding; abstractly, it is a tree, but computationally,
it is a string of UTF-8 characters, readily stored in a file, or communicated
over a network socket.
As a tree, it is readily converted to structures made out of pointers;
each level in the tree is a list, and all programming languages have highly
optimized list representations.
Computationally, this seems to be an optimal structure.
It is not clear what might actually be better, at least to the author of
this text.
If you, the reader, have a better idea, please let me know.
This question has been a nagging one for quite a while, and it would be
nice to make forward progress on it.
\end_layout
\begin_layout Standard
These typed s–expressions will be called
\begin_inset Quotes eld
\end_inset
Atomese
\begin_inset Quotes erd
\end_inset
.
A software realization of Atomese is provided by the AtomSpace.
That software realization is much older than the topics discussed in this
text, and was developed, designed and informed from other principles.
And yet, it converged onto the present topic.
Again, if there is a better way, it is not yet clear what that might be.
\end_layout
\begin_layout Section
Examples
\end_layout
\begin_layout Standard
Armed with the conception that
\begin_inset Quotes eld
\end_inset
everything in mathematics can be described in terms of jigsaws
\begin_inset Quotes erd
\end_inset
, and even that
\begin_inset Quotes eld
\end_inset
everything in physical nature can be described as jigsaws
\begin_inset Quotes erd
\end_inset
, it is appropriate to work through some examples.
The claim that
\begin_inset Quotes eld
\end_inset
all structure is representable with jigsaws
\begin_inset Quotes erd
\end_inset
is meant to be self–evident.
It is not meant to be intellectually deep; rather, it is closer to statements
such as
\begin_inset Quotes eld
\end_inset
all computable functions can be computed with a Turing machine
\begin_inset Quotes erd
\end_inset
, or, invoking the Church–Turing thesis,
\begin_inset Quotes eld
\end_inset
all sayable expressions can be written with Lambda Calculus
\begin_inset Quotes erd
\end_inset
.
This has many forms: Lambda Calculus is isomorphic to combinators, and
so
\begin_inset Quotes eld
\end_inset
all sayable sentences can be written with combinators
\begin_inset Quotes erd
\end_inset
.
Turing machines also have many equivalent forms, for example, the register
machines, and so
\begin_inset Quotes eld
\end_inset
all computable functions are computable with register machines
\begin_inset Quotes erd
\end_inset
.
There are similar claims in mathematics:
\begin_inset Quotes eld
\end_inset
set theory can provide a foundation for all of mathematics
\begin_inset Quotes erd
\end_inset
, or, more recently, that
\begin_inset Quotes eld
\end_inset
topoi can provide a foundation for all of mathematics
\begin_inset Quotes erd
\end_inset
, with topoi being (roughly) a point–free (
\begin_inset Quotes eld
\end_inset
pointless
\begin_inset Quotes erd
\end_inset
) description of topology in terms of frames and locales, together with
the Boolean algebra required to express logic.
The claim that
\begin_inset Quotes eld
\end_inset
everything is a jigsaw
\begin_inset Quotes erd
\end_inset
is no deeper or stronger than this.
Worse, it is infinitely more naive; the theory of topoi, and the category
theory from which it is built, has been elucidated, developed, articulated
by hundreds of authors writing thousands of articles and books totaling
hundreds of thousands of pages.
The idea that
\begin_inset Quotes eld
\end_inset
everything is a jigsaw
\begin_inset Quotes erd
\end_inset
has attracted no such attention, and does not yet have deep, sophisticated,
arcane explorations.
\end_layout
\begin_layout Standard
It does, however, touch fairly closely upon all these other representational
systems.
Much of what jigsaws do is reminiscent of category theory.
The fact that they obey the sheaf axioms touches with topoi, as topoi are,
roughly, founded on sheaf theory.
The fact that jigsaws have typed connectors touches on type theory, and
modern type theory is now generally understood, via Univalent Foundations,
to be intertwined with the
\begin_inset Quotes eld
\end_inset
internal languages
\begin_inset Quotes erd
\end_inset
of categories: The (syntax of the) internal language describes with can
be said in those categories.
The simplest example is that of Cartesian Closed Categories: the internal
language is precisely that of Lambda Calculus, effectively because currying
is a product–hom adjunction.
That is,
\begin_inset Formula $\left(A\times B\right)\to C=A\to\left(B\to C\right)$
\end_inset
; the Wikipedia article on currying gives a large number of examples of
currying as it appears in different fields of mathematics.
\begin_inset Foot
status collapsed
\begin_layout Plain Layout
Disclosure of conflicts: I wrote almost all of the Wikipedia article on
currying.
It is one of my favorites.
\end_layout
\end_inset
The underlying structure is that of tensor–hom adjunction, which has many
fascinating applications.
\end_layout
\begin_layout Standard
That is, jigsaws are not very far away from a broad assortment of mathematical
topics, and overlap in many ways.
However, it does not seem that they map cleanly and directly to any one,
and instead seem to straddle many.
Part of the project here in this text and elsewhere, in other texts, is
to articulate these straddles and maps.
\end_layout
\begin_layout Standard
Proposed examples include:
\end_layout
\begin_layout Itemize
Term algebra (because it is simple and absolutely free)
\end_layout
\begin_layout Itemize
Boolean Logic (because predicates and relations will be needed.)
\end_layout
\begin_layout Itemize
Theory of equality (because the theory of equality is the simplest theory
in which freeness is constrained by relationships)
\end_layout
\begin_layout Itemize
Non–free structures, quotients (because quotienting seems to be the generic
way in which cosets are definable, with the cosets being the objects of
the non–free theory.)
\end_layout
\begin_layout Itemize
Chomsky–style production rules; Backus–Nauer Form (BNF); languages generated
from grammars.
(Because this is an older but valid way of articulating the relationship
between syntax and language.) (Note again a traditional lack of specification
of what the output type is.)
\end_layout
\begin_layout Itemize
Unbounded arity
\end_layout
\begin_layout Itemize
Universe of Discourse
\end_layout
\begin_layout Itemize
Tensor product (because products are what allow lists, pairs to be specified.)
\end_layout
\begin_layout Itemize
Tensor–Hom adjunction aka currying (because this is the basic construct
arising in almost all categories.)
\end_layout
\begin_layout Itemize
Monoids, associativity, commutativity (Because these are commonplace, enabling
both enriched categories, and abelian categories.)
\end_layout
\begin_layout Itemize
Term rewriting, graph rewriting (Because rewriting is a cornerstone of generatin
g proofs, equivalences, homotopic equivalences.)
\end_layout
\begin_layout Itemize
Proofs, inference, deduction (as examples of confluent rewrites generating
morphisms)
\end_layout
\begin_layout Itemize
Turing machines, register machines (Because this is where computing starts,
with register machines eventually leading to RAM and stored–program computers.)
\end_layout
\begin_layout Standard
The goal of the above is to describe axioms as jigsaws.
But soon to follow must be homomorphisms and homeomorphisms and adjoint
relationships, since one of the goals is to enable the automatic exploration
and generation of equivalences and adjoint relationships.
n the last case, the adjoint mapping between Turning machines and register
machines.
\end_layout
\begin_layout Subsection
Term algebra
\end_layout
\begin_layout Standard
The goal here is to make contact between the conventional description, notation
and conventions of term algebras, and Atomese.
A reasonable place to start is the Wikipedia description of term algebras.
It is as follows:
\end_layout
\begin_layout Standard
\begin_inset Quotes eld
\end_inset
\emph on
A term algebra is a freely generated algebraic structure over a given signature.
For example, in a signature consisting of a single binary operation, the
term algebra over a set X of variables is exactly the free magma generated
by X.
Other synonyms for the notion include absolutely free algebra and anarchic
algebra.
\emph default
\begin_inset Quotes erd
\end_inset
\end_layout
\begin_layout Standard
Fine.
Realigning the vocabulary, a term algebra is the
\begin_inset Quotes eld
\end_inset
language
\begin_inset Quotes erd
\end_inset
generated by the
\begin_inset Quotes eld
\end_inset
syntax
\begin_inset Quotes erd
\end_inset
given by the
\begin_inset Quotes eld
\end_inset
signature
\begin_inset Quotes erd
\end_inset
.
Thus, we want to convert signatures to Atomese.
The Wikipedia article on signatures states:
\end_layout
\begin_layout Standard
\begin_inset Quotes eld
\end_inset
\emph on
A signature lists and describes the non–logical symbols of a formal language.
They are rarely made explicit in more philosophical treatments of logic.
\emph default
\begin_inset Quotes erd
\end_inset
\end_layout
\begin_layout Standard
Of course, the task at hand is not just to make these explicit, but overwhelming
ly so.
Quoting from Wikipedia, in full:
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
\begin_inset space \qquad{}
\end_inset
\begin_inset Box Frameless
position "t"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "87col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open
\begin_layout Subsubsection*
\emph on
Definition
\end_layout
\begin_layout Plain Layout
\emph on
Formally, a (single–sorted)
\series bold
signature
\series default
can be defined as a 4–tuple
\begin_inset Formula $\sigma=\left(S_{\mathrm{func}},S_{\mathrm{rel}},S_{\mathrm{const}},\mathrm{ar}\right)$
\end_inset
, where
\begin_inset Formula $S_{\mathrm{func}}$
\end_inset
and
\begin_inset Formula $S_{\mathrm{rel}}$
\end_inset
are disjoint sets not containing any other basic logical symbols, called
respectively
\end_layout
\begin_layout Itemize
\series bold
\emph on
function symbols
\series default
(examples:
\begin_inset Formula $\,+,\times$
\end_inset
),
\end_layout
\begin_layout Itemize
\series bold
\emph on
relation symbols
\series default
or
\series bold
predicates
\series default
(examples:
\begin_inset Formula $\,\leq,\,\in$
\end_inset
),
\end_layout
\begin_layout Itemize
\series bold
\emph on
constant symbols
\series default
(examples:
\begin_inset Formula $\,0,1$
\end_inset
),
\end_layout
\begin_layout Plain Layout
\emph on
and a function
\begin_inset Formula $\mathrm{ar}:S_{\mathrm{func}}\cup S_{\mathrm{rel}}\to\mathbb{N}$
\end_inset
which assigns a natural number called
\series bold
arity
\series default
to every function or relation symbol.
A function or relation symbol is called
\begin_inset Formula $n$
\end_inset
–ary if its arity is
\begin_inset Formula $n.$
\end_inset
Some authors define a nullary (
\begin_inset Formula $0$
\end_inset
–ary) function symbol as
\series bold
constant symbol
\series default
, otherwise constant symbols are defined separately.
\begin_inset Newline newline
\end_inset
\end_layout
\begin_layout Plain Layout
\emph on
A signature with no function symbols is called a
\series bold
relational signature
\series default
, and a signature with no relation symbols is called an
\series bold
algebraic signature
\series default
.
A
\series bold
finite signature
\series default
is a signature such that
\begin_inset Formula $S_{\mathrm{func}}$
\end_inset
and
\begin_inset Formula $S_{\mathrm{rel}}$
\end_inset
are finite.
More generally, the cardinality of a signature
\begin_inset Formula $\sigma=\left(S_{\mathrm{func}},S_{\mathrm{rel}},S_{\mathrm{const}},\mathrm{ar}\right)$
\end_inset
is defined as
\begin_inset Formula $\left|\sigma\right|=\left|S_{\mathrm{func}}\right|+\left|S_{\mathrm{rel}}\right|+\left|S_{\mathrm{const}}\right|.$
\end_inset
\begin_inset Newline newline
\end_inset
\end_layout
\begin_layout Plain Layout
\emph on
The
\series bold
language of a signature
\series default
is the set of all well formed sentences built from the symbols in that
signature together with the symbols in the logical system.
\end_layout
\end_inset
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
As always, such definitions are adapted for human readability and authorability,
and not for algorithmic simplicity.
Now, as we are living in modern times, I could always as an LLM to convert
the above description to something computable.
However, I have to give it some examples of what I mean, and so the following
is the example.
In fact, this entire text could be considered to be one giant prompt for
some LLM to digest and act upon.
My goal really is to automate the generation of languages, and Atomese
is my favored syntactical device for doing so.
If you are a human reader of this text, feel free to skim and let your
eyes glaze over.
I'm not sure you are missing much.
\end_layout
\begin_layout Standard
The example of a unary function symbol was given earlier.
Lets adapt it for the above example.
The signature as defined by Wikipedia is
\begin_inset Quotes eld
\end_inset
single–sorted
\begin_inset Quotes erd
\end_inset
, so we replace the ints and floats by a single type,
\begin_inset Quotes eld
\end_inset
any
\begin_inset Quotes erd
\end_inset
.
(A
\begin_inset Quotes eld
\end_inset
sort
\begin_inset Quotes erd
\end_inset
is a synonym for
\begin_inset Quotes eld
\end_inset
type
\begin_inset Quotes erd
\end_inset
or
\begin_inset Quotes eld
\end_inset
kind
\begin_inset Quotes erd
\end_inset
.
At present, no distinction is made between sorts, kinds and types.)
\end_layout
\begin_layout Standard
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
\begin_inset Box Frameless
position "t"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "100col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open
\begin_layout Plain Layout
\family sans
(LexicalEntryType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ItemType
\begin_inset Quotes eld
\end_inset
func
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ConnectorListType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
any
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
output
\begin_inset Quotes erd
\end_inset
))
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
any
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
input
\begin_inset Quotes erd
\end_inset
))))
\end_layout
\end_inset
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
The plus and times symbols
\begin_inset Formula $+,\times$
\end_inset
are conventionally written as infix symbols.
By human convention, these symbols have finite but unbounded arity, because
they commute, and no one wishes to dwell on the fact that they are actually
binary, and need to be lifted freely (by the
\begin_inset Quotes eld
\end_inset
trivial lifting lemma
\begin_inset Quotes erd
\end_inset
) to entire expressions.
But Wikipedia wishes that we assign a fixed arity, and so we shall.
The commutative or associative nature will not be taken for granted; the
argument order matters.
Thus, we write
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
\begin_inset Box Frameless
position "t"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "100col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open
\begin_layout Plain Layout
\family sans
(LexicalEntryType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ItemType
\begin_inset Quotes eld
\end_inset
plus
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ConnectorListType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
any
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
output
\begin_inset Quotes erd
\end_inset
))
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
any
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
input
\begin_inset Quotes erd
\end_inset
))
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
any
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
input
\begin_inset Quotes erd
\end_inset
))))
\end_layout
\end_inset
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
This is arity–two, because it has two inputs.
The output type is still explicitly specified, even though it is
\begin_inset Quotes eld
\end_inset
any
\begin_inset Quotes erd
\end_inset
.
The output connector must be present, as, without this connector, there
is no way to freelly generate the language by snapping together the jigsaws.
The function was renamed to
\begin_inset Quotes eld
\end_inset
plus
\begin_inset Quotes erd
\end_inset
so as to avoid possible confusion as to the meaning of symbols, and to
stick to a UTF–8 convention for strings, avoiding MathML in the actual
Atomese expression.
\end_layout
\begin_layout Standard
The constant symbols are easy: they are zero–ary terms having only an output.
For example,
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
\begin_inset Box Frameless
position "t"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "100col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open
\begin_layout Plain Layout
\family sans
(LexicalEntryType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ItemType
\begin_inset Quotes eld
\end_inset
zero
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ConnectorListType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
any
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
output
\begin_inset Quotes erd
\end_inset
))))
\end_layout
\end_inset
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
Every constant will have this form.
\end_layout
\begin_layout Standard
The Wikipedia articles played a bit fast and loose with the relations, mostly
because relations are implicitly obvious to any human reader.
To be precise, we need to write:
\end_layout
\begin_layout Standard
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
\begin_inset Box Frameless
position "t"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "100col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open
\begin_layout Plain Layout
\family sans
(LexicalEntryType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ItemType
\begin_inset Quotes eld
\end_inset
greater than
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ConnectorListType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
bool
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
output
\begin_inset Quotes erd
\end_inset
))
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
any
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
input
\begin_inset Quotes erd
\end_inset
))
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
any
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
input
\begin_inset Quotes erd
\end_inset
))))
\end_layout
\end_inset
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
Note that the output type is
\begin_inset Quotes eld
\end_inset
bool
\begin_inset Quotes erd
\end_inset
and not
\begin_inset Quotes eld
\end_inset
any
\begin_inset Quotes erd
\end_inset
.
So, strictly speaking, the claim of being single–sorted is off–by–one:
there is the sort of the terms, and the sort of boolean logic.
Left implicit were the logical connectives, so, for example:
\end_layout
\begin_layout Standard
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
\begin_inset Box Frameless
position "t"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "100col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open
\begin_layout Plain Layout
\family sans
(LexicalEntryType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ItemType
\begin_inset Quotes eld
\end_inset
boolean and
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ConnectorListType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
bool
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
output
\begin_inset Quotes erd
\end_inset
))
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
bool
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
input
\begin_inset Quotes erd
\end_inset
))
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
bool
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
input
\begin_inset Quotes erd
\end_inset
))))
\end_layout
\end_inset
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
This allows the relations to be combined with logical connectives, giving
the first–order language that is the term algebra.
It is first–order only because we've omitted any mention of variables,
or of the there–exists
\begin_inset Formula $\exists.x$
\end_inset
and for–all
\begin_inset Formula $\forall.x$
\end_inset
constructors needed for higher–order languages, and the walk up the Borel
hierarchy.
That's OK; the claim is that these two can be expressed in Atomese, with
the
\begin_inset Quotes eld
\end_inset
exercise left up to the reader
\begin_inset Quotes erd
\end_inset
.
It is, however, worth noting that Atomese provides a syntactic notation
for structure.
We have not yet broached to subject of the universe of discourse, and semantic
relations that arise therefrom.
In some sense, we want to do model theory, eventually; just not yet.
\end_layout
\begin_layout Subsection
Binary Trees
\end_layout
\begin_layout Standard
This is a good point at which to stop, and examine some of the meta–issues
arising from the above.
The easiest ones can be illustrated with binary trees.
\end_layout
\begin_layout Standard
A quick taste of semantics and the intended model is provided by binary
trees.
Consider the signature consisting of one binary function, two constants,
and zero relations.
It is (at the risk of inciting boredom)
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
\begin_inset Box Frameless
position "t"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "100col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open
\begin_layout Plain Layout
\family sans
(LexicalEntryType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ItemType
\begin_inset Quotes eld
\end_inset
binary function
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ConnectorListType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
any
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
input
\begin_inset Quotes erd
\end_inset
))
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
any
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
output
\begin_inset Quotes erd
\end_inset
))
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
any
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
output
\begin_inset Quotes erd
\end_inset
))))
\end_layout
\end_inset
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
and
\end_layout
\begin_layout Standard
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
\begin_inset Box Frameless
position "t"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "100col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open
\begin_layout Plain Layout
\family sans
(LexicalEntryType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ItemType
\begin_inset Quotes eld
\end_inset
root
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ConnectorListType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
any
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
output
\begin_inset Quotes erd
\end_inset
))))
\end_layout
\end_inset
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
and
\end_layout
\begin_layout Standard
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
\begin_inset Box Frameless
position "t"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "100col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open
\begin_layout Plain Layout
\family sans
(LexicalEntryType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ItemType
\begin_inset Quotes eld
\end_inset
leaf
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
(ConnectorListType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(ConnectorType
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(LinkType
\begin_inset Quotes eld
\end_inset
any
\begin_inset Quotes erd
\end_inset
)
\end_layout
\begin_layout Plain Layout
\family sans
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
\begin_inset space \qquad{}
\end_inset
(SexType
\begin_inset Quotes eld
\end_inset
input
\begin_inset Quotes erd
\end_inset
))))
\end_layout
\end_inset
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
It is presumably clear that this generates the language of all finite binary
trees, unbounded in size.
This is the intended, countable model.
Countable, because there are countably many such trees.
Turing machines are readily constructed that can enumerate all possible
finite trees, and as a language, one has Turing machines that can recognize
any given finite binary tree.
The finite binary trees are the sentences of this language.
All this is obvious.
\end_layout
\begin_layout Standard
The above ever so slightly evades the boundaries of a signature, however.
Signatures do not talk of sources and sinks: signatures implicitly terminate
with a term as the root.
This is not said out loud, because if one has a term such as
\begin_inset Formula $f\left(a,b,g\left(c,d\right)\right)$
\end_inset
the fact that the
\begin_inset Formula $f$
\end_inset
is the root of the tree is
\begin_inset Quotes eld
\end_inset
obvious
\begin_inset Quotes erd
\end_inset
, and attention is drawn only to the constant terms
\begin_inset Formula $a,b,c,d$
\end_inset
.
Rewriting these terms are jigsaw pieces exposes the fact that there is
an unconnected connector at the root.
If we really want a complete jigsaw assembly, we want to sink that connector
in some way, instead of leaving it dangling.
\end_layout
\begin_layout Standard
The other abuse above is that the roles of input and output have been reversed.
Normally, for an n–ary function symbol, there are n inputs, and only one
output: the term itself.
Here, the directionality has been reversed: two outputs and one input.
This seems egregious, as it can be solved simply by swapping in and out.
The swap was done for two reasons: first, so that binary trees can be drawn
with the conventional style, with arrows pointing away from the root, towards
the leaves, and not the other way around.
The second reason is to illustrate the fact that jigsaws impose no particular
constraint on arity or directionality.
Indeed, if the connectors were marked in some way other than heterosexual
connection, the notion of
\begin_inset Quotes eld
\end_inset
directionality
\begin_inset Quotes erd
\end_inset
would not even apply.
\end_layout
\begin_layout Subsubsection
The infinite tree
\end_layout
\begin_layout Standard
Slightly less obvious is that there is another model: the infinite binary
tree.
This model contains exactly one sentence: the one and only unique, infinite
binary tree.
This tree does not make use of the constant, and would be the only model
if the constant was omitted from the signature: it is
\begin_inset Quotes eld
\end_inset
trees all the way down
\begin_inset Quotes erd
\end_inset
.
This model is oracular.
As a string, this tree cannot be written down; it would be a string of
infinite length.
More than infinite; it is isomorphic to the Cantor set, and the number
of
\begin_inset Quotes eld
\end_inset
leaves
\begin_inset Quotes erd
\end_inset
are uncountable.
It is oracular, in that there is no Turing machine that can generate the
infinite binary tree (it would have to run
\begin_inset Quotes eld
\end_inset
longer than forever
\begin_inset Quotes erd
\end_inset
), nor recognize it (it would have to scan this longer–than–infinite string).
\end_layout
\begin_layout Standard
As humans, we know that such infinite binary trees exist, because we can
imagine them.
The Ancient Greeks were already able to envision infinity; it took Cantor
to show that there's another infinity, the uncountable infinity, and to
demonstrate that it is strictly larger, using the diagonal argument, and
then to construct a specific instance through the recursive removal of
interior line segments from the real number unit interval.
\end_layout
\begin_layout Standard
Exactly how are we to infer this magical, oracular existence of an overwhelming
large object? Well, it's not particularly hard: just employ infinite recursion.
Jumping the shark, this is most easily illustrated with a diagram.
\end_layout
\begin_layout Standard
\align center
\begin_inset Graphics
filename graphics/binary-tree.eps
width 70col%
\end_inset
\end_layout
\begin_layout Standard
Nowhere does it say that terms must be combined only into a directed acyclic
graph.
The figure on the right is generated by the term on the left, and one can
say, with some care, that it is finitely generated.
\end_layout
\begin_layout Standard
There's a bit of slight–of–hand, here, though.
In the middle figure, two outputs were connected to one input.
In what sense is this legal? In normal experience with functions, algebra
and programming, it is nonsense to have a function with only one input,
but somehow gets two.
There's no way to write
\begin_inset Formula $f\left(x\right)$
\end_inset
with two terms
\begin_inset Formula $g\left(a\right)$
\end_inset
and
\begin_inset Formula $h\left(b\right)$
\end_inset
and write down
\begin_inset Formula $f\left(g\left(a\right)\mbox{ and also }h\left(b\right)\right)$
\end_inset
: this is not a function, it makes no sense, its wildly insane.
Yet, in graph theory, there's nothing particularly wrong here, and in electroni
cs and house wiring, one solders together wires in all sorts of crazy ways.
\end_layout
\begin_layout Standard
The middle figure is valid as a graph, but it is not valid, at least not
naively valid, as a jigsaw assembly.
Implicit in the jigsaws is that the connectors are mated, one–to–one.
There are two ways to resolve this, to arrive at the middle figure: define
the input connector as a multi–connector, allowing one
\emph on
or more
\emph default
connections.
This is done as a matter of course in LG, where the
\family sans
@MV
\family default
connector type is famously a multi–connector.
This is done in LG only as a practical matter, to avoid excessively verbose
descriptions of verbs and adverbs.
The alternative is to define a second jigsaw, taking two inputs and generating
one output.
One then gets a clean, finite jigsaw assembly, with one–on–one mating and
no dangling connectors.
\end_layout
\begin_layout Standard
This has a serious downfall: it destroys the Cantorian infinity.
Cantor demands that each sub–branch of the infinite binary tree to be distinct,
even if otherwise indistinguishable.
If distinctness is destroyed, the infinity goes away, and we are left only
with a finite directed graph containing a pair of loops.
The intended model is that uncountable infinities exist, and that uncountable
infinities really are distinct from diagrams with two loops, even though
such a diagram can provide an OK imaginative representation of infinity,
which, owing to it's finite size, can be written on a single piece of paper,
or, more to the point, can be constructed within a computer with only a
finite amount of RAM.
\end_layout
\begin_layout Standard
I am belaboring this point in this text, as this is a recurring theme in
set theory and model theory: how is it that we can talk about infinities
in a coherent fashion? The set theorists and the model theorists have long
ago overcome these difficulties, able to mumble things even about
\begin_inset Quotes eld
\end_inset
ineffable cardinals
\begin_inset Quotes erd
\end_inset
and
\begin_inset Quotes eld
\end_inset
outer models
\begin_inset Quotes erd
\end_inset
.
That this could be an issue is exposed by assuming some naive, implicit,
as yet mostly unstated rules for mating jigsaw connectors.
\end_layout
\begin_layout Standard
The naive interpretation is that anything with a directed loop represents
an infinity.
The figure on the right, above, shows three directed loops.
It indicates a tiling of the infinite binary tree that would be different,
if the edges were colored.
However, they are not (everything is single–sorted), and so conceptually,
we
\begin_inset Quotes eld
\end_inset
know
\begin_inset Quotes erd
\end_inset
that it is the same infinite binary tree as represented in the middle,
because we
\begin_inset Quotes eld
\end_inset
know
\begin_inset Quotes erd
\end_inset
there is only one infinite tree.
But how do we prove this? The proof would need to involve the ability to
perform deductions on the re–arrangement of jigsaw pieces.
So far, we have not given any axioms explaining how jigsaw pieces connect!
Nor have we given axioms for how proofs are to be carried out!
\end_layout
\begin_layout Subsection
Many–sorted Signatures
\end_layout
\begin_layout Standard
The explicit indication of connector type would seem to leave no ambiguity
as to how typing is to be performed.
Nonetheless, a glance at the formal definition provided on Wikipedia is
revealing.
A verbatim copy follows:
\end_layout
\begin_layout Standard
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
\begin_inset space \qquad{}
\end_inset
\begin_inset Box Frameless
position "t"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "87col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status open
\begin_layout Subsubsection*
\emph on
Many–sorted signatures
\end_layout
\begin_layout Plain Layout
\emph on
For many–sorted logic and for many–sorted structures, signatures must encode
information about the sorts.
The most straightforward way of doing this is via symbol types that play
the role of generalized arities.
\end_layout
\begin_layout Subsubsection*
\emph on
Symbol types
\end_layout
\begin_layout Plain Layout
\emph on
Let
\begin_inset Formula $S$
\end_inset
be a set (of sorts) not containing the symbols
\begin_inset Formula $\times$
\end_inset
or
\begin_inset Formula $\to$
\end_inset
.
The symbol types over
\begin_inset Formula $S$
\end_inset
are certain words over the alphabet
\begin_inset Formula $S\cup\left\{ \times,\to\right\} $
\end_inset
: the relational symbol types
\begin_inset Formula $s_{1}\times\cdots\times s_{n}$
\end_inset
, and the functional symbol types
\begin_inset Formula $s_{1}\times\cdots\times s_{n}\to s^{\prime}$
\end_inset
, for non–negative integers
\begin_inset Formula $n$
\end_inset
and
\begin_inset Formula $s_{1},s_{2},\ldots,s_{n},s^{\prime}\in S$
\end_inset
.
(For
\begin_inset Formula $n=0$
\end_inset
, the expression
\begin_inset Formula $s_{1}\times\cdots\times s_{n}$
\end_inset
denotes the empty word.)
\end_layout
\begin_layout Subsubsection*
\emph on
Signature
\end_layout
\begin_layout Plain Layout
\emph on
A (many-sorted) signature is a triple
\begin_inset Formula $\left(S,P,\mathrm{type}\right)$
\end_inset
consisting of
\end_layout
\begin_layout Itemize
\emph on
a set
\begin_inset Formula $S$
\end_inset
of sorts,
\end_layout
\begin_layout Itemize
\emph on
a set
\begin_inset Formula $P$
\end_inset
of symbols, and
\end_layout
\begin_layout Itemize
\emph on
a map
\begin_inset Formula $\mathrm{type}$
\end_inset
which associates to every symbol in
\begin_inset Formula $P$
\end_inset
a symbol type over
\begin_inset Formula $S$
\end_inset
.
\end_layout
\end_inset
\begin_inset VSpace defskip
\end_inset
\end_layout
\begin_layout Standard
The above indicates a system that is very nearly identical to the jigsaw
representation of the prior section.
This time, an explicit output type is indicated for the function symbols.
The directionality is still implicit: the Cartesian product notation
\begin_inset Formula $s_{1}\times\cdots\times s_{n}$
\end_inset
\emph on
\emph default
is meant to be a list of inputs; the arrow
\begin_inset Formula $\to$
\end_inset
splits the list between input and output types.
Of course, jigsaws could specify two outputs, so the map from sorted signatures
to jigsaws is into, not onto.
\end_layout
\begin_layout Standard
The output type for relations remains implicit; it should have been written
as
\begin_inset Formula $s_{1}\times\cdots\times s_{n}\to\left\{ T,F\right\} $
\end_inset
.
The first–order logical connectives remain elided in the Wikipedia definition.
\end_layout
\begin_layout Standard
The third part of the Wikipedia definition can be ignored, under the presumption
of
\begin_inset Quotes eld
\end_inset
we already did that
\begin_inset Quotes erd
\end_inset
, or it can be made explicit.
The attempt on making it explicit immediately founders on multiple issues.
Explicit jigsaw representations need to be created for the following:
\end_layout
\begin_layout Itemize
A representation of a set, with ur–elements that are sorts.
\end_layout
\begin_layout Itemize
An ability to select (choose) a single element from a set.
\end_layout
\begin_layout Itemize
The ability to select a single element from this specific set, viz.
naming or referring to this set of sorts.
\end_layout
\begin_layout Itemize
The product type constructor, needed to create a list of sorts, which will
belong to the set of
\begin_inset Quotes eld
\end_inset
symbol types
\begin_inset Quotes erd
\end_inset
.
\end_layout
\begin_layout Itemize
The arrow type constructor, needed to create the function symbol types.
\end_layout
\begin_layout Itemize
A map, which, given a
\begin_inset Quotes eld
\end_inset
symbol name
\begin_inset Quotes erd
\end_inset
(the lexical entry name of the jigsaw), returns the
\begin_inset Quotes eld
\end_inset
symbol type
\begin_inset Quotes erd
\end_inset
.
Since the full jigsaw consists of the name, and the connector list, this
is as simple as projecting out the two components.
Alternately, (via currying) the jigsaw is assembled from these two pieces.
\end_layout
\begin_layout Standard
The full development of the explicit construction of jigsaws from small
pieces awaits the articulation of these mechanisms.
\end_layout
\begin_layout Subsection
Boolean Logic; Disjoint Unions; Flows
\end_layout
\begin_layout Standard
The specification of jigsaw pieces encounters many of the same conceptual
issues as categories.
Consider, for example, the logical connectives
\begin_inset Formula $\wedge,\vee,\lnot$
\end_inset
.
These can be rewritten as term symbols
\begin_inset Formula $\mathrm{and}\left(x,y\right),\mathrm{or}\left(x,y\right),\mathrm{not}\left(x\right)$
\end_inset
or even
\begin_inset Formula $\mathrm{and}:B\times B\to B$
\end_inset
with
\series bold
\begin_inset Formula $B$
\end_inset
\series default
indicating the type of the domain.
As with all such cases, one can readily confuse the type with the set that
is the disjoint collection of all of it's possible values; that is,
\begin_inset Formula $B=\left\{ T,F\right\} $
\end_inset
.
\end_layout
\begin_layout Subsection
Naive Set Theory
\end_layout
\begin_layout Standard
The construction for binary trees extends easily to a naive conception of
set theory: merely add function jigsaws for arbitrary, unbounded, finite
input arity.
Creating sets of infinite cardinailty remains an issue, given the constructions
explored so far.
The resulting set theory is
\begin_inset Quotes eld
\end_inset
naive
\begin_inset Quotes erd
\end_inset
in that we don't discuss the assortment of axioms and axiom schemas normally
used to define set theory; the arbitrary–arity jigsaws capture only a naive
conception of set membership.
\end_layout
\begin_layout Standard
xxx
\end_layout
\begin_layout Standard
membership, arrows, products, type constructors, commutativity.
\end_layout
\begin_layout Section
Open Issues
\end_layout
\begin_layout Standard
In the course of writing the above, a number of issues arise.
They are tracked here.
\end_layout
\begin_layout Itemize
Universe of Discourse – how is this to be managed and understood?
\end_layout
\begin_layout Itemize
Disjoint Union
\end_layout
\begin_layout Itemize
Given any network with pretensions of being a term algebra with relations
and logical connectives, i.e.
a model–theoretic model, one can attach vectors, matrices and tensors to
the vertexes with one, two, three edges coming from them, and form a trainable
network.
But what should one train on?
\end_layout
\begin_layout Itemize
The example prototype here is LTN, Logic Tensor Networks, from https://github.com
/logictensornetworks/logictensornetworks
\end_layout
\begin_layout Standard
xxx
\end_layout
\begin_layout Section*
The End
\end_layout
\end_body
\end_document