Predicate Calculus

The language of predicate calculus consists of:

• SYMBOLS
  • Variable symbols: x, y, z ...
  • Function symbols: f, g, h ...
  • Predicate symbols: P, Q, R, ...
  • Logic symbols
    • Connectives: $\neg, \wedge, \vee, \rightarrow$
    • Quantifiers: $\forall, \exists$
• TERMS
  • Constant: a, b, c ...
  • Variables
  • f(T) where f is a function and T is a term
  • Examples: f(a,x) g(x, f(a,x))
• ATOMIC FORMULAS (also called Propositions)
  • True and False
  • P(T) where P is a predicate (T is a term)

• LITERALS
  • Atomic formulas
  • Negated atomic formulas

• WELL-FORMED FORMULAS (WFFS - also called sentences)
  • A predicate applied to the correct number of terms
  • If P and Q are formulas then these are wffs:
    • $P \rightarrow Q$
    • $P \wedge Q$
    • $P \vee Q$
    • $\neg P$
  • If x is a variable, and P is a formula, then the following are wffs:
    • $\forall x P(x)$
    • $\exists x P(x)$

• SENTENCES
  • A wff with all variables in the scope of corresponding quantifiers
  • Examples:
    • Sentence $\forall x[Feathers(x) \rightarrow Bird(x)]$
    • Not a sentence: $\forall x[Feathers(x) \vee Feathers(y)]$
      because y is a free variable

• VALID: something is always true (Tautology)

• SATISFIABLE: something which has at least one set of values to make it true

• UNSATISFIABLE: something which is never true (Contradiction)