Finitary verifiability

One of the non-classical interpretations of logical formulas proposed with the aim of making precise the program suggested by A.N. Kolmogorov of interpreting statements of intuitionistic logic as a calculus of problems.

Kolmogorov [1] expressed the idea that as well as traditional logic, which systematizes a scheme of proofs of theoretical truths, there is also possible a logic systematization of a scheme of solutions of problems. Without making the concept of a problem precise, one can still look at some concrete problems, for example:

1) to find four natural numbers $ x, y, z, n $ that satisfy $ x ^ {n} + y ^ {n} = z ^ {n} $, $ n > 2 $;

2) to prove that the Fermat great theorem is false;

3) on the assumption that $ \pi $ can be expressed in the form $ \pi = m/n $, where $ m $ and $ n $ are integers, to find a similar expression for $ e $.

One can also define in a natural way the following operations on problems. If $ \mathfrak A $ and $ \mathfrak B $ are problems, then $ \mathfrak A \& \mathfrak B $ denotes the problem "solve both the problems A and B" ; $ \mathfrak A \lor \mathfrak B $ denotes "solve at least one of A or B" ; $ \mathfrak A \supset \mathfrak B $ denotes "assuming that a solution of A is given, find a solution of B (that is, reduce B to A)" ; $ \neg \mathfrak A $ denotes "assuming that a solution of A is given, arrive at a contradiction" .

If one substitutes any problems for the variables in a propositional formula constructed from variables $ a, b \dots $ by means of the logical connectives $ \& $, $ \lor $, $ \supset $, $ \neg $, then in accordance with the operations indicated one obtains some problem. A formula is called verifiable if there is a general method enabling one to solve any problem obtained in this way from the given formula. All formulas that are derivable in intuitionistic propositional calculus turn out to be verifiable in this sense. At the same time the formula $ A \lor \neg A $, which expresses the classical law of the excluded middle, cannot be verifiable, since if it were, that would mean that there would be a general method making it possible to obtain for every problem either a solution of it or a way of leading to a contradiction from the assumption that there is a solution of it.

This description of the interpretation of logical formulas is not sufficiently strict, and such concepts as a "problem" , a "solution of a problem" and a "general method" need to be made precise. One way of doing so is the concept of finitary verifiability, proposed by Yu.T. Medvedev .

A finitary problem is a problem with as solution an element of some non-empty finite collection $ F $ of admissible possibilities that are known beforehand. So, a finitary problem can be regarded as an ordered pair $ \mathfrak A = \langle F, X\rangle $, where $ F $ is the finite set of admissible possibilities for $ \mathfrak A $ and $ X $ is the set of solutions $ ( X \subseteq F ) $. If $ \mathfrak A = \langle F, X\rangle $, one writes $ F = \phi ( \mathfrak A ) $, $ X = \chi ( \mathfrak A ) $. Let $ \mathfrak A _ {1} $ and $ \mathfrak A _ {2} $ be arbitrary finitary problems with

$$ \phi ( \mathfrak A _ {i} ) = \ F _ {i} ,\ \ \chi ( \mathfrak A _ {i} ) = \ X _ {i} ,\ \ i = 1, 2. $$

Operations on finitary problems are defined as follows. For the conjunction $ \mathfrak A = \mathfrak A _ {1} \& \mathfrak A _ {2} $ one sets

$$ \phi ( \mathfrak A ) = \ F _ {1} \times F _ {2} ,\ \ \chi ( \mathfrak A ) = \ X _ {1} \times X _ {2} , $$

where $ A \times B $ denotes the Cartesian product of $ A $ and $ B $, that is, the set of all ordered pairs $ \langle a, b\rangle $, $ a \in A $, $ b \in B $. For the disjunction $ \mathfrak A = \mathfrak A _ {1} \lor \mathfrak A _ {2} $ one sets

$$ \phi ( \mathfrak A ) = \ F _ {1} + F _ {2} ,\ \ \chi ( \mathfrak A ) = \ X _ {1} + X _ {2} , $$

