Namespaces
Variants
Actions

Difference between revisions of "Logico-mathematical calculus"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
m (tex encoded by computer)
 
Line 1: Line 1:
 +
<!--
 +
l0607701.png
 +
$#A+1 = 105 n = 0
 +
$#C+1 = 105 : ~/encyclopedia/old_files/data/L060/L.0600770 Logico\AAhmathematical calculus,
 +
Automatically converted into TeX, above some diagnostics.
 +
Please remove this comment and the {{TEX|auto}} line below,
 +
if TeX found to be correct.
 +
-->
 +
 +
{{TEX|auto}}
 +
{{TEX|done}}
 +
 
''applied calculus''
 
''applied calculus''
  
A formalization of a mathematical theory. A logico-mathematical calculus is specified by its language and list of postulates (these elements form the [[Syntax|syntax]]) and in most cases it is endowed with a [[Semantics|semantics]]. The essential features that distinguish logico-mathematical calculi from axiomatic theories of traditional mathematics are: 1) the study of the logical tools used in the formulation of axioms and derivation rules (cf. [[Derivation rule|Derivation rule]]) that make it possible to deduce one statement from another; and 2) the transition from informal language to an exact [[Formal language|formal language]]. A logico-mathematical calculus is usually constructed on the basis of a [[Logical calculus|logical calculus]] (the basic logical calculus). The language of the logico-mathematical calculus is obtained from the language of this logical calculus by adding symbols for particular functions and predicates (and possibly removing the predicate variables and variables for functions). The list of postulates of the logico-mathematical calculus is obtained by adding to the list of postulates of the basic logical calculus (understood in relation to the new language) some postulates that describe the properties of the added functions and predicates. For example, the language of elementary group theory is obtained according to this scheme from the language of classical predicate calculus with equality: one adds the symbols <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l0607701.png" /> (multiplication), <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l0607702.png" /> (inversion) and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l0607703.png" /> (the identity), and discards all predicate symbols except equality. The additional postulate
+
A formalization of a mathematical theory. A logico-mathematical calculus is specified by its language and list of postulates (these elements form the [[Syntax|syntax]]) and in most cases it is endowed with a [[Semantics|semantics]]. The essential features that distinguish logico-mathematical calculi from axiomatic theories of traditional mathematics are: 1) the study of the logical tools used in the formulation of axioms and derivation rules (cf. [[Derivation rule|Derivation rule]]) that make it possible to deduce one statement from another; and 2) the transition from informal language to an exact [[Formal language|formal language]]. A logico-mathematical calculus is usually constructed on the basis of a [[Logical calculus|logical calculus]] (the basic logical calculus). The language of the logico-mathematical calculus is obtained from the language of this logical calculus by adding symbols for particular functions and predicates (and possibly removing the predicate variables and variables for functions). The list of postulates of the logico-mathematical calculus is obtained by adding to the list of postulates of the basic logical calculus (understood in relation to the new language) some postulates that describe the properties of the added functions and predicates. For example, the language of elementary group theory is obtained according to this scheme from the language of classical predicate calculus with equality: one adds the symbols $  \cdot $(
 +
multiplication), $  \mathop{\rm inv} $(
 +
inversion) and $  e $(
 +
the identity), and discards all predicate symbols except equality. The additional postulate
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l0607704.png" /></td> </tr></table>
+
$$
 +
\forall x  \forall y  \forall z \
 +
( e \cdot x = x  \&  \mathop{\rm inv} ( x) \cdot x = e  \&  ( x \cdot
 +
y ) \cdot z = x \cdot ( y \cdot z ) )
 +
$$
  
asserts that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l0607705.png" /> is the identity of the group, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l0607706.png" /> is the element inverse to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l0607707.png" /> and multiplication is associative.
+
asserts that $  e $
 +
is the identity of the group, $  \mathop{\rm inv} ( x) $
 +
is the element inverse to $  x $
 +
