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.|
|Sample Proof||Output Transcript|
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
We also need a special function to extract the formula from a theorem:
fun f (|- A) = A; end;
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 *)
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 =
|If you find all this Standard ML stuff desperately unintelligible, you could try the (even less intelligible!) transcription into C.|