Extensive Definition
In mathematics or logic, a finitary operation is
one, like those of arithmetic, that takes a
finite number of input values to produce an output. An operation
such as taking an integral of a function,
in calculus, is defined
in such a way as to depend on all the values of the function
(infinitely many of them, in general), and is so not prima facie
finitary. In the logic proposed for quantum
mechanics, depending on the use of subspaces of Hilbert
space as propositions, operations
such as taking the intersection
of subspaces are used; this in general cannot be considered a
finitary operation. What fails to be finitary can be called
infinitary.
A finitary argument is one which can be
translated into a finite set of
symbolic propositions starting from a finite set of axioms. In other words, it is a
proof
that can be written on a large enough sheet of paper (including all
assumptions).
The emphasis on finitary methods has historical
roots. Infinitary
logic studies logics that allow infinitely long statements and proofs. In such a logic, one can
regard the existential
quantifier, for instance, as derived from an infinitary
disjunction.
In the early 20th
century, logicians
aimed to solve the problem
of foundations; that is, answer the question: "What is the true
base of mathematics?" The program was to be able to rewrite all
mathematics starting using an entirely syntactical language without
semantics. In the words of David
Hilbert (referring to geometry), "it does not matter
if we call the things chairs, tables and beer mugs or points, lines
and planes."
The stress on finiteness came from the idea that
human mathematical thought is based on a finite number of
principles and all the reasonings follow essentially one rule: the
modus
ponens. The project was to fix a finite number of symbols
(essentially the numerals 1,2,3,... the letters
of alphabet and some special symbols like "+", "->", "(", ")",
etc.), give a finite number of propositions expressed in those
symbols, which were to be taken as "foundations" (the axioms), and
some rules of
inference which would model the way humans make conclusions.
From these, regardless of the semantic interpretation of the
symbols the remaining theorems should follow formally using only
the stated rules (which make mathematics look like a game with
symbols more than a science) without the need to rely on ingenuity.
The hope was to prove that from these axioms and rules all the
theorems of mathematics could be deduced.
The aim itself was proved impossible by Kurt
Gödel in 1931, with his
Incompleteness Theorem, but the general mathematical trend is
to use a finitary approach, arguing that this avoids considering
mathematical objects that cannot be fully defined.