Knowledge Representation and Reasoning: Basics of Logics

This page gives a quick and concise reminder of the important definitions that are reused all the time in this course.

Logics

In this course, we use an abstract definition of a logic. There are many logics (propositional logic and first order logic are two examples seen in the first year introduction to logic, but there are many more). A large family of logics can be defined following the same pattern. I define here the mathematical structure of a logic, that I will instantiate in different ways.

Formal definition

Logic

A logic L is a quadruple (Sym_L, For_L, Int_L, ⊨_L) where:

Sym_L is a set whose members are called the symbols of the logic L;
For_L is a set of finite sequences of symbols (that is, a subset of Sym_L ⋃ Sym_L² ⋃ Sym_L³ ⋃ … ⋃ Sym_Lⁿ ⋃ …), whose elements are called the formulas of the logic L;
Int_L is a set of algebraic structures whose members are called the interpretations of the logic L;
⊨_L ⊆ Int_L × For_L, that is, a binary relation between interpretations and formulas. This is called the satisfaction relation.

Syntax: The syntax of a logic L = (Sym_L, For_L, Int_L, ⊨_L) is the pair (Sym_L, For_L).

Semantics: The semantics of a logic L = (Sym_L, For_L, Int_L, ⊨_L) is the pair (Int_L, ⊨_L).

Notes regarding the definition

In this definition, the set of symbols contains the signs used to write logical formulas, but a symbol in the logic may correspond to multiple signs in our writing system. For instance, in propositional logic, a proposition is a single symbol but it is common to use a word or phrase to denote a proposition. For instance, It_Is_Raining may be a proposition.

The set of formulas is typically defined using a grammar. Sometimes, arbitrary sequences of symbols are called “formulas”, while the ones that are meaningful for the logic are called “well-formed formulas”. We will never consider arbitrary sequences of symbols, so for us, only well-formed formulas are formulas.

The set of interpretations often contains several parts, usually with one non-empty set called the universe or domain of interpretation, and usually a function that maps some distinguished symbols to some parts of the universe of interpretation. For instance, in first order logic, an interpretation contains such a set and there is a function that maps constants to elements of the universe and maps n-ary predicates to sets of n-tuples of elements of the universe.

The satisfaction relation relates a certain arrangement of the universe (an interpretation) to the formulas that are true in this arrangement of the universe.

Concepts common to all logics

In these definitions, we fix a logic L = (Sym_L, For_L, Int_L, ⊨_L). Note that, for any set S, we write 2^S to denote the powerset of S.

Theory: A theory is a set of formulas, that is, a subset of For_L, or an element of 2^For_L.

Note that the empty set is a theory, and a theory may have an infinite size. Of course, in practice (especially in a computer), we only deal with finite theories.

Satisfaction: An interpretation I ∈ Int_L satisfies a theory T ⊆ For_L if and only if for all formulas φ ∈ T, (I, φ) ∈ ⊨_L. In this case, we write T ⊨_L φ.

Model: A model of a theory T ⊆ For_L is an interpretation that satisfies T.

Satisfiability / consistency: A formula φ is satisfiable if there exists a model of {φ}. A theory T is consistent if there exists a model of T.

Validity / tautology: A formula φ is valid (or is a tautology) if every interpretation I ∈ Int_L satisfies it.

Unsatisfiability / inconsistency / contradiction: A formula φ is unsatisfiable (or is a contradiction) if no interpretation satisfies it. A theory T is inconsistent if it does not have a model.

Entailment: A theory T ⊆ For_L entails a formulas φ if and only if all models of T satisfy {φ}. In this case, we write T ⊨_L φ.

The entailment relation is extremely important. While it is common that interpretations are mathematical structures that cannot be represented in a computer (they may be infinite, or contain things that do not have a digital representation, such as the set of all real numbers), computers can store and manipulate formulas, and logically derive new formulas from given formulas.

Note that we use the same symbol for the satisfaction relation and the entailment relation. This is a common practice in knowledge representation because in practice, we almost exclusively deal with the notion of entailment, where T ⊨_L φ means that T is a theory and φ is a formula.

Deductive systems

Concepts of deductive systems

Deductive systems is what formalises the notion of logical deductions by proofs. They are key to the automation of reasoning by computers. Again, we assume a logic L having syntax (Sym_L, For_L).

Deductive system

