Namespaces
Variants
Actions

Difference between revisions of "Predicate calculus"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
(TeX)
 
Line 1: Line 1:
 +
{{TEX|done}}
 
A formal axiomatic theory; a calculus intended for the description of logical laws (cf. [[Logical law|Logical law]]) that are true for any non-empty domain of objects with arbitrary predicates (i.e. properties and relations) given on these objects.
 
A formal axiomatic theory; a calculus intended for the description of logical laws (cf. [[Logical law|Logical law]]) that are true for any non-empty domain of objects with arbitrary predicates (i.e. properties and relations) given on these objects.
  
In order to formulate the predicate calculus one must first fix an exact logico-mathematical language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p0743601.png" />. In the most common case of single-sorted first-order languages, such a language contains predicate variables <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p0743602.png" /> function symbols <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p0743603.png" /> with a varying number of argument places, and predicate symbols (predicate letters) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p0743604.png" /> also with a varying number of argument places. From the variables and function symbols one constructs the terms of the language, which are names of objects of the theory to be studied. Further, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p0743605.png" /> is an <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p0743606.png" />-place predicate symbol of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p0743607.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p0743608.png" />, and if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p0743609.png" /> are terms, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436010.png" /> is, by definition, an atomic (elementary) formula of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436011.png" />. The content of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436012.png" /> is that the statement according to which <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436013.png" /> are related through the relation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436014.png" /> is true.
+
In order to formulate the predicate calculus one must first fix an exact logico-mathematical language $\Omega$. In the most common case of single-sorted first-order languages, such a language contains predicate variables $x,y,z,\dots,$ function symbols $f,g,h,\dots$ with a varying number of argument places, and predicate symbols (predicate letters) $P,Q,R,\dots,$ also with a varying number of argument places. From the variables and function symbols one constructs the terms of the language, which are names of objects of the theory to be studied. Further, if $P$ is an $n$-place predicate symbol of $\Omega$, $n\geq0$, and if $t_1,\dots,t_n$ are terms, then $P(t_1,\dots,t_n)$ is, by definition, an atomic (elementary) formula of $\Omega$. The content of $P(t_1,\dots,t_n)$ is that the statement according to which $t_1,\dots,t_n$ are related through the relation $P$ is true.
  
By means of propositional connectives (cf. [[Propositional connective|Propositional connective]]) and quantifiers (cf. [[Quantifier|Quantifier]]) one constructs formulas of the language from the atomic formulas. The common choice of connectives and quantifiers in classical and intuitionistic predicate calculus is: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436015.png" /> or <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436016.png" /> (conjunction,  "and" ), <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436017.png" /> (disjunction, non-exclusive  "or" ), <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436018.png" /> or <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436019.png" /> (implication,  "implies" ,  "if … then" ), <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436020.png" /> (negation,  "not" ), <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436021.png" /> (the universal quantifier,  "for all" ), and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436022.png" /> (the existential quantifier,  "there exists" ). The corresponding non-atomic formulas of these calculi have the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436023.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436024.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436025.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436026.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436027.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436028.png" />. An occurrence of a variable <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436029.png" /> in a formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436030.png" /> is called bound if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436031.png" /> occurs in a part of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436032.png" /> of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436033.png" /> or <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436034.png" />. All other occurrences of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436035.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436036.png" /> are called free. A variable <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436037.png" /> is called a parameter of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436038.png" /> if there is at least one free occurrence of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436039.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436040.png" />. Intuitively speaking, a formula with parameters expresses a condition that is turned into a concrete statement if a model of the calculus is given, i.e. some non-empty domain of objects of study is chosen and predicates (i.e. relations on the domains of the objects) are ascribed to the predicate symbols, while the parameters are ascribed definite objects as values.
+
By means of propositional connectives (cf. [[Propositional connective|Propositional connective]]) and quantifiers (cf. [[Quantifier|Quantifier]]) one constructs formulas of the language from the atomic formulas. The common choice of connectives and quantifiers in classical and intuitionistic predicate calculus is: $\&$ or $\land$ (conjunction,  "and"), $\lor$ (disjunction, non-exclusive  "or"), $\to$ or $\supset$ (implication,  "implies" ,  "if … then"), $\neg$ (negation,  "not"), $\forall$ (the universal quantifier,  "for all"), and $\exists$ (the existential quantifier,  "there exists"). The corresponding non-atomic formulas of these calculi have the form $(\phi\land\psi)$, $(\phi\lor\psi)$, $(\phi\supset\psi)$, $\neg\phi$, $\forall x\phi$, $\exists x\phi$. An occurrence of a variable $x$ in a formula $\phi$ is called bound if $x$ occurs in a part of $\phi$ of the form $\exists x\psi$ or $\forall x\psi$. All other occurrences of $x$ in $\phi$ are called free. A variable $x$ is called a parameter of $\phi$ if there is at least one free occurrence of $x$ in $\phi$. Intuitively speaking, a formula with parameters expresses a condition that is turned into a concrete statement if a model of the calculus is given, i.e. some non-empty domain of objects of study is chosen and predicates (i.e. relations on the domains of the objects) are ascribed to the predicate symbols, while the parameters are ascribed definite objects as values.
  
 
A predicate calculus is specified by means of axioms and derivation rules. E.g., one of the usual formulations of classical predicate calculus contains the axioms
 
