Introduction

Introduction #

Revised

24 Aug 2023

Programming Environment #

from   collections import Counter
from   functools   import partial
from   itertools   import product
import re
from   typing      import List

# https://www.cs.colostate.edu/~cs220/fall17/assignments/PA1/

class Infix (object):
	def __init__ (self, func):
		self.func = func
	def __or__ (self, other):
		return self.func(other)
	def __ror__ (self, other):
		return Infix(partial(self.func, other))
	def __call__ (self, v1, v2):
		return self.func(v1, v2)

@Infix
def implies (p, q):
	return not p or q

@Infix
def iff (p, q):
	return (p |implies| q) and (q |implies| p)

def extract_variables (expr : str) -> set:
  sorted_variable_set = sorted(set(re.findall(r'\b[a-z]\b', expr)))
  return sorted_variable_set

TruthTable = list[list[bool]]

def truth_table (expr : str) -> List[List[bool]]:
	'''
	parameters
	==========
	`expr` [str] : a valid Python logical expression
	
	return
	======
	[list] each element is a row in the table
	'''

	letters = extract_variables(expr)
	#tokens  = expression.split()
	#letters = sorted(set(letter for letter in tokens if len(letter) == 1)) # get sorted, unique variables
	
	tt = [list(tup) for tup in product([True, False], repeat=len(letters))]
	for row in tt:
		for letter, val in zip(letters, row):
			exec(f'{letter}={val}')
		try:
		  row.append(eval(expr))
		except SyntaxError as e:
			raise

	return tt

# recursive implementation
def truth_table_recursor (letters : list) -> TruthTable:
  if len(letters) == 1: # base case
    return [[True], [False]]
  else:                 # recursive case
    return [elem + [True]  for elem in truth_table_recursor(letters[1:])] + \
           [elem + [False] for elem in truth_table_recursor(letters[1:])]
    #return list(itertools.chain.from_iterable([[elem + [True], elem + [False]] for elem in truth_table_recursor(letters[1:])]))
def truth_table (expr : str) -> TruthTable:
  letters = extract_variables(expr)
  tt      = truth_table_recursor(letters)
  for row in tt:
    for letter, val in zip(letters, row):
      exec(f'{letter}={val}')
    try:
      row.append(eval(expr))
    except SyntaxError as e:
      raise
  return tt

def count_satisfying (expr : str) -> int:
	'''
	parameters
	==========
	`expr` [str] : a valid Python logical expression

	return
	======
	[int] the number of assignments of the variables for which the result is True
	'''
	tt = truth_table(expr)
	return sum(row[-1] for row in tt)

def is_tautology (expr : str) -> bool:
	'''
	parameters
	==========
	`expr` [str] : a valid Python logical expression

	return
	======
	[bool] indicates whether the expression is a tautology or not
	'''
	tt = truth_table(expr)
	return sum(row[-1] for row in tt) == len(tt)

def are_equivalent (expr1 : str, expr2 : str) -> bool:
	'''
	parameters
	==========
	`expr1` [str] : a valid Python logical expression
	`expr2` [str] : a valid Python logical expression

	return
	======
	[bool] indicates whether the expressions are equivalent or not
	'''
	tt1 = truth_table(expr1)
	tt2 = truth_table(expr2)
	for row_tt1, row_tt2 in zip(tt1, tt2):
		if row_tt1[-1] != row_tt2[-1]:
			return False
	return True

expr = 'a |implies| b'
pad=12
print(f"{'expression' :<{pad}} {expr}")
print(f"{'truth table':<{pad}} {truth_table     (expr)}")
print(f"{'satisfying' :<{pad}} {count_satisfying(expr)}")
print(f"{'tautology'  :<{pad}} {is_tautology    (expr)}")

expression   a |implies| b
truth table  [[True, True, True], [False, True, True], [True, False, False], [False, False, True]]
satisfying   3
tautology    False

Propositional Logic (PL)#

Sentential Logic or Zeroth-Order Logic

Propositional Expression/Formula (Sentential Formula)
Rule of Inference (Inference/Transformation Rule)

\( \begin{array}{c|c|c} & \text{Arithmetic} & \text{Boolean Logic} \\ \hline \text{Values} & ..., -2, -1, 0, 1, 2, ... & \text{T}, \text{F} \\ \hline \text{Operators} & +, -, \times, \div & \land, \lor, \lnot \\ \end{array} \)

Unlike the indefinite (or infinite) number of values on which arithmetic operates, propositional logic only deals in two Boolean values: true and false.

\( \begin{array}{c|c|c|c} \text{Boolean} & \text{binary} & \text{Python} & \text{physical} \\ \hline \text{true, T} & 1 & \text{True} & \text{high voltage} \\ \text{false, F} & 0 & \text{False} & \text{low voltage} \\ \end{array} \)

print(type(True))
print(type(False))

<class 'bool'>
<class 'bool'>

Conjunction (and)#

Conjunction is represented by the symbol \(\land\).

Definition of the binary operation

\( \begin{array}{c|cc} \land & \text{T} & \text{F} \\ \hline \text{T} & \text{T} & \text{F} \\ \text{F} & \text{F} & \text{F} \\ \end{array} \)

Binary truth table

\( \begin{array}{cc|c} \text{P} & \text{Q} & \text{P} \land \text{Q} \\ \hline \text{T} & \text{T} & \text{T} \\ \text{T} & \text{F} & \text{F} \\ \text{F} & \text{T} & \text{F} \\ \text{F} & \text{F} & \text{F} \\ \end{array} \)

English

\(\text{P}\) The sky is blue.
\(\text{Q}\) The moon is full.
\(\text{P} \land \text{Q}\)
- The sky is blue and the moon is full.
- The sky is blue, but the moon is full.
- Despite the fact that the sky is blue, the moon is full.
- Although the sky is blue, the moon is full.

for P, Q in product((True, False), repeat=2):
  print(f"{str(P):<5} and {str(Q):<5} is {P and Q}")

True  and True  is True
True  and False is False
False and True  is False
False and False is False

expr = 'a and b'
pad=12
print(f"{'expression' :<{pad}} {expr}")
print(f"{'truth table':<{pad}} {truth_table     (expr)}")
print(f"{'satisfying' :<{pad}} {count_satisfying(expr)}")
print(f"{'tautology'  :<{pad}} {is_tautology    (expr)}")

expression   a and b
truth table  [[True, True, True], [False, True, False], [True, False, False], [False, False, False]]
satisfying   1
tautology    False

The conjunction of \(n\) propositional variables is true if and only if each variable is true. In other words, if at least one variable of a conjunction is false then the conjunction is false, otherwise it’s true.

P = True
Q = True
R = True
print(P and Q and R) # all((P, Q, R))

A = B = C = D = E = F = G = True
print(A and B and C and D and E and F and G)

G = False
print(A and B and C and D and E and F and G)

True
True
False

Inclusive Disjunction (or)#

Inclusive disjunction is represented by the symbol \(\lor\).

Definition

\( \begin{array}{c|cc} \lor & \text{T} & \text{F} \\ \hline \text{T} & \text{T} & \text{T} \\ \text{F} & \text{T} & \text{F} \\ \end{array} \)

Truth Table

\( \begin{array}{cc|c} \text{P} & \text{Q} & \text{P} \lor \text{Q} \\ \hline \text{T} & \text{T} & \text{T} \\ \text{T} & \text{F} & \text{T} \\ \text{F} & \text{T} & \text{T} \\ \text{F} & \text{F} & \text{F} \\ \end{array} \)

English

\(\text{P}\) The sky is blue.
\(\text{Q}\) The moon is full.
\(\text{P} \lor \text{Q}\) The sky is blue or the moon is full, or both.

for P, Q in product((True, False), repeat=2):
  print(f"{str(P):<5} or {str(Q):<5} is {P or Q}")

True  or True  is True
True  or False is True
False or True  is True
False or False is False

expr = 'a or b'
pad=12
print(f"{'expression' :<{pad}} {expr}")
print(f"{'truth table':<{pad}} {truth_table     (expr)}")
print(f"{'satisfying' :<{pad}} {count_satisfying(expr)}")
print(f"{'tautology'  :<{pad}} {is_tautology    (expr)}")

expression   a or b
truth table  [[True, True, True], [False, True, True], [True, False, True], [False, False, False]]
satisfying   3
tautology    False

The inclusive disjunction of \(n\) propositional variables is true if at least one variable is true. In other words, if no variable of an inclusive disjunction is true then the inclusive disjunction is false, otherwise it’s true.

P = True
Q = True
R = True
print(P or Q or R) # all((P, Q, R))

A = B = C = D = E = F = G = False
print(A or B or C or D or E or F or G)

G = True
print(A or B or C or D or E or F or G)

True
False
True

Negation #

Negation is represented by the symbol \(\lnot\). Negation is a unary function because it takes one input value.

Definition of the unary operation

\( \begin{array}{c|c} & \lnot \\ \hline \text{T} & \text{F} \\ \text{F} & \text{T} \\ \end{array} \)

Unary truth table

\( \begin{array}{c|c} \text{P} & \lnot \text{P} \\ \hline \text{T} & \text{F} \\ \text{F} & \text{T} \\ \end{array} \)

for P in (True, False):
  print(f"not {str(P):<5} is {not P}")

not True  is False
not False is True

expr = 'not a'
pad=12
print(f"{'expression' :<{pad}} {expr}")
print(f"{'truth table':<{pad}} {truth_table     (expr)}")
print(f"{'satisfying' :<{pad}} {count_satisfying(expr)}")
print(f"{'tautology'  :<{pad}} {is_tautology    (expr)}")

