What is Propositional Logic?

Propositional logic, a subset of mathematical logic, is a symbolic language that allows us to formalize and analyze arguments and assertions. At its core, propositional logic deals with propositions, which are statements that can be either true or false, but not both. This binary nature is crucial for creating clear, unambiguous expressions in logical analysis.

Basic Components of Propositional Logic

The building blocks of propositional logic are simple: propositions and logical connectives.

1. Propositions: These are simply statements that declare anything. For example, "The sun is shining" is a proposition. In propositional logic, these are typically represented by symbols like P, Q, and R.

2. Logical Connectives: These are operators that connect propositions, creating compound statements. The primary logical connectives include:

   • Conjunction ( ∧ ): The 'and' operator. ( P ∧ Q ) is true only if both P and Q are true.

   • Disjunction ( ∨ ): The 'or' operator. ( P ∨ Q ) is true if either P or Q (or both) are true.

   • Negation ( ¬ ): This inverts the truth value of a proposition. ( ¬P ) is true if P is false, and vice versa.

   • Implication ( → ): The 'if... then...' operator. ( P → Q ) is false only if P is true and Q is false.

   • Biconditional ( ↔ ): The 'if and only if' operator. ( P ↔ Q ) is true if both P and Q have the same truth value.

Why Propositional Logic is Fundamental for Formal Verification

Propositional logic plays an important role in formal verification. The clarity and precision of propositional logic make it an indispensable tool in this domain for several reasons:

1. Unambiguous Specifications: It allows for the creation of clear and precise specifications. The unambiguous nature of propositional logic ensures that the specifications are free from misinterpretation.

2. Systematic Analysis: Propositional logic provides a systematic way to analyze complex logical structures. Through truth tables and logical equivalences, one can methodically examine the behavior of logical expressions under different conditions.

3. Automated Reasoning: The binary nature of propositions is compatible with digital computers, enabling automated reasoning about software and hardware systems. This automation is key in handling the complexity of modern systems.

4. Detecting Logical Inconsistencies: In formal verification, identifying contradictions or inconsistencies in the specifications is crucial. Propositional logic, with its strict rules of inference and logical equivalences, excels at exposing such inconsistencies.

5. Basis for More Complex Logics: Propositional logic forms the foundation upon which more complex logical systems, like predicate logic and modal logic, are built. Understanding propositional logic is a prerequisite for delving into these advanced topics.

To better understand propositional logic, let’s consider some basic examples:

• Example 1: Let P represent "It is raining", and Q represent "The ground is wet". A simple propositional logic expression can be ( P → Q ), which reads as "If it is raining, then the ground is wet".

• Example 2: Consider P as "The server is online" and Q as "The website is accessible". The expression ( P ∧ ¬Q ) (The server is online and the website is not accessible) might indicate a problem outside the server affecting the website’s accessibility.

In these examples, propositional logic helps to model real-world situations in a way that is clear, precise, and conducive to systematic analysis, which is essential in the field of formal verification.

Truth Tables

Truth tables serve as a visual representation of the possible truth values of logical expressions based on the combination of truth values of their individual propositions. They break down complex logical statements into parts, displaying every potential scenario and the resulting truth value of the overall statement.

Applying Truth Tables to Analyze Statements

Using truth tables, we can analyze more complex logical statements. Let's consider the example from the given reference:

When planning a party, you want to know whom to invite. Among the people you would like to invite are three touchy friends. You know that if Alice attends, she will become unhappy if Bob is there. Bob will attend only if Charlie will be there, and Charlie will not attend unless Alice also does. You want at least two friends to be there. Which combinations of these three friends can you invite so as not to make someone unhappy?

Tautologies

Tautologies are statements that are true regardless of the truth values of their constituent propositions. Recognizing tautologies using truth tables is straightforward: if the resulting column of a truth table consists of all 'True' values, then the logical expression is a tautology.

A classic example of a tautology is the statement:

"Either it will rain tomorrow, or it won't."

Using our variables:

• P: "It will rain tomorrow."

The logical expression for this statement is ( P ∨ ¬P ).

Constructing the truth table:

As seen from the resulting column, the logical expression ( P ∨ ¬P ) is true in all scenarios. Thus, the statement "Either it will rain tomorrow, or it won't." is a tautology.

Logical Equivalence

We often encounter statements that may look different on the surface but are inherently conveying the same idea. This concept, where two different-looking statements have the same truth value in all scenarios, is called Logical Equivalence.

A straightforward method to ascertain that two statements are logically equivalent is by crafting a truth table for each of them. If the resulting columns for both statements match entirely, they are logically equivalent.

Recognizing logically equivalent statements holds significance. Reframing a mathematical statement can sometimes shed light on its inherent meaning or guide how one should go about proving or refuting it. With the systematic approach of truth tables, verifying the logical equivalence of two statements becomes feasible.

Example:
Consider the statements:

1. "It will not rain or snow"

2. "It will not rain and it will not snow"

At first glance, these might appear distinct, but they inherently convey the same meaning. This example helps illustrate a fundamental principle known as De Morgan's Laws:

1. The negation of a conjunction (AND) is equivalent to the disjunction (OR) of their negations:
   ¬(P ∧ Q) is logically equivalent to ¬P ∨ ¬Q.

2. The negation of a disjunction (OR) is equivalent to the conjunction (AND) of their negations:
   ¬(P ∨ Q) is logically equivalent to ¬P ∧ ¬Q.

