# First-order logic

**predicate logicfirst-orderpredicate calculusfirst-order theoryfirst order logicfirst-order predicate calculusfirst-order predicate logicfirst-order languagefirst orderquantification theory**

First-order logic—also known as predicate logic and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science.wikipedia

718 Related Articles

### Higher-order logic

**higher order logichigher-orderHigher Order**

The adjective "first-order" distinguishes first-order logic from higher-order logic in which there are predicates having predicates or functions as arguments, or in which one or both of predicate quantifiers or function quantifiers are permitted.

In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics.

### Automated theorem proving

**automated theorem provertheorem provertheorem proving**

Although the logical consequence relation is only semidecidable, much progress has been made in automated theorem proving in first-order logic.

Frege's Begriffsschrift (1879) introduced both a complete propositional calculus and what is essentially modern predicate logic.

### Compactness theorem

**compactnesscompact(countable) compactness property**

First-order logic also satisfies several metalogical theorems that make it amenable to analysis in proof theory, such as the Löwenheim–Skolem theorem and the compactness theorem.

In mathematical logic, the compactness theorem states that a set of first-order sentences has a model if and only if every finite subset of it has a model.

### Second-order logic

**second-ordersecond order logicexistential second-order logic**

Axiom systems that do fully describe these two structures (that is, categorical axiom systems) can be obtained in stronger logics such as 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.

### Propositional calculus

**propositional logicpropositionalsentential logic**

This distinguishes it from propositional logic, which does not use quantifiers or relations. While propositional logic deals with simple declarative propositions, first-order logic additionally covers predicates and quantification.

Unlike first-order logic, propositional logic does not deal with non-logical objects, predicates about them, or quantifiers.

### Peano axioms

**Peano arithmeticfirst-order arithmeticarithmetic**

Peano arithmetic and Zermelo–Fraenkel set theory are axiomatizations of number theory and set theory, respectively, into first-order logic.

The next three axioms are first-order statements about natural numbers expressing the fundamental properties of the successor operation.

### Existential quantification

**existential quantifierthere exists∃**

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.

In predicate logic, an existential quantification is a type of quantifier, a logical constant which is interpreted as "there exists", "there is at least one", or "for some".

### Logical connective

**logical operatorconnectivesconnective**

Relationships between predicates can be stated using logical connectives. 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.)

Logical connectives along with quantifiers are the two main types of logical constants used in formal systems such as propositional logic and predicate logic.

### Löwenheim–Skolem theorem

**(downward) Löwenheim–Skolem propertydownward Löwenheim–Skolem theoremLöwenheim-Skolem theorem**

First-order logic also satisfies several metalogical theorems that make it amenable to analysis in proof theory, such as the Löwenheim–Skolem theorem and the compactness theorem.

The (downward) Löwenheim–Skolem theorem is one of the two key properties, along with the compactness theorem, that are used in Lindström's theorem to characterize first-order logic.

### Zermelo–Fraenkel set theory

**ZFZFCZermelo–Fraenkel**

Peano arithmetic and Zermelo–Fraenkel set theory are axiomatizations of number theory and set theory, respectively, into first-order logic.

Formally, ZFC is a one-sorted theory in first-order logic.

### Gottlob Frege

**FregeFrege, GottlobFregean**

The foundations of first-order logic were developed independently by Gottlob Frege and Charles Sanders Peirce.

In effect, Frege invented axiomatic predicate logic, in large part thanks to his invention of quantified variables, which eventually became ubiquitous in mathematics and logic, and which solved the problem of multiple generality.

### Domain of discourse

**universe of discoursedomainarea of interest**

A theory about a topic is usually a first-order logic together with a specified domain of discourse over which the quantified variables range, finitely many functions from that domain to itself, finitely many predicates defined on that domain, and a set of axioms believed to hold for those things.

For example, in an interpretation of first-order logic, the domain of discourse is the set of individuals over which the quantifiers range.

### Logical conjunction

**conjunctionANDlogical 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.)

In predicate logic, universal quantification.

### Well-formed formula

**formulaformulaswell-formed**

The set of formulas (also called well-formed formulas or WFFs) is inductively defined by the following rules:

In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often simply formula, is a finite sequence of symbols from a given alphabet that is part of a formal language.

### Term (logic)

**termstermfirst-order terms**

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

A first-order term is recursively constructed from constant symbols, variables and function symbols.

### Quantifier (logic)

**quantifierquantifiersquantification**

First-order logic uses quantified variables over non-logical objects and allows the use of sentences that contain variables, so that rather than propositions such as Socrates is a man one can have expressions in the form "there exists X such that X is Socrates and X is a man" and there exists is a quantifier while X is a variable. While propositional logic deals with simple declarative propositions, first-order logic additionally covers predicates and quantification.

An interpretation for first-order predicate calculus assumes as given

### Universal quantification

**universal quantifieruniversally quantifieduniversal**

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.

In predicate logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any" or "for all".

### Non-logical symbol

**non-logical symbolsdescriptive signnon-logical**

The non-logical symbols represent predicates (relations), functions and constants on the domain of discourse.

The non-logical symbols of a language of first-order logic consist of predicates and individual constants.

### Proof theory

**proof-theoreticProof-theoreticallyderive**

First-order logic also satisfies several metalogical theorems that make it amenable to analysis in proof theory, such as the Löwenheim–Skolem theorem and the compactness theorem.

Each of these can give a complete and axiomatic formalization of propositional or predicate logic of either the classical or intuitionistic flavour, almost any modal logic, and many substructural logics, such as relevance logic or linear logic.

### Completeness (logic)

**completecompletenessincompleteness**

There are many deductive systems for first-order logic which are both sound (all provable statements are true in all models) and complete (all statements which are true in all models are provable).

For example, Gödel's completeness theorem establishes semantic completeness for first-order logic.

### Sentence (mathematical logic)

**sentencesentencesclosed formula**

A formula in first-order logic with no free variable occurrences is called a first-order sentence. These are the formulas that will have well-defined truth values under an interpretation.

In mathematical logic, a sentence of a predicate logic is a boolean-valued well-formed formula with no free variables.

### Charles Sanders Peirce

**PeirceC. S. PeirceCharles Peirce**

The foundations of first-order logic were developed independently by Gottlob Frege and Charles Sanders Peirce.

By the later 1890s he was devising existential graphs, a diagrammatic notation for the predicate calculus.

### Foundations of mathematics

**foundation of mathematicsfoundationsfoundational**

First-order logic is the standard for the formalization of mathematics into axioms and is studied in the foundations of mathematics.

This was still a second-order axiomatization (expressing induction in terms of arbitrary subsets, thus with an implicit use of set theory) as concerns for expressing theories in first-order logic were not yet understood.

### Predicate functor logic

Predicate functor logic, mainly due to Willard Quine.

In mathematical logic, predicate functor logic (PFL) is one of several ways to express first-order logic (also known as predicate logic) by purely algebraic means, i.e., without quantified variables.

### Predicate (mathematical logic)

**predicatepredicatespredication**

While propositional logic deals with simple declarative propositions, first-order logic additionally covers predicates and quantification.

In first-order logic, an atomic formula consists of a predicate symbol applied to an appropriate number of terms.