UP

Propositional Logic

See also: informal and semi-formal descriptions of propositional logic.
informal, semi-formal and formal descriptions of predicate logic.

This is a very simple formal specification of the version of propositional logic called PS by Hunter in [Hunter71]. The specification is written in Standard ML, a strict functional programming language, and can be considered formal since Standard ML does benefit from a formal semantic specification presented as a structured operational semantics, and is therefore a well defined notation. The specification has been run through the Moscow ML implementation of Standard ML, together with a small example proof. The system is a classical propositional logic with two connectives (not and implies) presented as a "Hilbert style" axiom system in which there is just one inference rule, modus ponens, and three axiom schemata.

syntax semantics proof rules Sample Proof Output Transcript

syntax

infix 5 ==>;

datatype formula =
		Pv of string
	|	not of formula
	|	op ==> of (formula * formula);

semantics

An interpretation is a map assigning to each propositional variable one of the two truth values true and false.

The truth value of a formula f under an interpretation i is feval i f, where feval is a (higher order) function taking two successive arguments, an interpretation i and a propositional formula f. feval is defined as follows (function application is shown as juxtaposition, brackets are not necessary for simple arguments): 

fun		feval v (Pv s)		= v s
	|	feval v (not f) 	= if (feval v f)=true
						then false
						else true
	|	feval v (f1 ==> f2)  	= if (feval v f1)=true
						then (feval v f2)
						else false;

feval: (string -> bool) -> formula -> bool;

A formula is tautological (and hence true) if it is true under every interpretation and contradictory (and hence false) if it is false under every interpretation.

proof rules

There is just one inference rule, modus ponens, and three axiom schemata, as follows. 
abstype pthm = |- of formula
with

Modus Ponens
exception MpFail;

fun MP (|- A) (|- (B ==> C)) = if A = B then |- C else |- raise MpFail
|   MP t1 t2 		     = t1;

Axiom Schemata
All instances of the following three schemata are theorems: 
fun PS1 A B	= |- (A ==> (B ==> A));

fun PS2 A B C	= |- ((A ==>(B ==> C)) ==> ((A ==> B) ==>(A ==> C)));

fun PS3 A B	= |- ((not A ==> not B) ==> (B ==> A));

We also need a special function to extract the formula from a theorem: 

fun f (|- A)	= A;

end;

A Small Proof

This is an LCF-like ML version of the proof given by Hunter of p ==> p. 
val f1	= (Pv "p") ==> (Pv "p");  (* this is the goal *)

val L1 	= PS1 (Pv "p") ((Pv "p") ==> (Pv "p"));
val L2 	= PS2 (Pv "p") ((Pv "p") ==> (Pv "p")) (Pv "p");
val L3	= MP L1 L2;
val L4	= PS1 (Pv "p") (Pv "p");
val L5	= MP L4 L3;
f1 = f L5; (* this checks that the result is the same as our goal *)

Output Transcript

This is the output from Moscow ML resulting from processing the above Standard ML script: 
> infix 5 ==>
> datatype formula
  con Pv = fn : string -> formula
  con not = fn : formula -> formula
  con ==> = fn : formula * formula -> formula
> val feval = fn : (string -> bool) -> formula -> bool
> val it = fn : (string -> bool) -> formula -> bool
> abstype pthm
  exn MpFail = MpFail : exn
  val MP = fn : pthm -> pthm -> pthm
  val PS1 = fn : formula -> formula -> pthm
  val PS2 = fn : formula -> formula -> formula -> pthm
  val PS3 = fn : formula -> formula -> pthm
  val f = fn : pthm -> formula
> val f1 = ==>(Pv "p", Pv "p") : formula
> val L1 =  : pthm
> val L2 =  : pthm
> val L3 =  : pthm
> val L4 =  : pthm
> val L5 =  : pthm
> val it = true : bool

If you find all this Standard ML stuff desperately unintelligible, you could try the (even less intelligible!) transcription into C.

up home © RBJ created 1997/10/20 modified 1998/04/08