8  One-subproof rules

8.1 \(\to\)I

Proof-formal syntax

Sample instance

\(\to\)I: Summary

Info	Description
Subproofs	\([\phi \vdash \psi]\)
Justification	One subproof (as a range)
Source	The subproof
Product	A formula with [\(\to\) MLO], whose antecedent is the assumption of the subproof, and whose consequent is the last line of the subproof
Formal syntax	\([\phi \vdash \psi ]\vdash (\phi \to \psi)\)

8.2 \(\neg\)I

Proof-formal syntax

Sample instance

\(\neg\)I: Summary

Info	Description
Subproofs	\([\phi \vdash \bot]\)
Justification	One subproof (as a range)
Source	The subproof
Product	A formula with [\(\neg\) MLO], the negation of the assumption of the subproof
Formal syntax	\([\phi \vdash \bot] \vdash \neg \phi\)