6  One-line rules

6.1 R

Proof-formal syntax

Sample instance

R: Summary

Info	Description
Subproof	None
Justification	One line
Source	Any (complete) line
Product	Identical to source
Formal syntax	\(\phi \vdash \phi\)

6.2 \(\neg\)E

Formal syntax

Sample instance

\(\neg\)E: Summary

Info	Description
Subproof	None
Justification	One line
Source	Any (complete) line with [\(\neg \neg\) MLO]
Product	Identical to source with \(\neg \neg\) removed
Formal syntax	\(\neg \neg \phi \vdash \phi\)

6.3 \(\vee\)I

Proof-formal syntax

Sample instance

\(\vee\)I: Summary

Info	Description
Subproofs	None
Justification	One line
Source	Any (complete) line
Product	Source with added disjunct; disjunct may be any formula
Formal syntax	\(\phi \vdash \{(\phi \vee \psi), (\psi \vee \phi)\)}

6.4 \(\wedge\)E

Proof-formal syntax

Sample instance

\(\wedge\)E: Summary

Info	Description
Subproofs	None
Justification	One line
Source	Any formula with [\(\wedge\) MLO]
Product	One or the other conjunct of the source
Formal syntax	\((\phi \wedge \psi) \vdash \{ \phi, \psi \}\)