Skip to content

Instantly share code, notes, and snippets.

@wongjiahau

wongjiahau/Proof.ts

Created May 3, 2021 13:40
Download ZIP

Revisions

  1. wongjiahau created this gist May 3, 2021.
    16 changes: 16 additions & 0 deletions Proof.ts
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,16 @@
    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))