# More common inference rules

Before learning about more handy rules of inference, let’s clarify a bit the notation in the next sections.

Capital letters A, B, and C here are not variables in the logic. They are pattern variables to be replaced with arbitrary boolean terms (with true/false values). Letters F and G represent terms whose values are functions. Capital letters X and Y are also pattern variables, for arbitrary terms of any type.

## Rewriting and replacement

Rewriting and replacement are core parts of inference in Prooftoys, and have their own page.

## Variations on substitution

From: Proof step with one or more free variables. To: Proof step with a term substituted for each variable.

### Universal instantiation

From: `forall {x. A}`. To: A with a term of your choice substituted for `x`.

### Substitution into a function body (beta reduction)

From: `{x. A} X`. To: `A`, with term `X` substituted for `x` throughout

This can be done anywhere in any formula.

#### Note on substitution

In the simple cases, all forms of substitution above work in the way you might expect from examples in any high school math textbook. There is a restriction in cases where the term undergoing substitution contains “bound” variables of its own.

For details on this see link TBD.

## Other rules

### Self-equality

`X = X`

The value of any expression is equal to itself.

### Universal quantifier elimination

From: `forall {x. B}` To: `B`

(Result of instantiating with `x`.)

### Universal quantifier introduction

From: `B` To: `forall {x. B}`

### Binding both sides of an equation

From: `X = Y` To: `{x. X} = {x. Y}`

(Consequence of `{x. X} = {x. X}`, then replacing the second `X` with `Y`.)

### Unbinding an equation

From: `g = {x. X}` To: `g x = X`

This is useful for converting a definition from the basic form to the usual form seen in first-order logics. For a function `g` of more than one variable, this rule can apply multiple times.

### Rebinding an equation

From: `g x = X` To: `g = {x. X}`

This is useful for converting a definition from the basic form to the usual form seen in first-order logics. Like unbinding, this rule can be applied multiple times for functions of multiple arguments.

### Removing irrelevant assumptions

If a conditional fact has an assumption with a variable that only appears (free) in that assumption and nowhere else in the statement of the fact, in almost all cases, that assumption can safely be removed. We can suggest the working of the inference like this:

From: a_1 and a_2 and … ⇒ C To: a_2 and … ⇒ C

The one limitation is that there must be some value for the variable that can make the irrelevant assumption true. So to use this rule in a proof, there must be a proof that such a value exists. Prooftoys doesn’t yet support this rule in its general form, but it supports a couple of common cases. These are useful cases, and Prooftoys can work out the existence fact on its own. The cases are:

<var> = <term>; and R <var>

In both cases, the variable `var` does not appear in the fact outside this one assumption.

For every assumption of these kinds, the existence of a value satisfying it is provable, so we can remove the assumption from the proof step.

### Some fancy forms of rewriting

A couple of often-useful inference rules in Prooftoys combine a couple of steps together and rewrite the result. These may take two steps and “conjoin” them using the boolean “and” operation. Then they rewrite a tautology to make it match the conjunction and infer a conclusion.

Proof steps that use these rules tend to have the word “consequence” in their description.

[[More to be written here.]]