and multiplication is associative.
  
 
Logico-mathematical calculi constructed on the basis of predicate calculus with equality serve to describe the most frequently encountered mathematical structures. Among them are formal arithmetic (cf. [[Arithmetic, formal|Arithmetic, formal]]), formalized analysis (with quantifiers of orders one and two), [[Axiomatic set theory|axiomatic set theory]], etc. The semantics of a logico-mathematical calculus gives interpretations of the variables, mathematical symbols (symbols of predicates and functions) and logical operations. These interpretations determine models of the logico-mathematical calculus. The truth of a formula in every model in which the axioms of some logico-mathematical calculus based on classical predicate calculus with equality are true implies, by the [[Gödel completeness theorem|Gödel completeness theorem]], that this formula can be deduced in the logico-mathematical calculus in question.
 
Logico-mathematical calculi constructed on the basis of predicate calculus with equality serve to describe the most frequently encountered mathematical structures. Among them are formal arithmetic (cf. [[Arithmetic, formal|Arithmetic, formal]]), formalized analysis (with quantifiers of orders one and two), [[Axiomatic set theory|axiomatic set theory]], etc. The semantics of a logico-mathematical calculus gives interpretations of the variables, mathematical symbols (symbols of predicates and functions) and logical operations. These interpretations determine models of the logico-mathematical calculus. The truth of a formula in every model in which the axioms of some logico-mathematical calculus based on classical predicate calculus with equality are true implies, by the [[Gödel completeness theorem|Gödel completeness theorem]], that this formula can be deduced in the logico-mathematical calculus in question.
  
The simplest in structure are quantifier-free logico-mathematical calculi. They are used most frequently to describe properties of different classes of computable functions. The language of a quantifier-free logico-mathematical calculus is constructed on the basis of the language of the propositional calculus with equality, or even consists of single equalities. In the first case the logical apparatus of the logico-mathematical calculus is classical propositional calculus, and in the second case it is designed as a calculus of equalities. In both cases the following are regarded as postulates: 1) defining equalities of the functions in question (for example, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l0607708.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l0607709.png" />); 2) the basic properties of equality; 3) arguments by the method of mathematical induction (most frequently on the pattern  "from f0= g0, fx'= hx, fx, gx'= hx, gx one can derive fx= gx" ); and 4) an argument corresponding to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077010.png" />-removal:  "given Ax, to derive At"  (the rule of substituting an object variable for a free variable). An example is the system PRA (primitive recursive arithmetic).
+
The simplest in structure are quantifier-free logico-mathematical calculi. They are used most frequently to describe properties of different classes of computable functions. The language of a quantifier-free logico-mathematical calculus is constructed on the basis of the language of the propositional calculus with equality, or even consists of single equalities. In the first case the logical apparatus of the logico-mathematical calculus is classical propositional calculus, and in the second case it is designed as a calculus of equalities. In both cases the following are regarded as postulates: 1) defining equalities of the functions in question (for example, $  x \cdot 0 = 0 $,  
 +
$  x \cdot y  ^  \prime  = x \cdot y + x $);  
 +
2) the basic properties of equality; 3) arguments by the method of mathematical induction (most frequently on the pattern  "from f0= g0, fx'= hx, fx, gx'= hx, gx one can derive fx= gx" ); and 4) an argument corresponding to $  \forall $-
 +
removal:  "given Ax, to derive At"  (the rule of substituting an object variable for a free variable). An example is the system PRA (primitive recursive arithmetic).
  
