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.

This article is written by Hongwei Xi.

Effective ATS: Encoding Propositional Logic