CSE 463/563, Spring 2005

Rules for "Send" and "Return"

Last Update: 14 February 2005

Note: or material is highlighted

Here are the details of how the rules of SEND and RETURN work in the system of propositional logic that we are using. Note that you may begin (or "call", or "enter"--choose your favorite metaphor) a subproof only if you are applying ¬INTRO, ¬ELIM, or INTRO.

SEND

We justify information legitimately flowing into a subproof with the rule SEND plus the citation of the earlier line number outside of the subproof. The justification SEND can be used, provided:

We are in a subproof with more asterisks (*) than the cited line.
The sentence being "sent" is exactly the sentence in the cited line.
Every line between the SEND line and the cited line has at least as many asterisks as the cited line.

RETURN

We justify information legitimately flowing out of a subproof with the rule RETURN plus the citation of a line in the subproof. The justification RETURN can be used, provided:

We are outside of the subproof, with one less asterisk than the cited line.
The sentence being returned is exactly the sentence in the cited line.
There is no line between the present line and the cited line with fewer asterisks than the cited line.
The cited line has the justification ¬INTRO, ¬ELIM, or INTRO.

From: Schagrin, Morton L.; Rapaport, William J.; & Dipert, Randall R. (1985), Logic: A Computer Approach (New York: McGraw-Hill)

SCI/ENGR Book Collection BC138 .S32 198