These laws hint at a unique "algebra" of statements, which is termed as Boolean algebra, wherein one statement can be transformed into another. By understanding and utilizing logical equivalences, it becomes possible to simplify complex logical expressions without resorting to exhaustive truth tables.

Another crucial equivalence to consider is the Double Negation:
¬¬P is logically equivalent to P.

For instance, the statement "It is not the case that c is not odd" can be simplified to "c is odd."

Predicate Logic

Predicate logic, also known as first-order logic (FOL) or quantificational logic, extends the capabilities of propositional logic to handle more complex statements that involve variables, quantifiers, and predicates. Unlike propositional logic, which deals with propositions as whole units, predicate logic breaks down statements into their constituent parts to analyze them in more depth.

• Predicates: Predicates are functions that return either true or false. They usually represent properties or relations. For instance, in the statement "x is even," "is even" is the predicate, which applies to the variable "x".

• Variables: Variables, like x, y, or z, stand in for objects within the domain of discourse. They can represent numbers, people, or any entity depending on the context.

• Quantifiers: Quantifiers specify the scope or quantity of a predicate over the domain. The two primary quantifiers are:

  • Universal Quantifier (∀) - Represents "for all" or "every." E.g., ∀x P(x) translates to "For every x, P(x) is true."

  • Existential Quantifier (∃) - Represents "there exists" or "for some." E.g., ∃x P(x) means "There exists an x such that P(x) is true."

• Constants: Constants represent specific, unchanging entities within the domain. For instance, in the domain of numbers, '1' is a constant.

A basic predicate logic formula may look like this: ∀x (P(x) → Q(x)), which reads "For all x, if P(x) is true, then Q(x) is also true."

Interpretation:

Interpreting predicate logic requires defining:

• A domain of discourse (D), specifying the set of all possible entities our variables can refer to.

• An interpretation function, which assigns meaning to predicates, functions, and constants within the domain.

Suppose we want to say, "All men are mortal." In predicate logic, we can represent this as: ∀x (M(x) → Mo(x)) Here, M(x) stands for "x is a man" and Mo(x) for "x is mortal". The statement reads, "For all x, if x is a man, then x is mortal."

Example Problem-1:

The Certora tutorial website has a great riddle they solve using the prover. Lets try to solve the same riddle using a truth table to get a better understanding of how a prover solves such a problem.

Four sisters, Sara, Ophelia, Nora, and Dawn, were each born in a different one of the months September, October, November, and December.

"This is terrible," said Ophelia one day. "None of us have an initial that matches the initial of her birth month."

"I don't mind at all," replied the girl who was born in September.

"That's easy for you to say," said Nora. "It would at least be cool if the initial of my birth month was a vowel, but no."

In which month was each girl born?

Lets start from the first clue and go step by step:

"This is terrible," said Ophelia one day. "None of us have an initial that matches the initial of her birth month."

"I don't mind at all," replied the girl who was born in September.

This means Ophelia was not born in September

"That's easy for you to say," said Nora. "It would at least be cool if the initial of my birth month was a vowel, but no."

This means Nora was not born in September since she answered the question and also October is not an option since it starts with O. The only option for Nora is December. Making December unavailable for the rest.

From there, we can see November is the only option for Ophelia, making October the only option for Sara and September the only option for Dawn.

Example Problem-2

This time we will use the Certora to find a solution to a simple logic problem.

In a room, there are three tiles placed in a horizontal row. Each tile can be one of three colors: Red, Blue, or Yellow. Each tile is distinct in color; no two tiles have the same color.

Clues:

1. The leftmost tile commented, "I'm not Yellow, and I certainly don't want Blue to my right."

2. The middle tile exclaimed, "I'm not fond of Red. Definitely not me."

3. The rightmost tile whispered, "I am not Blue"

// The colors
definition Red() returns uint8 = 1;
definition Blue() returns uint8 = 2;
definition Yellow() returns uint8 = 3;

rule findTheColors(
    uint8 First,
    uint8 Second,
    uint8 Third
) {
    // Tiles are one of the three colors
    require First == Red() || First == Blue() || First == Yellow();
    require Second == Red() || Second == Blue() || Second == Yellow();
    require Third == Red() || Third == Blue() || Third == Yellow();

    // The tiles are different colors
    require (
        First != Second &&
        First != Third &&
        Second != Third
    );

    // The leftmost tile commented, "I'm not Yellow, and I certainly don't want Blue to my right."
    require First != Yellow();
    require Second != Blue();

    // The middle tile exclaimed, "I'm not fond of Red. Definitely not me."
    require Second != Red();

    // The rightmost tile whispered, "I am not Blue"
    require Third != Blue();

    satisfy true;
}

When we run the .spec file, the prover will find us a candidate solution that adheres to our spec

Which translates to:

• The first tile is Blue

• The second tile is Yellow

• The third tile is Red

To check if this is a unique solution, we can replace the line
satisfy true; with this block:

   assert (
        First == Blue() &&
        Second == Yellow() &&
        Third == Red()
    );

If the prover can not find any violations, it means the solution we asserted is unique.

References:

• https://discrete.openmathbooks.org/dmoi2/sec_propositional.html

• https://docs.certora.com/projects/tutorials/en/latest/lesson1_prerequisites/formal_verification.html