The object variables of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077011.png" /> are <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077012.png" />; the function variables are <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077013.png" />; the natural numbers are <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077014.png" />. The function symbols (functors) are constructed from the primitive symbols, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077015.png" /> ( "successor" ), <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077016.png" /> (the constant function with value zero), <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077017.png" /> (the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077018.png" />-place function whose value is equal to the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077019.png" />-th argument), where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077020.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077021.png" /> are natural numbers, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077022.png" />, by means of substitution <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077023.png" /> and primitive recursion <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077024.png" />: If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077025.png" /> is an <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077026.png" />-place functor and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077027.png" /> are <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077028.png" />-place functors, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077029.png" /> (the result of substituting <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077030.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077031.png" />) is an <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077032.png" />-place functor; if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077033.png" /> is an <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077034.png" />-place functor and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077035.png" /> is an <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077036.png" />-place functor, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077037.png" /> is an <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077038.png" />-place functor (primitive recursion:
+
The object variables of $  \mathop{\rm PRA} $
 +
are $  ( a) , ( aa) , ( aaa) ,\dots $;  
 +
the function variables are $  ( f  ) , ( ff  ) , ( fff  ) ,\dots $;  
 +
the natural numbers are $  0 , 0  ^  \prime  , 0 ^ {\prime\prime} ,\dots $.  
 +
The function symbols (functors) are constructed from the primitive symbols, $  \prime $(  
 +
"successor" ), $  Z $(
 +
the constant function with value zero), $  [ J , n , m ] $(
 +
the $  m $-
 +
place function whose value is equal to the $  n $-
 +
th argument), where $  n $,  
 +
$  m $
 +
are natural numbers, $  n \leq  m $,  
 +
by means of substitution $  S $
 +
and primitive recursion $  R $:  
 +
If $  \phi $
 +
is an $  n $-
 +
place functor and $  \psi _ {1} \dots \psi _ {n} $
 +
are $  m $-
 +
place functors, then $  S [ \phi , \psi _ {1} \dots \psi _ {n} ] $(
 +
the result of substituting $  \psi _ {1} \dots \psi _ {n} $
 +
in $  \phi $)  
 +
is an $  m $-
 +
place functor; if $  \phi $
 +
is an $  n $-
 +
place functor and $  \psi $
 +
is an $  ( n + 2 ) $-
 +
place functor, then $  R [ \phi , \psi ] $
 +
is an $  ( n + 1 ) $-
 +
place functor (primitive recursion:
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077039.png" /></td> </tr></table>
+
$$
 +
R [ \phi , \psi ] ( 0 , X )  = \
 +
\phi ( X) ;
 +
$$
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077040.png" /></td> </tr></table>
+
$$
 +
R [ \phi , \psi ] ( y  ^  \prime  , X )  = \psi ( y , X , R [ \phi , \psi ] ( y , X ) ) \textrm{ )  } .
 +
$$
  
The terms of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077041.png" /> are <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077042.png" />, object variables and expressions of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077043.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077044.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077045.png" /> are terms and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077046.png" /> is a functor.
+
The terms of $  \mathop{\rm PRA} $
 +
are 0 $,  
 +
object variables and expressions of the form $  s  ^  \prime  $,  
 +
$  \phi ( s _ {1} \dots s _ {n} ) $,  
 +
where $  s , s _ {1} \dots s _ {n} $
 +
are terms and $  \phi $
 +
is a functor.
  
The formulas of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077047.png" /> are <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077048.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077049.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077050.png" /> are terms. Admissible values of object variables are natural numbers, and admissible values of function variables are primitive recursive functions (sometimes wider classes of computable functions, cf. [[Primitive recursive function|Primitive recursive function]]).
+
The formulas of $  \mathop{\rm PRA} $
 +
are $  r = s $,  
 +
where $  r $
 +
and $  s $
 +
are terms. Admissible values of object variables are natural numbers, and admissible values of function variables are primitive recursive functions (sometimes wider classes of computable functions, cf. [[Primitive recursive function|Primitive recursive function]]).
  
In the description of partial (not everywhere-defined) functions, apart from the equality predicate there appears the predicate <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077051.png" /> or <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077052.png" /> ( "defined" ); in this case <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077053.png" /> is interpreted as meaning that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077054.png" /> is defined if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077055.png" /> is, and that they take the same value whenever they are defined. One also adds means of representing a function that is universal for the class in question: Either a symbol for this function, or the rule: if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077056.png" /> is a term, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077057.png" /> is a functor (whose number in some previously fixed enumeration of the class in question is equal to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077058.png" />). The postulates of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077059.png" />-removal and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077060.png" />-introduction are modified:
+
In the description of partial (not everywhere-defined) functions, apart from the equality predicate there appears the predicate $  \uparrow $
 +
or $  ! $(  
 +
"defined" ); in this case $  r = s $
 +
is interpreted as meaning that $  r $
 +
is defined if and only if $  s $
 +
is, and that they take the same value whenever they are defined. One also adds means of representing a function that is universal for the class in question: Either a symbol for this function, or the rule: if $  t $
 +
is a term, then $  \langle  t\rangle $
 +
is a functor (whose number in some previously fixed enumeration of the class in question is equal to $  t $).  
 +
The postulates of $  \forall $-
 +
removal and $  \exists $-
 +
introduction are modified:
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077061.png" /></td> </tr></table>
+
$$
 +
A ( t) \& ! t  \rightarrow  \exists x  A ( x) ; \ \
 +
\forall x  A ( x) \& ! t  \rightarrow  A ( t) .
 +
$$
  
One adds the axiom <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077062.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077063.png" /> is an object variable or a constant, and also axioms of the form
+
One adds the axiom $  ! t $,  
 +
where $  t $
 +
is an object variable or a constant, and also axioms of the form
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077064.png" /></td> </tr></table>
+
$$
 +
! \phi ( t)  \rightarrow  ! t .
 +
$$
  
Logico-mathematical calculi are also used to describe computable functions of different types: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077065.png" /> is a type (the objects of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077066.png" /> are the natural numbers); if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077067.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077068.png" /> are types, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077069.png" /> is a type (of operations that transform objects of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077070.png" /> into objects of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077071.png" />). These are the finite types (see [[Types, theory of|Types, theory of]]). One also considers transfinite types. For every type one introduces variables and constants of this type, usually including a symbol for the operation all values of which are equal to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077072.png" />, and also the object <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077073.png" /> of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077074.png" />. For every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077075.png" />, among the constants of the type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077076.png" /> one often includes the operator of primitive recursion. Terms of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077077.png" /> are variables and constants of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077078.png" />, expressions of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077079.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077080.png" /> is a term of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077081.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077082.png" /> is a term of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077083.png" />, and also expressions of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077084.png" />, which is interpreted as the notation of the functional that transforms <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077085.png" /> into <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077086.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077087.png" /> is of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077088.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077089.png" /> is of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077090.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077091.png" />. Quantifier-free logico-mathematical calculi for functionals of finite types are used for the mathematical investigation of quantifier logico-mathematical calculi. In particular, by means of a quantifier-free system of primitive recursive functionals it has been possible to prove the relative consistency of formal arithmetic; the addition of the so-called bar-recursion operator makes it possible to prove the relative consistency of formal analysis.
+
Logico-mathematical calculi are also used to describe computable functions of different types: 0 $
 +
