See also: informal description of propositional logic
formal description of propositional logic
and What is Logic?.
This is a very simple semiformal specification of the version of propositional logic called PS by Hunter in [Hunter71]. I call the specification semiformal because I am not supplying a definition of the metalanguage in which it is written.  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. 

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 val i f, where val is a (higher order) function taking two successive arguments, an interpretation i and a propositional formula f. val is defined as follows (function application is shown as juxtaposition, brackets are not necessary for simple arguments):

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.
Modus Ponens
Axiom Schemata