expression   not a
truth table  [[True, False], [False, True]]
satisfying   1
tautology    False

Exclusive Disjunction (either or but not both)#

Definition of the binary operation

\( \begin{array}{c|cc} \oplus & \text{T} & \text{F} \\ \hline \text{T} & \text{F} & \text{T} \\ \text{F} & \text{T} & \text{F} \\ \end{array} \)

Binary truth table

\( \begin{array}{cc|c} \text{P} & \text{Q} & \text{P} \oplus \text{Q} \\ \hline \text{T} & \text{T} & \text{F} \\ \text{T} & \text{F} & \text{T} \\ \text{F} & \text{T} & \text{T} \\ \text{F} & \text{F} & \text{F} \\ \end{array} \)

English

\(\text{P}\) The sky is blue.
\(\text{Q}\) The moon is full.
\(\text{P} \oplus \text{Q}\) The sky is blue or the moon is full, but not both.

def xor (P: bool,
         Q: bool) -> bool:
  return    (P and not Q) \
         or (Q and not P)

for P, Q in product((True, False), repeat=2):
  print(xor(P, Q))

False
True
True
False

expr = 'not (not a or b) or not (a or not b)'
pad=12
print(f"{'expression' :<{pad}} {expr}")
print(f"{'truth table':<{pad}} {truth_table     (expr)}")
print(f"{'satisfying' :<{pad}} {count_satisfying(expr)}")
print(f"{'tautology'  :<{pad}} {is_tautology    (expr)}")

expression   not (not a or b) or not (a or not b)
truth table  [[True, True, False], [False, True, True], [True, False, True], [False, False, False]]
satisfying   2
tautology    False

Material Conditional/Implication (if then)#

Definition

\( \begin{array}{c|cc} \rightarrow & \text{T} & \text{F} \\ \hline \text{T} & \text{T} & \text{F} \\ \text{F} & \text{T} & \text{T} \\ \end{array} \)

Truth Table

\( \begin{array}{cc|c} \text{P} & \text{Q} & \text{P} \rightarrow \text{Q} \\ \hline \text{T} & \text{T} & \text{T} \\ \text{T} & \text{F} & \text{F} \\ \text{F} & \text{T} & \text{T} \\ \text{F} & \text{F} & \text{T} \\ \end{array} \)

English

\(\text{P}\) The sky is blue.
\(\text{Q}\) The moon is full.
\(\text{P} \rightarrow \text{Q}\) If the sky is blue, then the moon is full. (If P, then Q)
- Either the moon is full or the sky is not blue, or both. (Either Q or not P, or both)
- If the sky is blue the moon is full. (If P, Q)
- The moon is full if the sky is blue. (Q if P)
- The sky is blue implies the moon is full. (P implies Q)
- The sky is blue only if the moon is full. (P only if Q)
- The sky is blue is sufficient for the moon is full. (P is sufficient for Q)
- The moon is full is necessary for the sky is blue. (Q is necessary for P)

def ifthen (P: bool,
            Q: bool) -> bool:
  return not (P and not Q)

for P, Q in product((False, True), repeat=2):
  print(ifthen(P, Q))

True
True
False
True

expr = 'a |implies| b'
pad=12
print(f"{'expression' :<{pad}} {expr}")
print(f"{'truth table':<{pad}} {truth_table     (expr)}")
print(f"{'satisfying' :<{pad}} {count_satisfying(expr)}")
print(f"{'tautology'  :<{pad}} {is_tautology    (expr)}")

expression   a |implies| b
truth table  [[True, True, True], [False, True, True], [True, False, False], [False, False, True]]
satisfying   3
tautology    False

Converse Implication #

Definition

\( \begin{array}{c|cc} \leftarrow & \text{T} & \text{F} \\ \hline \text{T} & \text{T} & \text{T} \\ \text{F} & \text{T} & \text{F} \\ \end{array} \)

Truth Table

\( \begin{array}{cc|c} \text{P} & \text{Q} & \text{P} \leftarrow \text{Q} \\ \hline \text{T} & \text{T} & \text{T} \\ \text{T} & \text{F} & \text{T} \\ \text{F} & \text{T} & \text{F} \\ \text{F} & \text{F} & \text{T} \\ \end{array} \)

English

\(\text{P}\) The sky is blue.
\(\text{Q}\) The moon is full.
\(\text{P} \leftarrow \text{Q}\) The sky is blue if the moon is full. (P if Q)

expr = 'p or not q'
pad=12
print(f"{'expression' :<{pad}} {expr}")
print(f"{'truth table':<{pad}} {truth_table     (expr)}")
print(f"{'satisfying' :<{pad}} {count_satisfying(expr)}")
print(f"{'tautology'  :<{pad}} {is_tautology    (expr)}")

expression   p or not q
truth table  [[True, True, True], [False, True, False], [True, False, True], [False, False, True]]
satisfying   3
tautology    False

Contrapositive #

If not q, then not p.

\(\text{P} \rightarrow \text{Q} \overset{?}{\equiv} \lnot\text{Q} \rightarrow \lnot\text{P}\)

Proof by substitution

\( \begin{aligned} \text{P} \rightarrow \text{Q} && \\ (\lnot\text{P} \lor \text{Q}) && \text{conditionality} \\ (\text{Q} \lor \lnot\text{P}) && \text{commutativity} \\ (\lnot\lnot\text{Q} \lor \lnot\text{P}) && \text{double negation} \\ (\lnot\text{Q} \rightarrow \lnot\text{P}) && \text{conditionality} \\ \end{aligned} \)

\(\therefore \text{P} \rightarrow \text{Q} \equiv \lnot\text{Q} \rightarrow \lnot\text{P}\)

\(\blacksquare\)

Inverse #

If not p, then not q.

Biconditional #

Definition

\( \begin{array}{c|cc} \leftrightarrow & \text{T} & \text{F} \\ \hline \text{T} & \text{T} & \text{F} \\ \text{F} & \text{F} & \text{T} \\ \end{array} \)

Truth Table

\( \begin{array}{cc|c} \text{P} & \text{Q} & \text{P} \leftrightarrow \text{Q} \\ \hline \text{T} & \text{T} & \text{T} \\ \text{T} & \text{F} & \text{F} \\ \text{F} & \text{T} & \text{F} \\ \text{F} & \text{F} & \text{T} \\ \end{array} \)

English

\(\text{P}\) The sky is blue.
\(\text{Q}\) The moon is full.
\(\text{P} \leftrightarrow \text{Q}\) The sky is blue if and only if the moon is full. (P if and only if Q)

expr = 'a |iff| b'
pad=12
print(f"{'expression' :<{pad}} {expr}")
print(f"{'truth table':<{pad}} {truth_table     (expr)}")
print(f"{'satisfying' :<{pad}} {count_satisfying(expr)}")
print(f"{'tautology'  :<{pad}} {is_tautology    (expr)}")

expression   a |iff| b
truth table  [[True, True, True], [False, True, False], [True, False, False], [False, False, True]]
satisfying   2
tautology    False

Tautology #

Definition

\( \begin{array}{c|cc} \top & \text{T} & \text{F} \\ \hline \text{T} & \text{T} & \text{T} \\ \text{F} & \text{T} & \text{T} \\ \end{array} \)

Truth Table

\( \begin{array}{cc|c} \text{P} & \text{Q} & \text{P} \top \text{Q} \\ \hline \text{T} & \text{T} & \text{T} \\ \text{T} & \text{F} & \text{T} \\ \text{F} & \text{T} & \text{T} \\ \text{F} & \text{F} & \text{T} \\ \end{array} \)

def tautology (a: bool,
               b: bool) -> bool:
  return True

for P, Q in product((True, False), repeat=2):
  print(tautology(P, Q))

True
True
True
True

expr = 'a or not a'
pad=12
print(f"{'expression' :<{pad}} {expr}")
print(f"{'truth table':<{pad}} {truth_table     (expr)}")
print(f"{'satisfying' :<{pad}} {count_satisfying(expr)}")
print(f"{'tautology'  :<{pad}} {is_tautology    (expr)}")

expression   a or not a
truth table  [[True, True], [False, True]]
satisfying   2
tautology    True

Contradiction #

Definition

\( \begin{array}{c|cc} \bot & \text{T} & \text{F} \\ \hline \text{T} & \text{F} & \text{F} \\ \text{F} & \text{F} & \text{F} \\ \end{array} \)

Truth Table

\( \begin{array}{cc|c} \text{P} & \text{Q} & \text{P} \bot \text{Q} \\ \hline \text{T} & \text{T} & \text{F} \\ \text{T} & \text{F} & \text{F} \\ \text{F} & \text{T} & \text{F} \\ \text{F} & \text{F} & \text{F} \\ \end{array} \)

def contradiction (a: bool,
                   b: bool) -> bool:
  return False

for P, Q in product((True, False), repeat=2):
  print(contradiction(P, Q))

False
False
False
False

expr = 'not (a or not a)'
pad=12
print(f"{'expression' :<{pad}} {expr}")
print(f"{'truth table':<{pad}} {truth_table     (expr)}")
print(f"{'satisfying' :<{pad}} {count_satisfying(expr)}")
print(f"{'tautology'  :<{pad}} {is_tautology    (expr)}")

expression   not (a or not a)
truth table  [[True, False], [False, False]]
satisfying   0
tautology    False

Summary #

Unary Operations #

