Propositional Logic

Syntax

Symbols

We define the set C = {¬, ∧, ∨, →, ↔} of logical connectors (all different from each others), the couple B = {(, )} of opening and closing parentheses (B is for brackets) disjoint from C, and an infinite set P disjoint from B and C whose members are called propositions.

Symbols of PL

The symbols of PL are Sym_PL = B ⋃ C ⋃ P.

We will write distinct propositions with distinct sequences of latin characters like so: A, P, ItsRaining, etc. Although ItsRaining is written with a sequence of 10 latin characters, it is counted as a single symbol in propositional logic.

Formulas

Formulas of PL

Formulas are recursively built as the smallest set For_PL such that:

• for all x ∈ P, x ∈ For_PL;
• for all φ ∈ For_PL, ¬φ ∈ For_PL;
• for all φ, ψ ∈ For_PL, (φ ∧ ψ) ∈ For_PL;
• for all φ, ψ ∈ For_PL, (φ ∨ ψ) ∈ For_PL;
• for all φ, ψ ∈ For_PL, (φ → ψ) ∈ For_PL;
• for all φ, ψ ∈ For_PL, (φ ↔ ψ) ∈ For_PL.

Atom

An atom is a formula that is reduced to a single proposition.

Note that we use a light shading on formulas in order to clearly distinguish them, in particular, when a formula is an atom, it makes it clear whether we are using the symbol in the context of a proposition or in the context of a formula.

By convention, the following operator precedence is assumed: ¬ has higher precedence than ∧; ∧ has higher precedence than ∨; and ∨ has higher precedence than → and ↔. As a result, it is possible to write formulas by leaving parentheses implicit. Therefore, the following formulas are considered well formed:

(A ∨ B) ∧ (B ∨ ¬B) → D implicitly meaning (((A ∨ B) ∧ (B ∨ ¬B)) → D)

ItIsRaining → ItIsWetOutside implicitly meaning (ItIsRaining → ItIsWetOutside)

In addition to these usual definitions that apply to any logic, we introduce special syntactic forms that are generally useful for algorithms.

Literal

A literal L is a formula that is either an atom (that is, L ∈ P) or the negation of an atom (that is, L = ¬P where P ∈ P).

Conjunctive normal form (CNF)

A formula φ ∈ For_PL is in conjunctive normal form (or CNF for short) if and only if φ = ψ₁ ∧ … ∧ ψ_n for some n ∈ ℕ\{0} such that for all i ∈ {1, …, n}, there is p ∈ ℕ\{0} such that ψ_i = (L_i,1 ∨ … ∨ L_i,p), and L_i,j are literals.

Put differently, a formula is in CNF if it is a conjunction of disjunction of literals.

Semantics

Interpretations

Interpretations in PL

An interpretation in PL is a function 𝓘 : P ⟶ {true, false}.

An interpretation simply says which propositions are considered true, and which ones are considered false.

We can define an interpretation 𝓘 such that 𝓘(ItIsRaining) = true and 𝓘(ItIsWetOutside) = false.

Satisfaction relation

Satisfaction relation in PL

An interpretation 𝓘 in PL satisfies a formula φ (that is, (𝓘, φ) ∈ ⊨_PL, or 𝓘 ⊨_PL φ) if and only if the following holds:

• if φ is an atom, then 𝓘 ⊨_PL φ iff 𝓘(φ) = true;
• if φ = ¬ψ for some formula ψ, then 𝓘 ⊨_PL φ iff 𝓘 ⊭_PL ψ;
• if φ = (ψ₁ ∧ ψ₂) for some formulas ψ₁ and ψ₂, then 𝓘 ⊨_PL φ iff 𝓘 ⊨_PL ψ₁ and 𝓘 ⊨_PL ψ₂;
• if φ = (ψ₁ ∨ ψ₂) for some formulas ψ₁ and ψ₂, then 𝓘 ⊨_PL φ iff 𝓘 ⊨_PL ψ₁ or 𝓘 ⊨_PL ψ₂, or both;
• if φ = (ψ₁ → ψ₂) for some formulas ψ₁ and ψ₂, then 𝓘 ⊨_PL φ iff 𝓘 ⊨_PL ¬ψ₁ or 𝓘 ⊨_PL ψ₂, or both;
• if φ = (ψ₁ ↔ ψ₂) for some formulas ψ₁ and ψ₂, then 𝓘 ⊨_PL φ iff 𝓘 ⊨_PL (ψ₁ → ψ₂) and 𝓘 ⊨_PL (ψ₂ → ψ₁).

The interpretation 𝓘 of the previous example does not satisfy ItIsRaining → ItIsWetOutside. However, it satisfies ItIsRaining ∨ ItIsWetOutside as well as ¬ItIsWetOutside.

Note that given a finite theory T = {φ₁, …, φ_n} and any formula ψ, it holds that T ⊨_PL ψ if and only if {φ₁ ∧ … ∧ φ_n}⊨_PL ψ. This means that we can always replace a PL theory by a single formula. Therefore, we can assume that the relation ⊨_PL is between formulas rather than between theories and formulas.

Properties of PL

PL is decidable and its complexity belongs to the class of NP-complete problems.

Given any formula φ, there exists a formula ψ in CNF such that φ ⊨_PL ψ and ψ ⊨_PL φ.

For any formulas φ, ψ ∈ For_PL, φ ⊨_PL ψ if and only if φ → ψ is a tautology.

Deductive system

An example of a deductive system for PL that is both correct and complete can be defined as follows:

The deductive system SF₀

The deductive system SF₀ = (A₀, R₀) such that:

• for all formulas φ, ψ, χ ∈ For_PL, A₀ contains the formulas (φ → (ψ → φ)), ((φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))), and ((¬φ → ¬ψ) → (ψ → φ));
• for all formulas φ, ψ ∈ For_PL, R₀ contains the rule ({φ, (φ → ψ)}, ψ).

As written, SF₀ is not complete, because it only deals with formulas that contain symbols in B ⋃ P ⋃ {→, ¬}. However, every formula is logically equivalent to a formula that only uses symbols in B ⋃ P ⋃ {→, ¬}. The following rules can be added to ensure completeness, leading to the set of rules R⁺₀:

• for all formulas φ, ψ ∈ For_PL, R⁺₀ contains the rules ({(φ ∧ ψ)}, φ), ({(φ ∧ ψ)}, ψ), ({(φ ∨ ψ)}, (¬φ → ψ)), ({(φ ↔ ψ)}, ((φ → ψ) ∧ (ψ → φ))).