is a type (the objects of type 0 $
 +
are the natural numbers); if $  \sigma $
 +
and $  \tau $
 +
are types, then $  ( \sigma \rightarrow \tau ) $
 +
is a type (of operations that transform objects of type $  \sigma $
 +
into objects of type $  \tau $).  
 +
These are the finite types (see [[Types, theory of|Types, theory of]]). One also considers transfinite types. For every type one introduces variables and constants of this type, usually including a symbol for the operation all values of which are equal to 0 $,  
 +
and also the object $  \prime $
 +
of type $  ( 0 \rightarrow 0 ) $.  
 +
For every $  \sigma $,  
 +
among the constants of the type $  ( \sigma \rightarrow ( ( 0 \rightarrow ( \sigma \rightarrow \sigma ) ) \rightarrow ( 0 \rightarrow \sigma )) ) $
 +
one often includes the operator of primitive recursion. Terms of type $  \sigma $
 +
are variables and constants of type $  \sigma $,  
 +
expressions of the form $  r ( s) $,  
 +
where $  r $
 +
is a term of type $  ( \tau \rightarrow \sigma ) $
 +
and $  s $
 +
is a term of type $  \tau $,  
 +
and also expressions of the form $  \lambda x r $,  
 +
which is interpreted as the notation of the functional that transforms $  x $
 +
into $  r ( x) $,  
 +
where $  r $
 +
is of type $  \beta $,  
 +
$  x $
 +
is of type $  \alpha $
 +
and $  \sigma = ( \alpha \rightarrow \beta ) $.  
 +
Quantifier-free logico-mathematical calculi for functionals of finite types are used for the mathematical investigation of quantifier logico-mathematical calculi. In particular, by means of a quantifier-free system of primitive recursive functionals it has been possible to prove the relative consistency of formal arithmetic; the addition of the so-called bar-recursion operator makes it possible to prove the relative consistency of formal analysis.
  
 
An important property of some logico-mathematical calculi is completeness. This means that every formula not containing free variables is deducible or refutable. The completeness of a logico-mathematical calculus implies the solvability of the deducibility problem — the existence of an algorithm that determines for every formula whether it is deducible or not. An example of a complete logico-mathematical calculus is the theory of algebraically closed fields (the Tarski system). According to the [[Gödel incompleteness theorem|Gödel incompleteness theorem]], complete theories are rare: Any consistent, recursively-presented logico-mathematical calculus that contains a very restricted fragment of arithmetic is incomplete. For a wider class of logico-mathematical calculi the deducibility problem is algorithmically unsolvable.
 
