Correspondence of programs and logical proofs

Propositional logic

By known Currey-Howard Correspondence, the inhabited type corresponds to logical truth.

There was an initial thought of using | as disjunction and & as conjunction operator so that the inheritance hierarchy can be transferred to intuitionistic logic. Furthermore, if this is possible, the compiler can resolve properties such as commutativity or idempotence. However, it was seemingly impossible to implement a theorem A => B => A & B, so this plan was taken down.

The following is the list of current encoding of logical operators. They are known to be expressive enough for intuitionistic logic.

Disjunction

Logical disjunction (OR / _ ∨ _) has the following truth-table:

A	B	A ∨ B
0	0	0
0	1	1
1	0	1
1	1	1

This is represented as Either type in Scala program.

Conjunction

Logical conjunction (AND / _ ∧ _) has the following truth-table:

A	B	A ∧ B
0	0	0
0	1	0
1	0	0
1	1	1

This is represented as tuple in Scala program.

Implication

Logical implication (=>) has the following truth-table:

A	B	A => B
0	0	1
0	1	1
1	0	0
1	1	1

This is represented as functional type in Scala program.

Negation

Negation (￢ / NOT) has the following truth-table:

A	NOT A
0	1
1	0

This is represented as _ => Nothing in Scala program.

Double negation elimination

To enable double-negation elimination for classical logic, continuation-passing by exception handling is used.

The following code at ClassicalLogicSystem.scala

def eliminateDoubleNegation[A](doubleNeg: ￢[￢[A]]): A = doubleNeg(a => return a)

is desugared at compile-time into a code equivalent to Scalaz's Forall implementation.

Predicate Logic

// TODO

Set theory

// TODO