\( \begin{array}{c|ccl} \text{P} & 0 & 1 \\ \hline \bot & 0 & 0 & \text{contradiction (FALSE)} \\ \text{P} & 0 & 1 & \text{identity} \\ \lnot \text{P} & 1 & 0 & \text{negation (NOT)} \\ \top & 1 & 1 & \text{tautology (TRUE)} \\ \end{array} \)

Binary Operations #

\( \begin{array}{c|ccccl} \text{P} & 0 & 0 & 1 & 1 \\ \text{Q} & 0 & 1 & 0 & 1 \\ \hline \bot & 0 & 0 & 0 & 0 & \text{contradiction (FALSE)} \\ \land & 0 & 0 & 0 & 1 & \text{conjunction (AND)} \\ \not\rightarrow & 0 & 0 & 1 & 0 & \text{abjunction, nonimplication} \\ \text{P} & 0 & 0 & 1 & 1 & \text{identity} \\ \not\leftarrow & 0 & 1 & 0 & 0 & \text{converse nonimplication} \\ \text{Q} & 0 & 1 & 0 & 1 & \text{identity} \\ \oplus & 0 & 1 & 1 & 0 & \text{exclusive disjunction (XOR)} \\ \lor & 0 & 1 & 1 & 1 & \text{inclusive disjunction (OR)} \\ \downarrow & 1 & 0 & 0 & 0 & \text{not or (NOR)} \\ \leftrightarrow & 1 & 0 & 0 & 1 & \text{biconditional (XNOR)} \\ \lnot \text{Q} & 1 & 0 & 1 & 0 & \text{negation (NOT)} \\ \leftarrow & 1 & 0 & 1 & 1 & \text{converse implication/conditional} \\ \lnot \text{P} & 1 & 1 & 0 & 0 & \text{negation (NOT)} \\ \rightarrow & 1 & 1 & 0 & 1 & \text{implication/conditional} \\ \uparrow & 1 & 1 & 1 & 0 & \text{not and (NAND)} \\ \top & 1 & 1 & 1 & 1 & \text{tautology (TRUE)} \\ \end{array} \)

\( \begin{array}{cc|ccc} P & Q & P \land Q & P \lor Q & \lnot P \\ \hline \text{T} & \text{T} & \text{T} & \text{T} & \text{F} \\ \text{T} & \text{F} & \text{F} & \text{T} \\ \text{F} & \text{T} & \text{F} & \text{T} & \text{T} \\ \text{F} & \text{F} & \text{F} & \text{F} \\ \end{array} \)

Order of Operations #

negation
conjunction
disjunction

Number of operations #

How many n-ary operations are there? The number of values raised to the number of input tuples.

\(2^2=4\) unary operations (two values, two inputs)
\(2^{2^2}=16\) binary operations (two values, four input pairs)
\(2^{2^3}=256\) ternary operations (two values, eight input triples)

list(product((0,1), repeat=2))

[(0, 0), (0, 1), (1, 0), (1, 1)]

list(product((0,1), repeat=2**2))

[(0, 0, 0, 0),
 (0, 0, 0, 1),
 (0, 0, 1, 0),
 (0, 0, 1, 1),
 (0, 1, 0, 0),
 (0, 1, 0, 1),
 (0, 1, 1, 0),
 (0, 1, 1, 1),
 (1, 0, 0, 0),
 (1, 0, 0, 1),
 (1, 0, 1, 0),
 (1, 0, 1, 1),
 (1, 1, 0, 0),
 (1, 1, 0, 1),
 (1, 1, 1, 0),
 (1, 1, 1, 1)]

n-ary #

\( \begin{array}{ccc|cc} \text{P} & \text{Q} & \text{R} & \text{P} \land \text{Q} \land \text{R} & \text{P} \lor \text{Q} \lor \text{R} \\ \hline 0 & 0 & 0 & 0 & 0 \\ 0 & 0 & 1 & 0 & 1 \\ 0 & 1 & 0 & 0 & 1 \\ 0 & 1 & 1 & 0 & 1 \\ 1 & 0 & 0 & 0 & 1 \\ 1 & 0 & 1 & 0 & 1 \\ 1 & 1 & 0 & 0 & 1 \\ 1 & 1 & 1 & 1 & 1 \\ \end{array} \)

\( \begin{array}{cccc|cc} P & Q & ... & R & P \land Q \land ... \land R & P \lor Q \lor ... \lor R \\ \hline 0 & 0 & ... & 0 & 0 & 0 \\ 0 & 0 & ... & 1 & 0 & 1 \\ \vdots & \vdots & \ddots & \vdots & \vdots & \vdots \\ 1 & 1 & ... & 0 & 0 & 1 \\ 1 & 1 & ... & 1 & 1 & 1 \\ \end{array} \)

Propositional Tautology #

A propositional formula is a tautology if the formula is always true, regardless of the truth value of the individual propositions that it consists in.

\( \begin{array}{cc|c} \text{P} & \lnot \text{P} & \text{P} \lor \lnot \text{P} \\ \hline \text{T} & \text{F} & \text{T} \\ \text{F} & \text{T} & \text{T} \\ \end{array} \)

\( \begin{array}{cc|c} \text{P} & \text{Q} & (\text{P} \land \text{Q}) \rightarrow \text{P} \\ \hline \text{T} & \text{T} & \text{T} \\ \text{T} & \text{F} & \text{T} \\ \text{F} & \text{T} & \text{T} \\ \text{F} & \text{F} & \text{T} \\ \end{array} \)

To demonstrate that a compound proposition is not a tautology requires only a single set of propositional variables that make the compound proposition false.

Propositional Contradiction #

A propositional formula is a contradiction if the formula is always false, regardless of the truth value of the individual propositions that it consists in.

\( \begin{array}{cc|c} \text{P} & \lnot \text{P} & \text{P} \land \lnot \text{P} & \text{P} \leftrightarrow \lnot \text{P} \\ \hline \text{T} & \text{F} & \text{F} & \text{F} \\ \text{F} & \text{T} & \text{F} & \text{F} \\ \end{array} \)

To demonstrate that a compound proposition is not a contradiction requires only a single set of propositional variables that make the compound proposition true.

Logical Equivalence #

Two compound propositions are said to be logically equivalent if they have the same truth value regardless of the truth values of their individual propositions.

\( \begin{array}{ccc} \text{P} & \lnot \text{P} & \lnot\lnot\text{P} \\ \hline \text{T} & \text{F} & \text{T} \\ \text{F} & \text{T} & \text{F} \\ \end{array} \)

\( \text{P} \equiv \lnot\lnot\text{P} \)

Propositions \(\text{P}\) and \(\text{Q}\) are logically equivalent if and only if the proposition \(\text{P}\leftrightarrow\text{Q}\) is a tautology.

To demonstrate that two propositions are not logically equivalent only requires demonstrating a particular set of truth values for their individual propositions that cause the two compound propositions to have different truth values.

Laws of Propositional Logic #