An important property of some logico-mathematical calculi is completeness. This means that every formula not containing free variables is deducible or refutable. The completeness of a logico-mathematical calculus implies the solvability of the deducibility problem — the existence of an algorithm that determines for every formula whether it is deducible or not. An example of a complete logico-mathematical calculus is the theory of algebraically closed fields (the Tarski system). According to the [[Gödel incompleteness theorem|Gödel incompleteness theorem]], complete theories are rare: Any consistent, recursively-presented logico-mathematical calculus that contains a very restricted fragment of arithmetic is incomplete. For a wider class of logico-mathematical calculi the deducibility problem is algorithmically unsolvable.
Line 35: Line 147:
 
An important characteristic of a logico-mathematical calculus is its expressive capacity. It is often possible to introduce expressive tools that do not occur explicitly in the language of the calculus in question. Thus, in some quantifier-free languages it is possible to introduce logical connectives and restricted quantifiers:
 
An important characteristic of a logico-mathematical calculus is its expressive capacity. It is often possible to introduce expressive tools that do not occur explicitly in the language of the calculus in question. Thus, in some quantifier-free languages it is possible to introduce logical connectives and restricted quantifiers:
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077092.png" /></td> </tr></table>
+
$$
 +
x = y  \&  u = v  \textrm{ means }  | x - y | + | u - v | = 0 ,
 +
$$
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077093.png" /></td> </tr></table>
+
$$
 +
\forall  x \leq  a ( f ( x) = g ( x) ) \
 +
\textrm{ means }  \sum _ {x \leq  a } | f ( x) - g ( x) | = 0 .
 +
$$
  
In the language of formal arithmetic one can talk of finite sets, partial recursive functions, etc. Some logical connectives are expressible in terms of others; thus, in second-order calculi (including those based on intuitionistic logic) all connectives are expressible in terms of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077094.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077095.png" />; for example, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077096.png" /> is equivalent to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077097.png" />. The principal restrictions on the expressive capacity of the language are given by Tarski's theorem: Under the natural enumeration of the formulas of a language containing a minimum of arithmetic, it is impossible to give a formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077098.png" /> of this language such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l06077099.png" /> is true if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l060770100.png" /> is the number of a true formula. For some logico-mathematical calculi based on constructive (intuitionistic) logic the disjunction theorem holds: The deducibility of a closed formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l060770101.png" /> implies the deducibility of one of the formulas <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l060770102.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l060770103.png" />. In the investigation of the structure of such logico-mathematical calculi various analogues of the concept of [[Realizability|realizability]] are used. Questions of the consistency of logico-mathematical calculi, the independence of individual postulates, the existence of individual axiomatics (that is, such that every deducible formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l060770104.png" /> has a derivation that uses only the postulates for implication and the symbols that occur in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l060/l060770/l060770105.png" />), and the existence of interpretations of some logico-mathematical calculi in others, are investigated in [[Proof theory|proof theory]].
+
In the language of formal arithmetic one can talk of finite sets, partial recursive functions, etc. Some logical connectives are expressible in terms of others; thus, in second-order calculi (including those based on intuitionistic logic) all connectives are expressible in terms of $  \forall $
 +
and $  \rightarrow $;  
 +
for example, $  \exists x  A ( x) $
 +
is equivalent to $  \forall  P ( \forall  x ( A x \rightarrow P ) \rightarrow P ) $.  
 +
The principal restrictions on the expressive capacity of the language are given by Tarski's theorem: Under the natural enumeration of the formulas of a language containing a minimum of arithmetic, it is impossible to give a formula $  T ( x) $
 +
of this language such that $  T ( n) $
 +
is true if and only if $  n $
 +
is the number of a true formula. For some logico-mathematical calculi based on constructive (intuitionistic) logic the disjunction theorem holds: The deducibility of a closed formula $  A \lor B $
 +
implies the deducibility of one of the formulas $  A $
 +
and $  B $.  
 +
In the investigation of the structure of such logico-mathematical calculi various analogues of the concept of [[Realizability|realizability]] are used. Questions of the consistency of logico-mathematical calculi, the independence of individual postulates, the existence of individual axiomatics (that is, such that every deducible formula $  A $
 +
has a derivation that uses only the postulates for implication and the symbols that occur in $  A $),  
 +