A deductive system (also called a formal system) for L is a pair D = (A, R) such that:

A is a set of formulas in For_L, called the axioms of D;
R is a set of pairs in 2^For_L × For_L. The elements of R are called the inference rules, or simply the rules of D.

The idea of a deductive system is that every axiom in A is assumed to be a true formula (one that does not need proof to be accepted as true), while rules (P,κ) ∈ R say that if we know, or can prove, the formulas in P, then we can consider that the formula κ is true as well (that is, it is proved by application of the rule). Now we fix a deductive system D = (A, R) and give some more definitions:

Premise and conclusion: If r = (P, κ) is a rule in R, then we say that P is the premise of r and κ is the conclusion of r.

The premise of a rule is usually finite, but it is possible to build concrete deductive systems with rules having infinite premises. However, it will never be the case in this course. To simplify further definitions, we will write P(r) and κ(r) to denote the premise and conclusion, respectively, of a rule r.

Derivation: A formula κ derives from a theory T in the deductive system D if there is a rule r ∈ R such that P(r) ⊆ T ⋃ A. In this case, we write T ⊢^r κ

Proof

Let T be a theory and φ a formula. A proof of φ from T in deductive system D is a sequence (r₁, …, r_n) ∈ Rⁿ, with n ∈ ℕ such that:

by convention, we assume that if n = 0, it means that φ ∈ T;
otherwise, T ⊢^r₁ κ(r₁), and for all i ∈ {2, …, n}, T ⋃ {κ(r₁), …, κ(r_i−1)} ⊢^r_i κ(r_i), and κ(r_n) = φ.

When a proof of φ from T exists, we write T ⊢_D φ.

A proof is essentially a sequence of derivations that starts from the theory T, applies rules one by one while accumulating the derived formulas.

Note that so far, the notion of a deductive system completely ignores the semantics of the logic L, which means that some axioms, rules, derivations, or proofs can be completely meaningless in some deductive systems. For instance, it is possible that a deductive system for propositional logic contain the axiom P ∧ ¬P, where P is a proposition. We therefore introduce concepts that tie together deductive systems and the semantics of the logic.

Properties of deductive systems

Let L = (Sym_L, For_L, Int_L, ⊨_L) be a logic and D = (A, R) a deductive-system for L.

Correctness: We say that D is correct if and only if, for all theory T ⊆ For_L and formula φ ∈ For_L, if T ⊢_D φ, then T ⊨_L φ.

Completeness: We say that D is complete if and only if, for all theory T ⊆ For_L and formula φ ∈ For_L, if T ⊨_L φ, then T ⊢_D φ.

Knowledge representation normally aims at defining logics for which there exists a correct and complete deductive-system. Moreover, the deductive-system should be implementable and, if possible, efficiently. An implementation of a correct and complete deductive-system that always terminates is a decision procedure for the problem of deciding whether T ⊨_L φ or T ⊭_L φ given any pair (T, φ) as input.

Properties of logics

Deductive-system can be used to devise algorithms that automate deductions. There are multiple decision problems related to logics and reasoning, but the main one is the entailment problem, which is used to define certains properties of a logic.

Entailment problem: The entailment problem for a logic L = (Sym_L, For_L, Int_L, ⊨_L) is a decision problem that consists in telling whether a theory T ⊆ For_L entails a formula φ. A decision procedure for the entailment problem is called a reasoner for L.

What a reasoner can or cannot do defines some of the properties of L. Let us examine a few of these properties:

Decidability: A logic L is decidable if there exists a reasoner that always answers correctly in a finite amount of time for any input.

Semi-decidability: A logic is semi-decidable if there exists a reasoner that returns true if and only if T ⊨_L φ for any theory T and formula φ in the language of L.

Undecidability: A logic is undecidable if and only if it is not decidable.

Note that propositional logic is decidable, but first order logic is not. More precisely, first order logic is semi-decidable. When a logic is decidable, it is interesting to know how efficiently the decision can be computed. This leads to the notion of complexity of the logic.

Complexity: The complexity of a logic L is the smallest computational complexity of a reasoner that always terminates with a correct answer to the entailment problem.

Highly complex logics require more resources (processing time and/or memory) to reach a decision on entailment. However, logics of low complexity cannot express much knowledge concisely. For any knowledge-based systems, there must be a tradeoff between complexity and expressivity.