(→Ágak, területek: talán precízkedés, de odaírtam a záradékot a kalkulushoz, és belinkeltem az induktív definíciót.)
<!-- First-order logic is distinguished from [[higher-order logic]] in that it does not allow quantification over properties; i.e. it cannot express statements such as "for every ''property'' P, it is the case that..." (<math>\forall P</math>) or "there exists a property P such that..." (<math>\exists P</math>).
Nevertheless, first-order logic is strong enough to formalize all of [[set theory]] and thereby virtually all of [[mathematics]]. Its restriction to quantification over individuals makes it difficult to use for the purposes of [[topology]], but it is the classical logical theory underlying mathematics. It is a stronger theory than [[sentential logic]], but a weaker theory than [[second-order logic]].
A predicate calculus consists of
* formation rules (i.e. recursive definitions for forming well-formed formulas).
* transformation rules (i.e. [[inference rule]]s for deriving theorems).
* a (possibly countably infinite) set of axioms or axiom schemata.
There are two types of axioms: ''logical axioms'' which are valid with respect to the predicate calculus and ''non-logical axioms'' which are true under a special, i.e. the standard, interpretation of the theory of which they are part. For example, the non-logical [[Peano axioms]] are true under the standard interpretation of the symbolism of arithmetic, but they are not valid with respect to the predicate calculus.
When the set of axioms is infinite, it is required that there is an [[algorithm]] which can decide for a given well-formed formula whether it is an axiom or not. Furthermore, there should be an algorithm which can decide whether a given application of an inference rule is correct or not.
# Unlike the [[Propositional calculus]], first-order logic is undecidable. There is provably no [[decision procedure]] for determining for an arbitrary formula P, whether or not P is valid (see [[Halting problem]]). (Results came independently from [[Alonzo Church|Church]] and [[Alan Turing|Turing]].)
# The decision problem for validity is semidecidable. As [[Gödel's completeness theorem]] shows, for any '''valid''' formula P, P is provable.
# Monadic predicate logic (i.e., predicate logic with only predicates of one argument) is decidable.