and the existence of interpretations of some logico-mathematical calculi in others, are investigated in [[Proof theory|proof theory]].
  
 
====References====
 
====References====
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  D. Hilbert,  P. Bernays,  "Grundlagen der Mathematik" , '''1''' , Springer  (1968)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  P.S. Novikov,  "Elements of mathematical logic" , Oliver &amp; Boyd and Acad. Press  (1964)  (Translated from Russian)</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  S.C. Kleene,  "Introduction to metamathematics" , North-Holland  (1951)</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  A. Church,  "Introduction to mathematical logic" , '''1''' , Princeton Univ. Press  (1956)</TD></TR><TR><TD valign="top">[5]</TD> <TD valign="top">  R.C. Lyndon,  "Notes on logic" , v. Nostrand  (1966)</TD></TR></table>
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  D. Hilbert,  P. Bernays,  "Grundlagen der Mathematik" , '''1''' , Springer  (1968)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  P.S. Novikov,  "Elements of mathematical logic" , Oliver &amp; Boyd and Acad. Press  (1964)  (Translated from Russian)</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  S.C. Kleene,  "Introduction to metamathematics" , North-Holland  (1951)</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  A. Church,  "Introduction to mathematical logic" , '''1''' , Princeton Univ. Press  (1956)</TD></TR><TR><TD valign="top">[5]</TD> <TD valign="top">  R.C. Lyndon,  "Notes on logic" , v. Nostrand  (1966)</TD></TR></table>
 
 
  
 
====Comments====
 
====Comments====

Latest revision as of 04:11, 6 June 2020


applied calculus

A formalization of a mathematical theory. A logico-mathematical calculus is specified by its language and list of postulates (these elements form the syntax) and in most cases it is endowed with a semantics. The essential features that distinguish logico-mathematical calculi from axiomatic theories of traditional mathematics are: 1) the study of the logical tools used in the formulation of axioms and derivation rules (cf. Derivation rule) that make it possible to deduce one statement from another; and 2) the transition from informal language to an exact formal language. A logico-mathematical calculus is usually constructed on the basis of a logical calculus (the basic logical calculus). The language of the logico-mathematical calculus is obtained from the language of this logical calculus by adding symbols for particular functions and predicates (and possibly removing the predicate variables and variables for functions). The list of postulates of the logico-mathematical calculus is obtained by adding to the list of postulates of the basic logical calculus (understood in relation to the new language) some postulates that describe the properties of the added functions and predicates. For example, the language of elementary group theory is obtained according to this scheme from the language of classical predicate calculus with equality: one adds the symbols $ \cdot $( multiplication), $ \mathop{\rm inv} $( inversion) and $ e $( the identity), and discards all predicate symbols except equality. The additional postulate

$$ \forall x \forall y \forall z \ ( e \cdot x = x \& \mathop{\rm inv} ( x) \cdot x = e \& ( x \cdot y ) \cdot z = x \cdot ( y \cdot z ) ) $$

asserts that $ e $ is the identity of the group, $ \mathop{\rm inv} ( x) $ is the element inverse to $ x $ and multiplication is associative.

Logico-mathematical calculi constructed on the basis of predicate calculus with equality serve to describe the most frequently encountered mathematical structures. Among them are formal arithmetic (cf. Arithmetic, formal), formalized analysis (with quantifiers of orders one and two), axiomatic set theory, etc. The semantics of a logico-mathematical calculus gives interpretations of the variables, mathematical symbols (symbols of predicates and functions) and logical operations. These interpretations determine models of the logico-mathematical calculus. The truth of a formula in every model in which the axioms of some logico-mathematical calculus based on classical predicate calculus with equality are true implies, by the Gödel completeness theorem, that this formula can be deduced in the logico-mathematical calculus in question.

