Classical Propositional Logic in Elixir

I am a professor and I teach Introduction to Logic for Computing. One of the subjects I teach is Classical Propositional Logic. I use a Brazilian book as my main reference but this book is also quite good.

In Classical Propositional Logic there are two truth-values: true and false. A proposition is a declarative sentence which can be either true or false.

Examples of propositions are:

  • Elixir is a programming language.

We use symbolic logic and associate each proposition to a symbol. So, we could say that:

  • p represents “Elixir is a programming language.”

And from now on we forget about real sentences and only work with symbols.

We can construct more elaborate sentences using logical connectives. Each connective has an arity:

  • ¬ (negation, not) is an unary connective.

To the define a language for writing Classical Propositional Logic well-formed formulas, we need:

  • P, a set of symbols to represent propositions. Each symbol is called an atomic formula or atom.

In the example above P = {p, q, r}. P can be any non-empty countable set such as P={p1, p2, p3, …}.

Given a P, L(P) is a set of well-formed formulas where:

  • For every x in P, x is a well-formed formula.

Example:

Given P = {p, q, r},

L(P) = {p, q, r, ¬p, ¬q, ¬r, ¬¬p, ¬¬q, ¬¬r, …, (p∧q), …, (p∧(q∨¬¬r)), …}

Representing Formulas in Elixir

So, my initial idea for representing well-formed formulas, which from now on I will call only formulas, in Elixir is:

An atomic formula is represented by an atom:

  • p is represented as :p

The set of propositions is represented as a MapSet:

  • atoms = MapSet.new([:p, :q])

Connectives are represented by Elixir atoms of their names:

  • ¬ is :not

A non-atomic (complex) formula is represented as a list:

  • ¬p as [:not, :p]

A formula such as ¬(((p→q)∧r)∨s) will be represented as:

[:not, [ [ [:p, :implies, :q], :and, :r], :or, :s]]

Representing a Logical System in Elixir

So the next step is to represent a Logical System in Elixir. A Logical System for Classical Propositional Logic consists of:

  • a set of propositions
lp =
%{
atoms: MapSet.new([:p, :q, :r]),
connectives: %{not: 1, and: 2, or: 2,implies: 2}
}

This way we can obtain the arity of a connective with

lp[connectives][connective]

Veryfing if a list represents a formula in a language

I want to write a function such that:

is_formula(:p, lp)
true
is_formula([:not, :q], lp)
true
is_formula([:not, :s], lp)
false

That is, that answers true if and only if the first argument is a well-formed formula in the language defined by the second argument.

Easy? Let’s see.

I wrote the is_formula function with four clauses:

  • the first for atomic formulas

I also wrote a helper function called arity that returns the arity of a connective in a logical system.

Below some tests for the code.

My plan is to build a Tableau SAT Solver for Classical Propositional Logic. using strategies.

I know the code above is far from perfect. What should I change?

--

--

Associate Professor at UTFPR. Interested in programming (Elixir), logic and Deep Work.

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
Adolfo Neto

Associate Professor at UTFPR. Interested in programming (Elixir), logic and Deep Work.