Namespaces
Variants
Actions

Difference between revisions of "Finitary verifiability"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
m (tex encoded by computer)
 
Line 1: Line 1:
 +
<!--
 +
f0402101.png
 +
$#A+1 = 91 n = 0
 +
$#C+1 = 91 : ~/encyclopedia/old_files/data/F040/F.0400210 Finitary verifiability
 +
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}}
 +
 
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.
 
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 [[#References|[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:
 
Kolmogorov [[#References|[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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f0402101.png" /> that satisfy <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f0402102.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f0402103.png" />;
+
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|Fermat great theorem]] is false;
 
2) to prove that the [[Fermat great theorem|Fermat great theorem]] is false;
  
3) on the assumption that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f0402104.png" /> can be expressed in the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f0402105.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f0402106.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f0402107.png" /> are integers, to find a similar expression for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f0402108.png" />.
+
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f0402109.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021010.png" /> are problems, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021011.png" /> denotes the problem  "solve both the problems A and B" ; <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021012.png" /> denotes  "solve at least one of A or B" ; <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021013.png" /> denotes  "assuming that a solution of A is given, find a solution of B (that is, reduce B to A)" ; <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021014.png" /> denotes  "assuming that a solution of A is given, arrive at a contradiction" .
+
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021015.png" /> by means of the logical connectives <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021016.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021017.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021018.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021019.png" />, 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021020.png" />, which expresses the classical [[Law of the excluded middle|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.
+
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|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 .
 
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021021.png" /> of admissible possibilities that are known beforehand. So, a finitary problem can be regarded as an ordered pair <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021022.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021023.png" /> is the finite set of admissible possibilities for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021024.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021025.png" /> is the set of solutions <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021026.png" />. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021027.png" />, one writes <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021028.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021029.png" />. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021030.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021031.png" /> be arbitrary finitary problems with
+
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
  
<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/f/f040/f040210/f04021032.png" /></td> </tr></table>
+
$$
 +
\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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021033.png" /> one sets
+
Operations on finitary problems are defined as follows. For the conjunction $  \mathfrak A = \mathfrak A _ {1} \& \mathfrak A _ {2} $
 +
one sets
  
<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/f/f040/f040210/f04021034.png" /></td> </tr></table>
+
$$
 +
\phi ( \mathfrak A )  = \
 +
F _ {1} \times F _ {2} ,\ \
 +
\chi ( \mathfrak A )  = \
 +
X _ {1} \times X _ {2} ,
 +
$$
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021035.png" /> denotes the Cartesian product of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021036.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021037.png" />, that is, the set of all ordered pairs <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021038.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021039.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021040.png" />. For the disjunction <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021041.png" /> one sets
+
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
  
<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/f/f040/f040210/f04021042.png" /></td> </tr></table>
+
$$
 +
\phi ( \mathfrak A )  = \
 +
F _ {1} + F _ {2} ,\ \
 +
\chi ( \mathfrak A )  = \
 +
X _ {1} + X _ {2} ,
 +
$$
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021043.png" /> denotes the disjunctive union of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021044.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021045.png" />, that is, the set-theoretic union of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021046.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021047.png" />. For the implication <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021048.png" /> one sets <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021049.png" /> — the set of all mappings of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021050.png" /> to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021051.png" />, and one lets <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021052.png" /> be the set of those <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021053.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021054.png" /> for which <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021055.png" />. The negation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021056.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021057.png" /> is defined as the problem <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021058.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021059.png" /> 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).
+
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021060.png" /> for the variables <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021061.png" /> in a propositional formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021062.png" />, one obtains a composite problem <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021063.png" />. Here <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021064.png" /> is determined only by the sets <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021065.png" /> and does not depend on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021066.png" />. For fixed sets <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021067.png" />, the choice of different sets <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021068.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021069.png" />, will correspond to different problems <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021070.png" /> with the same set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021071.png" /> and, generally speaking, different sets <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021072.png" />. If there is an element of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021073.png" /> belonging to all such <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021074.png" />, then one says that the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021075.png" /> is solvable on the system of sets <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021076.png" />. If the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021077.png" /> is solvable on every system of finite sets <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021078.png" />, then it is called generally solvable or finitarily verifiable. This definition has a transparent meaning: A formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021079.png" /> is finitarily verifiable if one can solve every problem <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021080.png" /> if one knows just the sets of admissible solutions of the problems <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021081.png" />.
+
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021082.png" /> 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, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021083.png" /> 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, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021084.png" />). The Medvedev logic has the disjunctive property: If a formula of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021085.png" /> is finitarily verifiable, then at least one of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021086.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021087.png" /> is finitarily verifiable. If a propositional formula does not contain any of the logical symbols <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021088.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021089.png" /> or <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021090.png" />, 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/f/f040/f040210/f04021091.png" /> 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.
+
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====
 
====References====
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  A. Kolmogorov,  "Zur Deutung der intuitionistischen Logik"  ''Math. Z.'' , '''35'''  (1932)  pp. 58–65</TD></TR><TR><TD valign="top">[2a]</TD> <TD valign="top">  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</TD></TR><TR><TD valign="top">[2b]</TD> <TD valign="top">  Yu.T. Medvedev,  "Finite problems"  ''Soviet Math. Dokl.'' , '''3'''  (1962)  pp. 227–230  ''Dokl. Akad. Nauk SSSR'' , '''169''' :  1  (1966)  pp. 20–23</TD></TR></table>
 
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  A. Kolmogorov,  "Zur Deutung der intuitionistischen Logik"  ''Math. Z.'' , '''35'''  (1932)  pp. 58–65</TD></TR><TR><TD valign="top">[2a]</TD> <TD valign="top">  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</TD></TR><TR><TD valign="top">[2b]</TD> <TD valign="top">  Yu.T. Medvedev,  "Finite problems"  ''Soviet Math. Dokl.'' , '''3'''  (1962)  pp. 227–230  ''Dokl. Akad. Nauk SSSR'' , '''169''' :  1  (1966)  pp. 20–23</TD></TR></table>

Latest revision as of 19:39, 5 June 2020


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
How to Cite This Entry:
Finitary verifiability. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Finitary_verifiability&oldid=46923
This article was adapted from an original article by V.E. Plisko (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article