Fourth feature in the glossary to Grice's natural deduction system

The fourth and last feature in the glossary involves the operation of 'replacement', which Grice symbolises by division:

a/b

with an upper and a lower symbol.

The upper symbol is always the Substituend.

Replacements thus read

phi(th2/th1)

If th1 and th2 are terms (i.e. individual constants or bound variables),

phi(th2/th1) will read as

"the very result of substituting

each occurrence of the former term, th1,

in the formula phi, by

one occurrence of the latter term, th2,

such that it preserves subscripts at

substitution points."

----