The simplest in structure are quantifier-free logico-mathematical calculi. They are used most frequently to describe properties of different classes of computable functions. The language of a quantifier-free logico-mathematical calculus is constructed on the basis of the language of the propositional calculus with equality, or even consists of single equalities. In the first case the logical apparatus of the logico-mathematical calculus is classical propositional calculus, and in the second case it is designed as a calculus of equalities. In both cases the following are regarded as postulates: 1) defining equalities of the functions in question (for example, $ x \cdot 0 = 0 $, $ x \cdot y ^ \prime = x \cdot y + x $); 2) the basic properties of equality; 3) arguments by the method of mathematical induction (most frequently on the pattern "from f0= g0, fx'= hx, fx, gx'= hx, gx one can derive fx= gx" ); and 4) an argument corresponding to $ \forall $- removal: "given Ax, to derive At" (the rule of substituting an object variable for a free variable). An example is the system PRA (primitive recursive arithmetic).

The object variables of $ \mathop{\rm PRA} $ are $ ( a) , ( aa) , ( aaa) ,\dots $; the function variables are $ ( f ) , ( ff ) , ( fff ) ,\dots $; the natural numbers are $ 0 , 0 ^ \prime , 0 ^ {\prime\prime} ,\dots $. The function symbols (functors) are constructed from the primitive symbols, $ \prime $( "successor" ), $ Z $( the constant function with value zero), $ [ J , n , m ] $( the $ m $- place function whose value is equal to the $ n $- th argument), where $ n $, $ m $ are natural numbers, $ n \leq m $, by means of substitution $ S $ and primitive recursion $ R $: If $ \phi $ is an $ n $- place functor and $ \psi _ {1} \dots \psi _ {n} $ are $ m $- place functors, then $ S [ \phi , \psi _ {1} \dots \psi _ {n} ] $( the result of substituting $ \psi _ {1} \dots \psi _ {n} $ in $ \phi $) is an $ m $- place functor; if $ \phi $ is an $ n $- place functor and $ \psi $ is an $ ( n + 2 ) $- place functor, then $ R [ \phi , \psi ] $ is an $ ( n + 1 ) $- place functor (primitive recursion:

$$ R [ \phi , \psi ] ( 0 , X ) = \ \phi ( X) ; $$

$$ R [ \phi , \psi ] ( y ^ \prime , X ) = \psi ( y , X , R [ \phi , \psi ] ( y , X ) ) \textrm{ ) } . $$

The terms of $ \mathop{\rm PRA} $ are $ 0 $, object variables and expressions of the form $ s ^ \prime $, $ \phi ( s _ {1} \dots s _ {n} ) $, where $ s , s _ {1} \dots s _ {n} $ are terms and $ \phi $ is a functor.

The formulas of $ \mathop{\rm PRA} $ are $ r = s $, where $ r $ and $ s $ are terms. Admissible values of object variables are natural numbers, and admissible values of function variables are primitive recursive functions (sometimes wider classes of computable functions, cf. Primitive recursive function).

In the description of partial (not everywhere-defined) functions, apart from the equality predicate there appears the predicate $ \uparrow $ or $ ! $( "defined" ); in this case $ r = s $ is interpreted as meaning that $ r $ is defined if and only if $ s $ is, and that they take the same value whenever they are defined. One also adds means of representing a function that is universal for the class in question: Either a symbol for this function, or the rule: if $ t $ is a term, then $ \langle t\rangle $ is a functor (whose number in some previously fixed enumeration of the class in question is equal to $ t $). The postulates of $ \forall $- removal and $ \exists $- introduction are modified:

$$ A ( t) \& ! t \rightarrow \exists x A ( x) ; \ \ \forall x A ( x) \& ! t \rightarrow A ( t) . $$

One adds the axiom $ ! t $, where $ t $ is an object variable or a constant, and also axioms of the form

$$ ! \phi ( t) \rightarrow ! t . $$

