google03@xxxxxxxxxx wrote:
Suppose P is a proof of the proposition q. Is there a standard name for
q as a function of P?
For example, in the special case that the proof P consists of p, p->q,
and an application of modus ponens to derive q, then q is called the
'consequent'.
Is there a standard word for the thing that a more general proof
proves?
(I'm just trying to give a function in a computer program a sensible
name. Things like 'target', 'result, 'goal' or 'end' just don't seem
descriptive enough to me...)
'consequent' is very generic name as you've noted. You could use
the name(s) of the inference rule(s) I guess. E.g.,
q = MP(p)
--
-----------------------------------------------------
What we call 'I' is just a swinging door which moves
when we inhale and exhale.
Shunryu Suzuki
----------------------------------------------------
|