First-order Predicate Calculus Article Index for
First-order 		Website Links For
Logic 		 

Information About

First-order Predicate Calculus
  CATEGORIES ABOUT FIRST-ORDER LOGIC
   
logic
   
systems of formal logic
   
philosophical logic
   
model theory
   
discrete mathematics
   
APPAREL
BABY
BEAUTY
BOOKS
CAR TOYS
CELL PHONES
DVD'S
ELECTRONICS
GOURMET FOOD
GROCERIES
HEALTH & PERSONAL
HOME & GARDEN
JEWELRY
MUSIC
MUSIC INSTRUMENTS
OFFICE PRODUCTS
SOFTWARE
SPORTING GOODS
TOOLS & HARDWARE
TOYS
VIDEO GAMES
SHOPPING HOME
MORE SHOPPING...



While these will be two unrelated propositions, denoted for example by ''p'' and ''q''. In first-order logic however, both sentences would be connected by the same property: Man(x), where Man(x) means that x is a man. When x=Socrates we get the first proposition - ''p'', and when x=Plato we get the second proposition - ''q''. Such a construction allows for a much more powerful logic when quantifiers are introduced, such as "for every x..." - for example, "for every x, if Man(x), then...". Without quantifiers, every valid argument in FOL is valid in propositional logic, and vice versa.

The language of first-order logic has sufficient expressive power for the formalization of most of mathematics (see Second-order Logic for comparison). A First-order Theory consists of a set of Axioms (usually finite or Recursively Enumerable ) and the statements deducible from them. The popular set theory ZFC is an example of a first-order theory, and it is generally accepted that all of Classical Mathematics can be formalized
in ZFC . There are other theories that are commonly formalized independently in first-order logic such as Peano Arithmetic .


WHY IS FIRST-ORDER LOGIC NEEDED?


Propositional Logic is not adequate for formalizing valid arguments that rely on the internal structure of the propositions involved. To see this, consider the valid Syllogistic argument:

  • All men are mortal

  • Socrates is a man

  • Therefore, Socrates is mortal


which upon translation into Propositional Logic yields:

  • A

  • B

  • \Rightarrow C

    • (taking \Rightarrow to mean "therefore").


This translation is invalid: logic validates arguments according to their ''structure'', and nothing in the structure of this translated argument (C follows from A and B, for arbitrary A, B, C) suggests that it is valid. A translation that preserves the intuitive (and formal) validity of the argument must take into consideration the deeper structure of propositions, such as the essential notions of predication and quantification. Propositional logic deals only with truth-functional validity: any assignment of truth-values to the variables of the argument should make either the conclusion true or at least one of the premises false. Clearly we may (uniformly) assign truth values to the variables of the above argument such that A, B are both true but C is false. Hence the argument is truth-functionally invalid. On the other hand, it is impossible to (uniformly) assign truth values to the argument "A follows from (A and B)" such that (A and B) is true (hence A is true and B is true) and A false.


DEFINING FIRST-ORDER LOGIC


A predicate calculus consists of

The axioms considered here are ''logical'' Axioms which are part of classical FOL. Further, ''non-logical'' axioms are added to yield specific first-order theories that are based on the axioms of classical FOL (and hence are called ''classical first-order theories'', such as ''classical set-theory''). Take Peano Arithmetic for example: the axiom orall x P(x) ightarrow orall x P(x) (if P(x) is true for every x then P(x) is true for every x) is a logical axiom, but the axiom orall x \exists y Q(x,y) (i.e. for every x there exists y such that y=x+1, where Q(x,y) is interpreted as "y=x+1") is a non-logical axiom, but rather an axiom of the theory (an axiom of arithmetic rather than of logic). Axioms of the latter kind are also called axioms of first-order ''theories''.

The axioms of first-order theories are not regarded as truths of logic ''per se'', but rather as truths of the particular theory that usually has associated with it an intended interpretation of its non-logical symbols. (See an analogous idea at logical versus Non-logical Symbol s.) in the previous example, the second axiom is true only with the interpretation of the relation Q(x,y) as "y=x+1", and only in the theory of Peano Arithmetic .

Classical FOL does not have associated with it an intended interpretation of its non-logical vocabulary (except arguably a symbol denoting identity, depending on whether one regards such a symbol as logical).

It is important to note that FOL can be formalized in many equivalent ways; there is nothing canonical about the axioms and rules of inference given here. There are infinitely many equivalent formalizations all of which yield the same theorems and non-theorems, and all of which have equal right to the title 'FOL'.


