Proving Modus Ponens and Modus Tollens in Typescript

Proof.ts

export const modus_ponens
  // Proposition
  // Given: A => B and A
  // We can conclude: B
  : <A, B>(f: (a: A) => B, a: A) => B
  = <A, B>(f: (a: A) => B, a: A) => f(a)

// Note, in intuitionistic logic, ~A (a.k.a NOT A), is represented as A => never
export const modus_tollens
  // Proposition:
  // Given: A => B and ~B
  // We can conclude: ~A
  : <A, B>(f: (a: A) => B, not_b: (b: B) => never) => (a: A) => never 

  // Proof
  = <A, B>(f: (a: A) => B, not_b: (b: B) => never) => (a: A) => not_b(f(a))