Natural deduction translation into Kotlin

naturalDeduction.kt

@file:Suppress("NonAsciiCharacters")

sealed class Either<out A, out B>
data class Left<out A> constructor(val value: A) : Either<A, Nothing>()
data class Right<out B> constructor(val value: B) : Either<Nothing, B>()

typealias `∧`<φ, ψ> = Pair<φ, ψ>

typealias `∨`<φ, ψ> = Either<φ, ψ>

typealias `→`<φ, ψ> = (φ) -> ψ

typealias `¬`<φ> = (φ) -> Nothing

typealias `↔`<φ, ψ> = `∧`<(φ) -> ψ, (ψ) -> φ>

fun <φ, ψ> `∧I`(x: φ, y: ψ): `∧`<φ, ψ> = x to y

fun <φ, ψ> `∧E-1`(p: `∧`<φ, ψ>): φ = p.first

fun <φ, ψ> `∧E-2`(p: `∧`<φ, ψ>): ψ = p.second

fun <φ, ψ> `→I`(f: (φ) -> ψ): (φ) -> ψ = f

fun <φ, ψ> `→E`(x: φ, f: (φ) -> ψ): ψ = f(x)

fun <φ, ψ> `↔I`(x: (φ) -> ψ, y: (ψ) -> φ): `↔`<φ, ψ> = `∧I`(x, y)

fun <φ, ψ> `↔E-1`(x: `↔`<φ, ψ>): (φ) -> ψ = x.first

fun <φ, ψ> `↔E-2`(x: `↔`<φ, ψ>): (ψ) -> φ = x.second

fun <φ> `¬I`(f: (φ) -> Nothing): (φ) -> Nothing = f

fun <φ> `¬E`(x: φ, y: `¬`<φ>): Nothing = y(x)

fun <φ, ψ> `∨I-1`(x: φ): `∨`<φ, ψ> = Left(x)

fun <φ, ψ> `∨I-2`(x: ψ): `∨`<φ, ψ> = Right(x)

fun <φ, ψ, χ> `∨E`(x: `∨`<φ, ψ>, f: (φ) -> χ, g: (ψ) -> χ): χ =
    when (x) {
        is Left -> f(x.value)
        is Right -> g(x.value)
    }

// Exercise 2.7.2(a)
fun <φ, ψ> `{φ ∨ ψ} ⊢ ψ ∨ φ`(x: `∨`<φ, ψ>): `∨`<ψ, φ> =
    `∨E`(
        x,
        { `①` -> `∨I-2`(`①`) },
        { `②` -> `∨I-1`(`②`) }
    )

fun <φ> `φ ⊢ φ ∧ φ`(x: φ): `∧`<φ, φ> = `∧I`(x, x)

fun <φ, ψ> `⊢ φ ∧ ψ → ψ ∧ φ`(): (`∧`<φ, ψ>) -> `∧`<ψ, φ> =
    `→I` { `①` ->
        `∧I`(
            `∧E-2`(`①`),
            `∧E-1`(`①`)
        )
    }

fun <φ, ψ, χ> `{φ → ψ, ψ → χ} ⊢ φ → χ`(f: (φ) -> ψ, g: (ψ) -> χ): (φ) -> χ =
    `→I` { `①` ->
        `→E`(
            `→E`(
                `①`,
                f
            ),
            g
        )
    }

// Example 2.6.1
fun <φ> `⊢ φ → ¬¬φ`(): (φ) -> `¬`<`¬`<φ>> =
    `→I` { `②`: φ ->
        `¬I` { `①`: `¬`<φ> ->
            `¬E`(
                `②`,
                `①`,
            )
        }
    }

// Example 2.5.1
fun <φ, ψ> `{φ ↔ ψ} ⊢ ψ ↔ φ`(x: `↔`<φ, ψ>): `↔`<ψ, φ> =
    `↔I`(
        `↔E-2`(x),
        `↔E-1`(x),
    )