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.

Derivative of a Function.

Definition & Notation.

def. Derivative of a Function y = f(x) in point x is limit to which closes the ratio of increment of a function Δy to an increment of a variable Δx, when increment of a variable Δx closes to zero.



if such limit does not exist, then function has no derivative in this point.

derivative of a function y = f(x) we can note as:

, , , , .


Geometrical interpretation.

Geometrically, a derivative of a function is equal to a tanget of angle α, between the tangent line touching the graph of the function in a point x and positive direction of
the OX axis.




Additional notes.

Finding a derivative of a function we can call 'function differentiation'.

From definition we can see that derivative of a function is a quickness of the change of a function f(x), when x changes.


Calculations.

Let's calculate a few of function derivatives, using definiton.

1. y = sin(x).



We've used one of trigonometrical formulas (last one, for the sines difference):



... as well, as that is:



Similarly: (cos x)' = - sin x;

2. y = ax³, where a is any constant..



We've used Newton's Formula:



3. y = xⁿ, n - natural number.



We've used Newton's Formula again.

The same formula for derivative (x^k)' = kx^k-1 we can use for any k.


(an unfinished article, to be continued).

Java 8 Lambda Expressions.

Introduction.

Java version 8 adds a few of succint (terse, short, expressive) notations, compared to previous versions of that programming language.

There's more in Java 8 as well.


Lambda notation.



A comparison,
Java 8 lambda-notation vs. a pre-8 verbose notation.

... a source code file is available for download.


Method references.



A comparison,
Java 8 method-refence notation vs. a pre-8 verbose notation.

... a source code file is available for download.




Values can be applied to a static method references.

... a source code file is available for download.




Method references can be passed around & used in expressions,

Comparator class & BiFunction class are not in the same inheritance tree.

... a source code file is available for download.


Syntax conveniences.

... there are cases where we do not have to use complex instructions, delimited by brackets: { }.

... there are cases where we do not have to use a 'return' keyword, as last instruction's expression value is returned by default anyway.


Notes.

... it seems that most probably there's reflection involved with Java 8 Lambda Calculus.