From logic and math to code. For dummies. Part II: Higher-order logic

In the previous part, we talked about formal and informal systems and theirs part in software development. We found out that all logics start from basic Aristotle rules. But obviously, all our thoughts and speech cannot be described only with those rules.

Propositional calculus

In daily life our narrative speech consists of utterances — small units of speech, which can be treated as truth value. Let say we have two simple proposals:

• It’s cloudy (a)
• It’s raining (b)

Then we can say, that it’s raining when it’s cloudy:

a → b

This notation means implication. It’s close to if … else statement, apart from being a new proposal it must be a truth value. So in Boolean algebra implication corresponds to a function which takes arguments A and B and returns a truth value. And it returns false only when A is true, but B is false, which means in our context, that it’s cloudy, but not raining.

Could it be? Of course!
It means that our implication is false and to make it truly we should apply negation:

!(a → b)

or ¬(a → b) in math notation.

Now we have the complex proposal out of two simple ones, which gives us new information.
Besides that, propositional calculus has operators of conjunction, disjunction, exclusive OR and equality which you, for sure, familiar with.

But the problem of propositional calculus is in its limitation and simplification. It doesn’t know about sets, considering just atomic values. But our brain very actively uses deduction and induction to simplify the surrounding world. And it’s not possible without sets, categories and abstractions.

First-order logic

First order logic extends propositional logic and besides previously mentioned operators introduces quantifiers. Quantifiers are operators which make possible to operate over sets. There are two of them:

• Universal quantification ∀
• Existential quantification ∃

So now we can apply a quantifier to our weather proposal to get a more detailed result:

∃ a ∈ A a→b

Which can be read as: there are some clouds a from set of all clouds A, which always cause raining b.

And universal quantification could say that all of a belongs to A.

As you can see, such kind of statements are already closer to real life, than some atomic values.

Higher-order logic

And again we are limited because first-order logic can apply quantifiers only to atomic values. But in real life our complex definitions are based on another ones and those are respectively on another ones. Sometimes such a chain can last for a very long time until we get a concept that we cannot really explain. So higher-order logic extends first-order logic making it possible to apply quantifiers not only to atomic values but to sets and predicates as well.

By the way, what the heck is a predicate?

When we considered implication, we discovered, that it’s basically a function, which takes two arguments and returns truth values. So this is exactly what predicate does. It takes any amount of arguments, performs some logic and returns a truth value. Sometimes predicates are also called formulas.

Obviously, in order to understand whether our statement is true we have to evaluate the predicate, substituting arguments to our function.

And exactly at this moment we are finally getting pretty close to really exciting things:

• Curry–Howard correspondence
• Lambda calculus
• Functional programming languages (Haskell, ML)
• Dependent types
• Proof assistants (Coq, Agda, Idris)

But that will be discussed in the next part.