\( \begin{aligned} \text{Absorption} && \begin{aligned} \text{P} \lor (\text{P} \land \text{Q}) &\equiv \text{P} \\ \text{P} \land (\text{P} \lor \text{Q}) &\equiv \text{P} \end{aligned} \\ \text{Associativity} && \begin{aligned} (\text{P} \lor \text{Q}) \lor \text{R} &\equiv \text{P} \lor (\text{Q} \lor \text{R}) \\ (\text{P} \land \text{Q}) \land \text{R} &\equiv \text{P} \land (\text{Q} \land \text{R}) \end{aligned} \\ \text{Commutativity} && \begin{aligned} \text{P} \lor \text{Q} &\equiv \text{Q} \lor \text{P} \\ \text{P} \land \text{Q} &\equiv \text{Q} \land \text{P} \end{aligned} \\ \text{Complementarity} && \begin{aligned} \text{P} \land \lnot\text{P} &\equiv \text{F} \\ \lnot\text{T} &\equiv \text{F} \\ \text{P} \lor \lnot\text{P} &\equiv \text{T} \\ \lnot\text{F} &\equiv \text{T} \end{aligned} \\ \text{Conditionality} && \begin{aligned} \text{P} \rightarrow \text{Q} &\equiv \lnot\text{P} \lor \text{Q} \\ \text{P} \leftrightarrow \text{Q} &\equiv (\text{P} \rightarrow \text{Q}) \land (\text{Q} \rightarrow \text{P}) \end{aligned} \\ \text{Distributivity} && \begin{aligned} \text{P} \lor (\text{Q} \land \text{R}) &\equiv (\text{P} \lor \text{Q}) \land (\text{P} \lor \text{R}) \\ \text{P} \land (\text{Q} \lor \text{R}) &\equiv (\text{P} \land \text{Q}) \lor (\text{P} \land \text{R}) \end{aligned} \\ \text{Idempotency} && \begin{aligned} \text{P} \lor \text{P} &\equiv \text{P} \\ \text{P} \land \text{P} &\equiv \text{P} \end{aligned} \\ \text{Identity} && \begin{aligned} \text{P} \lor \text{F} &\equiv \text{P} \\ \text{P} \land \text{T} &\equiv \text{P} \end{aligned} \\ \text{De Morgan's} && \begin{aligned} \lnot(\text{P} \lor \text{Q}) &\equiv \lnot\text{P} \land \lnot\text{Q} \\ \lnot(\text{P} \land \text{Q}) &\equiv \lnot\text{P} \lor \lnot\text{Q} \end{aligned} \\ \text{Domination} && \begin{aligned} \text{P} \land \text{F} &\equiv \text{F} \\ \text{P} \lor \text{T} &\equiv \text{T} \end{aligned} \\ \text{Double Negation} && \begin{aligned} \lnot\lnot\text{P} &\equiv \text{P} \end{aligned} \\ \end{aligned} \)

De Morgan’s Laws #

\( \begin{aligned} \lnot(\text{P} \lor \text{Q}) &\equiv \lnot\text{P} \land \lnot\text{Q} \\ \lnot(\text{P} \land \text{Q}) &\equiv \lnot\text{P} \lor \lnot\text{Q} \\ \end{aligned} \)

Proof by truth table

\( \begin{array}{cc|cc|ccc} \text{P} & \text{Q} & \text{P} \lor \text{Q} & \lnot(\text{P} \lor \text{Q}) & \lnot\text{P} & \lnot\text{Q} & \lnot\text{P} \land \lnot\text{Q} \\ \hline \text{T} & \text{T} & \text{T} & \color{blue}\text{F} & \text{F} & \text{F} & \color{blue}\text{F} \\ \text{T} & \text{F} & \text{T} & \color{blue}\text{F} & \text{F} & \text{T} & \color{blue}\text{F} \\ \text{F} & \text{T} & \text{T} & \color{blue}\text{F} & \text{T} & \text{F} & \color{blue}\text{F} \\ \text{F} & \text{F} & \text{F} & \color{blue}\text{T} & \text{T} & \text{T} & \color{blue}\text{T} \\ \end{array} \)

\( \begin{array}{cc|cc|ccc} \text{P} & \text{Q} & \text{P} \land \text{Q} & \lnot(\text{P} \land \text{Q}) & \lnot\text{P} & \lnot\text{Q} & \lnot\text{P} \lor \lnot\text{Q} \\ \hline \text{T} & \text{T} & \text{T} & \color{blue}\text{F} & \text{F} & \text{F} & \color{blue}\text{F} \\ \text{T} & \text{F} & \text{F} & \color{blue}\text{T} & \text{F} & \text{T} & \color{blue}\text{T} \\ \text{F} & \text{T} & \text{F} & \color{blue}\text{T} & \text{T} & \text{F} & \color{blue}\text{T} \\ \text{F} & \text{F} & \text{F} & \color{blue}\text{T} & \text{T} & \text{T} & \color{blue}\text{T} \\ \end{array} \)

\( \therefore \begin{aligned} \lnot(\text{P} \lor \text{Q}) &\equiv \lnot\text{P} \land \lnot\text{Q} \\ \lnot(\text{P} \land \text{Q}) &\equiv \lnot\text{P} \lor \lnot\text{Q} \\ \end{aligned} \)

\(\blacksquare\)

Substitution #

If two propositions are logically equivalent, then one can be substituted for the other within a more complex proposition: the compound proposition after the substitution is logically equivalent to the compound proposition before the substitution. Substitution gives an alternate way of showing that two propositions are logically equivalent. If one proposition can be obtained from another by a series of substitutions using equivalent expressions, then the two propositions are logically equivalent.

\( \begin{aligned} \text{P} \rightarrow \text{Q} &\equiv \lnot\text{P} \lor \text{Q} \\ \therefore (\text{P} \lor \text{R}) \land (\text{P} \rightarrow \text{Q}) &\equiv (\text{P} \lor \text{R}) \land (\lnot\text{P} \lor \text{Q}) \\ \end{aligned} \)

\( \begin{aligned} \text{P} &\equiv \lnot\text{T} \land \text{R} \\ \text{Q} &\equiv \lnot\text{S} \lor \text{T} \\ \text{P} \rightarrow \text{Q} &\equiv \lnot\text{P} \lor \text{Q} \\ \therefore (\lnot\text{T} \land \text{R}) \rightarrow (\lnot\text{S} \lor \text{T}) &\equiv \lnot(\lnot\text{T} \land \text{R}) \lor (\lnot\text{S} \lor \text{T}) \\ \end{aligned} \)

Predicate Logic (RL)#

First-Order Logic or Quantificational Logic

Predicates #

A logical statement (or proposition) whose truth value is a function of one or more variables is called a predicate \(P(x_1,...,x_n)\).

For example

Let \(P(x):x\,\text{is even}\) be a predicate. Then the proposition \(P(1)\) is false but the proposition \(P(2)\) is true.
Let \(Q(x,y):x^2=y\) be a predicate. Then the proposition \(Q(5,25)\) is true.
Let \(R(x,y,z):x+y=z\) be a predicate. Then the proposition \(R(2,3,6)\) is false.

Quantifiers #

Universal Quantifiers #

The statement \(\forall x\,P(x)\) (“for all/every x, it is the case that P(x)”) asserts that \(P(x)\) is true for every possible value for \(x\) in its domain.

The symbol \(\forall\) is called the universal quantifier.

The statement \(\forall x\,P(x)\) is called a universally quantified statement.

\(\forall x\,P(x)\) is a proposition because it is either true or false.

\(\forall x\,P(x)\) is true if and only if \(P(n)\) is true for every \(n\) in the domain of variable \(x\).

If the domain is a finite set \(\{a_1,a_2,...,a_k\}\) then

\(\forall x\,P(x) \equiv P(a_1) \land P(a_2) \land ... \land P(a_k)\)

To demonstrate that \(\forall x\,P(x)\) is true requires demonstrating that \(P(a_1) \land P(a_2) \land ... \land P(a_k)\) is true. Some universally quantified statements can be shown to be true by showing that the predicate holds for an arbitrary element from the domain (where an arbitrary element means nothing is assumed about the element other than the fact that it is in the domain).

A counterexample for a universally quantified statement is an element in the domain for which the predicate is false. A single counterexample is sufficient to show that a universally quantified statement is false.

Example #

Let the domain of \(x\) be the set of positive integers.

\( \begin{aligned} \forall x \, \left( \frac{1}{x+1} \lt 1 \right) \end{aligned} \)

is true because the inequality holds when \(x\) is assigned an arbitrary value from the set of positive integers.

\( \begin{aligned} 0 &\lt x && \text{true for all positive integers} \, x \\ 1 &\lt x + 1 && \text{add one to both sides} \\ \frac{1}{x+1} &\le 1 && \text{divide both sides by} \, x+1 \\ \end{aligned} \)

\(\blacksquare\)

Existential Quantifiers #

The statement \(\exists x\,P(x)\) (“there exists an x, such that P(x)”) asserts that \(P(x)\) is true for at least one possible value for \(x\) in its domain.

The symbol \(\forall\) is called the existential quantifier.

The statement \(\forall x\,P(x)\) is called an existentially quantified statement.

\(\forall x\,P(x)\) is a proposition because it is either true or false.

\(\forall x\,P(x)\) is true if and only if \(P(n)\) is true for at least one \(n\) in the domain of variable \(x\).

If the domain is a finite set \(\{a_1,a_2,...,a_k\}\) then

\(\exists x\,P(x) \equiv P(a_1) \lor P(a_2) \lor ... \lor P(a_k)\)

To demonstrate that \(\exists x\,P(x)\) is true requires demonstrating that \(P(a_1) \lor P(a_2) \lor ... \lor P(a_k)\) is true. Some existentially quantified statements can be shown to be false by showing that the predicate is false for an arbitrary element from the domain (where an arbitrary element means nothing is assumed about the element other than the fact that it is in the domain).

Example #

Let the domain of \(x\) be the set of positive integers.

\( \begin{aligned} \exists x \, (x + 1 \lt x) \end{aligned} \)

is false because no positive integer satisfies the expression \(x + 1 \lt x\).

\( \begin{aligned} x + 1 &\lt x && \\ 1 &\not\lt 0 && \text{subtract x from both sides} \\ \end{aligned} \)

\(\blacksquare\)

Quantified Propositions #

A logical statement that includes a universal or existential quantifier is called a quantified statement.

Order of Operations

Quantifiers
Logical Operations

\(\forall x \, P(x) \land Q(x)\) is \((\forall x \, P(x)) \land Q(x)\), not \(\forall x \, (P(x) \land Q(x))\)

Variables #

Free Variables #

A variable \(x\) is the predicate \(P(x)\) is called a free variable because the variable is free to take on any value in the domain.

Bound Variables #

The variable \(x\) in the statement \(\forall x \, P(x)\) is a bound variable because the variable is bound to a quantifier.

A statement with no free variables is a proposition because the statement’s truth value can be determined.

Example #

In the statement \((\forall x \, P(x)) \land Q(x)\), the variable \(x\) in \(P(x)\) is bound by the universal quantifier, but the variable \(x\) in \(Q(x)\) is not bound by the universal quantifier. Therefore, the statement \((\forall x \, P(x)) \land Q(x)\) is not a proposition.

Example #

In the proposition

\(\forall x \, (P(x) \land Q(x))\)

the universal quantifier binds both occurrences of the variable \(x\). Therefore, the statement \(\forall x \, (P(x) \land Q(x))\) is a proposition.

Logical Equivalence of quantified propositions #

Two quantified propositions have the same logical meaning if they have the same truth value regardless of the value fo the predicates for the elements in the domain.

[Example]

Domain: a set of people invited to a party

Predicates:

\( \begin{aligned} P(x) &: x \, \text{came to the party} \\ S(x) &: x \, \text{was sick} \\ \end{aligned} \)

\( \begin{array}{c|cc} x & S(x) & P(x) \\ \hline \text{Joe} & \text{F} & \text{T} \\ \text{Theodore} & \text{T} & \text{F} \\ \text{Gertrude} & \text{F} & \text{T} \\ \text{Samuel} & \text{F} & \text{F} \\ \end{array} \)

\( \begin{aligned} P(\text{Gertrude}) &= \text{true} && \text{Gertrude came to the party.} \\ S(\text{Gertrude}) &= \text{false} && \text{Gertrude was sick.} \\ \forall x \, \lnot S(x) &= \text{false} && \text{Everyone was not sick.} \\ \exists x \, (S(x) \lor P(x)) &= \text{true} && \text{Someone was sick or came to the party.} \\ \exists x \, (S(x) \land P(x)) &= \text{false} && \text{Someone was sick and came to the party.} \\ \exists x \, S(x) \land \exists x \, P(x) &= \text{true} && \text{Someone was sick and someone came to the party.} \\ \end{aligned} \)

De Morgan’s laws for quantified propositions #

Let \(\{a_1,...,a_k\}\) be a finite domain of discourse.

De Morgan’s Law for Universally Quantified Statements

\( \begin{aligned} \lnot \forall x \, P(x) &\equiv \exists x \, \lnot P(x) \\ \exists x \, \lnot P(x) &\equiv \lnot P(a_1) \lor \lnot P(a_2) \lor ... \lor \lnot P(a_n) \\ \lnot P(a_1) \lor \lnot P(a_2) \lor ... \lor \lnot P(a_n) &\equiv \lnot(P(a_1) \land P(a_2) \land ... \land P(a_n)) \\ \lnot(P(a_1) \land P(a_2) \land ... \land P(a_n)) &\equiv \lnot \forall x \, P(x) \\ \end{aligned} \)

De Morgan’s Law for Existentially Quantified Statements

\( \begin{aligned} \lnot \exists x \, P(x) &\equiv \forall x \, \lnot P(x) \\ \forall x \, \lnot P(x) &\equiv \lnot P(a_1) \land \lnot P(a_2) \land ... \land \lnot P(a_n) \\ \lnot P(a_1) \land \lnot P(a_2) \land ... \land \lnot P(a_n) &\equiv \lnot(P(a_1) \lor P(a_2) \lor ... \lor P(a_n)) \\ \lnot(P(a_1) \lor P(a_2) \lor ... \lor P(a_n)) &\equiv \lnot \exists x \, P(x) \\ \end{aligned} \)

Nested Quantifiers #

If a predicate has more than one variable, then each variable must be bound by a separate quantifier. A logical expression with more than one quantifier that bind different variables in the same predicate is said to have nested quantifiers. The logical expression is a proposition if all the variables are bound.

\( \begin{aligned} \forall x \exists y P(x, y) && \text{proposition} && \text{x and y are bound} \\ \forall x Q(x,y) && \text{predicate} && \text{x is bound, y is free} \\ \exists y \exists z T(x, y, z) && \text{predicate} && \text{y and z are bound, x is free} \\ \end{aligned} \)

Example #

Consider the predicate

\(M(x, y) : \text{x sent an email to y}\)

Then the proposition

\( \forall x \forall y M(x, y) : \text{everyone sent an email to everyone} \)

(for all x in the domain, x sent an email to y, for all y in the domain (where x and y may be the same individual))

is true if \(M(x, y) = 1\) for every pair \((x, y) \in D\)

or false if \(M(x, y) = 0\) for at least one pair \((x, y) \in D\)

and the proposition

\( \exists x \exists y M(x, y) : \text{there is an individual who sent an email to some individual} \)

(for some x in the domain, x sent an email to y, for some y in the domain (where x and y may be the same individual))

is true if \(M(x, y) = 1\) for some pair \((x, y) \in D\)

or false if \(M(x, y) = 1\) for no pair \((x, y) \in D\)

Double universal, proof of falsity by counterexample #

Consider the proposition

\( P(x, y) = \forall x \forall y (xy = 1) \in \mathbb{Z}^+\cup\{0\} \)

English

“For any nonnegative integer \(x\) it is the case that for any nonnegative integer \(y\) the product of \(x\) and \(y\) is unity.”
“The product of any two nonnegative integers is unity.”

Proof by counterexample

The pair \((x = 1, y = 2)\) is a counterexample.
Therefore, \(P\) is false.

Double universal, proof of truth by no counterexample #

Consider the proposition

\( P(x, y) = \forall x \forall y ((x + y \ne x) \lor (y = 0)) \in \mathbb{Z}^+\cup\{0\} \)

English

“For any pair of nonnegative integers \((x, y)\) it is either the case that \(y = 0\) or \(x + y \ne x\).”

Proof

On the one hand, let \(y\) be some positive integer. Then it follows that \(x + y\) must not be equal to \(x\).
On the other hand, let \(x + y = x\). Then it follows that \(y\) must be equal to \(0\).
Any pair satisfies the proposition.
Therefore, \(P\) is true.

Double existential, proof of truth by example #

Consider the proposition

\( P(x, y) = \exists x \exists y (xy = 1) \in \mathbb{Z}^+\cup\{0\} \)

English

“There is some nonnegative integer \(x\) such that for some nonnegative integer \(y\) the product of \(x\) and \(y\) is unity.”
“There are two nonnegative integers whose product is unity.”

Proof by example

The pair \((x = 1, y = 1)\) is an example.
Therefore, \(P\) is true.

Double existential, proof of falsity by no example #

Consider the proposition

\( P(x, y) = \exists x \exists y ((x + y = x) \land (y \ne 0)) \in \mathbb{Z}^+\cup\{0\} \)

English

“There is a pair of nonnegative integers \((x, y)\) such that \(x + y = x\) but \(y \ne 0\).”

Proof

Let \(x + y = x\) be true.
Then it follows that \(y\) must be equal to \(0\).
But it is required that \(y \ne 0\).
Contradiction: \(y = 0 \land y \ne 0\).
No pair satisfies the proposition.
Therefore, \(P\) is false.

Example #

Consider the predicate

\( M(x, y) : \text{x sent an email to y} \)

\( \exists x \forall y M(x, y) \)

“Someone sent an email to everyone, including themselves.”

“For some x in the domain, x sent an email to each y in the domain.”

\( \forall x \exists y M(x, y) \)

“Everyone sent an email to someone, even if themself.”

“For each x in the domain, x sent an email to some y in the domain.”

Universal-existential, proof of truth by no counterexample #

Consider the proposition

\( P(x, y) = \forall x \exists y (x + y = 0) \in \mathbb{Z} \)

English

“For any integer \(x\) it is the case that there is some integer \(y\) such that the sum of \(x\) and \(y\) is zero.”
“For each integer \(x\), \(x + y = 0\) for some integer \(y\).”
“Any integer can be added to an integer to give you zero.”

Proof

Let \(x\) be an integer.
Then \(x + y = 0\) when \(y = -x\).
Any pair \((x, -x)\) satisfies the proposition.
Therefore, \(P\) is true.

Existential-universal, proof of falsity by counterexample #

Consider the proposition

\( P(x, y) = \exists x \forall y (x + y = 0) \in \mathbb{Z} \)

English

“There is some integer \(x\) such that for any integer \(y\) the sum of \(x\) and \(y\) is zero.”
“For some integer \(x\), \(x + y = 0\) for any integer \(y\).”
“There is an integer where adding it to any integer gives you zero.”

Proof

Let \(x\) be some integer.
Then \(x + y \ne 0\) for an integer \(y = -x + 1\).
The pair \((x, y = -x + 1)\) is a counterexample.
Therefore, \(P\) is false.

Universal-existential, proof of falsity by counterexample #

Consider the proposition

\( P(x, y) = \forall x \exists y (y^2 = x) \in \mathbb{Z} \)

English

“For each integer \(x\), \(x = y^2\) for some integer \(y\).”
“Each integer is the square of some integer.”

Proof

Let \(x = 2\).
Then \(y = \sqrt{2} \not\in \mathbb{Z}\).
\(x = 2\) is a counterexample.
Therefore, \(P\) is false.

Existential-universal, proof of truth by no counterexample #

Consider the proposition

\( P(x, y) = \exists x \forall y (x + y = y) \in \mathbb{Z} \)

English

“There is some integer \(x\) such that for any integer \(y\) the sum of \(x\) and \(y\) is \(y\).”
“For some integer \(x\), \(x + y = y\) for any integer \(y\).”
“Some integer is the additive identity element over the integers.”

Proof

Let \(x = 0\).
Then \(0 + y = y\) for any integer \(y\).
When \(x = 0\), all \(y\) satisfy the proposition.
Therefore, \(P\) is true.

Example #

Consider the proposition

\( P(x, y) = \forall x \forall y (xy = 1) \in \mathbb{R} \)

English

For every real number \(x\) it is the case that for any real number \(y\) the product of \(x\) and \(y\) is unity.
The product of any two real numbers is unity.

Proof

Let \(x = 0\).
Then \(xy = 0\) for any \(y\).
\(x = 0\) is a counterexample.
Therefore, \(P\) is false.

Consider the proposition

\( P(x, y) = \exists x \forall y (xy = 1) \in \mathbb{R} \)

English

There is some real number \(x\) such that for any real number \(y\) the product of \(x\) and \(y\) is unity.
There is a real number whose product with any real number is unity.

Proof

Let \(x = 0\).
Then \(xy = 0\) for any \(y\).
\(x = 0\) is a counterexample.
Therefore, \(P\) is false.

Consider the proposition

\( P(x, y) = \exists x \forall y (xy = y) \in \mathbb{R} \)

English

There is a real number \(x\) such that for any real number \(y\) the product of \(x\) and \(y\) is \(y\).
Some real number is the multiplicative identity element.

Proof

Let \(x = 1\).
Then \(xy = y\) for any \(y\).
\(x = 1\) is a example.
Therefore, \(P\) is true.

Consider the proposition

\( P(x, y) = \forall x \exists y (x^2 = y) \in \mathbb{R} \)

English

For any real number \(x\) it is the case that there is some real number \(y\) that is the square of \(x\).
The square of a real number is a real number.
The squaring operation is closed over the real numbers.

Proof

Let \(x \in \mathbb{R}\).
Then \(x^2 = y \in \mathbb{R}\).
Therefore, \(P\) is true.

De Morgan’s laws for nested quantifiers #

\( \begin{aligned} \lnot \forall x \forall y P(x, y) &\equiv \exists x \exists y \lnot P(x, y) \\ \lnot \forall x \exists y P(x, y) &\equiv \exists x \forall y \lnot P(x, y) \\ \lnot \exists x \forall y P(x, y) &\equiv \forall x \exists y \lnot P(x, y) \\ \lnot \exists x \exists y P(x, y) &\equiv \forall x \forall y \lnot P(x, y) \\ \end{aligned} \)

Example #

Consider the predicate

\( L(x, y) : \text{x likes y} \in \text{the set of all students in a school} \)

Then the following quantified propositions read

\( \begin{aligned} &\exists x \forall y L(x, y) && \text{someone likes everyone, including themself} \\ &\lnot \exists x \forall y L(x, y) && \text{it is not the case that someone likes everyone, including themself} \\ = &\forall x \lnot \forall y L(x, y) && \text{no one likes everyone (even if the only person they don't like is themself)} \\ = &\forall x \exists y \lnot L(x, y) && \text{everyone dislikes someone (even if the person they dislike is themself)} \\ \end{aligned} \)

Example #

\( \begin{aligned} &\lnot \exists x \exists y (\lnot P(x) \land Q(x)) && \\ \equiv &\forall x \lnot \exists y (\lnot P(x) \land Q(x)) && \text{De Morgan} \\ \equiv &\forall x \forall y \lnot (\lnot P(x) \land Q(x)) && \text{De Morgan} \\ \equiv &\forall x \forall y (P(x) \lor \lnot Q(x)) && \text{De Morgan} \\ \end{aligned} \)

Expressing universality sans identity in quantified statements #

Let \(P\) be a predicate. Then the following proposition predicates \(P\) of each pair \((x, y)\) except where \(x = y\).

\( \boxed{ \forall x \forall y ((x \ne y) \rightarrow P(x, y)) } \)

Example #

Consider the predicate

\( M(x, y) : \text{x sent an email to y} \in \{\text{A,B,C,D}\} \)

with the following truth table

\( \begin{array}{c|cc} & \text{A} & \text{B} & \text{C} & \text{D} \\ \hline \text{A} & \color{red}\text{F} & \text{T} & \text{T} & \text{T} \\ \text{B} & \text{T} & \color{red}\text{F} & \text{T} & \text{T} \\ \text{C} & \text{T} & \text{T} & \color{red}\text{F} & \text{T} \\ \text{D} & \text{T} & \text{T} & \text{T} & \color{red}\text{F} \\ \end{array} \)

\( \begin{aligned} \forall x \forall y M(x, y) && \text{false} && \text{Everyone sent an email to everyone, including themself.} \\ \forall x \forall y ((x \ne y) \rightarrow M(x, y)) && \text{true} && \text{Everyone sent an email to everyone else.} \\ \end{aligned} \)

\( \begin{aligned} & \forall x \forall y M(x, y) \\ \equiv & \forall y M(A, y) \land \forall y M(B, y) \land \forall y M(C, y) \land \forall y M(D, y) \\ \equiv & M(A, A) \land M(B, A) \land M(C, A) \land M(D, A) \land M(A, C) \land M(B, C) \land M(C, C) \land M(D, C) \land M(A, D) \land M(B, D) \land M(C, D) \land M(D, D) \land M(A, B) \land M(B, B) \land M(C, B) \land M(D, B) \\ \equiv & \text{F} \land \text{T} \land \text{T} \land \text{T} \land \text{T} \land \text{F} \land \text{T} \land \text{T} \land \text{T} \land \text{T} \land \text{F} \land \text{T} \land \text{T} \land \text{T} \land \text{T} \land \text{F} \\ \equiv & \text{F} \end{aligned} \)

\( \begin{aligned} & \forall x \forall y ((x \ne y) \rightarrow M(x, y)) \\ \equiv & \forall y ((A \ne y) \rightarrow M(A, y)) \land \forall y ((B \ne y) \rightarrow M(B, y)) \land \forall y ((C \ne y) \rightarrow M(C, y)) \land \forall y ((D \ne y) \rightarrow M(D, y)) \\ \equiv & ((A \ne A) \rightarrow M(A, A)) \land ((A \ne B) \rightarrow M(A, B)) \land ((A \ne C) \rightarrow M(A, C)) \land ((A \ne D) \rightarrow M(A, D)) \land ((B \ne A) \rightarrow M(B, A)) \land ((B \ne B) \rightarrow M(B, B)) \land ((B \ne C) \rightarrow M(B, C)) \land ((B \ne D) \rightarrow M(B, D)) \land ((C \ne A) \rightarrow M(C, A)) \land ((C \ne B) \rightarrow M(C, B)) \land ((C \ne C) \rightarrow M(C, C)) \land ((C \ne D) \rightarrow M(C, D)) \land ((D \ne A) \rightarrow M(D, A)) \land ((D \ne B) \rightarrow M(D, B)) \land ((D \ne C) \rightarrow M(D, C)) \land ((D \ne D) \rightarrow M(D, D)) \\ \equiv & (\text{F} \rightarrow \text{F}) \land (\text{T} \rightarrow \text{T}) \land (\text{T} \rightarrow \text{T}) \land (\text{T} \rightarrow \text{T}) \land (\text{T} \rightarrow \text{T}) \land (\text{F} \rightarrow \text{F}) \land (\text{T} \rightarrow \text{T}) \land (\text{T} \rightarrow \text{T}) \land (\text{T} \rightarrow \text{T}) \land (\text{T} \rightarrow \text{T}) \land (\text{F} \rightarrow \text{F}) \land (\text{T} \rightarrow \text{T}) \land (\text{T} \rightarrow \text{T}) \land (\text{T} \rightarrow \text{T}) \land (\text{T} \rightarrow \text{T}) \land (\text{F} \rightarrow \text{F}) \\ \equiv & \text{T} \land \text{T} \land \text{T} \land \text{T} \land \text{T} \land \text{T} \land \text{T} \land \text{T} \land \text{T} \land \text{T} \land \text{T} \land \text{T} \land \text{T} \land \text{T} \land \text{T} \land \text{T} \\ \equiv & \text{T} \end{aligned} \)

Example #

Consider the predicate

\( M(x, y) : \text{x sent an email to y} \in \{\text{A,B,C,D}\} \)

with the following truth table

\( \begin{array}{c|cc} M & \text{A} & \text{B} & \text{C} & \text{D} \\ \hline \text{A} & \text{F} & \text{F} & \color{blue}\text{T} & \text{F} \\ \text{B} & \text{F} & \color{blue}\text{T} & \text{F} & \text{F} \\ \text{C} & \text{F} & \text{F} & \text{F} & \color{blue}\text{T} \\ \text{D} & \text{F} & \color{blue}\text{T} & \text{F} & \text{F} \\ \end{array} \)

\( \begin{aligned} \forall x \exists y M(x, y) && \text{true} && \text{Everyone sent an email to someone (even if it was to themself).} \\ \forall x \exists y ((x \ne y) \land M(x, y)) && \text{false} && \text{Everyone sent an email to someone else.} \\ \end{aligned} \)

with the following truth table

\( \begin{array}{c|cc} M & \text{A} & \text{B} & \text{C} & \text{D} \\ \hline \text{A} & \text{F} & \text{F} & \color{blue}\text{T} & \text{F} \\ \text{B} & \text{F} & \text{F} & \color{blue}\text{T} & \text{F} \\ \text{C} & \text{F} & \text{F} & \text{F} & \color{blue}\text{T} \\ \text{D} & \text{F} & \color{blue}\text{T} & \text{F} & \text{F} \\ \end{array} \)

\( \begin{aligned} \forall x \exists y M(x, y) && \text{true} && \text{Everyone sent an email to someone (even if it was to themself).} \\ \forall x \exists y ((x \ne y) \land M(x, y)) && \text{true} && \text{Everyone sent an email to someone else.} \\ \end{aligned} \)

Expressing uniqueness in quantified statements #

Let \(P\) be a predicate. Then the following proposition predicates \(P\) of \(x\) and only \(x\).

\( \boxed{ \exists x (P(x) \land \forall y ((x \ne y) \rightarrow \lnot P(y))) } \)

An existentially quantified statement evaluates to true even if there is more than one element in the domain that causes the predicate to evaluate to true.

For example, if the domain is a set of people who attend a meeting and the predicate

\(L(x) : \text{x came late to the meeting}\)

then the quantified proposition

\( \begin{aligned} \exists x L(x) && \text{someone came late to the meeting} \end{aligned} \)

is true if there are one, two, or more people who came late to the meeting.

To express that one and only one person came late to the meeting

\( \begin{aligned} \exists x (L(x) \land \forall y ((x \ne y) \rightarrow \lnot L(y))) && \text{exactly one person came late to the meeting} \end{aligned} \)

Moving quantifiers #

Example #

Let the domain be a set of people.

1

Let \(M(x, y) : \text{x is married to y}\) and \(A(x) : \text{x is an adult}\) be predicates.

\( \begin{aligned} \forall x (A(x) \rightarrow \exists y M(x, y)) \equiv \forall x \exists y (A(x) \rightarrow M(x, y)) && \text{since y does not appear in the predicate A(x)} \end{aligned} \)

“every adult is married to someone” or “for every person \(x\), if \(x\) is an adult then there is a person \(y\) to whom \(x\) is married”

2

Let \(M(x, y) : \text{x is married to y}\) and \(A(x) : \text{x is an adult}\) be predicates.

\( \begin{aligned} & \forall x (A(x) \rightarrow (\exists y (M(x, y) \land \forall z ((z \ne y) \rightarrow \lnot M(x, z))))) \\ \equiv & \forall x \exists y \forall z (A(x) \rightarrow (M(x, y) \land ((z \ne y) \rightarrow \lnot M(x, z)))) && \text{since y does not appear in the predicate A(x) and z does not appear in the predicates A(x), M(x, y)} \end{aligned} \)

“every adult is married to exactly one adult” or “for every person \(x\), if \(x\) is an adult then there is a person \(y\) to whom \(x\) is married and for every person \(z\), if \(z\) is not the \(y\) to whom \(x\) is married then \(x\) is not married to \(z\)”

Logical Argument #

A logical argument is a sequence of propositions \(p_1, p_2, \dots, p_n\) called hypotheses followed by a final proposition \(c\) called the conclusion.

\( \begin{aligned} & p_1 \\ & p_2 \\ & \vdots \\ & p_n \\ \hline \therefore \,\, & c \\ \end{aligned} \)

Validity of a logical argument #

An argument is valid if the conclusion is true whenever the hypotheses are true; otherwise, the argument is invalid.

In other words, the argument is valid whenever the following proposition is a tautology.

\( (p_1 \land p_2 \land \dots \land p_n) \rightarrow c \)

To show that an argument is invalid, demonstrate an assignment of truth values to its variables that makes the hypotheses true but the conclusion false.

By commutativity, rearranging the hypotheses does not change the validity of the argument.

Example #

The following two representations are of the same argument.

\( \begin{aligned} & p \\ & p \rightarrow q \\ \hline \therefore \,\, & q \\ \end{aligned} \)

\( \begin{aligned} & p \rightarrow q \\ & p \\ \hline \therefore \,\, & q \\ \end{aligned} \)

The argument is valid so long as the following proposition is a tautology.

\( (p \land (p \rightarrow q)) \rightarrow q \)

In order to use a truth table to establish the validity of an argument, the truth table is constructed for all the hypotheses and the conclusion. Each row in which all the hypotheses are true is examined. If the conclusion is true in each of the examined rows, then the agument is valid. If there is any row in which all the hypotheses are true but the conclusion is false, then the argument is invalid.

Proof by truth table

\( \begin{array}{cc|cccc} p & q & p \rightarrow q \\ \hline \color{blue}\text{T} & \color{green}\text{T} & \color{blue}\text{T} \\ \text{T} & \text{F} & \text{F} \\ \text{F} & \text{T} & \text{T} \\ \text{F} & \text{F} & \text{T} \\ \end{array} \)

The argument is valid.

\(\blacksquare\)

Example #

Determine the validity of the following argument.

\( \begin{aligned} & p \rightarrow q \\ & p \lor q \\ \hline \therefore \,\, & q \\ \end{aligned} \)

The argument is valid if the following proposition is a tautology.

\( ((p \rightarrow q) \land (p \lor q)) \rightarrow q \)

Proof by truth table

\( \begin{array}{cc|cc} p & q & p \rightarrow q & p \lor q \\ \hline \text{T} & \color{green}\text{T} & \color{blue}\text{T} & \color{blue}\text{T} \\ \text{T} & \text{F} & \text{F} & \text{T} \\ \text{F} & \color{green}\text{T} & \color{blue}\text{T} & \color{blue}\text{T} \\ \text{F} & \text{F} & \text{T} & \text{F} \\ \end{array} \)

The argument is valid.

\(\blacksquare\)

Example #

Determine the validity of the following argument.

\( \begin{aligned} & \lnot p \\ & p \rightarrow q \\ \hline \therefore \,\, & \lnot q \\ \end{aligned} \)

The argument is valid if the following proposition is a tautology.

\( (\lnot p \land (p \rightarrow q)) \rightarrow \lnot q \)

The validity of an argument can be established by applying both the rules of inference and the laws of propositional logic in a logical proof.

A logical proof of an argument is a sequence of steps, each of which consists of a proposition and a justification. If the proposition in a step is a hypothesis, the justification is “hypothesis”; otherwise, the proposition must follow from the previous steps by applying one rule of inference or law of logic: the justification indicates which rule or law is used and the previous steps to which it is applied. The proposition in the last step in the proof must be the conclusion of the argument being proven.

Example #

Determine the validity of the following argument.

\( \begin{aligned} & (p \lor r) \rightarrow q \\ & q \rightarrow t \\ & r \\ \hline \therefore \,\, & t \\ \end{aligned} \)

Logical proof

\( \begin{aligned} 1 && r && \text{hypothesis} \\ 2 && p \lor r && \text{addition, 1} \\ 3 && (p \lor r) \rightarrow q && \text{hypothesis} \\ 4 && q && \text{modus ponens, 2, 3} \\ 5 && q \rightarrow t && \text{hypothesis} \\ 6 && t && \text{modus ponens, 4, 5} \\ \end{aligned} \)

The argument is valid.

\(\blacksquare\)

Rules of Inference for Quantified Propositions #

In order to apply the rules of inference to quantified expressions, the quantifier needs to be removed by plugging in a value from the domain to replace the variable \(x\).

The rules only apply to non nested quantifiers: applying the rules to nested quantifiers would require more constraints on which rules could be applied in particular situations.

Elements

A value that can be plugged in for a variable \(x\) is called an element of the domain of \(x\). Elements of the domain can be defined in a hypothesis of an argument. Elements of the domain can also be introduced within a proof in which case they are given generic names such as \(c\) or \(d\). There are two types of named elements used in logical proofs: an arbitrary element of a domain has no special properties other than those shared by all the elements of the domain; a particular element of the domain may have properties that are not shared by all the elements of the domain. Every domain element referenced in a proof must be defined on a separate line of the proof. If the element is defined in a hypothesis, it is always a particular element and the definition of that element in the proof is labeled “hypothesis”. If an element is introduced for the first time in the proof, the definition is labeled “element definition” and must specify whether the element is arbitrary or particular.

Instantiation

The rules existential instantiation and universal instantiation replace a quantified variable with an element of the domain.

Generalization

The rules existential generalization and universal generalization replace an element of the domain with a quantified variable.

Universal Instantiation #

\( \begin{aligned} & c && \text{an element, arbitrary or particular} \\ & \forall x P(x) \\ \hline \therefore \,\, & P(c) \\ \end{aligned} \)

Universal Generalization #

\( \begin{aligned} & c && \text{an arbitrary element} \\ & P(c) \\ \hline \therefore \,\, & \forall x P(x) \\ \end{aligned} \)

Existential Instantiation #

Each use of existential instantiation must define a new element with its own name.

\( \begin{aligned} & \exists x P(x) \\ \hline \therefore \,\, & (c \,\, \text{a particular element}) \land P(c) \\ \end{aligned} \)

Existential Generalization #

The argument is invalid.

\(\blacksquare\)

An argument with quantified propositions can be shown to be invalid by defining a domain and predicates for which the hypotheses are true but the conclusion is false.

Let the domain be \(\{c, d\}\).

\( \begin{array}{c|cc} x & P(x) & Q(x) \\ \hline c & \text{T} & \text{F} \\ d & \text{F} & \text{T} \\ \end{array} \)

\( \begin{aligned} \exists x P(x) & \equiv P(c) \lor P(d) \equiv \text{T} \lor \text{F} \equiv \text{T} \\ \exists x Q(x) & \equiv Q(c) \lor Q(d) \equiv \text{F} \lor \text{T} \equiv \text{T} \\ \exists x (P(x) \land Q(x)) & \equiv (P(c) \land Q(c)) \lor (P(d) \land Q(d)) \equiv (\text{T} \land \text{F}) \lor (\text{F} \land \text{T}) \equiv \text{F} \lor \text{F} \equiv \text{F} \\ \end{aligned} \)

Formal Languages #

Symbols #

A symbol is a mark made that can be made on piece of paper.

The symbols of a particular formal language should be related to a mathematical structure. Different interpretations of the symbols yield different conclusions regarding the truth of the formal statement.

Symbols

Constants
- Logical Symbols
  - Logical Connectives
  - Quantifiers
- Non Logical Symbols
  - Predicate/Relation Symbols (represents a property or relation)
    - equality
    - greater-than(-or-equal-to)
    - less-than(-or-equal-to)
  - Function Symbols
  - Individual Constant Symbols
Variables

Definition - first-order formal language #

A first-order language \(\mathfrak{L}\) is an infinite collection of distinct symbols, no one of which is properly contained in another, separated into the following categories.

Parentheses: \((\) \()\)
Connectives: \(\lor\) \(\lnot\)
Quantifier: \(\forall\)
Variables, one for each positive integer \(n\): \(v_1\) \(v_2\) \(\dots\) \(v_n\) \(\dots\) (the set of variable symbols is denoted \(Vars\))
Equality symbol: \(=\) (a particular binary relation symbol)
Constant symbols: some set of zero or more symbols
Function symbols: for each positive integer \(n\), some set of zero or more \(n\)-ary function symbols
Relation symbols: for each positive integer \(n\), some set of zero or more \(n\)-ary relation symbols

Note: Suppose a language contained both the constant symbol \(\hearts\) and the constant symbol \(\hearts\hearts\), which properly contains the former constant symbol. If the constant symbol \(\hearts\hearts\) showed up while a sequence of symbols was being read, it would be impossible to decide if it was one symbol or a sequence of two symbols. By not allowing symbols to be contained in other symbols, this type of confusion is avoided.

Functionally complete sets of logical connectives #

\(\{ \lnot, \lor \}\)

\( \begin{array}{cc|cc|cccc|cccc|cc|cc} p & q & \lnot p & \lnot q & p \lor q & \lnot p \lor q & p \lor \lnot q & \lnot p \lor \lnot q & \lnot(p \lor q) & \lnot(\lnot p \lor q) & \lnot(p \lor \lnot q) & \lnot(\lnot p \lor \lnot q) & p \lor \lnot p & \lnot(p \lor \lnot p) & \lnot(p \lor q) \lor \lnot(\lnot p \lor \lnot q) & \lnot(\lnot p \lor q) \lor \lnot(p \lor \lnot q) \\ \hline 1 & 1 & 0 & 0 & 1 & 1 & 1 & 0 & 0 & 0 & 0 & 1 & 1 & 0 & 1 & 0 \\ 1 & 0 & 0 & 1 & 1 & 0 & 1 & 1 & 0 & 1 & 0 & 0 & 1 & 0 & 0 & 1 \\ 0 & 1 & 1 & 0 & 1 & 1 & 0 & 1 & 0 & 0 & 1 & 0 & 1 & 0 & 0 & 1 \\ 0 & 0 & 1 & 1 & 0 & 1 & 1 & 1 & 1 & 0 & 0 & 0 & 1 & 0 & 1 & 0 \\ \hline & & & & & p \rightarrow q & p \leftarrow q & p \uparrow q & p \downarrow q & p \not\rightarrow q & p \not\leftarrow q & p \land q & p \top q & p \bot q & p \leftrightarrow q & p \oplus q \\ \end{array} \)

Definition - arity #

To say that a function symbol is \(n\)-ary or has arity \(n\) means that it is intended to represent a function of \(n\) variables.

Similarly, an \(n\)-ary relation symbol is intended to represent a relation on \(n\)-tuples of objects.

Formal language specification #

To specify a language, determine (and list) the constant symbols \(c_i\)’s, function symbols \(f_i^{a(f_i)}\)’s, and relation symbols \(R_i^{a(R_i)}\)’s (there can be uncountably many of each).

\( \mathfrak{L} \,\,\text{is}\,\, \{ c_1, c_2, \dots, f_1^{a(f_1)}, f_2^{a(f_2)}, \dots, R_1^{a(R_1)}, R_2^{a(R_2)}, \dots \} \)

The superscripts on the function symbols and the relation symbols indicate the arity of the associated symbols, so \(a\) is a mapping that assigns a natural number to a string that begins with an \(f\) or an \(R\), followed by a subscripted ordinal.

For example, the function symbol \(f_{17}^{233}\) says that the function associated with the 17th function symbol is a function of 233 variables.

Examples - formal languages #

\(\mathfrak{L}_G\) - a formal language for groups #

A group consists of a set and a binary operation that has certain properties including the existence of an identity element for the operation.

A language with one constant symbol \(0\) for the identity element, one binary function symbol \(+\), and no relation symbols.

\( \mathfrak{L}_G \,\,\text{is}\,\, \{ 0, + \} \)

A language with one constant symbol \(1\) for the identity element, one binary function symbol \(\cdot\), and one unary function symbol \(^{-1}\) which is designed to pick out the inverse of an element.

\( \mathfrak{L}_G \,\,\text{is}\,\, \{ 1, ^{-1}, \cdot \} \)

\(\mathfrak{L}_{ST}\) - a formal language for set theory #

\( \mathfrak{L}_{ST} \,\,\text{is}\,\, \{ \in \} \)

The language of set theory consists of one binary relation symbol \(\in\) which represents the elementhood relation: the interpretation of the string \(x \in y\) is that the set \(x\) is an element of the set \(y\).

It will be easier to define the relation symbol \(\subset\) and the constant symbol \(\varnothing\) in terms of more primitive symbols (not in terms of readability, but in terms of proving things about the language).

Definition by recursion - terms #

The point of having a language is to be able to make statements about certain kinds of mathematical systems. The statements of the language should have the ability to refer to objects in the mathematical structures under consideration. Therefore, some of the strings of the language need to refer to those objects. These strings are called the terms of \(\mathfrak{L}\).

If \(\mathfrak{L}\) is a language, a term of \(\mathfrak{L}\) is a nonempty finite string \(t\) of symbols from \(\mathfrak{L}\) such that either:

\(t\) is a variable, or
\(t\) is a constant symbol, or
\(t :\equiv ft_1t_2\dots t_n\) where \(f\) is an \(n\)-ary function symbol of \(\mathfrak{L}\) and each of the \(t_i\) is a term of \(\mathfrak{L}\) (read “\(t\) is \(ft_1t_2\dots t_n\)”)

The symbol \(:\equiv\) is not part of the language \(\mathfrak{L}\) but a metalinguistic symbol that means that the strings of \(\mathfrak{L}\)-symbols on each side of the \(:\equiv\) are identical.

The first and seconda clauses of the definition are the base cases.

The third clause of the definition is the recursive case: \(t\) is a term if it contains substrings that are terms. Since the substrings of \(t\) are shorter (contain fewer symbols) than \(t\), and as none of the symbols of \(\mathfrak{L}\) are made up of other symbols of \(\mathfrak{L}\), this causes no problems.

Example #

Let \(\mathfrak{L}\) be a language \(\{ \bar{0}, \bar{1}, \bar{2}, \dots, +, \cdot \}\) with one constant symbol for each natural number and two binary function symbols.

Then the following are terms of \(\mathfrak{L}\).
\(\overline{714}\)
\(+\bar{3}\bar{2}\)
\(\cdot + \bar{3}\bar{2}\bar{4}\)

\(\bar{1}\bar{2}\bar{3}\) is not a term of \(\mathfrak{L}\) but rather a sequence of three terms in a row.

Shorthand

The term \(+\bar{3}\bar{2}\) can be written in the more familiar form \(\bar{3} + \bar{2}\).
The term \(f\bar{1}\bar{2}\bar{3}\) can be written in the more familiar form \(f(\bar{1}, \bar{2}, \bar{3})\).

Unique Readability #

The property that strings have a unique parsing.

Unique readability holds for both terms and formulas.

Definition by recursion - well-formed formula #

The terms of \(\mathfrak{L}\) play the role of the nouns of the language. To make meaningful mathematical statements about some mathematical structure, we want to be able to make assertions about the objects of the structure. These assertions are the formulas of \(\mathfrak{L}\).

If \(\mathfrak{L}\) is a first-order language, a formula of \(\mathfrak{L}\) is a nonempty finite string \(\phi\) of symbols from \(\mathfrak{L}\) such that either:

Base Case (atomic formulas)

\(\phi :\equiv = t_1 t_2\) where \(t_1\) and \(t_2\) are terms of \(\mathfrak{L}\), or
\(\phi :\equiv Rt_1t_2\dots t_n\) where \(R\) is an \(n\)-ary relation symbol of \(\mathfrak{L}\) and \(t_1, t_2, \dots, t_n\) are all terms of \(\mathfrak{L}\), or

Recursive Case

\(\phi :\equiv (\lnot\alpha)\) where \(\alpha\) is a formula of \(\mathfrak{L}\), or
\(\phi :\equiv (\alpha \lor \beta)\) where \(\alpha\) and \(\beta\) are formulas of \(\mathfrak{L}\) (notice the use of infix notation for convenience here), or
\(\phi :\equiv (\forall v)(\alpha)\) where \(v\) is a variable and \(\alpha\) is a formula of \(\mathfrak{L}\)

A term is not a formula. If the terms are the nouns of the language, the formulas are the statements. Statements can be either true or false. Nouns cannot.

Proof by mathematical induction can be used to prove that something is true about every formula since the collection of formulas is defined recursively: the base case is used to verify that the theorem is true about every atomic formula (about every string that is known to be a formula from the base case of the definition); under the assumption that the theorem is true about simple formulas \(\alpha, \beta\), the inductive step of the proof proves that the theorem holds for a more complicated formula \(\phi\) that is generated by a recursive clause of the definition.

Quantifier scope #

If a formula \(\psi\) contains the subformula \((\forall v)(\alpha)\)–meaning that the string of symbols that constitute the formula \((\forall v)(\alpha)\) is a substring of the string of symbols that make up \(\psi\)–we say that the scope of the quantifier \(\forall\) is \(\alpha\). Any symbol in \(\alpha\) will be said to lie within the scope of the quantifier \(\forall\). A formula can have several different occurrences of the symbol \(\forall\), and each occurrence of the quantifier will have its own scope. Also, one quantifier can lie within the scope of another.

Atomic formula #

The atomic formulas of \(\mathfrak{L}\) are those formulas that satisfy clause (1) or (2) of the definition of a well-formed formula.

Ground expression #

A ground term is a term that does not contain variables.

A ground formula is a formula that does not contain variables.

A ground expression is a ground term or a ground formula.

Introduction

Contents