# 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)trueis_formula([:not, :q], lp)trueis_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?

--

--