A predicate calculus is specified by means of axioms and derivation rules. E.g., one of the usual formulations of classical predicate calculus contains the axioms
  
1) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436041.png" />;
+
1) $(\phi\supset(\psi\supset\phi))$;
  
2) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436042.png" />;
+
2) $((\phi\supset(\psi\supset\eta))\supset((\phi\supset\psi)\supset(\phi\supset\eta)))$;
  
3) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436043.png" />;
+
3) $((\phi\land\psi)\supset\phi)$;
  
4) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436044.png" />;
+
4) $((\phi\land\psi)\supset\psi)$;
  
5) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436045.png" />;
+
5) $(\phi\supset(\psi\supset(\phi\land\psi)))$;
  
6) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436046.png" />;
+
6) $((\phi\supset\eta)\supset((\psi\supset\eta)\supset((\phi\lor\psi)\supset\eta)))$;
  
7) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436047.png" />;
+
7) $(\phi\supset(\phi\lor\psi))$;
  
8) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436048.png" />;
+
8) $(\psi\supset(\phi\lor\psi))$;
  
9) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436049.png" />;
+
9) $(\neg\phi\supset(\phi\supset\psi))$;
  
10) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436050.png" />;
+
10) $((\phi\supset\psi)\supset((\phi\supset\neg\psi)\supset\neg\phi))$;
  
11) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436051.png" />;
+
11) $(\phi\lor\neg\phi)$;
  
12) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436052.png" />;
+
12) $(\forall x\phi\supset\phi(x|t))$;
  
13) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436053.png" />;
+
13) $(\phi(x|t)\supset\exists x\phi)$;
  
14) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436054.png" />;
+
14) $(\forall x(\phi\supset\psi)\supset(\phi\supset\forall x\psi))$;
  
15) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436055.png" />. Here, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436056.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436057.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436058.png" /> denote arbitrary formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436059.png" />, so that each of 1)–15) represents an axiom scheme generating a concrete axiom of the calculus for a concrete choice of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436060.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436061.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436062.png" />. Further, in 14) and 15) it is assumed that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436063.png" /> is not a parameter of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436064.png" />; in 12) and 13) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436065.png" /> denotes the result of simultaneous substitution of all free occurrences of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436066.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436067.png" /> by the term <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436068.png" />. (Moreover, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436069.png" /> shows up instead of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436070.png" /> in a part of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436071.png" /> of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436072.png" /> or <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436073.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436074.png" /> occurs in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436075.png" />, then one must additionally replace all bound occurrences of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436076.png" /> in this part by a variable not occurring in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436077.png" />; this is done in order not to distort the meaning of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436078.png" /> when replacing <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436079.png" /> with <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436080.png" />; such a distortion of meaning is called collision of variables.)
+
15) $(\forall x(\psi\supset\phi)\supset(\exists x\psi\supset\phi))$. Here, $\phi$, $\psi$ and $\eta$ denote arbitrary formulas of $\Omega$, so that each of 1)–15) represents an axiom scheme generating a concrete axiom of the calculus for a concrete choice of $\phi$, $\psi$ and $\eta$. Further, in 14) and 15) it is assumed that $x$ is not a parameter of $\phi$; in 12) and 13) $\phi(x|t)$ denotes the result of simultaneous substitution of all free occurrences of $x$ in $\phi$ by the term $t$. (Moreover, if $t$ shows up instead of $x$ in a part of $\phi$ of the form $\exists y\psi$ or $\forall y\psi$, where $y$ occurs in $t$, then one must additionally replace all bound occurrences of $y$ in this part by a variable not occurring in $\phi$; this is done in order not to distort the meaning of $\phi$ when replacing $x$ with $t$; such a distortion of meaning is called collision of variables.)
  
