First-order logic

First-order logic (FOL) is a formal deductive system used in mathematics, philosophy, linguistics, and computer science. A deductive system (also called a deductive apparatus of a Formal system) consists of the Axioms (or Axiom schemata and Rules of inference It goes by many names, including: first-order predicate calculus (FOPC), the lower predicate calculus, the language of first-order logic or predicate logic. Unlike natural languages such as English, FOL uses a wholly unambiguous formal language interpreted by mathematical structures. English is a West Germanic language originating in England and is the First language for most people in the United Kingdom, the United States A formal language is a set of words, ie finite strings of letters, or symbols. FOL is a system of deduction that extends propositional logic by allowing quantification over individuals of a given domain of discourse. This is a technical mathematical article about the area of mathematical logic variously known as "propositional calculus" or "propositional logic" Quantification has two distinct meanings In Mathematics and Empirical science, it refers to human acts known as Counting and Measuring The domain of discourse, sometimes called the universe of discourse, logical discourse, or simply discourse, is an analytic tool used in Deductive For example, it can be stated in FOL "Every individual has the property P".

While propositional logic deals with simple declarative propositions, first-order logic additionally covers predicates and quantification. In Mathematics, a predicate is either a relation or the Boolean-valued function that amounts to the Characteristic function or the Take for example the following sentences: "Socrates is a man", "Plato is a man". In propositional logic 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.

A first-order theory consists of a set of axioms (usually finite or recursively enumerable) and the statements deducible from them given the underlying deducibility relation. In Mathematical logic, a theory is a set of sentences in a Formal language. In traditional Logic, an axiom or postulate is a proposition that is not proved or demonstrated but considered to be either self-evident, or subject In Computability theory, traditionally called Recursion theory, a set S of Natural numbers is called recursively enumerable, computably Usually what is meant by 'first-order theory' is some set of axioms together with those of a complete (and sound) axiomatization of first-order logic, closed under the rules of FOL. (Any such system FOL will give rise to the same abstract deducibility relation, so we needn't have a fixed axiomatic system in mind. ) A first-order language has sufficient expressive power to formalize two important mathematical theories: ZFC set theory and Peano arithmetic. Zermelo–Fraenkel set theory with the axiom of choice, commonly abbreviated ZFC, is the standard form of Axiomatic set theory and as such is the most common In Mathematical logic, the Peano axioms, also known as the Dedekind-Peano axioms or the Peano postulates, are a set of Axioms for the Natural A first-order language cannot, however, categorically express the notion of countability even though it is expressible in the first-order theory ZFC under the intended interpretation of the symbolism of ZFC. See also Formal interpretation One who constructs a syntactical system usually has in mind from the outset some Interpretation of this Such ideas can be expressed categorically with second-order logic. In Logic and Mathematics second-order logic is an extension of First-order logic, which itself is an extension of Propositional logic.

1 Why is first-order logic needed?
- 1.1 Variables in first-order logic and in propositional logic
2 Defining first-order logic
3 Syntax of first-order logic
4 Additional syntactic concepts
- 4.1 Free and Bound Variables
- 4.2 Substitution
5 Proof theory
- 5.1 Inference rules
- 5.2 Axioms
  - 5.2.1 Quantifier axioms
  - 5.2.2 Equality and its axioms
6 Semantics
7 Predicate calculus
- 7.1 Provable identities
- 7.2 Provable inference rules
8 Metalogical theorems of first-order logic
9 Translating natural language to first-order logic
10 Limitations of first-order logic
11 Comparison with other logics
- 11.1 Algebraizations
12 Automation
13 References
14 See also
15 External links

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. This is a technical mathematical article about the area of mathematical logic variously known as "propositional calculus" or "propositional logic" 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
$\therefore$ C

(taking $\therefore$ to mean "therefore"). A syllogism, or logical appeal, (συλλογισμός &mdash "conclusion" "inference" (usually the categorical syllogism) is a kind of This is a technical mathematical article about the area of mathematical logic variously known as "propositional calculus" or "propositional logic"

According to propositional logic, this translation is invalid: Propositional 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.

In contrast, this argument can be easily translated into first-order logic:

$\forall x (\mathit{Man}(x) \rightarrow \mathit{Mortal}(x))$
$\,\mathit{Man}(\mathit{Socrates})$
$\therefore \mathit{Mortal}(\mathit{Socrates})$

(Where " $\forall x$ " means "for all x", " $\rightarrow$ " means "implies", $M a n (S o c r a t e s)$ means "Socrates is a man", and $M o r t a l (S o c r a t e s)$ means "Socrates is mortal". ) In plain English, this states that

for all x, if x is a man then x is mortal
Socrates is a man
therefore Socrates is mortal

FOL can also express the existence of something ( $\exists$ ), as well as predicates ("functions" that are true or false) with more than one parameter. For example, "there is someone who can be fooled every time" can be expressed as:

$\exists x (\mathit{Person}(x) \and \forall y (\mathit{time}(y) \rightarrow \mathit{Canfool}(x,y)))$

Where " $\exists x$ " means "there exists (an) x", " $\and$ " means "and", and $C a n f o o l (x, y)$ means "(person) x can be fooled (at time) y".

Variables in first-order logic and in propositional logic

Every propositional formula can be translated into an essentially equivalent first-order formula by replacing each propositional variable with a zero-arity predicate. For example, the formula $x \vee (y \wedge \neg z)$ can be translated into $P() \vee (Q() \wedge \neg R())$ , where P, Q and R are predicates of arity zero.

While variables in the propositional logics are used to represent conditions that can be true or false, variables in first-order logic represent objects the formula is referring to. In the example above, the variable x in $\forall x (\mathit{Man}(x) \rightarrow \mathit{Mortal}(x))$ is intended to indicate an arbitrary element of the human race, not a condition that can be true or false.

Defining first-order logic

A predicate calculus consists of

formation rules (i. e. recursive definitions for forming well-formed formulas). Recursion, in Mathematics and Computer science, is a method of defining functions in which the function being defined is applied within its own definition In Mathematical logic, a well-formed formula (often abbreviated WFF, pronounced "wiff" or "wuff" is a Symbol or string of symbols (a
a proof theory, made of:
- transformation rules (i. e. inference rules for deriving theorems). In Logic, a rule of inference (also called a transformation rule) is a function from sets of formulae to formulae
- axioms (possibly countably infinite many) or axiom schemata.
a semantics, telling which interpretation of the symbol makes the formula true.

The axioms considered here are logical axioms which are part of classical FOL. In traditional Logic, an axiom or postulate is a proposition that is not proved or demonstrated but considered to be either self-evident, or subject 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 in this article. 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'.

FOL is used as the basic "building block" for many mathematical theories. FOL provides several built-in rules, such as the axiom $\forall x P(x)\rightarrow \forall x P(x)$ (if P(x) is true for every x then P(x) is true for every x). Additional non-logical axioms are added to produce specific first-order theories based on the axioms of classical FOL; these theories built on FOL are called classical first-order theories. One example of a classical first-order theory is Peano arithmetic, which adds the axiom $\forall x \exists y Q(x,y)$ (i. In Mathematical logic, the Peano axioms, also known as the Dedekind-Peano axioms or the Peano postulates, are a set of Axioms for the Natural e. for every x there exists y such that y=x+1, where Q(x,y) is interpreted as "y=x+1"). This additional axiom is a non-logical axiom; it is not part of FOL, but instead is 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 symbols. Non-logical symbol is a technical term used in Logic In Logic, the non-logical symbols (sometimes also called non-logical constants) of a ) Thus, the axiom about Q(x,y) is true only with the interpretation of the relation Q(x,y) as "y=x+1", and only in the theory of Peano arithmetic. In Mathematical logic, the Peano axioms, also known as the Dedekind-Peano axioms or the Peano postulates, are a set of Axioms for the Natural 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). Classical set-theory is another example of a first-order theory (a theory built on FOL).

Syntax of first-order logic

Symbols

The terms and formulas of first-order logic are strings of symbols. As for all formal languages, the nature of the symbols themselves is outside the scope of formal logic; it is best to think of them as letters and punctuation symbols. A formal language is a set of words, ie finite strings of letters, or symbols. The alphabet (set of all symbols of the language) is divided into the application-specific non-logical symbols and the logical symbols. The latter are the same, and have the same meaning, for all applications.

Non-logical symbols

Main article: non-logical symbols

The non-logical symbols represent predicates (relations), functions and constants on the domain. Non-logical symbol is a technical term used in Logic In Logic, the non-logical symbols (sometimes also called non-logical constants) of a The set of non-logical symbols is known as the signature. ^[1]

Traditional approach

The traditional approach is to have only one, infinite, set of non-logical symbols (one signature) for all applications. Consequently, under the traditional approach there is only one language of first-order logic. ^[2] This approach is still common, especially in philosophically oriented books.

For every integer n > 0 we have the n-ary, or n-place, predicate symbols. In Logic, Mathematics, and Computer science, the arity (synonyms include type, adicity, and rank) of a function Because they represent relations between n elements, they are also called relation symbols. This article sets out the set-theoretic notion of relation For a more elementary point of view see Binary relations and Triadic relations For each arity n we have an infinite supply of them:

Pⁿ₀, Pⁿ₁, Pⁿ₂, Pⁿ₃, …
An infinite supply of constant symbols:

c₀, c₁, c₂, c₃, …
For every integer n > 0 infinitely many n-ary function symbols:

fⁿ₀, fⁿ₁, fⁿ₂, fⁿ₃, …

Mathematical approach

In modern mathematical treatments of first-order logic, the signature varies with the applications. Typical signatures in mathematics are {1, ×} or just {×} for groups, or {0, 1, +, ×, <} for ordered fields. In Mathematics, an ordered field is a field together with a Total ordering of its elements that agrees in a certain sense with the field operations

There are no restrictions on the number of non-logical symbols. The signature can be empty, finite, or infinite, even uncountable. In Mathematics, and more specifically Set theory, the empty set is the unique set having no ( Zero) members Every non-logical symbol is of one of the following types.

A set of predicate symbols (or relation symbols) each with some valence (or arity, number of its arguments) ≥1, which are often denoted by uppercase letters P, Q, R,. In Logic, Mathematics, and Computer science, the arity (synonyms include type, adicity, and rank) of a function . . .
- 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). In Mathematics, an ordered pair is a collection of two distinguishable objects one of which is identified as the first coordinate (or the first entry
A set of constant symbols, 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. Arithmetic or arithmetics (from the Greek word αριθμός = number is the oldest and most elementary branch of mathematics used by almost everyone In set theory, such a constant may stand for the empty set. In Mathematics, and more specifically Set theory, the empty set is the unique set having no ( Zero) members
A set of function symbols, 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". Arithmetic or arithmetics (from the Greek word αριθμός = number is the oldest and most elementary branch of mathematics used by almost everyone In set theory, it may stand for "the power set of x". In Mathematics, given a set S, the power set (or powerset) of S, written \mathcal{P}(S P ( S) In arithmetic, f(x,y) may stand for "x+y". Arithmetic or arithmetics (from the Greek word αριθμός = number is the oldest and most elementary branch of mathematics used by almost everyone 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). In Mathematics, an ordered pair is a collection of two distinguishable objects one of which is identified as the first coordinate (or the first entry 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 $\forall$ x 0(x) $\rightarrow$ 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. . . )").

We can recover the traditional approach by considering the following signature:

{P¹₀, P¹₁, P¹₂, P¹₃, …, P²₀, P²₁, P²₂, P²₃, …, P³₀, P³₁, P³₂, P³₃, …, …,

c₀, c₁, c₂, c₃, …, f¹₀, f¹₁, f¹₂, f¹₃, …, f²₀, f²₁, f²₂, f²₃, …, f³₀, f³₁, f³₂, f³₃, …, …}

Logical symbols

Besides logical connectives such as ∧, ∨ and ¬, the logical symbols include quantifiers, and variables. Table of logic symbolsIn Logic, two sentences (either in a formal language or a natural language may be joined by means of a logical connective to form a compound sentence Quantification has two distinct meanings In Mathematics and Empirical science, it refers to human acts known as Counting and Measuring A variable (ˈvɛərɪəbl is an Attribute of a physical or an abstract System which may change its Value while it is under Observation.

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): (logical not), (logical conditional). In Logic and Mathematics, negation or not is an operation on Logical values for example the logical value of a Proposition The material conditional, also known as the material implication or truth functional conditional, expresses a property of certain Conditionals in Logic
- $\neg$ (φ $\rightarrow$ $\neg$ ψ) is logically equivalent to φ $\wedge$ ψ (logical and). In Logic and/or Mathematics, logical conjunction or and is a two-place Logical operation that results in a value of true if both of φ $\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.
- $\neg$ φ $\rightarrow$ ψ 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, (φ $\rightarrow$ ψ) $\wedge$ (ψ $\rightarrow$ φ) 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. In Logic and Mathematics, logical biconditional (sometimes also known as the material biconditional) is a Logical operator connecting two statements Sometimes φ $\leftrightarrow$ ψ is written as φ $\equiv$ ψ.
Symbols denoting quantifiers: (universal quantification, typically read as "for all"). In Predicate logic, universal quantification is an attempt to formalize the notion that something (a Logical predicate) is true for everything, or every
- $\neg(\forall$ x $\neg$ φ) is logically equivalent to $\exists$ x φ (existential quantification, typically read as "there exists"). In Predicate logic, an existential quantification is the predication of a property or relation to at least one member of the domain 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 $\forall$ x or ( $\forall$ 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 $\rightarrow$ , $\wedge$ , and so on in front of their arguments rather than between them. Polish notation, also known as prefix notation, is a form of notation for Logic, Arithmetic, and Algebra. 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.

Variations

There are several further minor variations listed below:

The set of primitive symbols (operators and quantifiers) often varies. It is possible to include other operators as primitive, such as $\leftrightarrow$ (iff), $\wedge$ (and) and $\or$ (or), the truth constants T for "true" and F for "false" (these are operators of valence 0), and/or the Sheffer stroke (P | Q, aka NAND). Definition The NAND operation is a Logical operation on two Logical values typically the values of two Propositions that produces a value The minimum number of primitive symbols needed is one, but if we restrict ourselves to the operators listed above, we need three, as above.
Some books and papers use the notation φ $\Rightarrow$ ψ for φ $\rightarrow$ ψ. This is especially common in proof theory where $\rightarrow$ is easily confused with the sequent arrow. One also sees ~φ for $\neg$ φ, φ & ψ for φ $\wedge$ ψ, and a wealth of notations for quantifiers; e. Quantification has two distinct meanings In Mathematics and Empirical science, it refers to human acts known as Counting and Measuring g. , $\forall$ x φ may be written as (x)φ. This latter notation is common in texts on recursion theory.
It is often easier in practice to use a simpler notation that supports infix operators and omits unnecessary parentheses. Thus if P is a relation of valence 2, we often write "a P b" instead of "P a b"; for example, we write 1 < 2 instead of <(1 2). Similarly if f is a function of valence 2, we sometimes write "a f b" instead of "f(a b)"; for example, we write 1 + 2 instead of +(1 2). By convention, infix operators tend to use non-alphabetic function names. It is also common to omit some parentheses if this does not lead to ambiguity (leading to defining a precedence).
Sometimes it is useful to say that "P(x) holds for exactly one x", which can be expressed as $\exists!$ x P(x). This notation may be taken to abbreviate a formula such as $\exists$ x (P(x) $\wedge\forall$ y (P(y) $\rightarrow$ (x = y))) .

Computer programs that accept first-order logic representations will typically accept at least these quantifiers and operators (though they may use different symbols to represent them): $\forall$ (forall), $\exists$ (exists), $\neg$ (not), $\wedge$ (and), $\or$ (or), $\rightarrow$ (implies), and $\leftrightarrow$ (if and only if). The exclusive-or operator "xor" is also common.

The sets of constants, functions, and relations are usually considered to form a language, while the variables, logical operators, and quantifiers are usually considered to belong to the logic. For example, the language of group theory consists of one constant (the identity element), one function of valence 1 (the inverse) one function of valence 2 (the product), and one relation of valence 2 (equality), which would be omitted by authors who include equality in the underlying logic.

Formation rules

The formation rules define the terms and formulas of first order logic. When terms and formulas are represented as strings of symbols, these rules can be used to write a formal grammar for terms and formulas. In Formal semantics, Computer science and Linguistics, a formal grammar (also called formation rules) is a precise description of a Formal The concept of free variable is used to define the sentences as a subset of the formulas.

Terms

The set of terms is recursively defined by the following rules:

Any constant is a term. The word term is from the Latin terminus "boundary line limit" from the Indo-European root ter- "peg post boundary"
Any variable is a term.
Any expression f(t₁,. . . ,t_n) of n ≥ 1 arguments (where each argument t_i is a term and f is a function symbol of valence n) is a term.
Closure clause: Nothing else is a term. For example, predicates are not terms.

Formulas

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

Simple and complex predicates If P is a relation of valence n ≥ 1 and a₁, . In Mathematical logic, a well-formed formula (often abbreviated WFF, pronounced "wiff" or "wuff" is a Symbol or string of symbols (a In Mathematical logic, a formula is a type of Abstract object a token of which is a Symbol or string of symbols which may be . . , a_n are terms then P(a₁,. . . ,a_n) is well-formed. If equality is considered part of logic, then (a₁ = a₂) is well formed. All such formulas are said to be atomic. In Mathematical logic, an atomic formula (also known simply as an atom) is a formula with no deeper Propositional structure that is a formula
Inductive Clause I: If φ is a wff, then $\neg$ φ is a wff.
Inductive Clause II: If φ and ψ are wffs, then (φ $\rightarrow$ ψ) is a wff.
Inductive Clause III: If φ is a wff and x is a variable, then $\forall$ x φ is a wff.
Closure Clause: Nothing else is a wff.

For example, $\forall$ x $\forall$ y (P(f(x)) $\rightarrow\neg$ (P(x) $\rightarrow$ Q(f(y),x,z))) is a well-formed formula, if f is a function of valence 1, P a predicate of valence 1 and Q a predicate of valence 3. $\forall$ x x $\rightarrow$ is not a well-formed formula.

In Computer science terminology, a formula implements a built-in "boolean" type, while a term implements all other types. Computer science (or computing science) is the study and the Science of the theoretical foundations of Information and Computation and their

Example

In mathematics the language of ordered abelian groups has one constant 0, one unary function −, one binary function +, and one binary relation ≤. So:

0, x, y are atomic terms
+(x, y), +(x, +(y, −(z))) are terms, usually written as x + y, x + y − z
=(+(x, y), 0), ≤(+(x, +(y, −(z))), +(x, y)) are atomic formulas, usually written as x + y = 0, x + y - z ≤ x + y,
( $\forall$ x $\forall$ y ≤( +(x, y), z)) $\rightarrow$ ( $\forall$ x =(+(x, y), 0)) is a formula, usually written as ( $\forall$ x $\forall$ y x + y ≤ z) $\rightarrow$ ( $\forall$ x x + y = 0).

Additional syntactic concepts

Free and Bound Variables

Main article: Free variables and bound variables

In a formula, a variable may occur free or bound. In Mathematics, and in other disciplines involving Formal languages including Mathematical logic and Computer science, a free variable is a Intuitevely, a variable is free in a formula if it is not quantified: in $\forall y. P(x,y)$ , variable x is free while y is bound.

Atomic formulas If φ is an Atomic formula then x is free in φ if and only if x occurs in φ. In Mathematics, and in other disciplines involving Formal languages including Mathematical logic and Computer science, a free variable is a
Inductive Clause I: x is free in $\neg$ φ if and only if x is free in φ.
Inductive Clause II: x is free in (φ $\rightarrow$ ψ) if and only if x is free in φ and does not occur in ψ, or x is free in ψ and does not occur in φ, or x is free in both φ and ψ.
Inductive Clause III: x is free in $\forall$ y φ if and only if x is free in φ and x is a different symbol than y.
Closure Clause: x is bound in φ if and only if x occurs in φ and x is not free in φ.

For example, in $\forall$ x $\forall$ y (P(x) $\rightarrow$ Q(x,f(x),z)), x and y are bound variables, z is a free variable, and w is neither because it does not occur in the formula.

Freeness and boundness can be also specialized to specific occurrences of variables in a formula. For example, in $P(x) \rightarrow \forall x. Q(x)$ , the first occurrence of x is free while the second is bound. In other words, the x in $P (x)$ is free while the $x$ in $\forall x. Q(x)$ is bound.

Substitution

If t is a term and φ is a formula possibly containing the variable x, then φ[t/x] is the result of replacing all free instances of x by t in φ.

This replacement results in a formula that logically follows the original one provided that no free variable of t becomes bound in this process. If some free variable of t becomes bound, then to substitute t for x it is first necessary to change the names of bound variables of φ to something other than the free variables of t.

To see why this condition is necessary, consider the formula φ given by $\forall$ y y ≤ x ("x is maximal"). If t is a term without y as a free variable, then φ[t/x] just means t is maximal. However if t is y, the formula φ[y/x] is $\forall$ y y ≤ y which does not say that y is maximal. The problem is that the free variable y of t (=y) became bound when we substituted y for x in φ[y/x]. The intended replacement can be obtained by renaming the bound variable y of φ to something else, say z, so that the formula is then $\forall$ z z ≤ y. Forgetting this condition is a notorious cause of errors.

Proof theory

Inference rules

An inference rule is a function from sets of (well-formed) formulas, called premises, to sets of formulas called conclusions. In Logic, a rule of inference (also called a transformation rule) is a function from sets of formulae to formulae In Discourse and Logic, a premise is a claim that is a reason (or element of a set of reasons for or objection against some other claim In most well-known deductive systems, inference rules take a set of formulas to a single conclusion. (Notice this is true even in the case of most sequent calculi. In Proof theory and Mathematical logic, the sequent calculus is a widely known Proof calculus for First-order logic (and Propositional logic )

Inference rules are used to prove theorems, which are formulas provable in or members of a theory. In Mathematics, a theorem is a statement proven on the basis of previously accepted or established statements If the premises of an inference rule are theorems, then its conclusion is a theorem as well. In Discourse and Logic, a premise is a claim that is a reason (or element of a set of reasons for or objection against some other claim In other words, inference rules are used to generate "new" theorems from "old" ones--they are theoremhood preserving. Systems for generating theories are often called predicate calculi. These are described in a section below.

An important inference rule, modus ponens, states that if φ and φ $\rightarrow$ ψ are both theorems, then ψ is a theorem. In Classical logic, modus ponendo ponens ( Latin: mode that affirms by affirming; often abbreviated to MP or modus ponens) is a This can be written as following;

if $T \vdash \varphi$ and $T \vdash \varphi\rightarrow\psi$ , then $T \vdash \psi$

where $T \vdash \varphi$ indicates $\varphi$ is provable in theory T. There are deductive systems (known as Hilbert-style deductive systems) in which modus ponens is the sole rule of inference; in such systems, the lack of other inference rules is offset with an abundance of logical axiom schemes. In Logic, especially Mathematical logic, a Hilbert-style deduction system is a type of system of formal deduction attributed

A second important inference rule is Universal Generalization. Generalization is an inference rule of Predicate calculus which states that If \vdash P(x is true ( valid) then so It can be stated as

if $T \vdash \varphi$ , then $T \vdash \forall x \, \varphi$

Which reads: if φ is a theorem, then "for every x, φ" is a theorem as well. The similar-looking schema $\varphi\rightarrow\forall x \, \varphi$ is not sound, in general, although it does however have valid instances, such as when x does not occur free in φ (see Generalization (logic)). Generalization is an inference rule of Predicate calculus which states that If \vdash P(x is true ( valid) then so

Axioms

Here follows a description of the axioms of first-order logic. As explained above, a given first-order theory has further, non-logical axioms. The following logical axioms characterize a predicate calculus for this article's example of first-order logic^[3].

For any theory, it is of interest to know whether the set of axioms can be generated by an algorithm, or if there is an algorithm which determines whether a well-formed formula is an axiom.

If there is an algorithm to generate all axioms, then the set of axioms is said to be recursively enumerable. In Computability theory, traditionally called Recursion theory, a set S of Natural numbers is called recursively enumerable, computably

If there is an algorithm which determines after a finite number of steps whether a formula is an axiom or not, then the set of axioms is said to be recursive or decidable. In Computability theory, a set of Natural numbers is called recursive, computable or decidable if there is an Algorithm In that case, one may also construct an algorithm to generate all axioms: this algorithm simply builds all possible formulas one by one (with growing length), and for each formula the algorithm determines whether it is an axiom.

Axioms of first-order logic are always decidable. However, in a first-order theory non-logical axioms are not necessarily such.

Quantifier axioms

Quantifier axioms change according to how the vocabulary is defined, how the substitution procedure works, what the formation rules are and which inference rules are used. Here follows a specific example of these axioms

PRED-1: $(\forall x Z(x)) \rightarrow Z(t)$
PRED-2: $Z(t) \rightarrow (\exists x Z(x))$
PRED-3: $(\forall x (W \rightarrow Z(x))) \rightarrow (W \rightarrow \forall x Z(x))$
PRED-4: $(\forall x (Z(x) \rightarrow W)) \rightarrow (\exists x Z(x) \rightarrow W)$

These are actually axiom schemata: the expression W stands for any wff in which x is not free, and the expression Z(x) stands for any wff with the additional convention that Z(t) stands for the result of substitution of the term t for x in Z(x). In Mathematical logic, an axiom schema generalizes the notion of Axiom. Thus this is a recursive set of axioms. In Computability theory, a set of Natural numbers is called recursive, computable or decidable if there is an Algorithm

Another axiom, $Z \rightarrow \forall x Z$ , for Z in which x does not occur, is sometimes added.

Equality and its axioms

There are several different conventions for using equality (or identity) in first-order logic. This section summarizes the main ones. The various conventions all give essentially the same results with about the same amount of work, and differ mainly in terminology.

The most common convention for equality is to include the equality symbol as a primitive logical symbol, and add the axioms for equality to the axioms for first-order logic. The equality axioms are

x = x

x = y → f(. . . ,x,. . . ) = f(. . . ,y,. . . ) for any function f

x = y → (P(. . . ,x,. . . ) → P(. . . ,y,. . . )) for any relation P (including the equality relation itself)

These are, too, axiom schemata: they define an algorithm which decides whether a given formula is an axiom. In Mathematical logic, an axiom schema generalizes the notion of Axiom. Thus this is a recursive set of axioms. In Computability theory, a set of Natural numbers is called recursive, computable or decidable if there is an Algorithm

The next most common convention is to include the equality symbol as one of the relations of a theory, and add the equality axioms to the axioms of the theory. In practice this is almost indistinguishable from the previous convention, except in the unusual case of theories with no notion of equality. The axioms are the same, and the only difference is whether one calls some of them logical axioms or axioms of the theory.
In theories with no functions and a finite number of relations, it is possible to define equality in terms of the relations, by defining the two terms s and t to be equal if any relation is unchanged by changing s to t in any argument.

For example, in set theory with one relation $\in$ , we may define s = t to be an abbreviation for $\forall$ x (s $\in$ x $\leftrightarrow$ t $\in$ x) $\wedge$ $\forall$ x (x $\in$ s $\leftrightarrow$ x $\in$ t). This definition of equality then automatically satisfies the axioms for equality. In this case, one should replace the usual axiom of extensionality, $\forall x \forall y [ \forall z (z \in x \Leftrightarrow z \in y) \Rightarrow x = y]$ , by $\forall x \forall y [ \forall z (z \in x \Leftrightarrow z \in y) \Rightarrow \forall z (x \in z \Leftrightarrow y \in z) ]$ , i. In Axiomatic set theory and the branches of Logic, Mathematics, and Computer science that use it the axiom of extensionality, or axiom e. if x and y have the same elements, then they belong to the same sets.

In some theories it is possible to give ad hoc definitions of equality. For example, in a theory of partial orders with one relation ≤ we could define s = t to be an abbreviation for s ≤ t $\wedge$ t ≤ s.

Semantics

Interpretations

Main article: Interpretation (logic)

In logic and mathematics, an interpretation (also mathematical interpretation, logico-mathematical interpretation, or commonly a model) gives meaning to an artificial or formal language by assigning a denotation to all non-logical constants in that language or in a sentence of that language. In Logic an interpretation gives meaning to an artificial or Formal language or to a sentence of such a language by assigning a denotation (extension

For a given formal language L, or a sentence Φ of L, an interpretation assigns a denotation to each non-logical constant occurring in L or Φ. To individual constants it assigns individuals (from some universe of discourse); to predicates of degree 1 it assigns properties (more precisely sets) ; to predicates of degree 2 it assigns binary relations of individuals; to predicates of degree 3 it assigns ternary relations of individuals, and so on; and to sentential letters it assigns truth-values.

More precisely, an interpretation of a formal language L or of a sentence Φ of L, consists of a non-empty domain D (i. e. a non-empty set) as the universe of discourse together with an assignment that associates with each individual constant of L or of Φ an element of D with each sentential symbol of L or of Φ one of the truth-values T or F with each n-ary operation or function symbol of L or of Φ an n-ary operation with respect to D (i. e. a function from $D n$ into $D$ ) with each n-ary predicate of L or of Φ an n-ary relation among elements of D and (optionally) with some binary predicate I of L, the identity relation among elements of D.

In this way an interpretation provides meaning or semantic values to the terms or formulae of the language. The study of the interpretations of formal languages is called formal semantics. [1] In mathematical logic an interpretation is a mathematical object that contains the necessary information for an interpretation in the former sense.

The symbols used in a formal language include variables, logical-constants, quantifiers and punctuation symbols as well as the non-logical constants. The interpretation of a sentence or language therefore depends on which non-logical constants it contains. Languages of the sentential (or propositional) calculus are allowed sentential symbols as non-logical constants. Languages of the first order predicate calculus allow in addition individual constants, predicate symbols and operation or function symbols.

Models

A model is a pair $\langle D,I \rangle$ , where D is a set of elements called the domain while I is an interpretation of the elements of a signature (constants, functions, and predicates).

the domain D is a set of elements;
the interpretation I if a function that assigns something to constants, functions and predicates:
- each constant c is assigned is a value of the domain I(c)
- each function symbol f of arity n is assigned a function I(f) from $D n$ to $D$
- each predicate symbol P of arity n is assigned a relation I(P) over $D n$ or, equivalently, a function from $D n$ to ${t r u e, f a l s e}$

The following is an intuitive explanation of these elements.

The domain D is a set of "objects" of some kind. Intuitively, a first-order formula is a statement about objects; for example, $\exists x . P(x)$ states the existence of an object x such that the predicate P is true where referred to it. The domain is the set of considered objects. As an example, one can take $D$ to be the set of integer numbers.

The model also includes an interpretation of the signature. Since the elements of the signature are constants, function symbols, and predicate symbols, the interpretation gives the "value" of constants, functions, and predicates.

The interpretation of a constant is simply an object. This means that the interpretation tells which objects a given constant refers to. For example, an interpretation may assign the value $I (c) = 10$ to the constant $c$ .

The interpretation of a function symbol is a function. For example, the function symbol $f (_,_)$ of arity 2 can be interpreted as the function that gives the sum of its arguments. In other words, the symbol $f$ is associated the function I(f) of addition in this interpretation.

The difference between constants and functions is that a constants is associated to a single element of the domain, while a function of arity n is associated to an element for any possible n-tuple of elements of the domain.

The interpretation of a predicate of arity n is a set of n-tuples of elements of the domain. This means that, given an interpretation, a predicate, and n elements of the domain, one can tell whether the predicate is true over those elements and according to the given interpretation. As an example, an interpretation I(P) of a predicate P of arity two may be the set of pairs of integers such that the first one is less than the second. According to this interpretation, the predicate P would be true if its first argument is less than the second.

Evaluation

A formula evaluates to true or false given a model and an interpretation of the value of the variables. Such an interpretation $μ$ associates every variable to a value of the domain.

The evaluation of a formula under a model $M=\langle D,I \rangle$ and an interpretation $μ$ of the variables is defined from the evaluation of a term under the same pair. Note that the model itself contains an interpretation (which evaluates constants, functions, and predicates); we additionally have, separated from the model, an interpretation

every constant is assigned its value according to the interpretation of the model, that is, the value of c is I(c);
every variable is associated its value according to $μ$
a term $f(t_1,\ldots,t_n)$ is associated the value given by the interpretation of the function and the interpretation of the terms: if $v_1,\ldots,v_n$ are the values associated to $t_1,\ldots,t_n$ , the term is associated the value $I(f)(v_1,\ldots,v_n)$ ; recall that $I (f)$ is the interpretation of f, and so is a function from $D n$ to D;

The interpretation of a formula is given as follows.

a formula $P(t_1,\ldots,t_n)$ is associated the value true or false depending on whether $v_1,\ldots,v_n \in I(D)$ , where $v_1,\ldots,v_n$ are the evaluation of the terms $t_1,\ldots,t_n$ and $I (P)$ is the interpretation of $P$ , which by assumption is a subset of $D n$
a formula in the form $\neg A$ or $A \rightarrow B$ is evaluated in the obvious way
a formula $\exists x . A$ is true according to M and $μ$ if there exists an evaluation $μ'$ of the variables that only differs from $μ$ regarding the evaluation of x and such that

A is true according to the model M and the interpretation $μ'$

a formula $\forall x . A$ is true according to M and $μ$ if A is true for every pair composed by the model M and an interpretation $μ'$ that differs from $μ$ only on the value of x

If a formula does not contain free variables, then the evaluation of the variables does not affects its truth. In other words, in this case F is true according to M and $μ$ if and only if is true according to M and a different interpretation of the variables $μ'$ .

Validity and satisfiability

A model M satisfies a formula F if this formula is true according to M and every possible evaluation of its variables. A formula is valid if it is true in every possible model and interpretation of the variables.

A formula is satisfiabile if there exists a model and an interpretation of the variables that satisfy the formula.

Predicate calculus

The predicate calculus is a proper extension of the propositional calculus that defines which statements of first-order logic are provable. This is a technical mathematical article about the area of mathematical logic variously known as "propositional calculus" or "propositional logic" Many (but not all) mathematical theories can be formulated in the predicate calculus. The word theory has many distinct meanings in different fields of Knowledge, depending on their methodologies and the context of discussion. If the propositional calculus is defined with a suitable set of axioms and the single rule of inference modus ponens (this can be done in many ways), then the predicate calculus can be defined by appending to the propositional calculus several axioms and the inference rule called "universal generalization". In Classical logic, modus ponendo ponens ( Latin: mode that affirms by affirming; often abbreviated to MP or modus ponens) is a As axioms for the predicate calculus we take:

All tautologies of the propositional calculus, taken schematically so that the uniform replacement of a schematic letter by a formula is allowed.
The quantifier axioms, given above.
The above axioms for equality, if equality is regarded as a logical concept.

A sentence is defined to be provable in first-order logic if it can be derived from the axioms of the predicate calculus, by repeatedly applying the inference rules "modus ponens" and "universal generalization". In other words:

An axiom of the predicate calculus is provable in first-order logic by definition.
If the premises of an inference rule are provable in first-order logic, then so is its conclusion. In Discourse and Logic, a premise is a claim that is a reason (or element of a set of reasons for or objection against some other claim A conclusion is a Proposition, which is arrived at after the consideration of Evidence, Arguments or Premises Logic

If we have a theory T (a set of statements, called axioms, in some language) then a sentence φ is defined to be provable in the theory T if

$a_1 \wedge a_2 \wedge \ldots \wedge a_n \rightarrow \varphi$

is provable in first-order logic, for some finite set of axioms $a_1, a_2,\ldots,a_n$ of the theory T. In other words, if one can prove in first-order logic that φ follows from the axioms of T. This also means, that we replace the above procedure for finding provable sentences by the following one:

An axiom of T is provable in T.
An axiom of the predicate calculus is provable in T.
If the premises of an inference rule are provable in T, then so is its conclusion. In Discourse and Logic, a premise is a claim that is a reason (or element of a set of reasons for or objection against some other claim A conclusion is a Proposition, which is arrived at after the consideration of Evidence, Arguments or Premises Logic

One apparent problem with this definition of provability is that it seems rather ad hoc: we have taken some apparently random collection of axioms and rules of inference, and it is unclear that we have not accidentally missed out some vital axiom or rule. Gödel's completeness theorem assures us that this is not really a problem: any statement true in all models (semantically true) is provable in first-order logic (syntactically true). Gödel's completeness theorem is a fundamental theorem in Mathematical logic that establishes a correspondence between semantic truth and syntactic provability in In particular, any reasonable definition of "provable" in first-order logic must be equivalent to the one above (though it is possible for the lengths of proofs to differ vastly for different definitions of provability).

There are many different (but equivalent) ways to define provability. The above definition is typical for a "Hilbert style" calculus, which has many axioms but very few rules of inference. By contrast, a "Gentzen style" predicate calculus has few axioms but many rules of inference. In Proof theory and Mathematical logic, the sequent calculus is a widely known Proof calculus for First-order logic (and Propositional logic

Provable identities

The following sentences can be called "identities" because the main connective in each is the biconditional. In Logic and Mathematics, logical biconditional (sometimes also known as the material biconditional) is a Logical operator connecting two statements They are all provable in FOL, and are useful when manipulating the quantifiers:

$\lnot \forall x \, P(x) \Leftrightarrow \exists x \, \lnot P(x)$

$\lnot \exists x \, P(x) \Leftrightarrow \forall x \, \lnot P(x)$

$\forall x \, \forall y \, P(x,y) \Leftrightarrow \forall y \, \forall x \, P(x,y)$

$\exists x \, \exists y \, P(x,y) \Leftrightarrow \exists y \, \exists x \, P(x,y)$

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

$\exists x \, P(x) \lor \exists x \, Q(x) \Leftrightarrow \exists x \, (P(x) \lor Q(x))$

$P \land \exists x \, Q(x) \Leftrightarrow \exists x \, (P \land Q(x))$ (where

x

must not occur free in

P

)

$P \lor \forall x \, Q(x) \Leftrightarrow \forall x \, (P \lor Q(x))$ (where

x

must not occur free in

P

)

Provable inference rules

The main connective in the following sentences, also provable in FOL, is the conditional. The material conditional, also known as the material implication or truth functional conditional, expresses a property of certain Conditionals in Logic These sentences can be seen as the justification for inference rules in addition to modus ponens and universal generalization discussed above and assumed valid:

$\exists x \, \forall y \, P(x,y) \Rightarrow \forall y \, \exists x \, P(x,y)$

$\forall x \, P(x) \lor \forall x \, Q(x) \Rightarrow \forall x \, (P(x) \lor Q(x))$

$\exists x \, (P(x) \land Q(x)) \Rightarrow \exists x \, P(x) \land \exists x \, Q(x)$

$\exists x \, P(x) \land \forall x \, Q(x) \Rightarrow \exists x \, (P(x) \land Q(x))$

$\forall x \, P(x) \Rightarrow P(c)$ (If c is a variable, then it must not be previously quantified in P(x))

$P(c) \Rightarrow \exists x \, P(x)$ (there must be no free instance of x in P(c))

Metalogical theorems of first-order logic

Some important metalogical theorems are listed below in bulleted form. In Classical logic, modus ponendo ponens ( Latin: mode that affirms by affirming; often abbreviated to MP or modus ponens) is a What they roughly mean is that a sentence is valid if and only if it is provable. Furthermore, one can construct an algorithm which works as follows: if a sentence is provable, the algorithm will tell us that in a finite but unknown amount of time. If a sentence is unprovable, the algorithm will run forever, and we will not know whether the sentence is unprovable or provable and the algorithm has just not yet told us that. Such an algorithm is called semidecidable or recursively enumerable. In Computability theory, traditionally called Recursion theory, a set S of Natural numbers is called recursively enumerable, computably

One may construct an algorithm which will determine in finite number of steps whether a sentence is provable (a decidable algorithm) only for simple classes of first-order logic. In Logic, the term decidable refers to the existence of an Effective method for determining membership in a set of formulas

The decision problem for validity is recursively enumerable; in other words, there is a Turing machine that when given any sentence as input, will halt if and only if the sentence is valid (true in all models). In Computability theory, traditionally called Recursion theory, a set S of Natural numbers is called recursively enumerable, computably Turing machines are basic abstract symbol-manipulating devices which despite their simplicity can be adapted to simulate the logic of any Computer Algorithm
- As Gödel's completeness theorem shows, for any valid formula P, P is provable. Gödel's completeness theorem is a fundamental theorem in Mathematical logic that establishes a correspondence between semantic truth and syntactic provability in Conversely, assuming consistency of the logic, any provable formula is valid.
- The Turing machine can be one which generates all provable formulas in the following manner: for a finite or recursively enumerable set of axioms, such a machine can be one that generates an axiom, then generates a new provable formula by application of axioms and inference rules already generated, then generate another axiom, and so on. In Computability theory, traditionally called Recursion theory, a set S of Natural numbers is called recursively enumerable, computably Given a sentence as input, the Turing machine simply go on and generates all provable formulas one by one, and will halt if it generates the sentence.
Unlike the propositional logic, first-order logic is undecidable, provided that the language has at least one predicate of valence at least 2 other than equality. This is a technical mathematical article about the area of mathematical logic variously known as "propositional calculus" or "propositional logic" In Logic, the term decidable refers to the existence of an Effective method for determining membership in a set of formulas This means that there is no decision procedure that correctly determines whether an arbitrary formula is valid. In Computability theory and Computational complexity theory, a decision problem is a question in some Formal system with a yes-or-no answer depending on Because there is a Turing machine as described above, the undecidability is related to the unsolvability of the Halting problem: there is no algorithm which determines after a finite number of steps whether the Turing machine will ever halt for a given sentence as its input, hence whether the sentence is provable. In Logic, the term decidable refers to the existence of an Effective method for determining membership in a set of formulas In computability theory, the halting problem is a Decision problem which can be stated as follows given a description of a program and a finite input This result was established independently by Church and Turing. Alonzo Church ( June 14, 1903 – August 11, 1995) was an American Mathematician and logician Alan Mathison Turing, OBE, FRS (ˈt(jʊ(ərɪŋ (23 June 1912 &ndash 7 June 1954 was an English Mathematician
Monadic predicate logic (i. In Logic, the monadic predicate calculus is the fragment of Predicate calculus in which all predicate letters are monadic (that is they take e. , predicate logic with only predicates of one argument and no functions) is decidable.
The Bernays–Schönfinkel class of first-order formulas is also decidable. The Bernays–Schönfinkel class of formulas named after Paul Bernays and Moses Schönfinkel, is a decidable fragment of First-order logic formulas

Translating natural language to first-order logic

Concepts expressed in natural language must be "translated" to first-order logic (FOL) before FOL can be used to address them, and there are a number of potential pitfalls in this translation. In FOL, $p \or q$ means "p, or q, or both", that is, it is inclusive. In English, the word "or" is sometimes inclusive (e. g, "cream or sugar?"), but sometimes it is exclusive (e. g. , "coffee or tea?" is usually intended to mean one or the other, not both). Similarly, the English word "some" may mean "at least one, possibly all", but other times it may mean "not all, possibly none". The English word "and" should sometimes be translated as "or" (e. g. , "men and women may apply"). ^[4]

Limitations of first-order logic

All mathematical notations have their strengths and weaknesses; here are a few such issues with first-order logic.

Difficulty representing if-then-else

Oddly enough, FOL with equality (as typically defined) does not include or permit defining an if-then-else predicate or function if(c,a,b), where "c" is a condition expressed as a formula, while a and b are either both terms or both formulas, and its result would be "a" if c is true, and "b" if it is false. The problem is that in FOL, both predicates and functions can only accept terms ("non-booleans") as parameters, but the "obvious" representation of the condition is a formula ("boolean"). This is unfortunate, since many mathematical functions are conveniently expressed in terms of if-then-else, and if-then-else is fundamental for describing most computer programs.

Mathematically, it is possible to redefine a complete set of new functions that match the formula operators, but this is quite clumsy. ^[5] A predicate if(c,a,b) can be expressed in FOL if rewritten as $(c \wedge a) \or (\neg c \wedge b)$ (or, equivalently, $(c \rightarrow a) \wedge (\neg c \rightarrow b)$ ), but this is clumsy if the condition c is complex. Many extend FOL to add a special-case predicate named "if(condition, a, b)" (where a and b are formulas) and/or function "ite(condition, a, b)" (where a and b are terms), both of which accept a formula as the condition, and are equal to "a" if condition is true and "b" if it is false. These extensions make FOL easier to use for some problems, and make some kinds of automatic theorem-proving easier. ^[6] Others extend FOL further so that functions and predicates can accept both terms and formulas at any position.

Typing (Sorts)

FOL does not include types (sorts) into the notation itself, other than the difference between formulas ("booleans") and terms ("non-booleans"). Some argue that this lack of types is a great advantage ^[7], but many others find advantages in defining and using types (sorts), such as helping reject some erroneous or undesirable specifications^[8]. Those who wish to indicate types must provide such information using the notation available in FOL. Doing so can make such expressions more complex, and can also be easy to get wrong.

Single-parameter predicates can be used to implement the notion of types where appropriate. For example, in: $\forall x \mathit{Man}(x) \rightarrow \mathit{Mortal}(x)$ , the predicate $M a n (x)$ could be considered a kind of "type assertion" (that is, that $x$ must be a man). Predicates can also be used with the "exists" quantifier to identify types, but this should usually be done with the "and" operator instead, e. g. : $\exists x \mathit{Man}(x) \wedge \mathit{Mortal}(x)$ ("there exists something that is both a man and is mortal"). It is easy to write $\exists x \mathit{Man}(x) \rightarrow \mathit{Mortal}(x)$ , but this would be equivalent to $(\exists x \neg \mathit{Man}(x)) \or \exists x \mathit{Mortal}(x)$ ("there is something that is not a man, and/or there exists something that is mortal"), which is usually not what was intended. Similarly, assertions can be made that one type is a subtype of another type, e. g. : $\forall x \mathit{Man}(x) \rightarrow \mathit{Mammal}(x)$ ("for all $x$ , if $x$ is a man, then $x$ is a mammal").

Difficulty in characterizing finiteness or countability

Main article: Second-order logic

It follows from the Löwenheim–Skolem theorem that it is not possible to characterize finiteness or countability in first-order logic. In Logic and Mathematics second-order logic is an extension of First-order logic, which itself is an extension of Propositional logic. In Mathematical logic, the Löwenheim–Skolem theorem states that if a countable first-order theory has an infinite model then for every infinite Cardinal number For example, in first-order logic one cannot assert the least-upper-bound property for sets of real numbers, which states that every bounded, nonempty set of real numbers has a supremum; A second-order logic is needed for that. In Mathematics, the real numbers may be described informally in several different ways In Logic and Mathematics second-order logic is an extension of First-order logic, which itself is an extension of Propositional logic.

Graph reachability cannot be expressed

Many situations can be modeled as a graph of nodes and directed connections (edges). In Mathematics and Computer science, a graph is the basic object of study in Graph theory. For example, validating many systems requires showing that a "bad" state cannot be reached from a "good" state, and these interconnections of states can often be modelled as a graph. However, it can be proved that connectedness cannot be fully expressed in predicate logic. In other words, there is no predicate-logic formula $φ$ and $R$ as its only predicate symbol (of arity 2) such that $φ$ holds in a interpretation $I$ if and only if the extension of $R$ in $I$ describes a connected graph: that is, connected graphs cannot be axiomatized.

Note that given a binary relation $R$ encoding a graph, one can describe $R$ in terms of a conjunction of first order formulas, and write a formula $φ R$ which is satisfiable if and only if $R$ is connected. ^[9]

Comparison with other logics

Typed first-order logic allows variables and terms to have various types (or sorts). If there are only a finite number of types, this does not really differ much from first-order logic, because one can describe the types with a finite number of unary predicates and a few axioms. Sometimes there is a special type Ω of truth values, in which case formulas are just terms of type Ω.
First-order logic with domain conditions adds domain conditions (DCs) to classical first-order logic, enabling the handling of partial functions; these conditions can be proven "on the side" in a manner similar to PVS's type correctness conditions. PVS, or the Prototype Verification System, is a Specification language integrated with support tools and a Theorem prover. It also adds if-then-else to keep definitions and proofs manageable (they became too complex without them). ^[10]
The SMT-LIB Standard defines a language used by many research groups for satisfiability modulo theories; the full logic is based on FOL with equality, but adds sorts (types), if-then-else for terms and formulas (ite() and if. . then. . else. . ), a let construct for terms and formulas (let and flet), and a distinct construct declaring a set of listed values as distinct. Its connectives are not, implies, and, or, xor, and iff. ^[11]
Weak second-order logic allows quantification over finite subsets.
Monadic second-order logic allows quantification over subsets, or in other words over unary predicates.
Second-order logic allows quantification over subsets and relations, or in other words over all predicates. In Logic and Mathematics second-order logic is an extension of First-order logic, which itself is an extension of Propositional logic. For example, the axiom of extensionality can be stated in second-order logic as x = y ≡_def $\forall$ P (P(x) ↔ P(y)). In Axiomatic set theory and the branches of Logic, Mathematics, and Computer science that use it the axiom of extensionality, or axiom The strong semantics of second-order logic give such sentences a much stronger meaning than first-order semantics.
Higher-order logics allows quantification over higher types than second-order logic permits. In Mathematics, higher-order logic is distinguished from First-order logic in a number of ways These higher types include relations between relations, functions from relations to relations between relations, etc.
Intuitionistic first-order logic uses intuitionistic rather than classical propositional calculus; for example, ¬¬φ need not be equivalent to φ. Intuitionistic logic, or constructivist logic, is the Symbolic logic system originally developed by Arend Heyting to provide a formal basis for Brouwer Similarly, first-order fuzzy logics are first-order extensions of propositional fuzzy logics rather than classical logic. T-norm fuzzy logics are a family of Non-classical logics informally delimited by having a semantics which takes the real unit interval for the system of truth values and functions
Modal logic has extra modal operators with meanings which can be characterised informally as, for example "it is necessary that φ" and "it is possible that φ". A modal logic is any system of formal logic that attempts to deal with modalities.
In monadic predicate calculus predicates are restricted to having only one argument. In Logic, the monadic predicate calculus is the fragment of Predicate calculus in which all predicate letters are monadic (that is they take
Infinitary logic allows infinitely long sentences. Those unfamiliar with Mathematical logic or the concept of Ordinals are advised to consult those articles first For example, one may allow a conjunction or disjunction of infinitely many formulas, or quantification over infinitely many variables. Infinitely long sentences arise in areas of mathematics including topology and model theory. Topology ( Greek topos, "place" and logos, "study" is the branch of Mathematics that studies the properties of In Mathematics, model theory is the study of (classes of mathematical structures such as groups, Fields graphs or even models
First-order logic with extra quantifiers has new quantifiers Qx,. . . , with meanings such as "there are many x such that . . . ". Also see branching quantifiers and the plural quantifiers of George Boolos and others. In Logic a branching quantifier is a partial ordering \langle Qx_1\dots Qx_n\rangle of Quantifiers for Q∈{∀∃} In Mathematics and logic, plural quantification is the theory that an individual Variable x may take on George Stephen Boolos ( September 4, 1940, New York City – May 27, 1996) was a Philosopher and a Mathematical logician
Predicate Logic with Definitions (PLD, or D-logic) modifies FOL by formally adding syntactic definitions as a type of value (in addition to formulas and terms); these definitions can be used inside terms and formulas^[12].
Independence-friendly logic is characterized by branching quantifiers, which allow one to express independence between quantified variables. Independence-friendly logic ( IF logic) proposed by Jaakko Hintikka and Gabriel Sandu, aims at being a more natural and intuitive alternative to classical In Logic a branching quantifier is a partial ordering \langle Qx_1\dots Qx_n\rangle of Quantifiers for Q∈{∀∃}

Most of these logics are in some sense extensions of FOL: they include all the quantifiers and logical operators of FOL with the same meanings. Lindström showed that FOL has no extensions (other than itself) that satisfy both the compactness theorem and the downward Löwenheim–Skolem theorem. In Mathematical logic, the compactness theorem states that a (possibly Infinite) set of first-order sentences has a model, Iff every In Mathematical logic, the Löwenheim–Skolem theorem states that if a countable first-order theory has an infinite model then for every infinite Cardinal number A precise statement of Lindström's theorem requires a few technical conditions that the logic is assumed to satisfy; for example, changing the symbols of a language should make no essential difference to which sentences are true. In Mathematical logic, Lindström's theorem states that First-order logic is the strongest logic (satisfying certain conditions e

Algebraizations

Three ways of eliminating quantified variables from FOL, and that do not involve replacing quantifiers with other variable binding term operators, are known:

Cylindric algebra, by Alfred Tarski and his coworkers;
Polyadic algebra, by Paul Halmos;
Predicate functor logic, mainly due to Willard Quine. The notion of cylindric algebra, invented by Alfred Tarski, arises naturally in the algebraization of First-order logic. Alfred Tarski ( January 14, 1901, Warsaw, Russian ruled Poland – October 26, 1983, Berkeley California Paul Richard Halmos ( March 3 1916 &mdash October 2 2006) was a Hungarian -born Jewish American Mathematician In Mathematical logic, predicate functor logic (PFL is one of several ways to express First-order logic (formerly known as Predicate logic) by purely algebraic Willard Van Orman Quine (June 25 1908 Akron, Ohio &ndash December 25 2000 (known to intimates as "Van"

These algebras:

Are all proper extensions of the two-element Boolean algebra, and thus are lattices;
Do for FOL what Lindenbaum-Tarski algebra does for sentential logic;
Allow results from abstract algebra, universal algebra, and order theory to be brought to bear on FOL. Algebra is a branch of Mathematics concerning the study of structure, relation, and Quantity. In Mathematics and Abstract algebra, the two-element Boolean algebra is the Boolean algebra whose underlying set (or Universe or In Mathematics, a lattice is a Partially ordered set (also called a poset) in which every pair of elements has a unique Supremum (the elements' In Mathematical logic, the Lindenbaum-Tarski algebra A of a logical theory T consists of the Equivalence classes of sentences This is a technical mathematical article about the area of mathematical logic variously known as "propositional calculus" or "propositional logic" Abstract algebra is the subject area of Mathematics that studies Algebraic structures such as groups, rings, fields, modules Universal algebra (sometimes called general algebra) is the field of Mathematics that studies Algebraic structures themselves not examples ("models" Order theory is a branch of Mathematics that studies various kinds of Binary relations that capture the intuitive notion of ordering providing a framework for saying

Tarski and Givant (1987) show that the fragment of FOL that has no atomic sentence lying in the scope of more than three quantifiers, has the same expressive power as relation algebra. In Logic, sentences (which are declarative sentences also variously called Propositions or statements) are those strings of words or symbols which are Relation algebra is different from Relational algebra, a framework developed by Edgar Codd in 1970 for Relational databases. This fragment is of great interest because it suffices for Peano arithmetic and most axiomatic set theory, including the canonical ZFC. In Mathematical logic, the Peano axioms, also known as the Dedekind-Peano axioms or the Peano postulates, are a set of Axioms for the Natural Zermelo–Fraenkel set theory with the axiom of choice, commonly abbreviated ZFC, is the standard form of Axiomatic set theory and as such is the most common They also prove that FOL with a primitive ordered pair is equivalent to a relation algebra with two ordered pair projection functions. In Mathematics, an ordered pair is a collection of two distinguishable objects one of which is identified as the first coordinate (or the first entry

Automation

Theorem proving for first-order logic is one of the most mature subfields of automated theorem proving. Automated theorem proving ( ATP) or automated deduction, currently the most well-developed subfield of Automated reasoning (AR is the The logic is expressive enough to allow the specification of arbitrary problems, often in a reasonably natural and intuitive way. On the other hand, it is still semidecidable, and a number of sound and complete calculi have been developed, enabling fully automated systems. In Computability theory, traditionally called Recursion theory, a set S of Natural numbers is called recursively enumerable, computably In 1965 J. Alan Robinson achieved an important breakthrough with his resolution approach; to prove a theorem it tries to refute the negated theorem, in a goal-directed way, resulting in a much more efficient method to automatically prove theorems in FOL. In Mathematical logic and Automated theorem proving, resolution is a rule of Inference leading to a refutation Theorem-proving technique More expressive logics, such as higher-order and modal logics, allow the convenient expression of a wider range of problems than first-order logic, but theorem proving for these logics is less well developed.

A modern and particularly disruptive new technology is that of SMT solvers, which add arithmetic and propositional support to the powerful classes of SAT solvers. Satisfiability Modulo Theories (SMT problem is a Decision problem for logical formulas with respect to combinations of background theories expressed in classical

References

^ The word language is sometimes used as a synonym for signature, but this can be confusing because "language" can also refer to the set of formulas.
^ More precisely, there is only one language of each variant of one-sorted first-order logic: with or without equality, with or without functions, with or without propositional variables, ….
^ For another well-worked example, see Metamath proof explorer
^ Suber, Peter, Translation Tips, <http://www.earlham.edu/~peters/courses/log/transtip.htm>. Retrieved on 20 September 2007
^ Otter Example if.in, <http://www-unix.mcs.anl.gov/AR/otter/examples33/fringe/if.in>. Retrieved on 21 September 2007
^ Manna, Zohar (1974), Mathematical Theory of Computation, McGraw-Hill Computer Science Series, New York, New York: McGraw-Hill Book Company, pp. 77-147, ISBN 0-07-039910-7
^ Leslie Lamport, Lawrence C. Paulson. Should Your Specification Language Be Typed? ACM Transactions on Programming Languages and Systems. 1998. http://citeseer.ist.psu.edu/71125.html
^ Rushby, John. Subtypes for Specification. 1997. Proceedings of the Sixth European Software Engineering Conference (ESEC/FSE 97). http://citeseer.ist.psu.edu/328947.html
^ Huth, Michael & Ryan, Mark (2004), Logic in Computer Science, 2nd edition, pp. 138-139, ISBN 0-521-54310-X
^ Freek Wiedijk and Jan Zwanenburg. "First Order Logic with Domain Conditions" In Theorem Proving in Higher Order Logics. Book Series "Lecture Notes in Computer Science". Springer Berlin / Heidelberg. ISSN 0302-9743 (Print) 1611-3349 (Online), Volume 2758/2003. ISBN 978-3-540-40664-8. http://www.springerlink.com/content/8uh32tu7uf04yeex/
^ Ranise, Silvio and Cesare Tinelli. The SMT-LIB Standard: Version 1. 2 Aug 30, 2006. http://smt-lib.org/
^ Makarov, Victor. "Predicate Logic with Definitions". http://arxiv.org/pdf/cs/9906010

Jon Barwise and John Etchemendy, 2000. Kenneth Jon Barwise ( June 29, 1942 - March 5, 2000) was a US John W Etchemendy (b 1952 in Reno Nevada is Stanford University 's twelfth and current Provost. Language Proof and Logic. CSLI (University of Chicago Press) and New York: Seven Bridges Press.
David Hilbert and Wilhelm Ackermann 1950. David Hilbert ( January 23, 1862 &ndash February 14, 1943) was a German Mathematician, recognized as one of the most Wilhelm Friedrich Ackermann ( March 29, 1896, Herscheid municipality Germany &ndash December 24, 1962 Lüdenscheid Principles of Theoretical Logic (English translation). Principles of Mathematical Logic is the 1950 American translation of the 1938 second edition of David Hilbert 's and Wilhelm Ackermann 's classic text Chelsea. The 1928 first German edition was titled Grundzüge der theoretischen Logik.
Wilfrid Hodges, 2001, "Classical Logic I: First Order Logic," in Lou Goble, ed. Wilfrid Hodges (born 1941 is a British Mathematician, known for his work in Model theory. , The Blackwell Guide to Philosophical Logic. Blackwell.

External links

Stanford Encyclopedia of Philosophy: "Classical Logic -- by Stewart Shapiro. Automated theorem proving ( ATP) or automated deduction, currently the most well-developed subfield of Automated reasoning (AR is the The notion of cylindric algebra, invented by Alfred Tarski, arises naturally in the algebraization of First-order logic. Gödel's completeness theorem is a fundamental theorem in Mathematical logic that establishes a correspondence between semantic truth and syntactic provability in In Mathematical logic, Gödel's incompleteness theorems, proved by Kurt Gödel in 1931 are two Theorems stating inherent limitations of all but the most In Mathematical logic, a first-order theory is given by a set of axioms in somelanguage This is a list of rules of inference, logical laws that relate to mathematical formulae Mathematical logic is a subfield of Logic and Mathematics with close connections to Computer science and Philosophical logic. In Mathematical logic, predicate functor logic (PFL is one of several ways to express First-order logic (formerly known as Predicate logic) by purely algebraic Logical connectiveIn Logic, a set of symbols is commonly used to express logical representation The algebra of sets develops and describes the basic properties and laws of sets, the set-theoretic operations of union, intersection, and complementation The Stanford Encyclopedia of Philosophy (SEP is a freely-accessible Online encyclopedia of Philosophy maintained by Stanford University. Covers syntax, model theory, and metatheory for first-order logic in the natural deduction style.
forall x: an introduction to formal logic, by P. D. Magnus, covers formal semantics and proof theory for first-order logic.
Metamath: an ongoing online project to reconstruct mathematics as a huge first-order theory, using first-order logic and the axiomatic set theory ZFC. Zermelo–Fraenkel set theory with the axiom of choice, commonly abbreviated ZFC, is the standard form of Axiomatic set theory and as such is the most common Principia Mathematica modernized and done right. The Principia Mathematica is a 3-volume work on the Foundations of mathematics, written by Alfred North Whitehead and Bertrand Russell
Podnieks, Karl. Introduction to mathematical logic.
Cambridge Mathematics Tripos Notes : "[1] -- Notes typeset by John Fremlin. The notes cover part of a past Cambridge Mathematics Tripos course taught to undergraduates students (usually) within their third year. The course is entitled "Logic, Computation and Set Theory" and covers Ordinals and cardinals, Posets and zorn’s Lemma, Propositional logic, Predicate logic, Set theory and Consistency issues related to ZFC and other set theories.

Dictionary

-noun

(logic) A formal deductive system extended from propositional logic with the possibility to quantify over individuals of the domain of discourse.

© 2009 citizendia.org; parts available under the terms of GNU Free Documentation License, from http://en.wikipedia.org
network: | |

Contents