# Effective ATS: Encoding Propositional Logic

In this article, I present a direct encoding of propositional logic in ATS, illustrating through examples a simple form of formalized theorem-proving. For the entirety of the code used in this presentation, please see the files prop-logic.sats and prop-logic.dats.

## Encoding Truth Values

The truth values are encoded as abstract props PTRUE and PFALSE:

```absprop PTRUE // for true
absprop PFALSE // for false
```
There is one introduction rule but no elimination rule for true:
```praxi true_intr((*void*)): PTRUE
```
There is no introduction rule but one elimination rule for false:
```praxi false_elim{A:prop}(pf: PFALSE): A
```
Clearly, the rule false_elim states that any proposition can be derived from a proof of false.

## Encoding Negation

Given a proposition A, we use PNEG(A) for the negation of A:

```absprop PNEG(A: prop) // for negation
propdef ~(A: prop) = PNEG(A) // shorthand
```
For convenience, ~A can be written for PNEG(A). There is one introduction rule and one elimination rule for negation:
```praxi neg_intr{A:prop}(fpf: A -> PFALSE): ~A
praxi neg_elim{A:prop}(pf1: ~A, pf2: A): PFALSE
```
Essentially, neg_intr means that ~A is derivable if any proof of A can be used to build a proof of false. As for elimination of negation, neg_elim states that a proof of false can be built on the top of a proof of ~A and a proof of A.

By combining neg_elim and false_elim, we obtain the following rule stating that any proposition B can be derived from a proof of A and a proof of ~A:

```//
prfn
neg_elim2
{A:prop}{B:prop}
(pf1: A, pf2: ~A): B = false_elim(neg_elim(pf1, pf2))
//
```

## Encoding Conjunction

Given two propositions A and B, we use PCONJ(A, B) for the conjunction of A and B:

```absprop
PCONJ(A: prop, B: prop)
propdef &&(A: prop, B: prop) = PCONJ(A, B) // shorthand
```
For convenience, A && B can be written for PCONJ(A, B). There are one introduction rule and two elimination rules associated with conjunction:
```//
praxi
conj_intr
{A,B:prop} : (A, B) -> A && B
//
praxi
conj_elim_l{A,B:prop} : (A && B) -> A
praxi
conj_elim_r{A,B:prop} : (A && B) -> B
//
```
As an example, a proof is given below showing that conjunction is commutative:
```//
prfn
conj_commute
{A,B:prop}(pf: A && B): B && A =
conj_intr(conj_elim_r(pf), conj_elim_l(pf))
//
```

## Encoding Disjunction

Given two propositions A and B, we use PDISJ(A, B) for the disjunction of A and B:

```dataprop
PDISJ(A: prop, B: prop) =
| disj_intr_l(A, B) of (A)
| disj_intr_r(A, B) of (B)
//
propdef ||(A: prop, B: prop) = PDISJ(A, B)
//
```
For convenience, A || B can be written for PDISJ(A, B). As an example, a proof is given below showing that disjunction is commutative:
```//
prfn
disj_commute
{A,B:prop}(pf0: A || B): B || A =
case+ pf0 of
| disj_intr_l(pf0_l) => disj_intr_r(pf0_l)
| disj_intr_r(pf0_r) => disj_intr_l(pf0_r)
//
```
The two constructors disj_intr_l and disj_intr_r associated with PDISJ correspond to the two introduction rules associated with disjunction, and the following function disj_elim encodes the elimination rule associated with disjunction:
```//
prfn
disj_elim{A,B:prop}{C:prop}
(pf0: A || B, fpf1: A -> C, fpf2: B -> C): C =
case+ pf0 of
| disj_intr_l(pf0_l) => fpf1(pf0_l)
| disj_intr_r(pf0_r) => fpf2(pf0_r)
//
```
As another example, the following code implements a proof function showing that conjunction can be distributed over disjunction:
```prfn
conj_disj_distribute
{A,B,C:prop}
(
pf0: A && (B || C)
) : (A && B) || (A && C) = let
//
val pf0_l = conj_elim_l(pf0)
val pf0_r = conj_elim_r(pf0)
//
in
//
case+ pf0_r of
| disj_intr_l(pf0_rl) =>
disj_intr_l(conj_intr(pf0_l, pf0_rl))
// end of [disj_intr_l]
| disj_intr_r(pf0_rr) =>
disj_intr_r(conj_intr(pf0_l, pf0_rr))
// end of [disj_intr_r]
//
end // end of [conj_disj_distribute]
```

## Encoding Implication

Given two propositions A and B, we use PIMPL(A, B) for the implication of B from A:

```//
absprop
PIMPL(A: prop, B: prop)
//
infixr (->) ->>
propdef ->>(A: prop, B: prop) = PIMPL(A, B)
//
```
For convenience, A ->> B can be written for PIMPL(A, B). There is one introduction rule and one elimination rule for implication:
```//
praxi
impl_intr{A,B:prop}(pf: A -> B): A ->> B
//
praxi
impl_elim{A,B:prop}(pf1: A ->> B, pf2: A): B
//
```
Essentially, A implying B is interpreted as a function of the type A -> B.

As an example, a proof (A ->> (B ->> C)) ->> ((A ->> B) ->> (A ->> C)) is given as follows:

```prfn
Subst{A,B,C:prop}
(
// argless
) : (A ->> (B ->> C)) ->> ((A ->> B) ->> (A ->> C)) =
impl_intr(
lam pf1 =>
impl_intr(
lam pf2 =>
impl_intr(
lam pf3 =>
impl_elim(impl_elim(pf1, pf3), impl_elim(pf2, pf3))
)
)
)
```

## Encoding Equivalence

Given two propositions A and B, we use PEQUIV(A, B) for the (propositional) equivalence between A and B:

```absprop
PEQUIV(A: prop, B: prop)
propdef == (A: prop, B: prop) = PEQUIV(A, B)
```
For convenience, A == B can be written for PEQUIV(A, B). There is one introduction rule and two elimination rules for propositional equivalence:
```//
praxi
equiv_intr
{A,B:prop}(A ->> B, B ->> A): A == B
//
praxi
equiv_elim_l{A,B:prop}(pf: A == B): A ->> B
praxi
equiv_elim_r{A,B:prop}(pf: A == B): B ->> A
//
```

## The Law of Double Negation

The law of double negation can be encoded as follows:

```praxi LDN{A:prop}(~(~A)): A
```

## The Law of Excluded Middle

The law of excluded middle can be encoded as follows:

```praxi LEM{A:prop}((*void*)): A || ~A
```

## Peirce's Law

Peirce's law can be encoded as follows:

```praxi
Peirce{P,Q:prop}((*void*)): ((P ->> Q) ->> P) ->> P
```
This law of Peirce is equivalent to LEM, and it can be seen as a variant of LEM expressed only in terms of the implicative logic connective.