where $ A + B $ denotes the disjunctive union of $ A $ and $ B $, that is, the set-theoretic union of $ A \times \{ 1 \} $ and $ B \times \{ 2 \} $. For the implication $ \mathfrak A = \mathfrak A _ {1} \supset \mathfrak A _ {2} $ one sets $ \phi ( \mathfrak A ) = F _ {2} ^ { F _ {1} } $— the set of all mappings of $ F _ {1} $ to $ F _ {2} $, and one lets $ \chi ( \mathfrak A ) $ be the set of those $ f $ in $ F _ {2} ^ { F _ {1} } $ for which $ f ( X _ {1} ) \subseteq X _ {2} $. The negation $ \neg \mathfrak A $ of $ \mathfrak A $ is defined as the problem $ \mathfrak A \supset \mathfrak A _ {0} $, where $ \mathfrak A _ {0} $ is a fixed problem with an empty solution set (all the constructions from now on are independent of the concrete choice of such a problem).

Substituting finitary problems $ \mathfrak A _ {1} \dots \mathfrak A _ {n} $ for the variables $ p _ {1} \dots p _ {n} $ in a propositional formula $ A ( p _ {1} \dots p _ {n} ) $, one obtains a composite problem $ \mathfrak A = A ( \mathfrak A _ {1} \dots \mathfrak A _ {n} ) $. Here $ \phi ( \mathfrak A ) $ is determined only by the sets $ F _ {1} = \phi ( \mathfrak A _ {1} ) \dots F _ {n} = \phi ( \mathfrak A _ {n} ) $ and does not depend on $ X _ {1} = \chi ( \mathfrak A _ {1} ) \dots X _ {n} = \chi ( \mathfrak A _ {n} ) $. For fixed sets $ F _ {1} \dots F _ {n} $, the choice of different sets $ X _ {i} \subseteq F _ {i} $, $ i = 1 \dots n $, will correspond to different problems $ A ( \mathfrak A _ {1} \dots \mathfrak A _ {n} ) $ with the same set $ F $ and, generally speaking, different sets $ X $. If there is an element of $ F $ belonging to all such $ X $, then one says that the formula $ A $ is solvable on the system of sets $ F _ {1} \dots F _ {n} $. If the formula $ A ( p _ {1} \dots p _ {n} ) $ is solvable on every system of finite sets $ F _ {1} \dots F _ {n} $, then it is called generally solvable or finitarily verifiable. This definition has a transparent meaning: A formula $ A $ is finitarily verifiable if one can solve every problem $ A ( \mathfrak A _ {1} \dots \mathfrak A _ {n} ) $ if one knows just the sets of admissible solutions of the problems $ \mathfrak A _ {1} \dots \mathfrak A _ {n} $.

The set $ ML $ of all finitarily-verifiable propositional formulas is closed relative to derivability in intuitionistic propositional calculus, and contains all formulas that are derivable in that calculus. Thus, $ ML $ is an intermediate (or super-intuitionistic, or super-constructive) logic, called the Medvedev logic. This logic contains formulas that are not derivable in intuitionistic logic (such as, for example, $ (\neg a \supset ( b \lor c)) \supset ((\neg a \supset b) \lor (\neg a \supset c)) $). The Medvedev logic has the disjunctive property: If a formula of the form $ A \lor B $ is finitarily verifiable, then at least one of $ A $ and $ B $ is finitarily verifiable. If a propositional formula does not contain any of the logical symbols $ \neg $, $ \lor $ or $ \supset $, then it is finitarily verifiable if and only if it is derivable in intuitionistic propositional calculus. All finitarily-verifiable formulas are derivable in classical propositional calculus; at the same time, for example, the classically-derivable formula $ a \lor \neg a $ is not finitarily verifiable. Characterizations of the Medvedev logic in terms of algebraic models have been obtained. The concept of finitary verifiability can be extended in various ways to predicate formulas.

References

[1]	A. Kolmogorov, "Zur Deutung der intuitionistischen Logik" Math. Z. , 35 (1932) pp. 58–65
[2a]	Yu.T. Medvedev, "Interpretation of logical formulas by means of finite problems" Soviet Math. Dokl. , 7 : 4 (1966) pp. 857–860 Dokl. Akad. Nauk SSSR , 142 : 5 (1962) pp. 1015–1018
[2b]	Yu.T. Medvedev, "Finite problems" Soviet Math. Dokl. , 3 (1962) pp. 227–230 Dokl. Akad. Nauk SSSR , 169 : 1 (1966) pp. 20–23