Further, predicate calculus contains two derivation rules: a) if formulas <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436081.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436082.png" /> have been derived, then a derivation for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436083.png" /> exists (the rule of [[Modus ponens|modus ponens]]); and b) if a formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436084.png" /> has been derived and if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436085.png" /> is a variable, then a derivation for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p074/p074360/p07436086.png" /> exists (the rule of generalization).
+
Further, predicate calculus contains two derivation rules: a) if formulas $\phi$ and $(\phi\supset\psi)$ have been derived, then a derivation for $\psi$ exists (the rule of [[Modus ponens|modus ponens]]); and b) if a formula $\phi$ has been derived and if $x$ is a variable, then a derivation for $\forall x\phi$ exists (the rule of generalization).
  
The interpretation of the logical connectives in predicate calculus is the same as in [[Propositional calculus|propositional calculus]]. In connection with the interpretation of quantifiers, it should be noted that in classical predicate calculus they are treated with the use of the actual infinity. If an interpretation of the language is given, then every formula not containing parameters receives the value  "true"  or  "false" . A formula is called classically (universally) valid if in any interpretation and for all values ascribed to the parameters, it has the value  "true" . By virtue of the [[Gödel completeness theorem|Gödel completeness theorem]], the classically-valid formulas are exactly those which can be derived in classical predicate calculus. This theorem is an exact expression of the idea of a formalization of classical logic: In classical predicate calculus all logical laws that are true in all models can be derived.
+
The interpretation of the logical connectives in predicate calculus is the same as in [[Propositional calculus|propositional calculus]]. In connection with the interpretation of quantifiers, it should be noted that in classical predicate calculus they are treated with the use of the actual infinity. If an interpretation of the language is given, then every formula not containing parameters receives the value  "true"  or  "false". A formula is called classically (universally) valid if in any interpretation and for all values ascribed to the parameters, it has the value  "true". By virtue of the [[Gödel completeness theorem|Gödel completeness theorem]], the classically-valid formulas are exactly those which can be derived in classical predicate calculus. This theorem is an exact expression of the idea of a formalization of classical logic: In classical predicate calculus all logical laws that are true in all models can be derived.
  
 
Intuitionistic predicate calculus differs from classical predicate calculus in that axiom scheme 11) does not occur in its list of axiom schemes. The difference between the two calculi is reflected in the way the logical connectives and quantifiers are understood. In intuitionistic predicate calculus this understanding is within the framework of [[Intuitionism|intuitionism]]. The question of the completeness of intuitionistic predicate calculus is much more complicated and admits different solutions, depending on the particular semantics; but here too one can develop a very substantial theory of models, analogous to classical model theory (cf. [[Kripke models|Kripke models]]; [[Realizability|Realizability]]).
 
Intuitionistic predicate calculus differs from classical predicate calculus in that axiom scheme 11) does not occur in its list of axiom schemes. The difference between the two calculi is reflected in the way the logical connectives and quantifiers are understood. In intuitionistic predicate calculus this understanding is within the framework of [[Intuitionism|intuitionism]]. The question of the completeness of intuitionistic predicate calculus is much more complicated and admits different solutions, depending on the particular semantics; but here too one can develop a very substantial theory of models, analogous to classical model theory (cf. [[Kripke models|Kripke models]]; [[Realizability|Realizability]]).

