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), 
	!, 
	get_assoc(Atom, V, Answer).
pl_eval(~Phi, V, Answer) :- 
	pl_eval(Phi, V, Temp), 
	pl_eval_not(Temp, Answer).
pl_eval(Phi /\ Psi, V, Answer) :- 
	pl_eval(Phi, V, T1), 
	pl_eval(Psi, V, T2), 
	pl_eval_and(T1, T2, Answer).
pl_eval(Phi \/ Psi, V, Answer) :- 
	pl_eval(Phi, V, T1), 
	pl_eval(Psi, V, T2), 
	pl_eval_or(T1, T2, Answer).
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.