Rule of Simplification/Proof Rule/Tableau Form

From ProofWiki
Jump to navigation Jump to search

Proof Rule

Let $\phi \land \psi$ be a well-formed formula in a tableau proof whose main connective is the conjunction operator.

The Rule of Simplification is invoked for $\phi \land \psi$ in either of the two forms:


Form 1
Pool:    The pooled assumptions of $\phi \land \psi$      
Formula:    $\phi$      
Description:    Rule of Simplification      
Depends on:    The line containing $\phi \land \psi$      
Abbreviation:    $\operatorname {Simp}_1$ or $\land \EE_1$      


Form 2
Pool:    The pooled assumptions of $\phi \land \psi$      
Formula:    $\psi$      
Description:    Rule of Simplification      
Depends on:    The line containing $\phi \land \psi$      
Abbreviation:    $\operatorname {Simp}_2$ or $\land \EE_2$      


Sources