| First-order Logic |
Article Index for First-order |
Website Links For Logic |
Information AboutFirst-order Logic |
| CATEGORIES ABOUT FIRST-ORDER LOGIC | |
| logic | |
| systems of formal logic | |
| philosophical logic | |
| model theory | |
| discrete mathematics | |
|
First-order predicate calculus ('''FOPC''') or '''first-order logic''' ('''FOL''') is a system of Mathematical Logic , extending Propositional Logic (equivalently, Sentential Logic ), which is in turn extended by Second-order Logic . The Atomic Sentence s of first-order logic have the form ''P''(''t''1, ..., ''t''''n'') (a Predicate with one or more "subjects") rather than being propositional letters as in Propositional Logic . This is usually written without parentheses or commas, as below. The new ingredient of first-order logic not found in Propositional Logic is Quantification : where φ is any sentence, the new constructions ∀''x'' φ and ∃''x'' φ, read "for all ''x'', φ" and "for some ''x'', φ", are introduced. For convenience in explaining our intentions, we write φ as φ(''x'') and let φ(''a'') represent the result of replacing all (free) occurrences of ''x'' in φ(''x'') with ''a'', then ∀''x'' φ(''x'') means that φ(''a'') is true for any value of ''a'' and ∃''x'' φ(''x'') means that there is an ''a'' such that φ(''a'') is true. Values of the variables are taken from an understood Universe Of Discourse ; a refinement of first-order logic allows variables ranging over different sorts of object. In Second-order Logic (and further systems of Higher-order Logic ), quantifiers over predicate letters are introduced: for example, equality can be defined in second-order logic by ''x'' = ''y'' ≡def ∀''P'' (''P''(''x'') ↔ ''P''(''y'')). Quantification over predicates is not permitted in first-order logic. First-order logic has sufficient expressive power for the formalization of virtually all of mathematics. A First-order Theory consists of a set of Axioms (usually finite or Recursively Enumerable ) and the statements deducible from them. The usual set theory ZFC is an example of a first-order theory, and it is generally accepted that all of classical mathematics can be formalized in ZFC . There are other theories that are commonly formalized independently in first-order logic (though they do admit implementation in set theory) such as Peano Arithmetic . DEFINING FIRST-ORDER LOGIC A Predicate Calculus consists of
The axioms considered here are the ''logical'' axioms which are part of the predicate calculus. Further, ''non-logical'' axioms are added in specific first-order theories: these are not regarded as truths of logic but as truths of the particular theory under consideration. When the set of axioms is infinite, it is required that there is an Algorithm which can decide for a given well-formed formula whether it is an axiom or not. Furthermore, there should be an algorithm which can decide whether a given application of an inference rule is correct or not. It is important to note that the predicate calculus can be formalized in many equivalent ways; there is nothing canonical about the axioms and rules of inference given here, but any formalization will yield the same theorems of logic (and deduce the same theorems from any set of non-logical axioms). VOCABULARY The "vocabulary" is composed of # A set of predicate variables (or '''relations''') each with some '''valence''' (or '''arity''') ≥1, which are often denoted by uppercase letters ''P'', ''Q'', ''R'',... # A set of constants, often denoted by lowercase letters ''a'', ''b'', ''c'',... . # A set of functions, each of some valence ≥ 1, which are often denoted by lowercase letters ''f'', ''g'', ''h'',... . # An infinite set of variables, often denoted by lowercase letters ''x'', ''y'', ''z'',... . # Symbols denoting logical operators (or '''connectives'''): ¬ ( Logical Not ), ∧ ( Logical And ), ∨ ( Logical Or ), → ( Logical Conditional ), ↔ ( Logical Biconditional ). # Symbols denoting quantifiers: ∀ ( Universal Quantification ), ∃ ( Existential Quantification ). # Left and right parenthesis. # An identity or equality symbol = is sometimes but not always included in the vocabulary. There are several minor variations listed below: | ||
| ::{ Cellpadding | "5" |
|
|