VOCABULARY

Before setting up the formation rules, one has to describe the "vocabulary", which is composed of
# A set of predicate variables (or '''relations''') each with some '''valence''' (or ''' Arity ''', number of its arguments) ≥1, which are often denoted by uppercase letters ''P'', ''Q'', ''R'',... .
  • For example, ''P(x)'' is a predicate variables of valence 1. It can stand for "x is a man", for example.

  • ''Q(x,y)'' is a predicate variables of valence 2. It can stand for "x is greater than y" in arithmetic or "x is the father of y", for example.

  • It is possible to allow relations of valence 0; these could be considered as Propositional Variables . For example, ''P'', which can stand for any statement.

  • By using functions (see below), it is possible to dispense with all predicate variables with valence larger than one. For example, "''x>y''" (a predicate of valence 2, of the type ''Q(x,y)'')can be replaced by a predicate of valence 1 about the Ordered Pair (x,y).

    • # A set of constants, often denoted by lowercase letters at the beginning of the alphabet ''a'', ''b'', ''c'',... .

  • Examples: ''a'' may stand for Socrates. In Arithmetic , it may stand for 0. In Set Theory , such a constant may stand for the Empty Set .

    • # A set of functions, each of some valence ≥ 1, which are often denoted by lowercase letters ''f'', ''g'', ''h'',... .

  • Examples: ''f(x)'' may stand for "the father of x". In Arithmetic , it may stand for "-x". In Set Theory , it may stand for "the Power Set of x". In Arithmetic , ''f(x,y)'' may stand for "x+y". In Set Theory , it may stand for "the union of x and y".

  • A constant is really a function of valence 0. However it is traditional to use the term "function" only for functions of valence at least 1.

  • One can in principle dispense entirely with functions of arity > 2 and predicates of arity > 1 if there is a function symbol of arity 2 representing an Ordered Pair (or predicate symbols of arity 2 representing the projection relations of an ordered pair). The pair or projections need to satisfy the natural axioms.

  • One can in principle dispense entirely with functions and constants. For example, instead of using a constant ''0'' one may use a predicate ''0(x)'' (interpreted as "x=0"), and replace every predicate such as ''P(0,y)'' with orall x ''0(x)'' ightarrow ''P(x,y)''. A function such as ''f(x1,x2...)'' will similarly be replaced by a predicate ''F(x1,x2...,y)'' (interpreted as "y=f(x1,x2...)").

    • # An infinite set of variables, often denoted by lowercase letters at the end of the alphabet ''x'', ''y'', ''z'',... .

# Symbols denoting logical operators (or '''connectives'''):
eg ( Logical Not ), ightarrow ( Logical Conditional ).

    • eg(φ ightarrow

egψ) is logically equivalent to φ \wedge ψ ( Logical And ). φ \wedge ψ can be seen as a shorthand for this. Alternatively, one may add the \wedge symbol as a logical operator to the vocabulary, and appropriate axioms.

    • egφ ightarrow ψ is logically equivalent to φ \or ψ ( Logical Or ). φ \or ψ can be seen as a shorthand for this. Alternatively, one may add the \or symbol as a logical operator to the vocabulary, and appropriate axioms.

  • Similarly, (φ ightarrowψ)\wedge(ψ ightarrowφ) is logically equivalent to φ \leftrightarrow ψ ( Logical Biconditional ), and one may use the latter as a shorthand for this, or alternatively add this to the vocabulary and add appropriate axioms. Sometimes φ \leftrightarrow ψ is written as φ \equiv ψ.

    • # Symbols denoting quantifiers: orall ( Universal Quantification ).


    • eg( orall x

eg φ) is logically equivalent to \existsx φ ( Existential Quantification ). The latter can either be used as a shorthand for this, or added to the vocabulary together with appropriate axioms.
# Left and right parenthesis.
  • There are many different conventions about where to put parentheses; for example, one might write orall ''x'' or ( orall''x''). Sometimes one uses colons or full stops instead of parentheses to make formulas unambiguous. One interesting but rather unusual convention is " Polish Notation ", where one omits all parentheses, and writes ightarrow, \wedge, and so on in front of their arguments rather than between them. Polish notation is compact and elegant, but rare because it is hard for humans to read it.

    • # An identity or equality symbol = is sometimes but not always included in the vocabulary.

  • If equality is considered to be a part of first order logic, then the equality symbol behaves syntactically as a binary predicate. This case is sometimes called first order logic with equality.


There are several further minor variations listed below: