While deduction arrows indicate the logical structure of a proof, it can be useful to have another type of arrow, to help direct the reader to examine the nodes of the proof in a certain order.
For example, it is good to guide the reader to the introduction of new symbols, before visiting nodes that use those symbols.
For this, Proofscape diagrams offer flow arrows, which are drawn dashed instead of solid.
A, therefore B. C implies D.
There are three keywords in the flow keyword category:
and the rule governing the drawing of flow arrows is as follows:
A flow arrow will be drawn from node
Bwhen all the keywords between
B(if any) are in the modal and/or flow categories. In particular, a flow arrow will be drawn if there are no keywords at all between
A, therefore B. Let I. Then C, using D.
Suppose S. Then A. Now let I. Then B, by A and C.
Notice that in this last case there are two arrows leaving node
A, and the
purpose of the flow arrow is to tell us that we should consider the
I first, before considering node