# Propositional Logic

Propositional logic deals with the connectives `¬` (negation), `∧` (conjunction), `∨` (disjunction), `⇒` (implication), and `⇔` (equivalence).

## Syntax

The language of propositional logic contains the following symbols:

• infinitely many variables,
• the connectives `¬`, `∧`, `∨`, `⇒`, `⇔`, and
• parentheses `(`, `)`.

The set of propositional logic formulas, F, is the smallest one satisfying

• for all `X` such that `X` is a variable then `X` ∈ F,
• for all `φ` and `ψ`, if `φ` and `ψ` ∈ F, then `¬φ` ∈ F, `φ∧ψ` ∈ F, `φ∨ψ` ∈ F, `φ⇒ψ` ∈ F, and `φ⇔ψ` ∈ F,
• for all `φ` such that `φ` ∈ F then `(φ)` ∈ F.

We can also use the constants `t`, or `⊤`, for true, and `f`, or `⊥`, for false and have these as propositional formulas but not all authors use them.

## Semantics

The meaning of a connective is given by its truth table. These truth tables in combination with a truth assignment allow us to assign a truth value (`t` or `f`) to a formula.

A truth assignment, `γ` satisfies a formula `φ`, written `γ⊨φ`, if `φ` evaluates to `t` using `γ`. A formula `φ` is satisfiable if there is some truth assignment `γ` such that `γ⊨φ`.

A truth assignment, `γ` satisfies a set of formulas `Γ`, written `γ⊨Γ`, if `γ` satisfies every member of `Γ`.

A formula `φ` is logically valid, written `⊨φ`, if `φ` is satisfied by every truth assignment.

A formula `φ` is a logical consequence of the set of formulas `Γ`, written `Γ⊨φ`, if `φ` is satisfied by every truth assignment that satisfies `Γ`.

The formulas `φ` and `ψ` are equivalent, written `φ≡ψ` if they are satisfied by the same assignments.

### Implementation

The following is a Prolog implementation of the semantics of propositional logic. The code is specific to Barry's Prolog but should work on other Prolog implementations which provide association lists.

```	```
:- ensure_loaded(runtime(assoc)).    % A library that supplies get_assoc/3

%%%
%%% The syntax of propositional logic
%%%
%%% I use the built in parser and change/augment the Prolog operators to handle
%%% propositional logic.
%%%
:-op(200, fy, ~).                   % Negation
:-op(0, yfx, (/\)).
:-op(400, xfy, (/\)).               % Conjunction (not ISO associativity which is yfx)
:-op(0, yfx, (\/)).
:-op(500, xfy, (\/)).               % Disjunction (not ISO associativity which is yfx)
:-op(600, xfy, ==>).                % Implication
:-op(700, xfy, <=>).                % Equivalence

%%%
%%% pl_eval_not(P, NotP).
%%%
%%% The samantics of the propositional logic negation connective.
%%%
pl_eval_not(true, false).
pl_eval_not(false, true).

%%%
%%% pl_eval_and(C1, C2, Conjunction)
%%%
%%% The semantics of the propositional logic conjunction.
%%%
pl_eval_and(true, true, X) :- !, X = true.
pl_eval_and(_, _, false).

%%%
%%% pl_eval_or(C1, C2, Disjunction)
%%%
%%% The semantics of the propositional logic disjunction.
%%%
pl_eval_or(false, false, X) :- !, X = false.
pl_eval_or(_, _, true).

%%%
%%% pl_eval(F, V, Answer)
%%%
%%% Using the valuation (truth assignment) V we evaluate the formula F to Answer (true, false).
%%% This is the mathematical definition of the semantics of propositional logic.
%%% An association list is used to implement the truth assignment.
%%%
%%% assoc_to_list(V, [p-true, q-false, r-true]), pl_eval((p /\ q ==> q \/ r), V, Answer).
%%% assoc_to_list(V, [p-true, q-true, r-false]), pl_eval((p /\ q ==> q /\ r), V, Answer).
%%%
pl_eval(false, _, false).
pl_eval(true, _, true).
pl_eval(Atom, V, Answer) :-
atom(Atom),
!,
pl_eval(~Phi, V, Answer) :-
pl_eval(Phi, V, Temp),
pl_eval(Phi /\ Psi, V, Answer) :-
pl_eval(Phi, V, T1),
pl_eval(Psi, V, T2),
pl_eval(Phi \/ Psi, V, Answer) :-
pl_eval(Phi, V, T1),
pl_eval(Psi, V, T2),
pl_eval(Phi ==> Psi, V, Answer) :-
pl_eval(~Phi \/ Psi, V, Answer).
pl_eval(Phi <=> Psi, V, true) :-
pl_eval(Phi, V, T1),
pl_eval(Psi, V, T2),
T1 == T2,
!.
pl_eval(_ <=> _, _, false).
```
```

## References

Doets, Kees. From Logic to Logic Programming. MIT Press, 1994.
Harrison, John. Handbook of Practical Logic and Automated Reasoning. Cambridge, 2009.