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__.

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

absprop PTRUE // for true absprop PFALSE // for falseThere 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.
Given a proposition A, we use PNEG(A) for the negation of A:

absprop PNEG(A: prop) // for negation propdef ~(A: prop) = PNEG(A) // shorthandFor 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): PFALSEEssentially, 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)) //

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) // shorthandFor 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)) //

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]

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

// 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

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))
)
)
)
```

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 can be encoded as follows:

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

The law of excluded middle can be encoded as follows:

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

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.
This article is written by Hongwei Xi.