Firstorder logic

From Example Problems
Jump to navigation Jump to search

First-order predicate calculus or first-order logic (FOL) permits the formulation of quantified statements such as "there exists an x such that..." (Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \exists x} ) or "for any x, it is the case that..." (Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \forall x} ), where x is a member of the domain of discourse. A first-order (recursively-)axiomatisable theory is a theory that can be axiomatised as an extension of first-order logic by adding a recursively enumerable set of first-order sentences as axioms. What follows the "that..." is called the predicate and it expresses some property. A predicate is an expression that can be true of something. Thus, the expressions "is yellow" or "likes broccoli" are true of those things that are yellow or like broccoli, respectively.

First-order logic is mathematical logic that is distinguished from higher-order logic in that it does not allow quantification over properties. A property is an attribute of an object; thus a red object is said to have the property of redness. The property may be considered a form of object in its own right, able to possess other properties. A property is considered to be distinct from the objects which possess it. Thus first-order logic cannot express statements such as "for every property P, it is the case that..." or "there exists a property P such that...".

Nevertheless, first-order logic is strong enough to formalize all of set theory and thereby virtually all of mathematics. Its restriction to quantification over individuals makes it difficult to use for the purposes of topology, but it is the classical logical theory underlying mathematics. It is a stronger theory than sentential logic, but a weaker theory than second-order logic.

Defining first-order logic

A predicate calculus consists of

  • formation rules (i.e. recursive definitions for forming well-formed formulas).
  • transformation rules (i.e. inference rules for deriving theorems).
  • a (possibly countably infinite) set of axioms or axiom schemata.

There are two types of axioms: logical axioms which are valid with respect to the predicate calculus and non-logical axioms which are true under a special, i.e. the standard, interpretation of the theory of which they are part. For example, the non-logical Peano axioms are true under the standard interpretation of the symbolism of arithmetic, but they are not valid with respect to the predicate calculus.

When the set of axioms is infinite, it is required that there is an algorithm which can decide for a given well-formed formula whether it is an axiom or not. Furthermore, there should be an algorithm which can decide whether a given application of an inference rule is correct or not.

Vocabulary

The "vocabulary" is composed of

  1. Uppercase letters P, Q, R,... which are predicate variables.
  2. Lowercase letters a, b, c,... which are (individual) constants.
  3. Lowercase letters x, y, z,... which are (individual) variables.
  4. Lowercase letters f, g, h,... which are function variables.
  5. Symbols denoting logical operators: ¬ (logical not), Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \wedge} (logical and), Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \vee} (logical or), → (logical conditional), ↔ (logical biconditional).
  6. Symbols denoting quantifiers: Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \forall} (universal quantification), Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \exists} (existential quantification).
  7. Left and right parenthesis.

Some symbols may be omitted as primitive and taken as abbreviations instead; e.g. (P ↔ Q) is an abbreviation for (P → Q) Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \wedge} (Q → P). The minimum number of operators and quantifiers needed is three (or two if we define the operator nor or nand); for example, ¬, Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \wedge} , and Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \forall} suffice. A term is a constant, variable, or function symbol of n≥0 arguments.

Formation rules

The set of well-formed formulas (wffs) is recursively defined by the following rules:

  1. Simple and complex predicates If P is an n-adic (n ≥ 0) predicate, then Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Pa_1,...,a_n} is well-formed. If n ≤ 1, P is atomic.
  2. Inductive Clause I: If φ is a wff, then ¬ φ is a wff.
  3. Inductive Clause II: If φ and ψ are wffs, then Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (\phi \wedge \psi)} , Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (\phi \vee \psi)} , (φ → ψ), (φ ↔ ψ) are wffs.
  4. Inductive Clause III: If φ is a wff containing a free instance of variable x, then Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \forall x \, \varphi } and Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \exists x \, \varphi } are wffs. (Then any instance of x is said to be bound — not free — in Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \forall x \, \varphi } and Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \exists x \, \varphi } .)
  5. Closure Clause: Nothing else is a wff.

Transformation (inference) rules

Modus ponens suffices as the sole rule of inference. If there are no axiom schemata, then a rule of uniform substitution is also required.

Calculus

The predicate calculus is an extension of the propositional calculus. If the propositional calculus is defined with eleven axioms and one inference rule (modus ponens), not counting some auxiliary laws for the logical equivalence operator, then the predicate calculus can be defined by appending four additional axioms and one additional inference rule.

Axiomatic extension

The following four logical axioms characterize a predicate calculus:

  • PRED-1: Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \forall x Z(x) \rightarrow Z(y) }
  • PRED-2: Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Z(y) \rightarrow \exists x Z(x) }
  • PRED-3: Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \forall x (W \rightarrow Z(x)) \rightarrow (W \rightarrow \forall x Z(x)) }
  • PRED-4: Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \forall x (Z(x) \rightarrow W) \rightarrow (\exists x Z(x) \rightarrow W) }

These are actually axiom schemata, because the predicate letters W and Z in them can be replaced by any other predicate letters, without altering the validity of these formulae.

Inference rule

The inference rule called Universal Generalization is characteristic of the predicate calculus. It can be stated as

Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathit{if} \vdash Z(x), \mathit{then} \vdash \forall x Z(x)}

where Z(x) is supposed to stand for an already-proven theorem of predicate calculus and ∀xZ(x) is its closure with respect to the variable x. The predicate letter Z can be replaced by any other predicate letter.

Notice that Generalization is analogous to the Necessitation Rule of modal logic, which is

Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathit{if} \vdash P, \mathit{then} \vdash \Box P} .

Metalogical theorems of first-order logic

Some important metalogical theorems are listed below in bulleted form.

  1. Unlike the propositional calculus, first-order logic is undecidable. There is provably no decision procedure for determining for an arbitrary formula P, whether or not P is valid (see Halting problem). (Results came independently from Church and Turing.)
  2. The decision problem for validity is semidecidable. As Gödel's completeness theorem shows, for any valid formula P, P is provable.
  3. Monadic predicate logic (i.e., predicate logic with only predicates of one argument) is decidable.

See also

References

de:Prädikatenlogik fr:Calcul des prédicats he:תחשיב הפסוקים hu:Elsőrendű logika pl:Klasyczny rachunek logiczny sv:Predikatlogik ru:Логика первого порядка zh:一階邏輯