First Order Predicate Logic

See also: informal description of first order predicate logic
formal description of predicate logic
and What is Logic?.

This is a semi-formal specification of a simplified version of the predicate logic called Q by Hunter in [Hunter71]. I call the specification semi-formal 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.

syntax semantics proof rules


<term>::=Var <letter>(variable)
|<term>, <term_sequence>
<atomic_formula>::=P<letter>(<term_sequence>)(a predicate applied to a list of terms)
<formula>::=<atomic_formula>(a predicate applied to terms)
|not <formula>(negation)
|<formula> implies <formula>(implication)
|forall <letter>. <formula>(universal quantification)


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):

fpeval i v(P x seqt)equiv(tseval v seqt) memberof (i x)
fpeval i v(not f)equivnot (fpeval i v f)
fpeval i v(f1 implies f2)equiv(fpeval i v f1) implies (fpeval i v f2)
fpeval i v(forall x. f)equivforall y memberof dom(i). fpeval i (lambdaz. if z=x then y else v z) f
Where tseval evaluates a sequence of terms using a valuation v yielding a sequence of elements in the domain of interpretation, and may be defined:
tseval vnil=nil
tseval v((Var x), seqt)=((v x),(tseval v seqt))

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.

proof rules

There are just two inference rules, modus ponens and generalisation, and six axiom schemata, as follows.

Modus Ponens
From two theorems, one of the form:
turnstile A
and the other of the form:
turnstile A implies B
where A and B are arbitrary formulae, the conclusion:
turnstile B
may be derived.

From a theorem of the form:
turnstile A
turnstile forall v. A
for any variable v.

Axiom Schemata
All instances of the following schemata are theorems:
turnstile A implies (B implies A)

turnstile ((A implies (B implies C)) implies ((A implies B) implies (A implies C)))

turnstile ((not A implies not B) implies (B implies A))

turnstile (forall x. A) implies A [t/v] (renaming bound variables as necessary)

turnstile (A impliesforall x. A) (unless x occurs free in A)

turnstile (forall x. A implies B) implies ((forall x. A) implies (forall x. B))

up home © RBJ created 1997/10/18 modified 1997/10/25