Predicate Logic Basics.

Introduction.

This article joins the 'functional programming paradigm' with 'programming in logic', an another important & very well known programming paradigm.

We'll be using both a little of the 'Sets Theory', as well as 'Mathematical Analysis' & 'Logic'.


Predicates.

In mathematics, a predicate is commonly understood to be a Boolean-valued function P: X → {true, false}, called the predicate on X.


Predicate Language Syntax.

Logical formulas of the 'Predicate Calculus' are built from symbols, set of these symbols is called 'alphabet'.

To fully specify 'alphabet' we would need to include all of the symbols that belong to it.

For simplicity, we'll provide a definition that will specify only types of symbols, that might be included in 'alphabet'.


def. 1. A 'predicate calculus alphabet' consists of following symbols:
- constants,
- variables,
- function symbols,
- predicate symbols,
- logical functors,
- parentheses.


def. 2. For a given 'predicate calculus alphabet' the 'terms set' is defined as follows:
- each of constants is a 'term',
- each of variables is a 'term',
- if 'f' is a 'm-argument function symbol' and t₁, t₂, ... , t_m are terms,
    then f(t₁, t₂, ... , t_m) is a 'term'.


The 'terms' in the 'predicate calculus' are arguments of the 'predicate symbols'.

Predicate symbols assign each of the 'term argument' a boolean value from a set of {true, false}.

Assigning a 'predicate symbol' to a 'term argument' gives in a result the simplest of 'logical formulas', called also: 'atomic formula'.


def. 3. For each m-argument 'predicate symbol': 'R', if t₁, t₂, ... , t_m are 'terms',
    then R(t₁, t₂, ... , t_m) is an 'atomic formula'.


The 'complex formulas' are created by joining 'atomic formulas' using 'logical functors' and parentheses. Possibilities of creating 'complex formulas' are specified by the following definition.

def. 4. For a given 'alphabet', the 'predicate calculus formulas set' is defined as follows:
- each of the 'atomic formula' is a 'formula',
- for any 'formula' α, the (α) and ¬α are 'formulas',
- for any 'formulas' α and β, the α∧β, α∨β, α→β, α↔β are 'formulas',
- for any 'formula' α with a variable v, there are 'formulas': (∀_v)α and (∃_v)α.


Predicate Language Semantics.

Semantics for a 'predicate calculus' are defined by specifying a 'model', in which 'formulas' are interpreted.


def. 5. A 'model' is a pair <X, ι>, where X is a non-empty set called a 'domain' and ι is 'interpretation function' which:
- assigns for each of constants a certain 'domain' element,
- assigns for each of 'm-argument function symbol' a certain mapping from X^m on X,
- assigns for each of 'm-argument predicate symbol' a certain mapping from X^m on {true, false}.


In this context, predicates are treated as the 'relation names', for whose an 'interpretation function' assigns the 'relations on domain'.


def. 6. A 'valuation' of variables for a domain X is any function with a domain containing all of variables, with values in a set X.


For a given model and variables valuation, formulas can be valuated to specify their 'boolean value'.

We'll give only a definition for 'atomic formulas', for the 'complex formulas' can be specified using the known interpretation of the 'logical functors'.


def. 7. For a model <X,ι> and a variable valuation v, the values of the terms are specified as follows:
- for any constant x: V^v_{X, ι}(v) = ι(x);
- for any variable v: V^v_{X, ι}(v) = v(v);
- for any m-argument function symbol f and any terms t₁, ... , t_m:
     V^v_{X, ι}(f(t₁, ... , t_m)) = ι(v)(V^v_{X, ι}(t₁), ... , V^v_{X, ι}(t_m)).

Let's notice that a value of ι(v) is a function, with a value in a 'functions space', as defined in def. 5.

Then we interpret ι(v)(V^v_{X, ι}(t₁), ... , V^v_{X, ι}(t_m)) as a complex function composition.


def. 8. For a model <X,ι> and a variable valuation v,
    the value of an 'atomic formula' R(t₁, ... , t_m), where:
      R is an m-argument predicate symbol,
      t₁, t₂, ... , t_m are terms,
        is specified as follows:
          V^v_{X, ι}(R(t₁, ... , t_m)) = ι(R)(V^v_{X, ι}(t₁), ... , V^v_{X, ι}(t_m)).

Again a value of ι(v) is a function, we have a complex function composition here as well.


Formulas' logical value are basis to specify: satisfiedness, satisfiability & truthfulness of the boolean formulas.


def. 9. Any formula α is satisfied in a model with a variable valuation v, when:
    V^v_{X, ι}(α) = 'true'.

def. 10. Any formula α is satisfiable, if there exists a model and a variable valuation, for which α is satisfied.

def. 11. Any formula α is true, when for any model and a variable valuation:
    α is satisfied.


Symetrically we define falsifiedness, falisfiability & falseness of the boolean formulas.

The 'falseness' property can also be defined using formulas' sets.

def. 12. Formulas set F_S is false (self-contradictory), when conjunction of all formulas from this set F_S is not satisfiable.


Entailment & Inference in a Predicate Calculus.

There are two types of consequences, as far as the 'entailment & inference in a predicate calculus' reaches:
- semantic consequence (logical consequence, entailment),
- syntactic consequence (inference).


def. 13. Formula α is a semantic consequence of a formulas set { β₁, β₂, ... , β_m }, if for all models and variable valuations, for which formula β₁ ∧ β₂ ∧ ... ∧ β_m is satisfied, formula α is also satisfied. We can note it as: { β₁, β₂, ... , β_m } ⊧ α.


Syntactic consequence is defined, by assuming a certain inference system, consisting of a logical axioms set & of a inference rules set. Axioms are logical formulas, rules specify a way of deriving formulas from different formulas.


An inference rule noted as follows:



Means that based on formulas: β₁, β₂, ... , β_m (that are premises), we can infer in a single step the formula α (that is a conclusion).


def. 14. A proof of a formula α based on a formulas set S is:
    a serie of formulas:
      β₁, β₂, ... , β_m = α,
        in which for every i = 1, 2, ..., m :
          a formula β_i is:
            - an axiom,
            - or a S-set element,
            - or a result of using a certain inference rule on rules preceding it in a proof.


deft. 15. A formula α is a syntactic consequence of a formulas set S, in a certain inference system, if in this a system exists a proof of this formula based on S. We can note it as: S ⊦ α.


def. 16. Inference system is correct, if for any formulas set S and an α formula, a syntactic consequence S ⊦ α entails semantic consequence S ⊧ α.


def. 17. Inference system is complete, if for any formulas set S and an α formula, a semantic consequence S ⊧ α entails syntactic consequence S ⊦ α.


There are many different (assuming different axioms & inference rules) correct & complete inference systems for the predicate calculus.