|
First-order logic—also known as first-order predicate calculus and
predicate logic—is a collection of formal systems used in
mathematics, philosophy, linguistics, and computer science.
First-order logic
Contents 1 Introduction 2 Syntax 2.1 Alphabet 2.1.1 Logical symbols 2.1.2 Non-logical symbols 2.2 Formation rules 2.2.1 Terms 2.2.2 Formulas 2.2.3 Notational conventions 2.3 Free and bound variables 2.4 Example: ordered abelian groups 3 Semantics 3.1 First-order structures 3.2 Evaluation of truth values 3.3 Validity, satisfiability, and logical consequence 3.4 Algebraizations 3.5 First-order theories, models, and elementary classes 3.6 Empty domains 4 Deductive systems 4.1 Rules of inference 4.2 Hilbert-style systems and natural deduction 4.3 Sequent calculus 4.4 Tableaux method 4.5 Resolution 4.6 Provable identities 5 Equality and its axioms 5.1
First-order logic
6 Metalogical properties 6.1 Completeness and undecidability 6.2 The Löwenheim–Skolem theorem 6.3 The compactness theorem 6.4 Lindström's theorem 7 Limitations 7.1 Expressiveness 7.2 Formalizing natural languages 8 Restrictions, extensions, and variations 8.1 Restricted languages 8.2 Many-sorted logic 8.3 Additional quantifiers 8.4 Infinitary logics 8.5 Non-classical and modal logics 8.6 Fixpoint logic 8.7 Higher-order logics 9 Automated theorem proving and formal methods 10 See also 11 Notes 12 References 13 External links Introduction[edit] While propositional logic deals with simple declarative propositions, first-order logic additionally covers predicates and quantification. A predicate takes an entity or entities in the domain of discourse as input and outputs either True or False. Consider the two sentences "Socrates is a philosopher" and "Plato is a philosopher". In propositional logic, these sentences are viewed as being unrelated and might be denoted, for example, by variables such as p and q. The predicate "is a philosopher" occurs in both sentences, which have a common structure of "a is a philosopher". The variable a is instantiated as "Socrates" in the first sentence and is instantiated as "Plato" in the second sentence. While first-order logic allows for the use of predicates, such as "is a philosopher" in this example, propositional logic does not.[5] Relationships between predicates can be stated using logical connectives. Consider, for example, the first-order formula "if a is a philosopher, then a is a scholar". This formula is a conditional statement with "a is a philosopher" as its hypothesis and "a is a scholar" as its conclusion. The truth of this formula depends on which object is denoted by a, and on the interpretations of the predicates "is a philosopher" and "is a scholar". Quantifiers can be applied to variables in a formula. The variable a in the previous formula can be universally quantified, for instance, with the first-order sentence "For every a, if a is a philosopher, then a is a scholar". The universal quantifier "for every" in this sentence expresses the idea that the claim "if a is a philosopher, then a is a scholar" holds for all choices of a. The negation of the sentence "For every a, if a is a philosopher, then a is a scholar" is logically equivalent to the sentence "There exists a such that a is a philosopher and a is not a scholar". The existential quantifier "there exists" expresses the idea that the claim "a is a philosopher and a is not a scholar" holds for some choice of a. The predicates "is a philosopher" and "is a scholar" each take a single variable. In general, predicates can take several variables. In the first-order sentence "Socrates is the teacher of Plato", the predicate "is the teacher of" takes two variables. An interpretation (or model) of a first-order formula specifies what each predicate means and the entities that can instantiate the variables. These entities form the domain of discourse or universe, which is usually required to be a nonempty set. For example, in an interpretation with the domain of discourse consisting of all human beings and the predicate "is a philosopher" understood as "was the author of the Republic", the sentence "There exists a such that a is a philosopher" is seen as being true, as witnessed by Plato. Syntax[edit] There are two key parts of first-order logic. The syntax determines which collections of symbols are legal expressions in first-order logic, while the semantics determine the meanings behind these expressions. Alphabet[edit] Unlike natural languages, such as English, the language of first-order logic is completely formal, so that it can be mechanically determined whether a given expression is legal. There are two key types of legal expressions: terms, which intuitively represent objects, and formulas, which intuitively express predicates that can be true or false. The terms and formulas of first-order logic are strings of symbols, which together form the alphabet of the language. As with all formal languages, the nature of the symbols themselves is outside the scope of formal logic; they are often regarded simply as letters and punctuation symbols. It is common to divide the symbols of the alphabet into logical symbols, which always have the same meaning, and non-logical symbols, whose meaning varies by interpretation. For example, the logical symbol ∧ displaystyle land always represents "and"; it is never interpreted as "or". On the other hand, a non-logical predicate symbol such as Phil(x) could be interpreted to mean "x is a philosopher", "x is a man named Philip", or any other unary predicate, depending on the interpretation at hand. Logical symbols[edit] There are several logical symbols in the alphabet, which vary by author but usually include: The quantifier symbols ∀ and ∃ The logical connectives: ∧ for conjunction, ∨ for disjunction, → for implication, ↔ for biconditional, ¬ for negation. Occasionally other logical connective symbols are included. Some authors use Cpq, instead of →, and Epq, instead of ↔, especially in contexts where → is used for other purposes. Moreover, the horseshoe ⊃ may replace →; the triple-bar ≡ may replace ↔; a tilde (~), Np, or Fpq, may replace ¬; , or Apq may replace ∨; and &, Kpq, or the middle dot, ⋅, may replace ∧, especially if these symbols are not available for technical reasons. (Note: the aforementioned symbols Cpq, Epq, Np, Apq, and Kpq are used in Polish notation.) Parentheses, brackets, and other punctuation symbols. The choice of such symbols varies depending on context. An infinite set of variables, often denoted by lowercase letters at the end of the alphabet x, y, z, ... . Subscripts are often used to distinguish variables: x0, x1, x2, ... . An equality symbol (sometimes, identity symbol) =; see the section on equality below. It should be noted that not all of these symbols are required – only one of the quantifiers, negation and conjunction, variables, brackets and equality suffice. There are numerous minor variations that may define additional logical symbols: Sometimes the truth constants T, Vpq, or ⊤, for "true" and F, Opq, or ⊥, for "false" are included. Without any such logical operators of valence 0, these two constants can only be expressed using quantifiers. Sometimes additional logical connectives are included, such as the Sheffer stroke, Dpq (NAND), and exclusive or, Jpq. Non-logical symbols[edit] The non-logical symbols represent predicates (relations), functions and constants on the domain of discourse. It used to be standard practice to use a fixed, infinite set of non-logical symbols for all purposes. A more recent practice is to use different non-logical symbols according to the application one has in mind. Therefore, it has become necessary to name the set of all non-logical symbols used in a particular application. This choice is made via a signature.[6] 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.[7] This approach is still common, especially in philosophically oriented books. For every integer n ≥ 0 there is a collection of n-ary, or n-place, predicate symbols. Because they represent relations between n elements, they are also called relation symbols. For each arity n we have an infinite supply of them: Pn0, Pn1, Pn2, Pn3, ... For every integer n ≥ 0 there are infinitely many n-ary function symbols: f n0, f n1, f n2, f n3, ... In contemporary mathematical logic, the signature varies by application. Typical signatures in mathematics are 1, × or just × for groups, or 0, 1, +, ×, < for ordered fields. There are no restrictions on the number of non-logical symbols. The signature can be empty, finite, or infinite, even uncountable. Uncountable signatures occur for example in modern proofs of the Löwenheim–Skolem theorem. In this approach, every non-logical symbol is of one of the following types. A predicate symbol (or relation symbol) with some valence (or arity, number of arguments) greater than or equal to 0. These are often denoted by uppercase letters P, Q, R,... . Relations of valence 0 can be identified with propositional variables. For example, P, which can stand for any statement. For example, P(x) is a predicate variable of valence 1. One possible interpretation is "x is a man". Q(x,y) is a predicate variable of valence 2. Possible interpretations include "x is greater than y" and "x is the father of y". A function symbol, with some valence greater than or equal to 0. These are often denoted by lowercase letters f, g, h,... . Examples: f(x) may be interpreted as 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, g(x,y) may stand for "x+y". In set theory, it may stand for "the union of x and y". Function symbols of valence 0 are called constant symbols, and are often denoted by lowercase letters at the beginning of the alphabet a, b, c,... . The symbol a may stand for Socrates. In arithmetic, it may stand for 0. In set theory, such a constant may stand for the empty set. The traditional approach can be recovered in the modern approach by simply specifying the "custom" signature to consist of the traditional sequences of non-logical symbols. Formation rules[edit] The formation rules define the terms and formulas of first order logic.[8] When terms and formulas are represented as strings of symbols, these rules can be used to write a formal grammar for terms and formulas. These rules are generally context-free (each production has a single symbol on the left side), except that the set of symbols may be allowed to be infinite and there may be many start symbols, for example the variables in the case of terms. Terms[edit] The set of terms is inductively defined by the following rules: Variables. Any variable is a term. Functions. Any expression f(t1,...,tn) of n arguments (where each argument ti is a term and f is a function symbol of valence n) is a term. In particular, symbols denoting individual constants are nullary function symbols, and are thus terms. Only expressions which can be obtained by finitely many applications of rules 1 and 2 are terms. For example, no expression involving a predicate symbol is a term. Formulas[edit] The set of formulas (also called well-formed formulas[9] or WFFs) is inductively defined by the following rules: Predicate symbols. If P is an n-ary predicate symbol and t1, ..., tn are terms then P(t1,...,tn) is a formula. Equality. If the equality symbol is considered part of logic, and t1 and t2 are terms, then t1 = t2 is a formula. Negation. If φ is a formula, then ¬ displaystyle lnot φ is a formula. Binary connectives. If φ and ψ are formulas, then (φ → displaystyle rightarrow ψ) is a formula. Similar rules apply to other binary logical connectives. Quantifiers. If φ displaystyle varphi is a formula and x is a variable, then ∀ x φ displaystyle forall xvarphi (for all x, φ displaystyle varphi holds) and ∃ x φ displaystyle exists xvarphi (there exists x such that φ displaystyle varphi ) are formulas. Only expressions which can be obtained by finitely many applications of rules 1–5 are formulas. The formulas obtained from the first two rules are said to be atomic formulas. For example, ∀ x ∀ y ( P ( f ( x ) ) → ¬ ( P ( x ) → Q ( f ( y ) , x , z ) ) ) displaystyle forall xforall y(P(f(x))rightarrow neg (P(x)rightarrow Q(f(y),x,z))) is a formula, if f is a unary function symbol, P a unary predicate symbol, and Q a ternary predicate symbol. On the other hand, ∀ x x → displaystyle forall x,xrightarrow is not a formula, although it is a string of symbols from the alphabet. The role of the parentheses in the definition is to ensure that any formula can only be obtained in one way by following the inductive definition (in other words, there is a unique parse tree for each formula). This property is known as unique readability of formulas. There are many conventions for where parentheses are used in formulas. For example, some authors use colons or full stops instead of parentheses, or change the places in which parentheses are inserted. Each author's particular definition must be accompanied by a proof of unique readability. This definition of a formula does not support defining an if-then-else function ite(c, a, b), where "c" is a condition expressed as a formula, that would return "a" if c is true, and "b" if it is false. This is because both predicates and functions can only accept terms as parameters, but the first parameter is a formula. Some languages built on first-order logic, such as SMT-LIB 2.0, add this.[10] Notational conventions[edit] For convenience, conventions have been developed about the precedence of the logical operators, to avoid the need to write parentheses in some cases. These rules are similar to the order of operations in arithmetic. A common convention is: ¬ displaystyle lnot is evaluated first ∧ displaystyle land and ∨ displaystyle lor are evaluated next Quantifiers are evaluated next → displaystyle to is evaluated last. Moreover, extra punctuation not required by the definition may be inserted to make formulas easier to read. Thus the formula ( ¬ ∀ x P ( x ) → ∃ x ¬ P ( x ) ) displaystyle (lnot forall xP(x)to exists xlnot P(x)) might be written as ( ¬ [ ∀ x P ( x ) ] ) → ∃ x [ ¬ P ( x ) ] . displaystyle (lnot [forall xP(x)])to exists x[lnot P(x)]. In some fields, it is common to use infix notation for binary relations and functions, instead of the prefix notation defined above. For example, in arithmetic, one typically writes "2 + 2 = 4" instead of "=(+(2,2),4)". It is common to regard formulas in infix notation as abbreviations for the corresponding formulas in prefix notation, cf. also term structure vs. representation. The definitions above use infix notation for binary connectives such as → displaystyle to . A less common convention is Polish notation, in which one writes → displaystyle rightarrow , ∧ displaystyle wedge , and so on in front of their arguments rather than between them. This convention allows all punctuation symbols to be discarded. Polish notation is compact and elegant, but rarely used in practice because it is hard for humans to read it. In Polish notation, the formula ∀ x ∀ y ( P ( f ( x ) ) → ¬ ( P ( x ) → Q ( f ( y ) , x , z ) ) ) displaystyle forall xforall y(P(f(x))rightarrow neg (P(x)rightarrow Q(f(y),x,z))) becomes "∀x∀y→Pfx¬→ PxQfyxz". Free and bound variables[edit] Main article: Free variables and bound variables In a formula, a variable may occur free or bound. Intuitively, a variable is free in a formula if it is not quantified: in ∀ y P ( x , y ) displaystyle forall y,P(x,y) , variable x is free while y is bound. The free and bound variables of a formula are defined inductively as follows. Atomic formulas. If φ is an atomic formula then x is free in φ if and only if x occurs in φ. Moreover, there are no bound variables in any atomic formula. Negation. x is free in ¬ displaystyle neg φ if and only if x is free in φ. x is bound in ¬ displaystyle neg φ if and only if x is bound in φ. Binary connectives. x is free in (φ → displaystyle rightarrow ψ) if and only if x is free in either φ or ψ. x is bound in (φ → displaystyle rightarrow ψ) if and only if x is bound in either φ or ψ. The same rule applies to any other binary connective in place of → displaystyle rightarrow . Quantifiers. x is free in ∀ displaystyle forall y φ if and only if x is free in φ and x is a different symbol from y. Also, x is bound in ∀ displaystyle forall y φ if and only if x is y or x is bound in φ. The same rule holds with ∃ displaystyle exists in place of ∀ displaystyle forall . For example, in ∀ displaystyle forall x ∀ displaystyle forall y (P(x) → displaystyle 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. Free and bound variables of a formula need not be disjoint sets: x is both free and bound in P ( x ) → ∀ x Q ( x ) displaystyle P(x)rightarrow forall x,Q(x) . Freeness and boundness can be also specialized to specific occurrences of variables in a formula. For example, in P ( x ) → ∀ x Q ( x ) displaystyle 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 ) displaystyle P(x) is free while the x displaystyle x in ∀ x Q ( x ) displaystyle forall x,Q(x) is bound. A formula in first-order logic with no free variables is called a first-order sentence. These are the formulas that will have well-defined truth values under an interpretation. For example, whether a formula such as Phil(x) is true must depend on what x represents. But the sentence ∃ x Phil ( x ) displaystyle exists x, text Phil (x) will be either true or false in a given interpretation. Example: ordered abelian groups[edit] In mathematics the language of ordered abelian groups has one constant symbol 0, one unary function symbol −, one binary function symbol +, and one binary relation symbol ≤. Then: The expressions +(x, y) and +(x, +(y, −(z))) are terms. These are usually written as x + y and x + y − z. The expressions +(x, y) = 0 and ≤(+(x, +(y, −(z))), +(x, y)) are atomic formulas. These are usually written as x + y = 0 and x + y − z ≤ x + y. The expression ( ∀ x ∀ y [ ≤ ( + ( x , y ) , z ) → ∀ x ∀ y + ( x , y ) = 0 ) ] displaystyle (forall xforall y,[mathop leq (mathop + (x,y),z)to forall x,forall y,mathop + (x,y)=0)] is a formula, which is usually written as ∀ x ∀ y ( x + y ≤ z ) → ∀ x ∀ y ( x + y = 0 ) . displaystyle forall xforall y(x+yleq z)to forall xforall y(x+y=0). This formula has one free variable, z. The axioms for ordered abelian groups can be expressed as a set of sentences in the language. For example, the axiom stating that the group is commutative is usually written ( ∀ x ) ( ∀ y ) [ x + y = y + x ] . displaystyle (forall x)(forall y)[x+y=y+x]. Semantics[edit] An interpretation of a first-order language assigns a denotation to all non-logical constants in that language. It also determines a domain of discourse that specifies the range of the quantifiers. The result is that each term is assigned an object that it represents, and each sentence is assigned a truth value. In this way, an interpretation provides semantic meaning to the terms and formulas of the language. The study of the interpretations of formal languages is called formal semantics. What follows is a description of the standard or Tarskian semantics for first-order logic. (It is also possible to define game semantics for first-order logic, but aside from requiring the axiom of choice, game semantics agree with Tarskian semantics for first-order logic, so game semantics will not be elaborated herein.) The domain of discourse D is a nonempty set of "objects" of some kind. Intuitively, a first-order formula is a statement about these objects; for example, ∃ x P ( x ) displaystyle exists xP(x) states the existence of an object x such that the predicate P is true where referred to it. The domain of discourse is the set of considered objects. For example, one can take D displaystyle D to be the set of integer numbers. The interpretation of a function symbol is a function. For example, if the domain of discourse consists of integers, a 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 with the function I(f) which, in this interpretation, is addition. The interpretation of a constant symbol is a function from the one-element set D0 to D, which can be simply identified with an object in D. For example, an interpretation may assign the value I ( c ) = 10 displaystyle I(c)=10 to the constant symbol c displaystyle c . The interpretation of an n-ary predicate symbol is a set of n-tuples of elements of the domain of discourse. This means that, given an interpretation, a predicate symbol, and n elements of the domain of discourse, one can tell whether the predicate is true of those elements according to the given interpretation. For example, an interpretation I(P) of a binary predicate symbol P 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. First-order structures[edit] Main article: Structure (mathematical logic) The most common way of specifying an interpretation (especially in mathematics) is to specify a structure (also called a model; see below). The structure consists of a nonempty set D that forms the domain of discourse and an interpretation I of the non-logical terms of the signature. This interpretation is itself a function: Each function symbol f of arity n is assigned a function I(f) from D n displaystyle D^ n to D displaystyle D . In particular, each constant symbol of the signature is assigned an individual in the domain of discourse. Each predicate symbol P of arity n is assigned a relation I(P) over D n displaystyle D^ n or, equivalently, a function from D n displaystyle D^ n to t r u e , f a l s e displaystyle mathrm true,false . Thus each predicate symbol is interpreted by a Boolean-valued function on D. Evaluation of truth values[edit] A formula evaluates to true or false given an interpretation, and a variable assignment μ that associates an element of the domain of discourse with each variable. The reason that a variable assignment is required is to give meanings to formulas with free variables, such as y = x displaystyle y=x . The truth value of this formula changes depending on whether x and y denote the same individual. First, the variable assignment μ can be extended to all terms of the language, with the result that each term maps to a single element of the domain of discourse. The following rules are used to make this assignment: Variables. Each variable x evaluates to μ(x) Functions. Given terms t 1 , … , t n displaystyle t_ 1 ,ldots ,t_ n that have been evaluated to elements d 1 , … , d n displaystyle d_ 1 ,ldots ,d_ n of the domain of discourse, and a n-ary function symbol f, the term f ( t 1 , … , t n ) displaystyle f(t_ 1 ,ldots ,t_ n ) evaluates to ( I ( f ) ) ( d 1 , … , d n ) displaystyle (I(f))(d_ 1 ,ldots ,d_ n ) . Next, each formula is assigned a truth value. The inductive definition used to make this assignment is called the T-schema. Atomic formulas (1). A formula P ( t 1 , … , t n ) displaystyle P(t_ 1 ,ldots ,t_ n ) is associated the value true or false depending on whether ⟨ v 1 , … , v n ⟩ ∈ I ( P ) displaystyle langle v_ 1 ,ldots ,v_ n rangle in I(P) , where v 1 , … , v n displaystyle v_ 1 ,ldots ,v_ n are the evaluation of the terms t 1 , … , t n displaystyle t_ 1 ,ldots ,t_ n and I ( P ) displaystyle I(P) is the interpretation of P displaystyle P , which by assumption is a subset of D n displaystyle D^ n . Atomic formulas (2). A formula t 1 = t 2 displaystyle t_ 1 =t_ 2 is assigned true if t 1 displaystyle t_ 1 and t 2 displaystyle t_ 2 evaluate to the same object of the domain of discourse (see the section on equality below). Logical connectives. A formula in the form ¬ ϕ displaystyle neg phi , ϕ → ψ displaystyle phi rightarrow psi , etc. is evaluated according to the truth table for the connective in question, as in propositional logic. Existential quantifiers. A formula ∃ x ϕ ( x ) displaystyle exists xphi (x) is true according to M and μ displaystyle mu if there exists an evaluation μ ′ displaystyle mu ' of the variables that only differs from μ displaystyle mu regarding the evaluation of x and such that φ is true according to the interpretation M and the variable assignment μ ′ displaystyle mu ' . This formal definition captures the idea that ∃ x ϕ ( x ) displaystyle exists xphi (x) is true if and only if there is a way to choose a value for x such that φ(x) is satisfied. Universal quantifiers. A formula ∀ x ϕ ( x ) displaystyle forall xphi (x) is true according to M and μ displaystyle mu if φ(x) is true for every pair composed by the interpretation M and some variable assignment μ ′ displaystyle mu ' that differs from μ displaystyle mu only on the value of x. This captures the idea that ∀ x ϕ ( x ) displaystyle forall xphi (x) is true if every possible choice of a value for x causes φ(x) to be true. If a formula does not contain free variables, and so is a sentence, then the initial variable assignment does not affect its truth value. In other words, a sentence is true according to M and μ displaystyle mu if and only if it is true according to M and every other variable assignment μ ′ displaystyle mu ' . There is a second common approach to defining truth values that does not rely on variable assignment functions. Instead, given an interpretation M, one first adds to the signature a collection of constant symbols, one for each element of the domain of discourse in M; say that for each d in the domain the constant symbol cd is fixed. The interpretation is extended so that each new constant symbol is assigned to its corresponding element of the domain. One now defines truth for quantified formulas syntactically, as follows: Existential quantifiers (alternate). A formula ∃ x ϕ ( x ) displaystyle exists xphi (x) is true according to M if there is some d in the domain of discourse such that ϕ ( c d ) displaystyle phi (c_ d ) holds. Here ϕ ( c d ) displaystyle phi (c_ d ) is the result of substituting cd for every free occurrence of x in φ. Universal quantifiers (alternate). A formula ∀ x ϕ ( x ) displaystyle forall xphi (x) is true according to M if, for every d in the domain of discourse, ϕ ( c d ) displaystyle phi (c_ d ) is true according to M. This alternate approach gives exactly the same truth values to all sentences as the approach via variable assignments. Validity, satisfiability, and logical consequence[edit] See also: Satisfiability If a sentence φ evaluates to True under a given interpretation M, one says that M satisfies φ; this is denoted M ⊨ φ displaystyle MvDash varphi . A sentence is satisfiable if there is some interpretation under which it is true. Satisfiability of formulas with free variables is more complicated, because an interpretation on its own does not determine the truth value of such a formula. The most common convention is that a formula with free variables is said to be satisfied by an interpretation if the formula remains true regardless which individuals from the domain of discourse are assigned to its free variables. This has the same effect as saying that a formula is satisfied if and only if its universal closure is satisfied. A formula is logically valid (or simply valid) if it is true in every interpretation. These formulas play a role similar to tautologies in propositional logic. A formula φ is a logical consequence of a formula ψ if every interpretation that makes ψ true also makes φ true. In this case one says that φ is logically implied by ψ. Algebraizations[edit] An alternate approach to the semantics of first-order logic proceeds via abstract algebra. This approach generalizes the Lindenbaum–Tarski algebras of propositional logic. There are three ways of eliminating quantified variables from first-order logic that do not involve replacing quantifiers with other variable binding term operators: Cylindric algebra, by
Alfred Tarski
These algebras are all lattices that properly extend the two-element Boolean algebra. Tarski and Givant (1987) showed that the fragment of first-order logic that has no atomic sentence lying in the scope of more than three quantifiers has the same expressive power as relation algebra. This fragment is of great interest because it suffices for Peano arithmetic and most axiomatic set theory, including the canonical ZFC. They also prove that first-order logic with a primitive ordered pair is equivalent to a relation algebra with two ordered pair projection functions. First-order theories, models, and elementary classes[edit] A first-order theory of a particular signature is a set of axioms, which are sentences consisting of symbols from that signature. The set of axioms is often finite or recursively enumerable, in which case the theory is called effective. Some authors require theories to also include all logical consequences of the axioms. The axioms are considered to hold within the theory and from them other sentences that hold within the theory can be derived. A first-order structure that satisfies all sentences in a given theory is said to be a model of the theory. An elementary class is the set of all structures satisfying a particular theory. These classes are a main subject of study in model theory. Many theories have an intended interpretation, a certain model that is kept in mind when studying the theory. For example, the intended interpretation of Peano arithmetic consists of the usual natural numbers with their usual operations. However, the Löwenheim–Skolem theorem shows that most first-order theories will also have other, nonstandard models. A theory is consistent if it is not possible to prove a contradiction from the axioms of the theory. A theory is complete if, for every formula in its signature, either that formula or its negation is a logical consequence of the axioms of the theory. Gödel's incompleteness theorem shows that effective first-order theories that include a sufficient portion of the theory of the natural numbers can never be both consistent and complete. For more information on this subject see List of first-order theories and Theory (mathematical logic) Empty domains[edit] Main article: Empty domain The definition above requires that the domain of discourse of any interpretation must be a nonempty set. There are settings, such as inclusive logic, where empty domains are permitted. Moreover, if a class of algebraic structures includes an empty structure (for example, there is an empty poset), that class can only be an elementary class in first-order logic if empty domains are permitted or the empty structure is removed from the class. There are several difficulties with empty domains, however: Many common rules of inference are only valid when the domain of discourse is required to be nonempty. One example is the rule stating that ϕ ∨ ∃ x ψ displaystyle phi lor exists xpsi implies ∃ x ( ϕ ∨ ψ ) displaystyle exists x(phi lor psi ) when x is not a free variable in ϕ displaystyle phi . This rule, which is used to put formulas into prenex normal form, is sound in nonempty domains, but unsound if the empty domain is permitted. The definition of truth in an interpretation that uses a variable assignment function cannot work with empty domains, because there are no variable assignment functions whose range is empty. (Similarly, one cannot assign interpretations to constant symbols.) This truth definition requires that one must select a variable assignment function (μ above) before truth values for even atomic formulas can be defined. Then the truth value of a sentence is defined to be its truth value under any variable assignment, and it is proved that this truth value does not depend on which assignment is chosen. This technique does not work if there are no assignment functions at all; it must be changed to accommodate empty domains. Thus, when the empty domain is permitted, it must often be treated as a special case. Most authors, however, simply exclude the empty domain by definition. Deductive systems[edit] A deductive system is used to demonstrate, on a purely syntactic basis, that one formula is a logical consequence of another formula. There are many such systems for first-order logic, including Hilbert-style deductive systems, natural deduction, the sequent calculus, the tableaux method, and resolution. These share the common property that a deduction is a finite syntactic object; the format of this object, and the way it is constructed, vary widely. These finite deductions themselves are often called derivations in proof theory. They are also often called proofs, but are completely formalized unlike natural-language mathematical proofs. A deductive system is sound if any formula that can be derived in the system is logically valid. Conversely, a deductive system is complete if every logically valid formula is derivable. All of the systems discussed in this article are both sound and complete. They also share the property that it is possible to effectively verify that a purportedly valid deduction is actually a deduction; such deduction systems are called effective. A key property of deductive systems is that they are purely syntactic, so that derivations can be verified without considering any interpretation. Thus a sound argument is correct in every possible interpretation of the language, regardless whether that interpretation is about mathematics, economics, or some other area. In general, logical consequence in first-order logic is only semidecidable: if a sentence A logically implies a sentence B then this can be discovered (for example, by searching for a proof until one is found, using some effective, sound, complete proof system). However, if A does not logically imply B, this does not mean that A logically implies the negation of B. There is no effective procedure that, given formulas A and B, always correctly decides whether A logically implies B. Rules of inference[edit] Further information: List of rules of inference A rule of inference states that, given a particular formula (or set of formulas) with a certain property as a hypothesis, another specific formula (or set of formulas) can be derived as a conclusion. The rule is sound (or truth-preserving) if it preserves validity in the sense that whenever any interpretation satisfies the hypothesis, that interpretation also satisfies the conclusion. For example, one common rule of inference is the rule of 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 φ. The substitution rule states that for any φ and any term t, one can conclude φ[t/x] from φ provided that no free variable of t becomes bound during the substitution process. (If some free variable of t becomes bound, then to substitute t for x it is first necessary to change the bound variables of φ to differ from the free variables of t.) To see why the restriction on bound variables is necessary, consider the logically valid formula φ given by ∃ x ( x = y ) displaystyle exists x(x=y) , in the signature of (0,1,+,×,=) of arithmetic. If t is the term "x + 1", the formula φ[t/y] is ∃ x ( x = x + 1 ) displaystyle exists x(x=x+1) , which will be false in many interpretations. The problem is that the free variable x of t became bound during the substitution. The intended replacement can be obtained by renaming the bound variable x of φ to something else, say z, so that the formula after substitution is ∃ z ( z = x + 1 ) displaystyle exists z(z=x+1) , which is again logically valid.
The substitution rule demonstrates several common aspects of rules of
inference. It is entirely syntactical; one can tell whether it was
correctly applied without appeal to any interpretation. It has
(syntactically defined) limitations on when it can be applied, which
must be respected to preserve the correctness of derivations.
Moreover, as is often the case, these limitations are necessary
because of interactions between free and bound variables that occur
during syntactic manipulations of the formulas involved in the
inference rule.
Hilbert-style systems and natural deduction[edit]
A deduction in a
Hilbert-style deductive system
A 1 , … , A n ⊢ B 1 , … , B k , displaystyle A_ 1 ,ldots ,A_ n vdash B_ 1 ,ldots ,B_ k , where A1, ..., An, B1, ..., Bk are formulas and the turnstile symbol ⊢ displaystyle vdash is used as punctuation to separate the two halves. Intuitively, a sequent expresses the idea that ( A 1 ∧ ⋯ ∧ A n ) displaystyle (A_ 1 land cdots land A_ n ) implies ( B 1 ∨ ⋯ ∨ B k ) displaystyle (B_ 1 lor cdots lor B_ k ) . Tableaux method[edit] A tableaux proof for the propositional formula ((a ∨ ¬b) Λ b) → a. Further information: Method of analytic tableaux Unlike the methods just described, the derivations in the tableaux method are not lists of formulas. Instead, a derivation is a tree of formulas. To show that a formula A is provable, the tableaux method attempts to demonstrate that the negation of A is unsatisfiable. The tree of the derivation has ¬ A displaystyle lnot A at its root; the tree branches in a way that reflects the structure of the formula. For example, to show that C ∨ D displaystyle Clor D is unsatisfiable requires showing that C and D are each unsatisfiable; this corresponds to a branching point in the tree with parent C ∨ D displaystyle Clor D and children C and D. Resolution[edit] The resolution rule is a single rule of inference that, together with unification, is sound and complete for first-order logic. As with the tableaux method, a formula is proved by showing that the negation of the formula is unsatisfiable. Resolution is commonly used in automated theorem proving. The resolution method works only with formulas that are disjunctions of atomic formulas; arbitrary formulas must first be converted to this form through Skolemization. The resolution rule states that from the hypotheses A 1 ∨ ⋯ ∨ A k ∨ C displaystyle A_ 1 lor cdots lor A_ k lor C and B 1 ∨ ⋯ ∨ B l ∨ ¬ C displaystyle B_ 1 lor cdots lor B_ l lor lnot C , the conclusion A 1 ∨ ⋯ ∨ A k ∨ B 1 ∨ ⋯ ∨ B l displaystyle A_ 1 lor cdots lor A_ k lor B_ 1 lor cdots lor B_ l can be obtained. Provable identities[edit] Many identities can be proved, which establish equivalences between particular formulas. These identities allow for rearranging formulas by moving quantifiers across other connectives, and are useful for putting formulas in prenex normal form. Some provable identities include: ¬ ∀ x P ( x ) ⇔ ∃ x ¬ P ( x ) displaystyle lnot forall x,P(x)Leftrightarrow exists x,lnot P(x) ¬ ∃ x P ( x ) ⇔ ∀ x ¬ P ( x ) displaystyle lnot exists x,P(x)Leftrightarrow forall x,lnot P(x) ∀ x ∀ y P ( x , y ) ⇔ ∀ y ∀ x P ( x , y ) displaystyle forall x,forall y,P(x,y)Leftrightarrow forall y,forall x,P(x,y) ∃ x ∃ y P ( x , y ) ⇔ ∃ y ∃ x P ( x , y ) displaystyle exists x,exists y,P(x,y)Leftrightarrow exists y,exists x,P(x,y) ∀ x P ( x ) ∧ ∀ x Q ( x ) ⇔ ∀ x ( P ( x ) ∧ Q ( x ) ) displaystyle forall x,P(x)land forall x,Q(x)Leftrightarrow forall x,(P(x)land Q(x)) ∃ x P ( x ) ∨ ∃ x Q ( x ) ⇔ ∃ x ( P ( x ) ∨ Q ( x ) ) displaystyle exists x,P(x)lor exists x,Q(x)Leftrightarrow exists x,(P(x)lor Q(x)) P ∧ ∃ x Q ( x ) ⇔ ∃ x ( P ∧ Q ( x ) ) displaystyle Pland exists x,Q(x)Leftrightarrow exists x,(Pland Q(x)) (where x displaystyle x must not occur free in P displaystyle P ) P ∨ ∀ x Q ( x ) ⇔ ∀ x ( P ∨ Q ( x ) ) displaystyle Plor forall x,Q(x)Leftrightarrow forall x,(Plor Q(x)) (where x displaystyle x must not occur free in P displaystyle P ) Equality and its axioms[edit] There are several different conventions for using equality (or identity) in first-order logic. The most common convention, known as first-order logic with equality, includes the equality symbol as a primitive logical symbol which is always interpreted as the real equality relation between members of the domain of discourse, such that the "two" given members are the same member. This approach also adds certain axioms about equality to the deductive system employed. These equality axioms are:[citation needed] Reflexivity. For each variable x, x = x. Substitution for functions. For all variables x and y, and any function symbol f, x = y → f(...,x,...) = f(...,y,...). Substitution for formulas. For any variables x and y and any formula φ(x), if φ' is obtained by replacing any number of free occurrences of x in φ with y, such that these remain free occurrences of y, then x = y → (φ → φ'). These are axiom schemas, each of which specifies an infinite set of axioms. The third schema is known as Leibniz's law, "the principle of substitutivity", "the indiscernibility of identicals", or "the replacement property". The second schema, involving the function symbol f, is (equivalent to) a special case of the third schema, using the formula x = y → (f(...,x,...) = z → f(...,y,...) = z). Many other properties of equality are consequences of the axioms above, for example: Symmetry. If x = y then y = x. Transitivity. If x = y and y = z then x = z.
First-order logic
In the theory of partial orders with one relation symbol ≤, one could define s = t to be an abbreviation for s ≤ t ∧ displaystyle wedge t ≤ s. In set theory with one relation ∈ displaystyle in , one may define s = t to be an abbreviation for ∀ displaystyle forall x (s ∈ displaystyle in x ↔ displaystyle leftrightarrow t ∈ displaystyle in x) ∧ displaystyle wedge ∀ displaystyle forall x (x ∈ displaystyle in s ↔ displaystyle leftrightarrow x ∈ displaystyle in t). This definition of equality then automatically satisfies the axioms for equality. In this case, one should replace the usual axiom of extensionality, which can be stated as ∀ x ∀ y [ ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ x = y ] displaystyle forall xforall y[forall z(zin xLeftrightarrow zin y)Rightarrow x=y] , with an alternative formulation ∀ x ∀ y [ ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ z ( x ∈ z ⇔ y ∈ z ) ] displaystyle forall xforall y[forall z(zin xLeftrightarrow zin y)Rightarrow forall z(xin zLeftrightarrow yin z)] , which says that if sets x and y have the same elements, then they also belong to the same sets. Metalogical properties[edit]
One motivation for the use of first-order logic, rather than
higher-order logic, is that first-order logic has many metalogical
properties that stronger logics do not have. These results concern
general properties of first-order logic itself, rather than properties
of individual theories. They provide fundamental tools for the
construction of models of first-order theories.
Completeness and undecidability[edit]
Gödel's completeness theorem, proved by
Kurt Gödel
Σ 1 1 displaystyle Sigma _ 1 ^ 1 also enjoys compactness. Lindström's theorem[edit] Main article: Lindström's theorem Per Lindström showed that the metalogical properties just discussed actually characterize first-order logic in the sense that no stronger logic can also have those properties (Ebbinghaus and Flum 1994, Chapter XIII). Lindström defined a class of abstract logical systems, and a rigorous definition of the relative strength of a member of this class. He established two theorems for systems of this type: A logical system satisfying Lindström's definition that contains
first-order logic and satisfies both the Löwenheim–Skolem theorem
and the compactness theorem must be equivalent to first-order logic.
A logical system satisfying Lindström's definition that has a
semidecidable logical consequence relation and satisfies the
Löwenheim–Skolem theorem
Limitations[edit] Although first-order logic is sufficient for formalizing much of mathematics, and is commonly used in computer science and other fields, it has certain limitations. These include limitations on its expressiveness and limitations of the fragments of natural languages that it can describe. For instance, first-order logic is undecidable, meaning a sound, complete and terminating decision algorithm for provability is impossible. This has led to the study of interesting decidable fragments such as C2, first-order logic with two variables and the counting quantifiers ∃ ≥ n displaystyle exists ^ geq n and ∃ ≤ n displaystyle exists ^ leq n (these quantifiers are, respectively, "there exists at least n" and
"there exists at most n").[11]
Expressiveness[edit]
The
Löwenheim–Skolem theorem
Type Example Comment Quantification over properties If John is self-satisfied, then there is at least one thing he has in common with Peter Requires a quantifier over predicates, which cannot be implemented in single-sorted first-order logic: Zj→ ∃X(Xj∧Xp) Quantification over properties Santa Claus has all the attributes of a sadist Requires quantifiers over predicates, which cannot be implemented in single-sorted first-order logic: ∀X(∀x(Sx → Xx)→Xs) Predicate adverbial John is walking quickly Cannot be analysed as Wj ∧ Qj; predicate adverbials are not the same kind of thing as second-order predicates such as colour Relative adjective Jumbo is a small elephant Cannot be analysed as Sj ∧ Ej; predicate adjectives are not the same kind of thing as second-order predicates such as colour Predicate adverbial modifier John is walking very quickly - Relative adjective modifier Jumbo is terribly small An expression such as "terribly", when applied to a relative adjective such as "small", results in a new composite relative adjective "terribly small" Prepositions Mary is sitting next to John The preposition "next to" when applied to "John" results in the predicate adverbial "next to John" Restrictions, extensions, and variations[edit]
There are many variations of first-order logic. Some of these are
inessential in the sense that they merely change notation without
affecting the semantics. Others change the expressive power more
significantly, by extending the semantics through additional
quantifiers or other new logical symbols. For example, infinitary
logics permit formulas of infinite size, and modal logics add symbols
for possibility and necessity.
Restricted languages[edit]
First-order logic
Because ∃ x ϕ ( x ) displaystyle exists xphi (x) can be expressed as ¬ ∀ x ¬ ϕ ( x ) displaystyle neg forall xneg phi (x) , and ∀ x ϕ ( x ) displaystyle forall xphi (x) can be expressed as ¬ ∃ x ¬ ϕ ( x ) displaystyle neg exists xneg phi (x) , either of the two quantifiers ∃ displaystyle exists and ∀ displaystyle forall can be dropped. Since ϕ ∨ ψ displaystyle phi lor psi can be expressed as ¬ ( ¬ ϕ ∧ ¬ ψ ) displaystyle lnot (lnot phi land lnot psi ) and ϕ ∧ ψ displaystyle phi land psi can be expressed as ¬ ( ¬ ϕ ∨ ¬ ψ ) displaystyle lnot (lnot phi lor lnot psi ) , either ∨ displaystyle vee or ∧ displaystyle wedge can be dropped. In other words, it is sufficient to have ¬ displaystyle neg and ∨ displaystyle vee , or ¬ displaystyle neg and ∧ displaystyle wedge , as the only logical connectives. Similarly, it is sufficient to have only ¬ displaystyle neg and → displaystyle rightarrow as logical connectives, or to have only the
Sheffer stroke
0 displaystyle ;0 one may use a predicate 0 ( x ) displaystyle ;0(x) (interpreted as x = 0 displaystyle ;x=0 ), and replace every predicate such as P ( 0 , y ) displaystyle ;P(0,y) with ∀ x ( 0 ( x ) → P ( x , y ) ) displaystyle forall x;(0(x)rightarrow P(x,y)) . A function such as f ( x 1 , x 2 , . . . , x n ) displaystyle f(x_ 1 ,x_ 2 ,...,x_ n ) will similarly be replaced by a predicate F ( x 1 , x 2 , . . . , x n , y ) displaystyle F(x_ 1 ,x_ 2 ,...,x_ n ,y) interpreted as y = f ( x 1 , x 2 , . . . , x n ) displaystyle y=f(x_ 1 ,x_ 2 ,...,x_ n ) . This change requires adding additional axioms to the theory at hand, so that interpretations of the predicate symbols used have the correct semantics. Restrictions such as these are useful as a technique to reduce the number of inference rules or axiom schemas in deductive systems, which leads to shorter proofs of metalogical results. The cost of the restrictions is that it becomes more difficult to express natural-language statements in the formal system at hand, because the logical connectives used in the natural language statements must be replaced by their (longer) definitions in terms of the restricted collection of logical connectives. Similarly, derivations in the limited systems may be longer than derivations in systems that include additional connectives. There is thus a trade-off between the ease of working within the formal system and the ease of proving results about the formal system. It is also possible to restrict the arities of function symbols and predicate symbols, in sufficiently expressive theories. One can in principle dispense entirely with functions of arity greater than 2 and predicates of arity greater than 1 in theories that include a pairing function. This is a function of arity 2 that takes pairs of elements of the domain and returns an ordered pair containing them. It is also sufficient to have two predicate symbols of arity 2 that define projection functions from an ordered pair to its components. In either case it is necessary that the natural axioms for a pairing function and its projections are satisfied. Many-sorted logic[edit] Main article: Many-sorted logic This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (June 2013) (Learn how and when to remove this template message) Ordinary first-order interpretations have a single domain of discourse over which all quantifiers range. Many-sorted first-order logic allows variables to have different sorts, which have different domains. This is also called typed first-order logic, and the sorts called types (as in data type), but it is not the same as first-order type theory. Many-sorted first-order logic is often used in the study of second-order arithmetic. When there are only finitely many sorts in a theory, many-sorted first-order logic can be reduced to single-sorted first-order logic.[13] One introduces into the single-sorted theory a unary predicate symbol for each sort in the many-sorted theory, and adds an axiom saying that these unary predicates partition the domain of discourse. For example, if there are two sorts, one adds predicate symbols P 1 ( x ) displaystyle P_ 1 (x) and P 2 ( x ) displaystyle P_ 2 (x) and the axiom ∀ x ( P 1 ( x ) ∨ P 2 ( x ) ) ∧ ¬ ∃ x ( P 1 ( x ) ∧ P 2 ( x ) ) displaystyle forall x(P_ 1 (x)lor P_ 2 (x))land lnot exists x(P_ 1 (x)land P_ 2 (x)) . Then the elements satisfying P 1 displaystyle P_ 1 are thought of as elements of the first sort, and elements satisfying P 2 displaystyle P_ 2 as elements of the second sort. One can quantify over each sort by using the corresponding predicate symbol to limit the range of quantification. For example, to say there is an element of the first sort satisfying formula φ(x), one writes ∃ x ( P 1 ( x ) ∧ ϕ ( x ) ) displaystyle exists x(P_ 1 (x)land phi (x)) . Additional quantifiers[edit] Additional quantifiers can be added to first-order logic. Sometimes it is useful to say that "P(x) holds for exactly one x", which can be expressed as ∃ ! displaystyle exists ! x P(x). This notation, called uniqueness quantification, may be taken to abbreviate a formula such as ∃ displaystyle exists x (P(x) ∧ ∀ displaystyle wedge forall y (P(y) → displaystyle rightarrow (x = y))).
First-order logic
Infinitary logics[edit] Main article: Infinitary logic Infinitary logic allows infinitely long sentences. 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. Infinitary logic generalizes first-order logic to allow formulas of infinite length. The most common way in which formulas can become infinite is through infinite conjunctions and disjunctions. However, it is also possible to admit generalized signatures in which function and relation symbols are allowed to have infinite arities, or in which quantifiers can bind infinitely many variables. Because an infinite formula cannot be represented by a finite string, it is necessary to choose some other representation of formulas; the usual representation in this context is a tree. Thus formulas are, essentially, identified with their parse trees, rather than with the strings being parsed. The most commonly studied infinitary logics are denoted Lαβ, where α and β are each either cardinal numbers or the symbol ∞. In this notation, ordinary first-order logic is Lωω. In the logic L∞ω, arbitrary conjunctions or disjunctions are allowed when building formulas, and there is an unlimited supply of variables. More generally, the logic that permits conjunctions or disjunctions with less than κ constituents is known as Lκω. For example, Lω1ω permits countable conjunctions and disjunctions. The set of free variables in a formula of Lκω can have any cardinality strictly less than κ, yet only finitely many of them can be in the scope of any quantifier when a formula appears as a subformula of another.[14] In other infinitary logics, a subformula may be in the scope of infinitely many quantifiers. For example, in Lκ∞, a single universal or existential quantifier may bind arbitrarily many variables simultaneously. Similarly, the logic Lκλ permits simultaneous quantification over fewer than λ variables, as well as conjunctions and disjunctions of size less than κ. Non-classical and modal logics[edit] Intuitionistic first-order logic uses intuitionistic rather than classical propositional calculus; for example, ¬¬φ need not be equivalent to φ. First-order modal logic allows one to describe other possible worlds as well as this contingently true world which we inhabit. In some versions, the set of possible worlds varies depending on which possible world one inhabits. Modal logic has extra modal operators with meanings which can be characterized informally as, for example "it is necessary that φ" (true in all possible worlds) and "it is possible that φ" (true in some possible world). With standard first-order logic we have a single domain and each predicate is assigned one extension. With first-order modal logic we have a domain function that assigns each possible world its own domain, so that each predicate gets an extension only relative to these possible worlds. This allows us to model cases where, for example, Alex is a Philosopher, but might have been a Mathematician, and might not have existed at all. In the first possible world P(a) is true, in the second P(a) is false, and in the third possible world there is no a in the domain at all. first-order fuzzy logics are first-order extensions of propositional fuzzy logics rather than classical propositional calculus. Fixpoint logic[edit] Fixpoint logic extends first-order logic by adding the closure under the least fixed points of positive operators.[15] Higher-order logics[edit] Main article: Higher-order logic The characteristic feature of first-order logic is that individuals can be quantified, but not predicates. Thus ∃ a ( Phil ( a ) ) displaystyle exists a( text Phil (a)) is a legal first-order formula, but ∃ Phil ( Phil ( a ) ) displaystyle exists text Phil ( text Phil (a)) is not, in most formalizations of first-order logic. Second-order
logic extends first-order logic by adding the latter type of
quantification. Other higher-order logics allow quantification over
even higher types than second-order logic permits. These higher types
include relations between relations, functions from relations to
relations between relations, and other higher-type objects. Thus the
"first" in first-order logic describes the type of objects that can be
quantified.
Unlike first-order logic, for which only one semantics is studied,
there are several possible semantics for second-order logic. The most
commonly employed semantics for second-order and higher-order logic is
known as full semantics. The combination of additional quantifiers and
the full semantics for these quantifiers makes higher-order logic
stronger than first-order logic. In particular, the (semantic) logical
consequence relation for second-order and higher-order logic is not
semidecidable; there is no effective deduction system for second-order
logic that is sound and complete under full semantics.
Second-order logic with full semantics is more expressive than
first-order logic. For example, it is possible to create axiom systems
in second-order logic that uniquely characterize the natural numbers
and the real line. The cost of this expressiveness is that
second-order and higher-order logics have fewer attractive metalogical
properties than first-order logic. For example, the
Löwenheim–Skolem theorem
Logic portal
ACL2
Notes[edit] ^ Hodgson, Dr. J. P. E., "First Order Logic", Saint Joseph's
University, Philadelphia, 1995.
^ Hughes, G. E., & Cresswell, M. J., A New Introduction to Modal
Logic (London: Routledge, 1996), p.161.
^ Mendelson, Elliott (1964). Introduction to Mathematical Logic. Van
Nostrand Reinhold. p. 56.
^ Eric M. Hammer:
Semantics for Existential Graphs, Journal of
Philosophical Logic, Volume 27, Issue 5 (October 1998), page 489:
"Development of first-order logic independently of Frege, anticipating
prenex and Skolem normal forms"
^ Goertzel, B., Geisweiller, N., Coelho, L., Janičić, P., &
Pennachin, C., Real-World Reasoning: Toward Scalable, Uncertain
Spatiotemporal, Contextual and Causal
Inference (
Amsterdam
References[edit] Andrews, Peter B. (2002); An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed., Berlin: Kluwer Academic Publishers. Available from Springer. Avigad, Jeremy; Donnelly, Kevin; Gray, David; and Raff, Paul (2007); "A formally verified proof of the prime number theorem", ACM Transactions on Computational Logic, vol. 9 no. 1 doi:10.1145/1297658.1297660 Barwise, Jon (1977); "An Introduction to First-Order Logic", in Barwise, Jon, ed. (1982). Handbook of Mathematical Logic. Studies in Logic and the Foundations of Mathematics. Amsterdam, NL: North-Holland. ISBN 978-0-444-86388-1. Barwise, Jon; and Etchemendy, John (2000); Language Proof and Logic, Stanford, CA: CSLI Publications (Distributed by the University of Chicago Press) Bocheński, Józef Maria (2007); A Précis of Mathematical Logic, Dordrecht, NL: D. Reidel, translated from the French and German editions by Otto Bird Ferreirós, José (2001); The Road to Modern Logic — An Interpretation, Bulletin of Symbolic Logic, Volume 7, Issue 4, 2001, pp. 441–484, doi:10.2307/2687794, JSTOR 2687794 Gamut, L. T. F. (1991); Logic, Language, and Meaning, Volume 2: Intensional Logic and Logical Grammar, Chicago, Illinois: University of Chicago Press, ISBN 0-226-28088-8 Hilbert, David; and Ackermann, Wilhelm (1950); Principles of Mathematical Logic, Chelsea (English translation of Grundzüge der theoretischen Logik, 1928 German first edition) Hodges, Wilfrid (2001); "Classical Logic I: First Order Logic", in Goble, Lou (ed.); The Blackwell Guide to Philosophical Logic, Blackwell Ebbinghaus, Heinz-Dieter; Flum, Jörg; and Thomas, Wolfgang (1994); Mathematical Logic, Undergraduate Texts in Mathematics, Berlin, DE/New York, NY: Springer-Verlag, Second Edition, ISBN 978-0-387-94258-2 Rautenberg, Wolfgang (2010), A Concise Introduction to Mathematical Logic (3rd ed.), New York, NY: Springer Science+Business Media, doi:10.1007/978-1-4419-1221-3, ISBN 978-1-4419-1220-6 Tarski, Alfred and Givant, Steven (1987); A Formalization of Set Theory without Variables. Vol.41 of American Mathematical Society colloquium publications, Providence RI: American Mathematical Society, ISBN 978-0821810415. External links[edit] Hazewinkel, Michiel, ed. (2001) [1994], "Predicate calculus",
Encyclopedia of Mathematics,
Springer Science+Business Media
v t e Mathematical logic General Formal language Formation rule Formal proof Formal semantics Well-formed formula Set Element Class Classical logic Axiom Rule of inference Relation Theorem Logical consequence Type theory Symbol Syntax Theory Systems Formal system Deductive system Axiomatic system Hilbert style systems Natural deduction Sequent calculus Traditional logic Proposition Inference Argument Validity Cogency Syllogism Square of opposition Venn diagram Propositional calculus Boolean logic Boolean functions Propositional calculus Propositional formula Logical connectives Truth tables Many-valued logic Predicate logic First-order Quantifiers Predicate Second-order Monadic predicate calculus Naive set theory Set
Empty set
Element
Enumeration
Extensionality
Finite set
Infinite set
Subset
Power set
Countable set
Uncountable
Set theory Foundations of mathematics
Zermelo–Fraenkel set theory
Axiom
Model theory Model Interpretation Non-standard model Finite model theory Truth value Validity Proof theory Formal proof Deductive system Formal system Theorem Logical consequence Rule of inference Syntax Computability theory Recursion
Recursive set
Recursively enumerable
|
