Propositional Logic

#folder

Propositional Logic is also known as zeroth-order logic

Diagram

Syntax

Definition

A formula in propositional logic consists of the following symbols:

  1. Two constant symbols: true and false
  2. Prime proposition symbols (letters)
  3. Propositional connectives ()
  4. Brackets

$

logical connectives

Logical Connectives

Table

Symbols listed from highest to lowest precedence:

Symbol Informal meaning
negation
conjunction (and, both)
disjunction (or, one of)
implication
if and only if
Rules

Well-formed formulas of propositional logic are obtained by the following construction rules:

  1. Proposition symbols and constants are WFF (atomic formulas)
  2. If and are WFFs, then each of the following are WFF (compound propositions):

Semantics

See: Logic#Semantics

Definition

Semantics give propositions meanings by the WFF of a syntax to its truth table/truth function

Abstract

  • Satisfiable <=> contingent or tautology
  • Formula is not satisfiable <=> contradiction
  • A formula is a tautology <=> is a contradiction

Boolean Valuation

Info

A boolean valuations is a function denoted with []

List

In all boolean valuations:

  1. ,
  3. For connectives:

This may seem obvious since we have already attached the meaning of the syntax to these operators. However, syntax without semantics has no meaning, and is only used to form well-formed formulas.

Example

what is the meaning of this formula in the following boolean valuation?

solution

Validity

Definition

An argument is valid iff for all boolean valuations where the premises are T, the conclusion is T.

Logical Implication

Definition

A formula logically implies a formula if and only if for all boolean valuations, if then , and we write:

where the formulas are in red and meta-symbols are in black.

Logical Equivalence

Definition

Two formulas, and are logically equivalent if and only if for all boolean valuations, , and we write:

Formula Properties

Diagram

Satisfiability

Definition

A formula is satisfiable iff there exists a boolean valuation such that

Tautology

$

tautology

Tautology

The opposite of a contradiction is a tautology.

Definition

An assertion that is true in every interpretation

Example

  • is always true
  • is always true

Formula is a tautology iff for every boolean evaluation

Note

We write when is a tautology

Example

is not a tautology

Syntax Semantics

Contradiction

$

contradiction

Proof Method - Contradiction

Definition

Let be a statement. Note that either or must be false, so the compound statement is always false.

Example

  • " is true" is a contradiction
  • is always false

Formula is a contradiction iff for every boolean evaluation

Contingency

Definition

A contingent formula is one that is neither a tautology nor a contradiction, i.e a mix of T/F

Consistency

Definition

A collection of formulas is consistent iff there exists a boolean valuation in which all the formulas are

We have the issue of vacuous truths, meaning that nothing can be proven about a system if there are inconsistent premises. Often our premises describe the environment a system executes in. We need to make sure these premises are consistent, such that the environment we describe could possibly exist.

Normal Forms

Every formula can be converted to an equivalent formula in CNF and DNF.

Literal

Definition

A literal is a proposition symbol or the negation of a proposition symbol

Disjunctive Normal Form (DNF)

Definition

A formula is in disjunctive normal form if it is a disjunction of one or more clauses, where a clause is a conjunction of literals or a single literal

Cognate with the concept of canonical sum-of-products.

Example

It is very easy to find a satisfying assignment in DNF because you only need one clause to be true

Conjunctive Normal Form (CNF)

Definition

A formula is in conjunctive normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals or a single literal

Cognate with the concept of canonical product-of-sums.

Example

Example

Find the conjunctive normal form of

solution

Most SAT (satisfiability solvers) accept a formula in CNF form. SAT solving is a well-known NP-complete problem. We can't avoid that complexity.

There is an algorithm for converting any propositional logic formula into CNF in linear time by adding extra variables (Tseytin Transformation).

We can convert any propositional logic problem to CNF in linear time, but determining the satisfiability is NP-complete. For DNF, the complexity is in the conversion and not the solving.

Example: Separation Minima

Imagine you're a requirements engineer for a system that determines how much separation is required between two aircraft in the North Atlantic Region. The inputs are information about the aircraft, and the output should be information about how much vertical separation is required.

For two aircraft A and B, the vertical separation minimum shall be:

  1. Under what conditions are each of the amounts of vertical separation required?
  2. Is there an amount of vertical separation required for all possible input conditions?
  3. Is there only one amount of vertical separation required for all possible input conditions? (i.e., is the specification unambiguous?)

solution
(1)

Where:

(2)
Show that our formula is satisfiable with a Transformational Proof:

proof

(3)
Proof with Semantic Tableaux:

proof