Latest revision as of 18:05, 22 September 2014

A formal axiomatic theory; a calculus intended for the description of logical laws (cf. Logical law) that are true for any non-empty domain of objects with arbitrary predicates (i.e. properties and relations) given on these objects.

In order to formulate the predicate calculus one must first fix an exact logico-mathematical language $\Omega$. In the most common case of single-sorted first-order languages, such a language contains predicate variables $x,y,z,\dots,$ function symbols $f,g,h,\dots$ with a varying number of argument places, and predicate symbols (predicate letters) $P,Q,R,\dots,$ also with a varying number of argument places. From the variables and function symbols one constructs the terms of the language, which are names of objects of the theory to be studied. Further, if $P$ is an $n$-place predicate symbol of $\Omega$, $n\geq0$, and if $t_1,\dots,t_n$ are terms, then $P(t_1,\dots,t_n)$ is, by definition, an atomic (elementary) formula of $\Omega$. The content of $P(t_1,\dots,t_n)$ is that the statement according to which $t_1,\dots,t_n$ are related through the relation $P$ is true.

By means of propositional connectives (cf. Propositional connective) and quantifiers (cf. Quantifier) one constructs formulas of the language from the atomic formulas. The common choice of connectives and quantifiers in classical and intuitionistic predicate calculus is: $\&$ or $\land$ (conjunction, "and"), $\lor$ (disjunction, non-exclusive "or"), $\to$ or $\supset$ (implication, "implies" , "if … then"), $\neg$ (negation, "not"), $\forall$ (the universal quantifier, "for all"), and $\exists$ (the existential quantifier, "there exists"). The corresponding non-atomic formulas of these calculi have the form $(\phi\land\psi)$, $(\phi\lor\psi)$, $(\phi\supset\psi)$, $\neg\phi$, $\forall x\phi$, $\exists x\phi$. An occurrence of a variable $x$ in a formula $\phi$ is called bound if $x$ occurs in a part of $\phi$ of the form $\exists x\psi$ or $\forall x\psi$. All other occurrences of $x$ in $\phi$ are called free. A variable $x$ is called a parameter of $\phi$ if there is at least one free occurrence of $x$ in $\phi$. Intuitively speaking, a formula with parameters expresses a condition that is turned into a concrete statement if a model of the calculus is given, i.e. some non-empty domain of objects of study is chosen and predicates (i.e. relations on the domains of the objects) are ascribed to the predicate symbols, while the parameters are ascribed definite objects as values.

A predicate calculus is specified by means of axioms and derivation rules. E.g., one of the usual formulations of classical predicate calculus contains the axioms

1) $(\phi\supset(\psi\supset\phi))$;

2) $((\phi\supset(\psi\supset\eta))\supset((\phi\supset\psi)\supset(\phi\supset\eta)))$;

3) $((\phi\land\psi)\supset\phi)$;

4) $((\phi\land\psi)\supset\psi)$;

5) $(\phi\supset(\psi\supset(\phi\land\psi)))$;

6) $((\phi\supset\eta)\supset((\psi\supset\eta)\supset((\phi\lor\psi)\supset\eta)))$;

7) $(\phi\supset(\phi\lor\psi))$;

8) $(\psi\supset(\phi\lor\psi))$;

9) $(\neg\phi\supset(\phi\supset\psi))$;

10) $((\phi\supset\psi)\supset((\phi\supset\neg\psi)\supset\neg\phi))$;

11) $(\phi\lor\neg\phi)$;

12) $(\forall x\phi\supset\phi(x|t))$;

13) $(\phi(x|t)\supset\exists x\phi)$;

14) $(\forall x(\phi\supset\psi)\supset(\phi\supset\forall x\psi))$;

