See also: informal description of first order predicate logic
formal description of predicate logic
and What is Logic?.
This is a semiformal specification of a simplified version of the predicate logic called Q 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 predicate logic with two propositional connectives (not and implies) presented as a "Hilbert style" axiom system in which there are two inference rules (modus ponens and generalisation), and four axiom schemata. 

An interpretation consists of a set of elements, which is called the domain of the interpretation, together with an assignment to each predicate letter of a set of finite sequences of elements from the domain.
A valuation is an assignment to each variable of an element in the domain of interpretation.
The truth value of a formula f under an interpretation i and valuation v is fpeval i v f, where fpeval is a (higher order) function taking three successive arguments, and is defined as follows (function application is shown as juxtaposition, brackets are not necessary for simple arguments):

A formula is valid (and hence true) if it is true under every interpretation/valuation combination and contradictory (and hence false) if it is false under every interpretation/valuation. 
There are just two inference rules, modus ponens and generalisation, and six axiom schemata, as follows.
Modus Ponens
Generalisation
Axiom Schemata
