How to write code

Check out the /math directory from the repo for many examples.

The object language

Types

Every statement in the object language is assigned a type. A type is either:

a primitive type,
a functional type, or
a macro type.

Primitive types

"The statement type."
type st;

Primitive types can be declared by writing type <type name>;. The docstring for the type can also be written within the double quotes. All primitive types with a different name are considered different.

Functional types

Functional types can be created from existing types by using the type constructor $\to$ . For example, if cls and st are types, then [cls, cls -> st] is the type of the function that maps two cls type terms to one st type term.

Macro types

Macro types provide an alias for an already existing type. For example, the following code declares the macro type pr as an alias for the functional type [cls -> st]:

"The unary predicate type."
type pr = [cls -> st];

Terms

Now that types are defined, we can now define terms that are assigned one of those types. A term can either be an undefined term or a macro term.

Undefined terms

"Verum (T). Denotes an arbitrary tautology."
$\top$
st T;

You can change the appearance of the term by writing a corresponding $\LaTeX$ code between the $ signs. The above example sets the appearance of the term T as $\top$ (\top).

Undefined terms with a functional type can also be defined as follows:

"The binary logical connective AND (TFFF)."
$\land$
[st, st -> st] A;

However it is recommended to write instead like this:

"The binary logical connective AND (TFFF)."
[precedence=596]
$#1<<\land>>#2$
st A(st p, st q);

One advantage of writing like this is that you can make the function call A(p, q) be displayed as $p\land q$ (p \land q) instead of $\land(p, q)$ (\land(p, q)).

[precedence=596] sets the operator precedence of A as 596. The operator precedence is the mechanism that determines whether additional parentheses are required or not when displaying the expressions in $\LaTeX$ .
#1 and #2 serve as placeholders for the first and the second argument of the function, respectively. When the function call is displayed, the placeholders are replaced with the arguments and then rendered as $\LaTeX$ .
The segment enclosed with << and >> is the clickable part that when clicked, displays the definition and the description of the term.

Function expressions and function calls

The object language also has syntaxes for function expressions and function calls.

Function calls

Function calls, just like one would normally write doing mathematics or programming, can be written by first writing the function name followed by arguments separated by commas and enclosed with parentheses. The number of arguments and the types of arguments must correspond to the type of the function.

For example, in order to call the function A with the arguments T and T, one can write A(T, T). If the type of the function A is [st, st -> st], in order to match the input type, the term T should have the type st.

Function expressions

You can write function expressions to create anonymous functions, much like writing lambda expressions in many programming languages. For example, a function with one input parameter p of type st and an output of A(p, T) can be written as:

(st p) => A(p, T)

or,

(st p) => { A(p, T) }

The curly braces can either be omitted or not. Since the above function returns a st type term, it is automatically assigned the type [st -> st].

Macro terms

Macro terms provide an alias for an already existing expression. For example, the following code declares the macro term F as an alias for the expression N(T):

"falsum (F)."
$\bot$
st F = N(T);

Macro terms with a functional type can also be defined as follows:

"[#A] for unary predicates."
$\land$
[pr, pr -> pr] Af = (pr f, pr g) => {
	(cls z) => A(f(z), g(z))
};

However it is recommended to write instead like this:

"[#A] for unary predicates."
$\left(#1<<\land>>#2\right)$
pr Af(pr f, pr g) {
	(cls z) => A(f(z), g(z))
}

Compared to the syntax for the undefined terms, the above declaration includes the body that describes the macro term.

Axioms and proofs

Axioms can be written like this:

"Conjunction introduction."
axiom Ai(st p: @1, st q: @2) {
	p, q |- A(p, q)
}

The axiom keyword denotes that the above schema is an axiom. The mathematical symbol $\vdash$ is written as |-. The selectors @1 and @2 are to automatically detect the arguments when applying the ⊦E rules. Axioms and theorems should be defined as a nullary schema even though no parameters are necessary. Like this:

"Axiom of empty set."
axiom ax_emptyset() {
	set(emptyset)
}

Theorems can be written like this:

"Conjunection introduction, applied twice."
theorem A3i(st p: @1, st q: @2, st r: @3) {
	p, q, r |- {
		[[@h1; @h2] > Ai; @h3] > Ai
	}
}

The selectors @h1, @h2, and @h3 each denote the first, second, and the third hypotheses p, q, and r. Therefore

[@h1; @h2] > Ai

becomes

[p; q] > Ai

which becomes

[p; q] > Ai(p, q)

since the arguments (p, q) are automatically detected. Since Ai(p, q) is equal to p, q |- A(p, q), the above expression becomes

[p; q] > (p, q |- A(p, q))

The > operator is for applying the ⊦E rule, which compares the left operand p, q to the LHS of |-, i.e., p, q, and if they are equal, creates a proof chain from the left and right operand of > operator to the RHS of |-. Therefore the above expression becomes

A(p, q)

and

[A(p, q); r] > Ai

becomes

A(A(p, q), r)

Therefore, in Fitch notation, A3i can be written like this:

1 ┃ p                      hypothesis
2 ┃ q                      hypothesis
3 ┃ r                      hypothesis
  ┣━━━
4 ┃ p ∧ q                  ⊦E, Ai, [1, 2]
5 ┃ (p ∧ q) ∧ r            ⊦E, Ai, [4, 3]
6 p, q, r ⊦ (p ∧ q) ∧ r    ⊦I [1–5]

The above diagram can also be seen from the proof explorer. math-o-matic proof checker checks if the proof has been successful and if it is the theorem is colored green.

(TODO)