View source for Logico-mathematical calculus

<!--
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''

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

$$ 
\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|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,  $  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|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|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 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|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====
<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====
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====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  S.C. Kleene,   "Mathematical logic" , Wiley  (1967)</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  C.C. Chang,   H.J. Keisler,   "Model theory" , North-Holland  (1973)</TD></TR></table>