15) $(\forall x(\psi\supset\phi)\supset(\exists x\psi\supset\phi))$. Here, $\phi$, $\psi$ and $\eta$ denote arbitrary formulas of $\Omega$, so that each of 1)–15) represents an axiom scheme generating a concrete axiom of the calculus for a concrete choice of $\phi$, $\psi$ and $\eta$. Further, in 14) and 15) it is assumed that $x$ is not a parameter of $\phi$; in 12) and 13) $\phi(x|t)$ denotes the result of simultaneous substitution of all free occurrences of $x$ in $\phi$ by the term $t$. (Moreover, if $t$ shows up instead of $x$ in a part of $\phi$ of the form $\exists y\psi$ or $\forall y\psi$, where $y$ occurs in $t$, then one must additionally replace all bound occurrences of $y$ in this part by a variable not occurring in $\phi$; this is done in order not to distort the meaning of $\phi$ when replacing $x$ with $t$; such a distortion of meaning is called collision of variables.)

Further, predicate calculus contains two derivation rules: a) if formulas $\phi$ and $(\phi\supset\psi)$ have been derived, then a derivation for $\psi$ exists (the rule of modus ponens); and b) if a formula $\phi$ has been derived and if $x$ is a variable, then a derivation for $\forall x\phi$ exists (the rule of generalization).

The interpretation of the logical connectives in predicate calculus is the same as in propositional calculus. In connection with the interpretation of quantifiers, it should be noted that in classical predicate calculus they are treated with the use of the actual infinity. If an interpretation of the language is given, then every formula not containing parameters receives the value "true" or "false". A formula is called classically (universally) valid if in any interpretation and for all values ascribed to the parameters, it has the value "true". By virtue of the Gödel completeness theorem, the classically-valid formulas are exactly those which can be derived in classical predicate calculus. This theorem is an exact expression of the idea of a formalization of classical logic: In classical predicate calculus all logical laws that are true in all models can be derived.

Intuitionistic predicate calculus differs from classical predicate calculus in that axiom scheme 11) does not occur in its list of axiom schemes. The difference between the two calculi is reflected in the way the logical connectives and quantifiers are understood. In intuitionistic predicate calculus this understanding is within the framework of intuitionism. The question of the completeness of intuitionistic predicate calculus is much more complicated and admits different solutions, depending on the particular semantics; but here too one can develop a very substantial theory of models, analogous to classical model theory (cf. Kripke models; Realizability).

One also uses other formulations of predicate calculus, the most important of which, from the point of view of proof theory, are the calculus of natural deduction (cf. Natural logical deduction) and the sequent calculi (cf. Sequent calculus).

Predicate calculus is a very common basis for the construction of logical calculi intended for the description of fragments of some concrete mathematical theory. E.g., if one wishes to describe some class of true statements of set theory, then one can construct logical calculi in terms of set theory in which, apart from the axioms and derivation rules of classical predicate calculus (the logical postulates), additional non-logical axioms will figure, describing properties of sets. The axiom of choice is a typical example of a non-logical axiom in set theory.

Predicate calculus is sometimes called narrow predicate calculus, first-order predicate calculus or first-order functional calculus, as distinct from calculi containing quantifiers over predicates and corresponding convolution axioms, expressing the existence of the respective predicates. Such a kind of calculus, which already does not have a pure logical character, is often called a higher-order predicate calculus. The theory of types is an example of such a calculus (cf. Types, theory of). Besides classical and intuitionistic predicate calculus there are other types of logical systems describing logical laws which can be expressed by other logical tools or from other methodological positions. Amongst these are modal predicate calculus, inductive logic, etc.

References

[1] D. Hilbert, P. Bernays, "Grundlagen der Mathematik" , 1–2 , Springer (1934–1939)
[2] S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[3] P.S. Novikov, "Elements of mathematical logic" , Oliver & Boyd (1964) (Translated from Russian)
[4] G. Takeuti, "Proof theory" , North-Holland (1975)


Comments

References

[a1] J.L. Bell, M. Machover, "A course in mathematical logic" , North-Holland (1977)
[a2] W.S. Hatcher, "Foundations of mathematics" , Saunders (1968)
How to Cite This Entry:
Predicate calculus. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Predicate_calculus&oldid=16765
This article was adapted from an original article by A.G. Dragalin (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article