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 As 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.