Classical Propositional Logic in Elixir

  • Elixir is a programming language.
  • José Valim is Brazilian.
  • Socrates is mortal.
  • p represents “Elixir is a programming language.”
  • q represents “José Valim is Brazilian.”
  • r represents “Socrates is mortal.”
  • ¬ (negation, not) is an unary connective.
  • ∧ (conjunction, and), → (implication, implies, if..then) and ∨ (disjunction, or) are binary connectives.
  • P, a set of symbols to represent propositions. Each symbol is called an atomic formula or atom.
  • a set of connectives.
  • 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).

Representing Formulas in Elixir

  • p is represented as :p
  • q is represented as :q
  • atoms = MapSet.new([:p, :q])
  • ¬ is :not
  • ∧ is :and
  • → is :implies
  • ∨ is :or
  • ¬p as [:not, :p]
  • (p∧q) as [:p, :and, :q]
  • (p∨q) as [:p, :or, :q]
  • (p→q) as [:p, :implies, :q]
[:not, [ [ [:p, :implies, :q], :and, :r], :or, :s]]

Representing a Logical System in Elixir

  • 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}
}

Veryfing if a list represents a formula in a language

is_formula(:p, lp)
true
is_formula([:not, :q], lp)
true
is_formula([:not, :s], lp)
false
  • 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.

--

--

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

Love podcasts or audiobooks? Learn on the go with our new app.

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

Adolfo Neto

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