Logico-mathematical calculi are also used to describe computable functions of different types: $ 0 $ is a type (the objects of type $ 0 $ are the natural numbers); if $ \sigma $ and $ \tau $ are types, then $ ( \sigma \rightarrow \tau ) $ is a type (of operations that transform objects of type $ \sigma $ into objects of type $ \tau $). These are the finite types (see Types, theory of). One also considers transfinite types. For every type one introduces variables and constants of this type, usually including a symbol for the operation all values of which are equal to $ 0 $, and also the object $ \prime $ of type $ ( 0 \rightarrow 0 ) $. For every $ \sigma $, among the constants of the type $ ( \sigma \rightarrow ( ( 0 \rightarrow ( \sigma \rightarrow \sigma ) ) \rightarrow ( 0 \rightarrow \sigma )) ) $ one often includes the operator of primitive recursion. Terms of type $ \sigma $ are variables and constants of type $ \sigma $, expressions of the form $ r ( s) $, where $ r $ is a term of type $ ( \tau \rightarrow \sigma ) $ and $ s $ is a term of type $ \tau $, and also expressions of the form $ \lambda x r $, which is interpreted as the notation of the functional that transforms $ x $ into $ r ( x) $, where $ r $ is of type $ \beta $, $ x $ is of type $ \alpha $ and $ \sigma = ( \alpha \rightarrow \beta ) $. Quantifier-free logico-mathematical calculi for functionals of finite types are used for the mathematical investigation of quantifier logico-mathematical calculi. In particular, by means of a quantifier-free system of primitive recursive functionals it has been possible to prove the relative consistency of formal arithmetic; the addition of the so-called bar-recursion operator makes it possible to prove the relative consistency of formal analysis.

An important property of some logico-mathematical calculi is completeness. This means that every formula not containing free variables is deducible or refutable. The completeness of a logico-mathematical calculus implies the solvability of the deducibility problem — the existence of an algorithm that determines for every formula whether it is deducible or not. An example of a complete logico-mathematical calculus is the theory of algebraically closed fields (the Tarski system). According to the Gödel incompleteness theorem, complete theories are rare: Any consistent, recursively-presented logico-mathematical calculus that contains a very restricted fragment of arithmetic is incomplete. For a wider class of logico-mathematical calculi the deducibility problem is algorithmically unsolvable.

An important characteristic of a logico-mathematical calculus is its expressive capacity. It is often possible to introduce expressive tools that do not occur explicitly in the language of the calculus in question. Thus, in some quantifier-free languages it is possible to introduce logical connectives and restricted quantifiers:

$$ x = y \& u = v \textrm{ means } | x - y | + | u - v | = 0 , $$

$$ \forall x \leq a ( f ( x) = g ( x) ) \ \textrm{ means } \sum _ {x \leq a } | f ( x) - g ( x) | = 0 . $$

In the language of formal arithmetic one can talk of finite sets, partial recursive functions, etc. Some logical connectives are expressible in terms of others; thus, in second-order calculi (including those based on intuitionistic logic) all connectives are expressible in terms of $ \forall $ and $ \rightarrow $; for example, $ \exists x A ( x) $ is equivalent to $ \forall P ( \forall x ( A x \rightarrow P ) \rightarrow P ) $. The principal restrictions on the expressive capacity of the language are given by Tarski's theorem: Under the natural enumeration of the formulas of a language containing a minimum of arithmetic, it is impossible to give a formula $ T ( x) $ of this language such that $ T ( n) $ is true if and only if $ n $ is the number of a true formula. For some logico-mathematical calculi based on constructive (intuitionistic) logic the disjunction theorem holds: The deducibility of a closed formula $ A \lor B $ implies the deducibility of one of the formulas $ A $ and $ B $. In the investigation of the structure of such logico-mathematical calculi various analogues of the concept of realizability are used. Questions of the consistency of logico-mathematical calculi, the independence of individual postulates, the existence of individual axiomatics (that is, such that every deducible formula $ A $ has a derivation that uses only the postulates for implication and the symbols that occur in $ A $), and the existence of interpretations of some logico-mathematical calculi in others, are investigated in proof theory.

References

[1] D. Hilbert, P. Bernays, "Grundlagen der Mathematik" , 1 , Springer (1968)
[2] P.S. Novikov, "Elements of mathematical logic" , Oliver & Boyd and Acad. Press (1964) (Translated from Russian)
[3] S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[4] A. Church, "Introduction to mathematical logic" , 1 , Princeton Univ. Press (1956)
[5] R.C. Lyndon, "Notes on logic" , v. Nostrand (1966)

Comments

The term "logico-mathematical calculus" is not in common use in English: a more usual name for this concept is "(first-order theoryfirst-order) logical theorytheory" .

References

[a1] S.C. Kleene, "Mathematical logic" , Wiley (1967)
[a2] C.C. Chang, H.J. Keisler, "Model theory" , North-Holland (1973)
How to Cite This Entry:
Logico-mathematical calculus. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Logico-mathematical_calculus&oldid=47710
This article was adapted from an original article by G.E. Mints (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article