Substitutivity of Implication D sub Let 91, W/k be a list including all distinct individual variables which occur free in m or N If M is positive in A, then 9…(M>N)(AAx 2. If M is negative in a, the en Hyr …9(M>N)(ANA 3. If M is positive in a and hMoN, then A→AN 4. If M is negative in a and hmon, then A→A Logic in Computer Science - p 6/27Substitutivity of Implication ⊃ Sub Let y1, · · · , yk be a list including all distinct individual variables which occur free in M or N. 1. If M is positive in A, then ` ∀y1 · · · yk(M ⊃ N) ⊃ (A ⊃ AMN ) 2. If M is negative in A, then ` ∀y1 · · · yk(M ⊃ N) ⊃ (AMN ⊃ A) 3. If M is positive in A and ` M ⊃ N, then ` A ⊃ AMN 4. If M is negative in A and ` M ⊃ N, then ` AMN ⊃ A Logic in Computer Science – p.6/27