This document is your guide for the MathLingua language, its structure, design, and syntax.

The MathLingua Language is composed of a structural sublanguage, a statement sublanguage, and a text sublanguage. These languages work together to describe mathematical knowledge.

Before diving deeper into the syntax of MathLingua, the interaction between these sublanguages will be illustrated through the use of an example.

Note that throughout this text MathLingua examples will displayed in a tabbed
pane. You can click on the *Source* and *Rendered* buttons to switch between
the MathLingua source and the associated rendered form.

First we will start with the definition of an *integer*.

[\integer]

Defines:n

means:

."$n?$ is one of the numbers $\ldots, -2, -1, 0, 1, 2, \ldots$"

Metadata:

.written:"\textrm{integer}"

Defines:n

means:

."$n?$ is one of the numbers $\ldots, -2, -1, 0, 1, 2, \ldots$"

Metadata:

.written:"\textrm{integer}"

[\integer]

Defines:\[n\]

means:

.$n$ is one of the numbers $\ldots, -2, -1, 0, 1, 2, \ldots$

Metadata:

.written:\textrm{integer}

Defines:\[n\]

means:

.$n$ is one of the numbers $\ldots, -2, -1, 0, 1, 2, \ldots$

Metadata:

.written:\textrm{integer}

A Defines: is used to define a mathematical entity and
specify a *signature* used to represent that entity.
In this case, the \integer signature defines
n as one of the numbers $\ldots, -2, -1, 0, 1, 2, \ldots$.

This definition illustrates the use of the *text sublanguage*. The text sublanguage is
used within double quotes. The content between double quotes can
be any valid LaTeX (where the amsmath and amssymb package contents are available).

There are more features the text sublanguage provides, but for now, just think of it as a way to specify math knowledge using LaTeX.

Next, to illustrate the *statement sublanguage* we will describe what it means
for an integer to divide another integer.

[d \divides n]

Represents:

assuming:

.'n, d is \integer'

that:

.exists:k

suchThat:

.'k is \integer'

.'n = d*k'

Metadata:

.written:"d?? | n??"

Represents:

assuming:

.'n, d is \integer'

that:

.exists:k

suchThat:

.'k is \integer'

.'n = d*k'

Metadata:

.written:"d?? | n??"

[d \divides n]

Represents:

assuming:

.\[n, d\]is\[\textrm{integer}\]

that:

.exists:\[k\]

suchThat:

.\[k\]is\[\textrm{integer}\]

.\[n = d * k\]

Metadata:

.written:d | n

Represents:

assuming:

.\[n, d\]is\[\textrm{integer}\]

that:

.exists:\[k\]

suchThat:

.\[k\]is\[\textrm{integer}\]

.\[n = d * k\]

Metadata:

.written:d | n

A Represents: is used to described what a mathematical notation means. Notice unlike an \integer which describes a thing, what it means for integer d to divide an integer n is a concept. Thus a Represents: is used instead of a Defines:.

Next, you will notice the code above has text within single quotes. Such text is part of
the *statement sublangage*. Unlike the text sublanguage which is essentially any valid
LaTeX, the statement sublanguage is has a strict syntax. This syntax is inspired by LaTeX
but is distinct from it, and is used to describe the *meaning* of a statement.

Specifically, signatures used in single quotes reference their associated Defines: or Represents:. This association is unique. That is, for any signature, there is at most one Defines: or Represents: associated with it that describes its meaning.

Note there may be no such association yet if the meaning has not yet been defined. This is the case with * above that has not yet been formally defined in a Defines: or Represents:.

Moreover, a Defines: or Represents: specifies how the item it is describing is written, which is used to render the item. For example, from the code above, p \divides q is written as the letter p followed by a vertical line followed by the letter q. Note, that the p is associated with d in the definition and q with n when rendering the p \divides q.

We have actually been using the *structural sublanguage* this entire time. However, to
make it more clear, consider the following definition of a *prime number*.

[\prime]

Defines:p

means:

.'p is \integer'

.'p > 1'

.for:d

where:

.'d \divides p'

then:

.or:

.'d = 1'

.'d = n'

Metadata:

.written:"\textrm{prime}"

Defines:p

means:

.'p is \integer'

.'p > 1'

.for:d

where:

.'d \divides p'

then:

.or:

.'d = 1'

.'d = n'

Metadata:

.written:"\textrm{prime}"

[\prime]

Defines:\[p\]

means:

.\[p\]is\[\textrm{integer}\]

.\[p > 1\]

.for:\[d\]

where:

.\[d | p\]

then:

.or:

.\[d = 1\]

.\[d = n\]

Metadata:

.written:\textrm{prime}

Defines:\[p\]

means:

.\[p\]is\[\textrm{integer}\]

.\[p > 1\]

.for:\[d\]

where:

.\[d | p\]

then:

.or:

.\[d = 1\]

.\[d = n\]

Metadata:

.written:\textrm{prime}

The *structural sublanguage* is the text around the single and double quote items.
Specifically the, Defines:means:Metadata:,
for:where:then:, and or:
are part of the *structural sublanguage* and form the structure of the mathematical
knowledge (a definition in this case).

The structural language uses indentation to align sections of a structure that go together and uses a dot and space to specify arguments to a section that occur on their own line.

The meaning of the definition above can be read from top to bottom following the indentation. That is, it states that a \prime defines a p that satisfies p is an integer, p is greater than one, and for any d, where d divides p then either d equals 1 or d equals n.

Now we can define a theorem that uses the above definitions and representations. Note
that the arguments of a section are joined by *and*. That is the theorem below says
for a, b, and
p where a and
b are integers *and* p is prime
*and* p divides the product of a
and b, then either p divides
a or p divides
b.

Theorem:

.for:a,b,p

where:

.'a, b is \integer'

.'p is \prime'

.'p \divides a*b'

then:

.or:

.'p \divides a'

.'p \divides b'

.for:a,b,p

where:

.'a, b is \integer'

.'p is \prime'

.'p \divides a*b'

then:

.or:

.'p \divides a'

.'p \divides b'

Theorem:

.for:\[a\],\[b\],\[p\]

where:

.\[a, b\]is\[\textrm{integer}\]

.\[p\]is\[\textrm{prime}\]

.\[p | a * b\]

then:

.or:

.\[p | a\]

.\[p | b\]

.for:\[a\],\[b\],\[p\]

where:

.\[a, b\]is\[\textrm{integer}\]

.\[p\]is\[\textrm{prime}\]

.\[p | a * b\]

then:

.or:

.\[p | a\]

.\[p | b\]

The rest of this document is still a work in progress. Check back regularly for updates.