# 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.

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

 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.

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.