Propositional and Predicate Calculus

Logics are systems concerned with the relationships between statements. Two very important systems of logic are the propositional calculus and the predicate calculus, also sometimes known as zeroeth-order logic, and first-order logic, respectively.

Propositional Calculus

Propositional calculus is the system of logic concerned with relationships between simple statements, also called propositions.

• Propositions are atomic statements that may be considered to be either true or false.
  • "The sky is blue."
  • "The table has seven legs."
• Propositions are often represented by symbols, such as \(P\) and \(Q\).
  • \(P\) could be used to represent the proposition "The sky is blue."
  • \(Q\) could be used to represent the proposition "The table has seven legs."

Given proposition symbols as atomic logical formulas, composite logical statements can be formed using logical operators.

• Conjunctions of two logical formulas are formed using the operator \(\wedge\) meaning "and".
  • \(P \wedge Q\) could mean that both "the sky is blue" and "the table has seven legs".
• Disjunctions of two logical formulas are formed using the operator \(\vee\) meaning "or".
  • \(P \vee Q\) could mean that either "the sky is blue" or "the table has seven legs" (or both).
• Negations of a logical formula are formed using the operator \(\neg\) meaning "not". \(\neg P\) could mean that it is not true that "the sky is blue".
• Implications of two logical formulas are formed using the operator \(\implies\) meaning "implies".
  • \(P \implies Q\) could mean that "the sky is blue" implies that "the table has seven legs", in other words, if "the sky is blue", then "the table has seven legs".
• Equivalences of two logical formulas are formed using the operator \(\equiv\) meaning "is equivalent to".
• \(P \equiv Q\) could mean that "the sky is blue" is equivalent to the statement that "the table has seven legs", in other words, if and only if "the sky is blue", then "the table has seven legs".

Truth Tables

Truth tables are useful to describe the meaning of the logical operators.

\(P\)	\(Q\)	\(P \wedge Q\)
false	false	false
false	true	false
true	false	false
true	true	true

\(P\)	\(Q\)	\(P \vee Q\)
false	false	false
false	true	true
true	false	true
true	true	true

\(P\)	\(\neg P\)
false	true
true	false

\(P\)	\(Q\)	\(P \implies Q\)
false	false	true
false	true	true
true	false	false
true	true	true

\(P\)	\(Q\)	\(P \equiv Q\)
false	false	true
false	true	false
true	false	false
true	true	true

Tautologies

Tautologies are logical statements that are true by virtue of their logical structure, independent of the truth or falsity of the constituent propositions. For example, a well-known tautology is the logical formula \(P \vee \neg P\). If we suspect that a formula is a tautology, then one way of verifying the fact is to work out its truth table.

\(P\)	\(\neg P\)	\(P \vee \neg P\)
false	true	true
true	false	true

Another important tautology is modus ponens: \(((P \implies Q) \wedge P) \implies Q\).

\(P\)	\(Q\)	\(P \implies Q\)	\((P \implies Q) \wedge P\)	\(((P \implies Q) \wedge P)\implies Q\)
false	false	true	false	true
false	true	true	false	true
true	false	false	false	true
true	true	true	true	true

Exercise

• Develop a Haskell representation for formulas of the propositional calculus.
• Write the following Haskell functions.
  • A function that extracts all the unique propositional symbols of a formula.
  • A function that determines the truth of a formula, given an environment specifying the truth values of all the symbols in a formula.
  • A function that determines whether a formula is a tautology, by the truth table method: consider all possible truth value assignments to propositions and determine the truth of the formula for each assignment.

Solution

• The algebraic data type for propositional formulas is straightforward.

  data PF = Prop Char | Neg PF | Conj PF PF | 
                 Disj PF PF | Imp PF PF | Equiv PF PF deriving Show
  

• We use a strategy of having a helper function that adds propositions to a given list if they are not already in the list.

  unique_props x = up_helper x []
  up_helper (Prop c) props 
     | elem c props   = props
     | otherwise      = c:props
  up_helper (Neg f) propList = up_helper f propList
  up_helper (Conj f g) propList = up_helper f (up_helper g propList)
  up_helper (Disj f g) propList = up_helper f (up_helper g propList) 
  up_helper (Imp f g) propList = up_helper f (up_helper g propList) 
  up_helper (Equiv f g) propList = up_helper f (up_helper g propList)
  

• To evaluate a logical formula given an environment, we let the environment be an explicit list of all propositions that have the value True, with all other propositions implicitly False. This makes the evaluator straightforward.

  eval_logic (Prop p) propEnv = elem p propEnv
  eval_logic (Neg f) propEnv = not (eval_logic f propEnv)
  eval_logic (Conj f g) propEnv = (eval_logic f propEnv) && (eval_logic g propEnv) 
  eval_logic (Disj f g) propEnv = (eval_logic f propEnv) || (eval_logic g propEnv) 
  eval_logic (Imp f g) propEnv = (not (eval_logic f propEnv)) || (eval_logic g propEnv) 
  eval_logic (Equiv f g) propEnv = (eval_logic f propEnv) == (eval_logic g propEnv) 
  

• To compute truth tables, we let entries be a pair consisting of a proposition environment and the value of the formula in that environment.

  truth_table_entry f propEnv = (propEnv, eval_logic f propEnv)
  

• To determine all the possible truth value assignments, we use a recursive function.

  all_truth_val_assignments [] = [[]]
  all_truth_val_assignments (p1:more) = 
      let all_assigs_more = all_truth_val_assignments more
          in map (p1:) all_assigs_more ++ all_assigs_more
  

• The truth table is then easy to put together.

  truth_table f =
  	let props = unique_props f
  	    in map (truth_table_entry f) (all_truth_val_assignments props)
  

This lets us determine whether we have a tautology as a formula with True in every row.

*Main> truth_table (Disj (Prop 'x') (Neg (Prop 'x')))
[("x",True),("",True)]

*Main> truth_table (Imp (Conj (Imp (Prop 'p') (Prop 'q')) (Prop 'p')) (Prop 'q'))
[("pq",True),("p",True),("q",True),("",True)]