# Prooftoys logic concepts

### Types of values

The most basic kinds of things the logic works with are “true”,
“false”, and *individuals*. In Prooftoys “true” and “false” are
written as `T`

and `F`

.

Numbers are the sorts of *individuals* you will usually encounter in
Prooftoys. Everything in the logic that is not a truth value or an
individual is a function, with input(s) and an output value.

Functions such as addition and multiplication have inputs that are numbers (individuals) and outputs that are also numbers. Function inputs and outputs can also be boolean, and a function can even have a function as its input or its value or both.

Much more explanation of functions with boolean inputs, or outputs, or both, is in the section Logic through pictures.

#### Terminology

**Boolean value.** Simply either `T`

(*true*)
or `F`

(*false*), named in honor of George
Boole, a pioneer in the development of these ideas. These are
also known as the *truth values*.

**Predicate.** A *predicate* tests a value and gives a true/false
result. For example, a test whether a number is even is a predicate.
Every predicate can be thought of as a collection. In Prooftoys there
is no technical difference between “the set of all positive numbers”
and the predicate that tests whether something is a positive number.

**Relation.** A *relation* such as “less than” tests whether a number
is less than another number, for example `x < y`

. It has two inputs
and gives a true/false result.

So predicates and relations are functions that produce values that are
`true`

or `false`

, and a predicate can also be thought of as a
collection.

**Collection.** Collections are functions whose values are boolean, so
there is no technical difference between a collection and a predicate
or relation.

**Fact.** In Prooftoys we refer to any proved statement as a *fact*.
Prooftoys has a registry of selected facts that are already proved
for you, and may offer to apply them for you. Rules that are
described as using facts work with these “well known” facts.
Tautologies are also considered facts, because Prooftoys can prove
them on demand.

**Term.** Mathematical statements have structure in which the
statement has parts and a part of a statement may also have parts.
For example the (true) statement `(x = y) == (y = x)`

has three parts:
`x = y`

, `==`

, and `y = x`

. The part `x = y`

also has three parts:
`x`

, `=`

, and `y`

. In the language of Prooftoys each of these parts,
whether large or small, is a *term*.

**Instance, substitution instance.** A *substitution instance* of a
term is simply the result of applying some substitution to the term.
Every term is also a substitution instance of itself. Documentation
of Prooftoys often uses just *instance* with the same meaning.

**Conditional.** A conditional term is any term that matches the
syntactic pattern `A => B`

. Many proof steps are conditional
statements, the whole statement having this form.

**Assumption(s), antecedent.** The left side of a conditional term is
its antecedent. If the left side has the form `A1 & A2 & ... => C`

,
all of the `A`

s can be called assumptions.

**Conclusion, consequent.** The right side of a conditional term is
known as its conclusion or consequent.

###### Related to function terms

**Syntactic pattern**, or just **pattern**. A syntactic pattern looks
like a term in the Prooftoys language. But if it is described as a
*pattern* to match, then the variables in the pattern are like blank
spaces in a form. Any term in the language that can be made by
filling in those blanks matches the pattern if it also satisfies any
other requirements stated for it.

Sometimes in a pattern, instead of using variable names we use a
longer name or description, written between “<” and “>”, for example:
`\<name>`

instead of `X`

.

**Function term.** A function term is any term that matches the
pattern `{x. X}`

, where `x`

is any variable and `X`

is any term. This
notation is like the “set notation” seen in textbooks, but generalized
to describe arbitrary functions, not just collections.

**Body** (of a *function term*). In a function term matching the
pattern `{x. X}`

, the part matching `X`

is the *body* of the function
term.

**Binding**. A *function term* is also known as a *binding*. In a
function term matching the pattern `{v. X}`

, the variable `v`

is
*bound* in the function term, and every occurrence of that name in `X`

is a *bound occurrence*.

**Free variable.** A free variable of a term is one that has an
occurrence somewhere in the term that is not a *bound occurrence*.
If a term contains no *function terms*, all of its variables are
free variables.

**Bound variable.** In a function term matching the pattern `{x. Z}`

,
the variable that matches `x`

in the pattern is the *bound variable*
of the function term.

**Bound occurrence.** Any appearance of the *bound variable* of a
*function term* in the *body* of the term is a *bound occurrence*.
For example in `{x. x > 0}`

, the one occurrence of `x`

in `x > 0`

is a *bound occurrence*.

**Free occurrence.** A *free occurrence* of a variable name
in a term is an occurrence that is not a *bound occurrence*.