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.
- José Valim is Brazilian.
- Socrates is mortal.
We use symbolic logic and associate each proposition to a symbol. So, we could say that:
- p represents “Elixir is a programming language.”
- q represents “José Valim is Brazilian.”
- r represents “Socrates is mortal.”
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.
- ∧ (conjunction, and), → (implication, implies, if..then) and ∨ (disjunction, or) are binary connectives.
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.
- a set of connectives.
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.
- If x is in L(P), ¬x is in L(P).
- If x and y are in L(P), then (x∧y), (x→y) and (x∨y) are in L(P).
- Everything else is not in in L(P).
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
- q is represented as :q
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
- ∧ is :and
- → is :implies
- ∨ is :or
A non-atomic (complex) formula is represented as a list:
- ¬p as [:not, :p]
- (p∧q) as [:p, :and, :q]
- (p∨q) as [:p, :or, :q]
- (p→q) as [:p, :implies, :q]
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
- a set of connectives. Each connective is a symbol-arity pair in Map.
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
- the second for formulas where the main connective is unary
- the second for formulas where the main connective is binary
- the last to return that a formula is not well formed.
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?
