Predicate calculus

From Free net encyclopedia

Template:Mergeto

In mathematical logic the predicate calculus, predicate logic or calculus of propositional functions is a formal system used to describe mathematical theories.

The predicate calculus is an extension of propositional calculus, which is inadequate for describing more complex mathematical structures. Grammatically speaking the predicate calculus adds a predicate-subject structure and quantifiers on top of the existing propositional calculus. A subject is a name for a member of a given group of individuals (a set) and a predicate is a relation on this group.

It is much harder to reason in predicate logic than in propositional calculus. In general, truth-tables are not suitable for predicate logic, as a universally quantified predicate may have an infinite domain of interest.

Identities

<math>\neg \forall x P(x) \Leftrightarrow \exists x \neg P(x)</math>

<math>\neg \exists x P(x) \Leftrightarrow \forall x \neg P(x)</math>

<math>\forall x \forall y P(x,y) \Leftrightarrow \forall y \forall x P(x,y)</math>

<math>\exists x \exists y P(x,y) \Leftrightarrow \exists y \exists x P(x,y)</math>

<math>\forall x P(x) \land \forall x Q(x) \Leftrightarrow \forall x (P(x) \land Q(x)) </math>

<math>\exists x P(x) \lor \exists x Q(x) \Leftrightarrow \exists x (P(x) \lor Q(x)) </math>

Inference rules

<math>\exists x \forall y P(x,y) \Rightarrow \forall y \exists x P(x,y)</math>

<math>\forall x P(x) \lor \forall x Q(x) \Rightarrow \forall x (P(x) \lor Q(x)) </math>

<math>\exists x (P(x) \land Q(x)) \Rightarrow \exists x P(x) \land \exists x Q(x)</math>

<math>\exists x P(x) \land \forall x Q(x) \Rightarrow \exists x (P(x) \land Q(x)) </math>

<math>\forall x P(x) \Rightarrow P(c)</math> (If c is a variable, then it must not already be quantified somewhere in P(x))

<math>P(c) \Rightarrow \exists x P(x)</math> (x must not appear free in P(c))

See also

• First order predicate calculus
• Second order predicate calculus

Template:Mathlogic-stubcs:Predikátová logika de:Prädikatenlogik fr:Calcul des prédicats he:תחשיב הפסוקים nl:Predikatenlogica pl:Klasyczny rachunek logiczny ru:Логика первого порядка sv:Predikatlogik zh:谓词演算