Propositional logic (or propositional calculus) is, according to Wikipedia, “a branch of mathematical logic concerned with the study of propositions (whether they are true or false) that are formed by other propositions with the use of logical connectives, and how their value depends on the truth value of their components.”

I was introduced to this topic during my third-year of college in a course
titled *Introduction to Formal Logic*. I did not have high expectations going
in (my primary motivation was avoiding more writing-intensive electives), but
it turned out to be one of my favorite courses. One aspect that I found
particularly intriguing about the course was that much of the material seemed
to lend itself nicely to automation—whether it be the construction of
truth tables or even the analysis of proofs. Indeed, there are a number of
existing online tools such as:

The Logic Daemon by Texas A&M University, which “checks proofs and can provide hints for students attempting to construct proofs in a natural deduction system for sentential (propositional) and first-order predicate (quantifier) logic”;

truth table generators by Michael Rieppel, Jamie Wong or Lawrence Turner (among others); and

the various utilities developed by Logictools.

I intend to re-implement (and, where possible, try to improve upon) much of the functionality mentioned above with the goals of gaining a more thorough understanding of the topic and releasing a full-featured, open-source library named Tombstone.js (if you’re wondering why I chose the name “Tombstone,” it was inspired by the typographical symbol).

## Evaluating Well-Formed Formulas

The first step was to implement the ability to evaluate arbitrary well-formed formulas (WFFs). This requires a definition of our vocabulary, which consists of sentence variables ($\{A,B, \dots, Z\}$), parentheses and connectives.

Symbol | Name | Example |
---|---|---|

~ | negation | ~P ("not P") |

& | conjunction | P & Q ("P and Q") |

|| | disjunction | P || Q ("P or Q") |

-> | implication | P -> Q ("If P, then Q") |

<-> | equivalence | P <-> Q ("P if and only if Q") |

A formula is considered well-formed according to the following conditions:

All sentence variables are WFFs.

If $\phi$ is a WFF, then ~$\phi$ is also a WFF.

If $\phi$ and $\psi$ are WFFs, then ($\phi$ & $\psi$), ($\phi$ || $\psi$), ($\phi$ -> $\psi$) and ($\phi$ <-> $\psi$) are WFFs.

Nothing else is a WFF.

From here, I decided to use the shunting-yard algorithm to convert WFFs
to Reverse Polish notation (RPN) for evaluation. In RPN, every operator
follows its operands—for example, `P & Q`

becomes `P Q &`

. This parsing
strategy is more commonly associated with mathematical expressions but it seems
to work well for logic too. You can see the algorithm in action below.

Once in RPN, we can easily evaluate the expression or construct a graphical representation of the formula’s structure (known as a parse tree) as seen below.

## Truth Tables

Now that we can evaluate arbitrary WFFs, generating truth tables is just a matter of evaluating an expression at all of its variable combinations.

## Conclusion

While Tombstone.js is still in its early stages of development, I think this is a promising start. An approximate roadmap for future development is as follows.

Extend truth table generation to allow for copying in HTML, Markdown, $\LaTeX$, reStructuredText or plain text;

add the ability to analyze proofs; and

create a website to showcase Tombstone.js.

I am also considering re-writing the project (that is, the two files it currently contains) in TypeScript. This seems like it would offer a number of interesting features without sacrificing browser support, which is something I would like to keep as high as possible.

Check back for future updates!

## References

- Allen, Colin and Michael Hand.
*Logic Primer*. Cambridge, Mass.: MIT Press, 2001. Print.