The Language

The universe … cannot be understood unless one first learns to comprehend the language in which it is written. It is written in the language of mathematics. – Galileo Galilei

Statements and expressions

The language has only expressions, which are often referred to as terms. A statement in the language is just an expression whose value is boolean — either true or false.

Expression syntax

There are only three kinds of expressions: atomic expressions, which are either a variable or a constant; function calls, which are either in (prefix) function call form or infix form; and functional expressions.

If plus is a function that adds two numbers, then an expression such as x + y is equivalent to plus x y. An operator can always be used without its special precedence handling by directly surrounding it with parentheses, as in (+) x y, which represents the same term as x + y.

There are infix operators such as + and - for addition and subtraction, each having a certain precedence; unary prefix operators such as the - for the negative of a number; and function calls. (Predicates and relations are functions that return true/false values.)

The concept of precedence is the same as the concept of “order of operations” in textbooks, extended to include the additional operators used in logic. It is also the same idea as precedence in computer languages.

Constants and variables

The logic has two kinds of names: identifiers and operator names. An identifier is an alphabetic character possibly followed by additional letters, digits, and finally underscores ("_"), which render as “prime” marks ("’").

All variable names are identifiers. A name that is a single letter, optionally followed by one or more digits, possibly followed by underscores, is a variable name. If there are any digits, they will display as a subscript on the identifier. The names “T”, “F”, and “R” are reserved for constants and cannot be used as variable names.

An infix operator name is a sequence of printing (currently ASCII) characters that are not letters or digits, brackets, braces, parentheses, colon (":"), “~”, or (".").

Numeric literals are a sequence of digits optionally preceded by “-”. (In all other situations “-” is an infix operator.) Numeric literals are always integers. Numeric literals as arguments to prefix-style function calls or operators must be enclosed in parentheses, like (-5) to avoid ambiguity with subtraction.

Operators and infix

Except as noted, constants named as operators are treated as infix operators, and infix expressions are parsed according to their precedence.

To suppress the infix nature of an operator, enclose its name in parentheses, as in (+).

The precedences of Prooftoys infix operators in order from lowest to highest, in the input syntax, are:

 ==
  =>
  |
  &
  ??
  =, !=, <, <=, >, >=
  divides, in, notin, subset?, mapsFrom, mapsTo
  intersect, union, @@
  +, -
  *, /, div, mod
  ^
  user-defined operators

Items on the same line have equal precedence. All infix operators are left-associative, so a + b - c is the same as (a + b) - c and a => b => c is the same as (a => b) => c. The \==, which displays as ≡, is for boolean equivalence, which is equality of true/false values.

Unary operators

The operator name ~ represents boolean negation. Similarly, \~* represents the multiplicative inverse, so \~*x is equal to 1/x. All operators with names beginning with ~ are unary. Calls to unary operators are the same syntactically as ordinary calls to functions.

Function calls

Ordinary calls to functions, using a constant or variable name, or a functional expression (see below), use prefix syntax with the function before its arguments. In this syntax, to call a function f with argument x, write f x, where f could be any expresssion, though it should have a function as its value. For example R x means “x is a real number”.

To call a function with more arguments, just write the expressions for all the arguments following the expression for the function, e.g. log x 10. An expression f g x represents a call to f with two arguments, g and x. A call to f with argument g x is written as f (g x).

Function calls have precedence over all infix operators, so sin x/2 means the same as (sin x) / 2.

Examples

For example, a statement that might be conventionally written as

would be written in Prooftoys as

or omitting the parentheses around the function call, like this:

Functional expressions

Any expression can be enclosed in parentheses to guarantee its grouping, but an expression enclosed in braces always represents a function. For example a definition of a function that squares a number might look like:

(Function and predicate definitions are usually written without a functional expression, for example square x = x * x. The two styles of definitions are fully equivalent.)

Similarly, a predicate that is true just for positive numbers could be defined as:

providing a conventional set notation.

For a relation (e.g. two argument predicate), the logic uses nested lambdas. So we define “greater than” in terms of “less than” like this:

This is equivalent to the definition greater x y == y < x.

Displaying functional expressions

If a function does not return a boolean value, Prooftoys may also display it surrounded with parentheses, or with a “pointer-like” marker rather than “.”.

Quantifiers

A typical statement with a universal quantifier has a form like:

and a typical existential statement looks something like:

How can that be? In this logic, quantifiers are defined predicates, not primitives of the language. They take an argument that is a collection. The universal quantifier predicate is named “forall” and displays as ∀. The existential quantifier is named “exists” and displays as ∃.

The term {x. p x} can be read as set notation, as something like “the collection of x that have the property p”.

The boolean term ∀ {x. p x} is true exactly if every possible value of x has property p.

Quantifiers without braces

An expression of the form {x. p x} can be shortened to just p, and in some situations you will see a statement such as

This is sometimes referred to as Prooftoys “native form” and is often used in preference to the more conventional-looking equivalent:

Next steps

A good next step might be to introduce yourself to inference in Prooftoys.