Yury M. Volin
Mountain View, CA, USA.
DOI: 10.4236/apm.2026.161003   PDF    HTML   XML   92 Downloads   343 Views   Citations

Abstract

A system of finitary arithmetic is introduced, and a proof for its consistency is proposed. It is shown that the proof of the consistency of finitary arithmetic, formalized in Peano arithmetic, implies the consistency of Peano arithmetic. Due to the results of the article, Peano arithmetic should be suspected of being inconsistent.

Keywords

Inconsistency and Consistency, Peano Arithmetic, Natural Deduction of Prawitz, Normalization of Natural Deduction, Language , Minimal Arithmetic, Finitary Arithmetic

Share and Cite:

1. Introduction

The fundamental questions of metamathematics are the questions of consistency and completeness of existing axiomatic theories. Among the latter, two stand out: the ZFC theory and Peano arithmetic. In the ZFC theory, practically everything that has been done and is being done in mathematics can be formalized (except for special questions related to “very large sets”, which the majority of mathematicians do not care about). And Peano arithmetic, from certain positions, is the first step in the hierarchy of axiomatic theories, on the basis of which one can obtain deep results. According to Kronecker’s apt remark, natural numbers are created by God; everything else is the work of human hands. By virtue of the generally accepted postulate of mathematical logic, from a contradiction one can (immediately) obtain a deduction of all formulas. Therefore, the question of the consistency of the axiomatic theories used is so important and relevant.

According to two famous theorems of Gödel on incompleteness, retold by many authors (see, for example, [1]-[4]), a consistent axiomatic theory containing arithmetic is incomplete, and its consistency cannot be proved by means formalized in this theory itself. The general opinion of mathematicians now comes down to the fact that Peano arithmetic is certainly consistent (a rare exception is the work [5]), and set theory is almost certainly consistent. This point of view was expressed in the book [2], the authors of which, in my opinion, very successfully, compactly, and clearly, set out the main elements of metamathematics related to its fundamental problems of consistency and completeness of axiomatic theories.

In works [6]-[8], the inconsistency of set theory was demonstrated. In doing so, the prohibitions on the formation of sets that were introduced into set theory to avoid the paradoxes discovered in it at the end of the 19th century were taken into account. Therefore, the proof given in works [6]-[8] implies the inconsistency of the axiomatic theory ZFC.

This paper is devoted to the problem of the consistency of arithmetic. A system of “finitary arithmetic” is introduced, and a proof of its consistency is proposed. It is shown that a proof of the consistency of finitary arithmetic using the resources available to Peano arithmetic implies the consistency of Peano arithmetic, and hence its inconsistency. Therefore, the question arises of whether there is a proof of the consistency of finitary arithmetic that uses resources no more powerful than those of Peano arithmetic. The simplest answer to this question is as follows: any proof of the consistency of finitary arithmetic is not formalizable in Peano arithmetic, because its formalizability implies, by Gödel’s second incompleteness theorem, that Peano arithmetic is inconsistent. But the consistency of Peano arithmetic is a hypothesis (based on intuitive obviousness and long-standing human practice), and not a definitively established fact. At the same time, the finiteness of the set of finite numbers (and the variable in the universal quantifier in finitary arithmetic only ranges over these numbers) makes it possible to prove induction in finitary arithmetic using the means of minimal arithmetic.

Therefore, Peano arithmetic should be suspected of being inconsistent.

The initial developments related to this topic were presented by the author in [9].

2. Some Metamathematics

To make the work of the reader of this article, for whom metamathematics is not a special area of interest, easier, we will provide some general information from the field of metamathematics, contained in the books [1]-[4] and a number of others.

Metamathematics deals with formal objects of three types: formal symbols of some alphabet, formal expressions (each expression consists of a finite number of symbols), and finite sets and sequences of expressions. Formal expressions consist of formulas and terms. Terms denote the mathematical objects being studied (natural numbers, geometric objects, sets, etc.), and formulas denote statements (phrases) about the objects. Formulas may contain variables with respect to which individual formal objects are values. Formulas without free variables are called sentences. Finite sequences of expressions denote deductions of some formulas from others. Metamathematics studies deductions and formulates the corresponding results for various axiomatic theories, setting the task of making its work with the simplest and most generally accepted mathematical tools.

Gödel introduced the numbering of metamathematical objects, assigning each object (symbol, expression, and finite set of expressions) its own number (some natural number). After the introduction of Gödel numbers, the arithmetization of metamathematics occurred: its statements became possible to consider as theorems of arithmetic or as statements about theorems of arithmetic.

Let us give a description of Peano arithmetic in one of the accepted variants (see [2] [3]). We will use the notation Ar for it.

The language of Ar (the language of arithmetic) contains one sort of variables $x,y,z,\cdots$ (with possible indices) running over the natural numbers $0,1,2,\cdots$ , a constant 0 (denoting the natural number 0), one predicate symbol “=”, one unary function symbol $S$ ($Sx$ denotes the number following the number $x$ ), and two binary function symbols to denote the operations of addition and multiplication of natural numbers.

Based on the natural deduction rules of Pravitz (see below), we will also use notations a, b, c, … for the variables.

The terms of Ar are all variables, 0, $Sx$ , $S0$ , $x+y$ , $\cdot y$ , … The terms 0, $S0$ , $SS0$ , … naturally correspond to the natural numbers 0, 1, 2, … They are called numerals and are also written as follows: 0, 1, 2, … The numerals corresponding to the Gödel numbers are called Gödel numerals.

Atomic formulas of Ar have the form ($t=r$ ), where $t,r$ are arbitrary terms of the language.

Non-logical axioms of Ar are divided into four groups.

Axioms of equality:

1) $a=a$ ;

2) $a=b\wedge a=c\to b=c$ .

Successors axioms:

3) $Sa\ne 0$ ;

4) ($Sa=Sb)\leftrightarrow a=b$ .

Axioms of complete mathematical induction:

5) $A\left(0\right)\wedge \forall x\left(A\left(x\right)\to A\left(Sx\right)\right)\to \forall xA\left(x\right)$ where $A$ is an arbitrary formula.

The defining axioms for addition and multiplication:

6) $a+0=a$ ;

7) $a+Sb=S\left(a+b\right)$ ;

8) $a\cdot 0=0$ ;

9) $a\cdot Sb=a\cdot b+a$ .

The order relation between numbers in Peano arithmetic can be introduced using the formula $\exists x\left(Sx+a=b\right)$ : $a<b$ means that $\exists x\left(Sx+a=b\right)$ . But for our purpose, it is more convenient to consider the order relation as one more primary concept consistent with those introduced above. Therefore, we add the following additional axioms: $\neg Sa<0$ , $a<Sb=a<b\vee a=b$ , $a<b\vee a=b\vee b<a$ (see [3]).

When speaking of a theory $T$ , we mean a theory containing Ar, in the narrow or broad sense. The broad sense means that the language of Ar can be interpreted in the language of $T$ so that the formulas and terms of Ar become formulas and terms of $T$ , and all the axioms of Ar turn out to be theorems of $T$ . The theory ZFC is such a theory. Ar, of course, is a special case of $T$ . Every deduction in Ar is simultaneously a deduction in $T$ .

If in $T$ a formula $A$ is deducible from a finite set of formulas Г, then this fact is written as $\text{Г}{⊢}_{T}A$ (for brevity, $\text{Г}⊢A$ may be written, and $T$ may be stipulated or follows from the context). Г is the set of input formulas of the deduction, and $A$ is its output formula. If Г is an empty set, then we speak of a proof of $A$ in the system $T$ and write $⊢A$ or $T⊢A$ .

The introduction of Gödel numbers for the language of arithmetic allows us to interpret some arithmetic formulas as statements about metamathematical objects in the language of arithmetic. Let $\text{P}\left(x_1,\cdots ,x_{\text{m}}\right)$ be an arithmetic predicate that takes the values “true” or “false” depending on the values of the variables $x_1,\cdots ,x_m$ . We say that the arithmetic formula $P\left(x_1,\cdots ,x_m\right)$ numerically expresses the predicate $\text{P}\left(x_1,\cdots ,x_m\right)$ if, for any specific set $\left(n_1,\cdots ,n_m\right)$ of natural numbers, the following holds:

1. If $\text{P}\left(n_1,\cdots ,n_m\right)$ is true, then $\text{Ar}⊢P\left(n_1,\cdots ,n_m\right)$ ;

2. If $\text{P}\left(n_1,\cdots ,n_m\right)$ is a lie, then $\text{Ar}⊢\neg P\left(n_1,\cdots ,n_m\right)$ .

In this case, the predicate $\text{P}\left(x_1,\cdots ,x_m\right)$ is called numerically expressible.

If the predicate $\text{P}\left(x_1,\cdots ,x_m\right)$ had some metamathematical meaning, then it is natural to attribute the same meaning to the formula $P\left(x_1,\cdots ,x_m\right)$ , which numerically expresses it.

An axiomatic system $T$ is inconsistent if for some sentence $A$ it yields a contradiction: $T⊢A\wedge \neg A$ . The theory is incomplete if, for some $A$ , this sentence is neither provable nor refutable (i.e., not provable $\neg A$ ). In this case, we say that proposition $A$ is undecidable.

Metamathematics distinguishes a class of numerically expressible arithmetic predicates. In particular, all so-called primitive recursive arithmetic predicates are such. Let $\text{PRF}\left(y,z\right)$ be a predicate that is true if and only if z is the Gödel number of a proof in Ar of a formula that has Gödel number $y$ . As Gödel showed, this predicate is numerically expressible. Let the arithmetic formula $Prf\left(y,z\right)$ numerically express the predicate $\text{PRF}\left(y,z\right)$ , and $\text{PR}\left(y\right)=\exists z\text{PRF}\left(y,z\right)$ . $\text{PR}\left(y\right)$ is true if and only if the formula with Gödel number y is provable in Ar, and has the meaning of a provability predicate. Define $Pr\left(y\right)=\exists zPrf\left(y,z\right)$ . The formula $Pr\left(n\right)$ is provable when the predicate $\text{PR}\left(n\right)$ is true.

Let $p$ be the Gödel number of the formula $\neg Pr\left(y\right)$ . Then the sentence $\neg Pr\left(p\right)$ can be interpreted as a sentence asserting its own unprovability. Gödel, having constructed the sentence $\neg Pr\left(p\right)$ , proved that $\neg Pr\left(p\right)$ and $Pr\left(p\right)$ are not provable in Ar if Ar is $\omega$ -consistent ($\omega$ -consistency is a property of a system that is as natural as, but stronger than, simple consistency). In other words, the sentence $\neg Pr\left(p\right)$ is neither provable nor refutable, i.e., it is undecidable. This proves the incompleteness of the theory Ar (under the condition of its ω-consistency). Gödel’s first incompleteness theorem is complemented by his second theorem, according to which the consistency of Ar cannot be proven by means formalized in Ar if Ar is consistent.

These results extend naturally to any theory $T$ that contains arithmetic.

3. Natural deduction of Prawitz

In our opinion, natural deduction is a particularly convenient tool for studying deductions in axiomatic systems, having the advantage of visibility over both the direct application of the predicate logical postulates and sequent calculus. Certainly, there can be another point of view, and it is necessary to add that a combination of tools may also prove useful. The author of the article [4] discusses the usefulness of combining natural deduction and the sequent calculus. We use the combination of natural deduction and direct application of the predicate calculus.

Systems of natural deduction and the calculus of sequent were introduced by Gentzen (see [4]).

The fundamental exposition of natural deduction is contained in the classical work of Prawitz [10]. Its peculiarity is the full absence of logical axioms. There are only deduction rules that allow one to prove all known logical axioms. The system of rules of natural deduction is equivalent to the usual predicate calculus, and with the addition of descriptive constants and non-logical axioms, it can be the basis for constructing any axiomatic theory (for example, Peano arithmetic or ZFC set theory). Each deduction can be designed as a natural deduction. The advantage of the rules of natural deduction is their clarity. All of them actually copy the rules used by mathematicians in informal deduction.

Another peculiarity of the Prawitz system is the absence of free variables. All variables $x,y,z$ (with possible indices) are bound, and the individual parameters $a,b,c$ act as free variables. There is a countable set of both in the alphabet of the system. One more peculiarity: the presence of a logical constant for the falsity (absurdity) $\text{Λ}$ and the absence of a symbol for negation. By definition, $\neg A$ is a formula $A\to \text{Λ}$ , and all functions of the symbol $\neg$ are fulfilled.

For the sake of completeness, let us first present the list of postulates (logical axioms and deduction rules) of predicate calculus [1]. For consistency of presentation, individual parameters will be used as free variables, as in natural deduction (Table 1).

Table 1. Logical axioms and deduction rules of predicate calculus.

1a. $A\to \left(B\to A\right)$ (logical axiom)	2. $A,A\to B/B$ (deduction rule)
1b. $\left(A\to B\right)\to \left(\left(A\to \left(B\to C\right)\right)\to \left(A\to C\right)\right)$	4a. $A\wedge B\to A$
3. $A\to \left(B\to A\wedge B\right)$	4b. $A\wedge B\to B$
5a. $A\to A\vee B$	6. $\left(A\to C\right)\to \left(\left(B\to C\right)\to \left(A\vee B\right)\to C\right)$
5b. $B\to A\vee B$
7. $\left(A\to B\right)\to \left(\left(A\to \neg B\right)\to \neg A\right)$	8. $\neg \neg A\to A$
9. $C\to A\left(a\right)/C\to \forall xA\left(x\right)$	10. $\forall xA\left(x\right)\to A\left(t\right)$
11. $A\left(t\right)\to \exists xA\left(x\right)$	12. $A\left(a\right)\to C/\exists xA\left(x\right)\to C$

Constraints: $C$ and $\exists xA\left(x\right)$ do not contain parameter $a$ .

Postulates 1 - 8 are postulates of the propositional calculus, and postulates 9 - 12 are additional postulates of the predicate calculus. Note that axiom 8 is equivalent to the formula $A\vee \neg A$ (expressing the law of excluded middle).

The terms of predicate calculus are (bound) variables and individual parameters.

Every formula derived in predicate calculus is true in any model (under any interpretation of the language in which the formulas of predicate calculus are written). A remarkable property of predicate calculus is that the converse also holds: if a formula is true under any interpretation of the language, then it is derived in predicate calculus. Such formulas are called logical laws. Logical laws are true by virtue of their form, regardless of their content (see, for example, [2]).

Now, we will give a complete list of the rules of natural deduction as it is given by Prawitz [10]. The rules are divided into introduction rules ($I$ -rules) and elimination rules ($E$ -rules) of logical symbols. Rules 1, 3, 5, 7, 9 are introduction rules, and rules 2, 4, 6, 8, 10 are elimination rules. Rule 11 is called the ${\text{Λ}}_I$ -rule, and rule 12 is called the ${\text{Λ}}_C$ -rule.

Table 2. Logical rules of natural deduction.

1. If there are deductions $\text{Г}⊢A$ and $\text{Г}⊢B$ , then there is a deduction Г⊢A∧B. (This rule is related to the deduction step $\left(A,B/A\wedge B\right)$ where $A,B$ are the first and second premisses of the step, and $A\wedge B$ is its consequence; both premisses in this rule are called major). 2. If there is a deduction $\text{Г}⊢A\wedge B$ , then there are deductions $\text{Г}⊢A$ and $\text{Г}⊢B$ ($A\wedge B/A$ and $A\wedge B/B$ ). 3. If there is a deduction $\text{Г}⊢A$ or a deduction $\text{Г}⊢B$ , then there is a deduction $\Gamma ⊢A\vee B$ ($A/A\vee B$ or $B/A\vee B$ ). 4. If there is a deduction $\text{Г}⊢A\vee B$ and there are deductions $\left(\text{Г},A\right)⊢C$ and $\left(\text{Г},B\right)⊢C$ , then there is a deduction $\text{Г}⊢C$ ($A\vee B,C,C/C$ ). 5. If there is a deduction $\left(\text{Г},A\right)⊢B$ , then there is a deduction $\text{Г}⊢A \to B$ ($B/A\to B$ ). 6. If there are deductions $\text{Г}⊢A$ and $\text{Г}⊢A\to B$ , then there is a deduction $\text{Г}⊢B$ ($A,A\to B/B$ , premiss $A$ in this rule is called minor, and premiss $A\to B$ is called major). 7. If there is a deduction $\text{Г}⊢A\left(a\right)$ and the parameter $a$ is not included in any of the unclosed assumptions on which $A\left(a\right)$ depends, then there is a deduction $\text{Г}⊢\forall xA\left(x\right)$ ($A\left(a\right)/\forall xA\left(x\right)$ ). 8. If there is a deduction $\text{Г}⊢\forall xA\left(x\right)$ and $t$ is a term in the language used, then there is a deductioin $\text{Г}⊢A\left(t\right)$ ($\forall xA\left(x\right)/A\left(t\right)$ ). 9. If there is a deduction $\text{Г}⊢A\left(t\right)$ , then there is a deduction $\text{Г}⊢\exists xA\left(x\right)$ ($A\left(t\right)/\exists xA\left(x\right)$ ). 10. If there are deductions $\text{Г}⊢\exists xA\left(x\right)$ and $\left(\text{Г},A\left(a\right)\right)⊢B$ , and the parameter $a$ is not included in the formula $\exists xA\left(x\right)$ , in $B$ and in none of the unclosed assumptions on which $B$ depends, except $A\left(a\right)$ , then there is a deduction $\text{Г}⊢B$ ($\exists xA\left(x\right),B/B$ ). 11. If there is a deduction $\text{Г}⊢\text{Λ}$ , then there is a deduction $\text{Г}⊢A$ (everything follows from a contradiction) ($\text{Λ}/A$ ). 12. If there is a deduction $\left(\text{Г},\neg A\right)⊢\text{Λ}$ , then there is a deduction $\text{Г}⊢A$ ($\text{Λ}/A$ ).

Here $A,B,C$ are formulas, and $\text{Г}$ is a finite set of formulas representing unclosed assumptions. Note that rule 11 follows from rule 12.

The rules of deductions provide a description of what is done at individual steps of the deduction by specifying the premisses, conclusion, and closing assumptions.

The full list of rules applies to the classical system. In the case of the intuitionistic system, rule 12 is missing. Prawitz uses the notations C and I for the classical and intuitionistic systems.

The parameter $a$ in the introduction rule 7 is called the proper parameter of the rule (rule $\forall \text{I}$ ). The same is true for the parameter $a$ in deletion rule 10 (rule $\exists \text{E}$ ).

The deduction is a tree of formulas and consists of steps, where the output formula at a given step is located under the input ones. Formulas and occurrences of formulas should be distinguished (Running ahead, we note that the same applies to sub-deductions of the deduction: the same sub-deduction can have several occurrences in the deduction, as well as to the parameters $a,b,c$ ). An occurrence of a formula in a deduction is a formula plus the place it occupies in the deduction. Following Prawitz, we use the same notations for formulas and occurrences of formulas. The context should always show whether we are talking about a formula $A$ , an occurrence of a formula $A$ , or a set of occurrences of a formula of the form $A$ . At the very bottom of the deduction is the deduced (final) formula, and at the very top are the initial formulas (formulas above which there are no other formulas): assumptions and axioms.

Assumptions are divided into unclosed (hypotheses) and closed. Above, in the deduction rules (see Table 2), to the left of the $⊢$ symbol, unclosed assumptions are indicated (taken for brevity with a possible reserve). Proof is a deduction when, in the end, all assumptions are closed (and therefore $\text{Г}$ is an empty set).

At each step of the deduction, the output formula of the step is derived from the input formulas (premisses) and, possibly, some assumptions are closed (transferred from the category of unclosed to the category of closed). It is said that the occurrence of formula $A$ depends on those assumptions that are above it in the deduction (and only they are significant at this step of the deduction).

Closing assumptions is an important moment in natural deduction. Let us describe it. In rule 5, when passing from $B$ to $A \to B$ , all unclosed assumptions of the form $A$ , on which $B$ depends, are closed (discharged). In rule 12, unclosed assumptions of the form $\neg A$ are closed. In rule 4, assumptions of the form $A$ and $B$ are closed. And in rule 10, assumptions of the form $A\left(a\right)$ are discharged. $\text{Г}$ is a finite set of unclosed assumptions. More precisely, what was said above does not speak about the closure of assumptions, but about the possibility of closing assumptions. Prawitz speaks about closure at the first opportunity and introduces an alternative definition of deduction, when the closure of an assumption can be carried out at any subsequent step of the deduction (Figure 1).

Some rules of natural deduction closely mirror the logical axioms or rules of deduction of predicate calculus. This applies in particular to rule 8 of Table 2 and axiom 10 of Table 1. In other cases, the connection between them may not be immediately obvious. In this regard (and to facilitate the understanding of this article by readers unfamiliar with natural deduction), we present a proof of axiom 1b of Table 1.

Figure 1. Proof of the axiom $\left(A\to B\right)\to \left(\left(A\to \left(B\to C\right)\right)\to \left(A\to C\right)\right)$ using natural deduction.

To prove the inconsistency of a system according to Prawitz means to present a proof whose output is the formula $\text{Λ}$ . As it is easy to see, this is equivalent to proving $A$ and $\neg A$ .

Prawitz introduces the concept of a pure parameter and shows that any deduction can be transformed into a deduction with pure parameters (which makes the deduction simpler and more observable). The latter means that any proper parameter of rule 7 (rule ∀I) or rule 10 (rule ∃E) is a proper parameter of exactly one application of the rule and is distinct from all parameters that are not proper in the deduction. A proper parameter of the application of rule 7 occurs in the deduction only in occurrences of formulas located above the conclusion $\forall xA\left(x\right)$ , and any proper parameter of the application of rule 10 occurs only in deduction formulas located above the premiss $B$ .

We extend this requirement of Prawitz by requiring that in formulas of the form $\forall xA\left(x\right)$ the variables $x$ be distinct.

Let us move on to the key point related to natural deduction, to deduction reductions. A deduction is reduced when the step of introducing a logical symbol is followed by the step of removing. Prawitz describes 5 reductions. Three of them are shown in Figures 2-4 (we will not need the others). On the left is the deduction before the reduction, and on the right is an equivalent, simpler deduction after the reduction. A formula that is an output formula for the introduction step and an input formula for the removal step is called a maximal formula. As a result of the reduction, a part of the general deduction, which is its sub-deduction, is replaced by another sub-deduction (simpler in some respect). Below, ${\Pi }_i$ denotes a sub-deduction. If formula $A$ is below ${\Pi }_i$ , then $A$ is the output formula of the sub-deduction ${\Pi }_i$ , and if it is above ${\Pi }_i$ , then $A$ is the input formula.

$\left(A\right)$ denotes the set of occurrences of formulas of the form $A$ , and $\left({\Pi }_1\right)$ denotes the set of occurrences of sub-deductions of the form ${\Pi }_1$ .

Figure 2. $\wedge$ -reduction ($A\wedge B$ is the maximal formula).

Figure 3. →-reduction ($A\to B$ is the maximal formula).

Figure 4. $\forall$ -reduction ($\forall xA\left(x\right)$ is the maximal formula).

In the case of $\forall$ -reduction, all occurrences of the parameter $a$ in the sub-deduction ${\Pi }_1\left(a\right)$ are replaced by occurrences of the term $t$ .

Normalization of the deduction is the process of successive removal of maximal formulas from it using reductions. If there are no maximal formulas in the deduction, it is called normal. The normalization process is not as simple as it seems at first glance. The fact is that after removing a maximal formula, new ones may appear, and the total number of maximal formulas in the deduction may increase.

Prawitz introduces the system C′ (see [10]). The language of C′ contains only $\text{Λ},\wedge ,\to ,\forall$ as logical constants. The logical constant $\vee$ and the existential quantifier $\exists$ are defined in one of the usual ways. Prawitz proposes to express $A\vee B$ by the formula $\neg A\to B$ , and $\exists xA$ by the formula $\neg \forall x\neg A$ . The system C′ is adequate for the classical system C. Moreover, Prawitz restricts the application of rule 12 to the case where $A$ is an atomic formula and proves that such a restriction does not reduce the generality of the results obtained.

Let us make some useful refinements and modifications to the natural deduction of Prawitz, consistent with its style and intent, and allowing for a more convenient and clear presentation of certain points in the subsequent exposition. We will divide the occurrences of parameters into non-free and free, requiring that the following conditions be satisfied. Every occurrence of a parameter in an axiom is free, and in a hypothesis, non-free. In the case of a formula that is not the initial one, an occurrence of a parameter $a$ in $A\left(a\right)$ will be called non-free if this occurrence depends on an unclosed assumption containing the parameter $a$ . Otherwise, the occurrence will be called free. In steps of the form ($A\left(a\right)/\forall xA\left(x\right)$ ), satisfying rule 7, all occurrences of the parameter $a$ in $A\left(a\right)$ must be free. In the case of a step of the form $\left(\forall xA\left(x\right)/A\left(t\right)\right)$ , all individual parameters occurring in the term $t$ are free.

Prawitz proves that every deduction in the language C′ for natural deduction can be normalized.

Theorem 1. If there is a deduction $\text{Г}⊢A$ in C′, then there is a normal deduction $A$ from $\text{Г}$ with pure parameters.

Following Prawitz, we call the degree of a formula $A$ the number of occurrences of logical constants (except for Λ) in $A$ . The proof is carried out using substantive (informal) inductions. The inductive quantity is the pair $\left(\alpha ,\beta \right)$ , where $\alpha$ is the maximum degree of the maximal formula in the deduction, and $\beta$ is the number of maximal formulas that have the maximum degree. $\left({\alpha }_1,{\beta }_1\right)<\left({\alpha }_2,{\beta }_2\right)$ , if ${\alpha }_1<{\alpha }_2$ or (${\alpha }_1={\alpha }_2$ , ${\beta }_1<{\beta }_2$ ). Prawitz shows that the process of removing maximal formulas can be organized in such a way that at each step of the process, the inductive quantity decreases. Therefore, after a finite number of steps, we obtain a normal deduction equivalent to the original one. Also, Prawitz shows how an arbitrary natural deduction can be transformed into an equivalent deduction with pure parameters. This is done by systematically renaming the parameters. And it is easy to see that if the original deduction was normal, then the resulting one will be normal as well.

Let us take the main branch $\left(A_1,A_2,\cdots ,A_n\right)$ of the deduction П in C′ in the predicate calculus. The main branch is a sequence of occurrences of formulas located in the deduction one under the other, where $A_1$ is an assumption (closed or unclosed), $A_n$ is a final formula of the deduction and $A_i$ can only be a major premiss (thus, in case of step ($A,A\to B/B$ ) $A_i=A\to B$ , but not the formula $A_i=A$ ). It is easy to see that the main branch always exists.

From Theorem 1, the following conclusions can be drawn:

Theorem 2. Let П be a normal deduction in C′ and $\left(A_1,A_2,\cdots ,A_n\right)$ be the main branch of the deduction. Then there exists a formula $A_i$ (called the minimal formula of the branch) that divides the branch into two parts: the deletion part ($E$ -part) and the introduction part ($I$ -part) (one of the parts may be empty), with the following properties:

1) Each formula $A_j$ in the $E$ -part (i.e., $j<i$ ) is a major premiss of the $E$ -rule and contains $A_{j+1}$ as a subformula;

2) $A_i$ , given $i<n$ , is a premiss of the $I$ -rule or the ${\text{Λ}}_C$ -rule;

3) Each formula $A_j$ in the $I$ -part, except for the last one (i.e., $i<j<n$ ), is a premiss of the $I$ -rule and a subformula of $A_{j+1}$ .

From Theorem 2, the following conclusions can be immediately drawn:

Theorem 3. In predicate calculus, the system C′ is consistent.

Prawitz presented the following simple proof. Suppose that Λ is provable in C′ and П is a normal proof of Λ. Let $\left(A_1,A_2,\cdots ,A_n\right)$ be the main branch of the proof. By Theorem 2, the $I$ -part is missing in the main branch. But then $A_1$ is an unclosed assumption (since assumptions are closed only in the $I$ -part), which contradicts the fact that Π is a proof.

We have discussed the issues related to natural deduction of Prawitz in such detail as to enable a greater number of readers to become acquainted with the work, gaining an adequate understanding of its content, difficulties, and results.

4. Deductions in Arithmetic

We will talk further about deductions in arithmetic. In this case, the initial formula in normal deduction can be an axiom.

Let us expand the definition of an arithmetic term by introducing details that take into account the peculiarities of Prawitz’s natural deduction. We will distinguish between the term itself and the term in a formula. A term itself is a finite string of symbols for which the following conditions are satisfied: 1) The constant 0 is a term. 2) Every individual parameter is a term. 3) - 5) If $t,t_1,t_2$ are terms, then $St$ , $t_1+t_2$ and $t_1\cdot t_2$ are also terms. 6) There are no other terms than those defined according to 1 - 5.

This is the usual inductive definition. Individual parameters in a term itself will be called parameters of the term.

In the case of a term in a formula, its parameters can be either individual parameters or variables (which are always bound by a universal quantifier). This is a feature of natural deduction. Note that the transformation of an individual parameter into a bound variable occurs in steps 7 and the induction steps.

A closed term is a term without parameters.

We will call the system Ar without the axioms of induction, minimal arithmetic (see [3]). In minimal arithmetic, it is proved: $a<b\to t\left(a\right)<t\left(b\right)$ where $t$ is a term with one parameter.

Theorems 1 and 2 are formulated and proved without changes.

The existence theorem of normal deduction allows one to prove the consistency of minimal arithmetic almost as easily as the consistency of predicate calculus.

Theorem 4. Minimal arithmetic is consistent.

The only difference between the current situation and the one that took place during the proof of Theorem 3 is that a priori, the initial formula of the main branch $A_1$ can be an axiom. But all axioms of minimal arithmetic are either atomic or have degree 1 or 2 (the degree of a formula is the number of occurrences of logical constants (except for Λ). And it is easy to see that in this case, the contradiction symbol Λ cannot be a minimal formula of the branch. Therefore, minimal arithmetic is consistent.

Let us now take the system Ar in its entirety. We include induction in C′ using one more rule of deduction (the induction rule of deduction), which formalizes the induction step as shown in Figure 5.

Figure 5. Induction step in natural deduction.

The parameter $a$ is not included in any of the unclosed assumptions on which the formula $A\left(a\right)\to A\left(Sa\right)$ depends, and so it is free.

We will call the premiss $A\left(0\right)$ the minor premiss, and the premiss $A\left(a\right)\to A\left(Sa\right)$ the major premiss.

The definition of the main branch of the deduction is preserved (taking into account what was said above).

The parameter $a$ will be called the proper parameter of the induction rule. Thus, we have expanded the concept of a proper parameter. But, since we are now talking about the Ar system based on the C′ language, we have proper parameters of only two types: proper parameters of the $\forall \text{I}$ -rule and proper parameters of the induction rule. Based on the results and comments of the book [10], we can limit our considerations to deductions with pure parameters and assume that the closure of assumptions occurs at the steps immediately preceding steps 7 or the induction steps.

The restriction on the use of the parameter $a$ in the induction rule is that $a$ must be free in $A\left(a\right)\to A\left(Sa\right)$ .

From now on, we will consider only deductions whose parameters are all proper parameters (rule 7 or induction rule). Such deductions as one can easily see are proofs. If $a_i$ is a proper parameter of rule 7 or the induction rule, then its occurrence in the deduction can only take place above the output formula $\forall x\left(A\left(x\right)\right)$ of the corresponding step.

For every closed term $t$ , there is a unique natural number $n$ for which $t=n$ is provable in minimal arithmetic, and for all other $m$ $\neg \left(t=m\right)$ is provable [3].

The value of a closed term $t$ is a natural number $n$ for which $t=n$ is provable in minimal arithmetic. We will assume that the values of the term’s parameters are numerals. And the values of a term with parameters are the values of closed terms after replacing the parameters with their values. So, a term with parameters can have many values. The minimum value of a term with parameters is the value of the closed term obtained if all parameters are replaced by the numeral 0. The minimum value is indeed minimal.

In conclusion to this section, we give a simpler proof of the consistency of predicate calculus and minimal arithmetic, which does not require complete normalization of deductions. In fact, to carry out the proof, we need not the normalization of the entire deduction, but the normalization of one of its main branches. Let there be an arbitrary deduction П and a main branch $\left(A_1,A_2,\cdots ,A_n\right)$ . We will normalize the formulas of the branch, moving from its end to its beginning. Difficulties arise in the case of →-reduction, when some formulas appear above the first formula of the main branch, and so the main branch is extended. Then, having reached $A_1$ , we encounter a situation where the new deduction contains above $A_1$ formulas $\left(B_1,B_2,\cdots ,B_m\right)$ and the process of normalization of the branch formulas must be continued. It is easy to see, however, that the process cannot be infinite, because in the deduction П the set of different sequences of formulas $\left(B_1,B_2,\cdots ,B_m\right)$ , where $B_i$ is above $B_{i+1}$ , is finite. Therefore, after a finite number of reductions, we obtain an equivalent deduction with a normalized main branch.

We will call weak normalization of the deduction the normalization of one of its main branches.

And thus, we have proved the following theorem:

Theorem 5. For any deduction П, there exists an equivalent deduction ${\text{П}}_1$ that is weakly normalized.

Theorem 5 immediately implies the consistency of predicate calculus and minimal arithmetic.

5. Finitary Arithmetic and a Proof of the Consistency of Peano Arithmetic

Now, let us go to the main point of the article: the proof of the consistency of Peano arithmetic.

The proof consists of 5 lemmas.

Let there be a deduction П in Peano arithmetic, $N$ be a fixed natural number, and $N$ be the corresponding numeral.

We introduce a finite rule, which states that for steps of the form $\forall xA\left(x\right)\to A\left(t\right)$ (step 10 in Table 1), the minimum value of the term $t$ must not exceed $N$ .

If the finite rule holds for all deduction steps of the form $\forall xA\left(x\right)\to A\left(t\right)$ , then we say that the deduction satisfies the finite rule with parameter $N$ .

Lemma 1. Let Π be a deduction in Peano arithmetic in language C′. For sufficiently large $N$ , Π satisfies the finite rule with parameter $N$ .

Let us introduce a system of finitary arithmetic. Finitary arithmetic differs from Peano arithmetic in the following way. A natural number $N$ is introduced and fixed ($N$ is a parameter of the system). All natural numbers not exceeding $N$ (and only they) are considered as finite numbers. Thus, in finitary arithmetic, there are two types of objects: natural numbers and finite numbers. Each finite number is also a natural number, but not vice versa. All the axioms of Peano arithmetic, with the exception of the axioms of mathematical induction, are preserved without adaptation. In formulas of the form $\forall xA\left(x\right)$ , the variable $x$ runs over finite numbers (not over all natural numbers). Thus, in finitary arithmetic (unlike Peano arithmetic), infinity is present as potential, not as actual.

For an analogy, we point to the Neumann-Bernays set system [11], which Gödel used to prove the compatibility of the generalized continuum hypothesis and the axiom of choice with other axioms of set theory (this theory is equivalent to ZF theory). In the Neumann-Bernays theory, there are two types of objects: sets and classes. Each set is a class, but the converse may not hold. In the expression $\forall xA\left(x\right)$ , $x$ is a set and one of the axioms is formulated (verbally) as follows: if $\forall xA\left(x\right)$ holds and $a$ is a set, then $A\left(a\right)$ holds.

For greater clarity and unambiguous understanding, we add the following. The alphabet C′ is extended by adding the symbol $N$ . The terms of finitary arithmetic are all the terms of Peano arithmetic with the addition of the term $N$ . The postulates of finitary arithmetic are, firstly, all the postulates of Peano arithmetic, except for the axioms of induction, rule 9, and axiom 10 (see section 2 and Table 1 in section 3). An axiom is added: $N=S\cdots S0$ ($S$ is repeated $N$ times, where $N$ is a fixed natural number). The old axioms of induction and postulates 9, 10 of Table 1 are replaced by new ones in which the variable $x$ ranges over finite numbers (i.e., natural numbers that do not exceed $N$ ). Axiom 10 of Table 1 will now look like this: $\forall xA\left(x\right)\to A\left(t\right)$ , if $t\le N$ .

Let us clarify the last sentence. Let the term $t\left(n_1,\cdots ,n_p\right)$ be closed for the set of numerals $\left(n_1,\cdots ,n_p\right)$ , and $t\left(n_1,\cdots ,n_p\right)\le N$ . In this case, we say that $\left(n_1,\cdots ,n_p\right)$ is an admissible set of numerals. Axiom 10 of Table 1 in finitary arithmetic is formulated as follows: if $\left(n_1,\cdots ,n_p\right)$ is an admissible set of numerals for the term $t$ , then $\forall xA\left(x\right)\to A\left(t\left(n_1,\cdots ,n_p\right)\right)$ . In this form, the new axiom 10 actually copies the previous one, differing from it only in what is understood by an admissible set of numerals. In Peano arithmetic, any set $\left(n_1,\cdots ,n_p\right)$ for which the term $t\left(n_1,\cdots ,n_p\right)$ became closed was admissible. In finitary arithmetic, the admissible sets are narrowed, but all conclusions remain correct as long as the admissible sets are not empty.

Lemma 2. The set of admissible numerals for term $t$ is non-empty if and only if $t\left(0,\cdots ,0\right)\le N$ .

The result follows from the fact that the value of the term $t\left(0,\cdots ,0\right)$ is the minimum among the values of the term $t\left(a_1,\cdots ,a_p\right)$ .

Let us introduce a list of all its parameters for the deduction П: $\left(a_1,\cdots ,a_M\right)$ , and we will write each term $t$ as follows: $t=t\left(a_1,\cdots ,a_M\right)$ (with obvious consideration of only those $a_i$ on which $t$ actually depends). Let Ω be the set of sets of numerals $\left(n_1,\cdots ,n_M\right)$ that are admissible for each term $t$ in the deduction Π. It follows from Lemma 2 that Ω is non-empty if and only if $t\left(0,\cdots ,0\right)\le N$ for every term $t$ in the deduction.

It should be noted that finitary arithmetic is not uniquely defined, but rather up to the value of a chosen and fixed parameter $N$ .

It should also be noted that, unlike standard finite models of arithmetic, in finitary arithmetic, there are infinitely many objects (natural numbers), and it is potentially infinite, while finite models of arithmetic are both actually and potentially finite.

Lemma 3. Finitary arithmetic is consistent.

Let us consider a deduction П with parameter $N$ in finitary arithmetic and show that this deduction can be interpreted as a deduction in minimal arithmetic. Indeed, let $\forall xA\left(x\right)$ be a subformula of a formula $F$ of finitary arithmetic. We replace it with the subformula $\forall x\left(x\le N\to A\left(x\right)\right)$ . By performing this operation on all subformulas $\forall xA\left(x\right)$ , we obtain an interpretation of $F$ in minimal arithmetic, which we denote $\tilde{F}$ . We perform this interpretation for all formulas of finitary arithmetic.

It is easy to see that all formula-interpretations satisfy the logical postulates in Table 1. It is also easy to see that the interpretations of all axioms of finitary arithmetic, except for the axioms of induction, are provable in minimal arithmetic.

Consider the induction axiom $F=A\left(0\right)\wedge \forall x\left(A\left(x\right)\to A\left(Sx\right)\right)\to \forall xA\left(x\right)$ of finitary arithmetic. It will be interpreted by the formula $\tilde{F}=\tilde{A}\left(0\right)\wedge \forall x\left(x\le N\to \left(\tilde{A}\left(x\right)\to \tilde{A}\left(Sx\right)\right)\right)\to \forall x\left(x\le N\to \tilde{A}\left(x\right)\right)$ . Let $\tilde{A}\left(0\right)$ and $\forall x\left(x\le N\to \left(\tilde{A}\left(x\right)\to \tilde{A}\left(Sx\right)\right)\right)$ be provable in minimal arithmetic. Then, obviously, $\tilde{A}\left(1\right),\cdots ,\tilde{A}\left(N\right)$ and the formula $\forall x\left(x\le N\to \tilde{A}\left(x\right)\right)$ are provable (see [3]). Thus, under our interpretation, all formulas provable in finitary arithmetic are also provable in minimal arithmetic. Therefore, finitary arithmetic is consistent.

Lemma 4. Let П be a deduction in Peano arithmetic with language C′ and a final formula $B$ , satisfying the finitary rule with some parameter $N$ . This deduction induces a deduction of $B$ in finitary arithmetic with parameter $N$ .

Let us consider П as a deduction written in the formalism of natural deduction. We recall that we assume (and this is quite justified) that each parameter in the deduction is a proper parameter of a single application of rule 7 of Table 2 or the induction rule. All steps of П, except for the steps of the form $\forall xA\left(x\right)/A\left(t\right)$ related to rule 8 of Table 2, can obviously also be considered as steps of a deduction in finitary arithmetic. If the finite rule is satisfied, then the set Ω is non-empty, and steps of the form $\forall xA\left(x\right)/A\left(t\right)$ can also be considered as deduction steps in finitary arithmetic. Thus, the deduction Π of $B$ in Peano arithmetic induces a deduction in finitary arithmetic.

Lemma 5. Peano arithmetic is consistent.

Let us proceed as follows. Assume that Peano arithmetic is inconsistent and П is a proof of its inconsistency with output formula Λ. Using Lemmas 1-4, we obtain a deduction of Λ in finitary arithmetic with some parameter $N$ . But finitary arithmetic is always consistent, and we arrive at a contradiction with the assumption made.

If the proof presented above can be formalized in Ar, then, according to Gödel’s second incompleteness theorem, Peano arithmetic would turn out to be inconsistent.

6. Conclusion

The results obtained in this article show that if the consistency of finitary arithmetic can be proven for all values of the parameter $N$ using means formalized in Peano arithmetic, then this implies the inconsistency of Peano arithmetic. The number of finite numbers is finite, and the variable $x$ in formulas of the form $\forall xA\left(x\right)$ ranges only over these numbers, which makes induction provable in finitary arithmetic using the means of minimal arithmetic. Moreover, all the metamathematics used in proving Lemmas 1 - 5 look elementary. Therefore, Peano arithmetic should be strongly suspected of being inconsistent.

Conflicts of Interest

The author declares no conflicts of interest regarding the publication of this paper.

References

[1]	Kleene, S.C. (1952) Introduction to Metamathematics. American Elsevier Publishing Company, Inc.
[2]	Kolmogorov, A.N. and Dragalin, A.G. (2004) Mathematical Logic. URSS. (In Russian)
[3]	Boolos, G.S., Burgess, J.P. and Jeffrey, R.C. (2006) Computability and Logic. Cambridge University Press.[CrossRef]
[4]	Girard, J.-Y. (1987) Proof Theory and Logical Complexity. Bibliopolis.
[5]	Davis, D. (2005) Wither Mathematics? Notices of the AMS, 52, 1350-1356.
[6]	Volin, Y.M. (2023) About the Strange Tree Paradox and Possible Inconsistency of Set Theory. Advances in Pure Mathematics, 13, 694-713.[CrossRef]
[7]	Volin, Y.M. (2024) On the Proof of the Contradiction of Set Theory. Advances in Pure Mathematics, 14, 139-159.[CrossRef]
[8]	Volin, Y.M. (2024) Completion of the Proof of the Contradiction of Set Theory. Advances in Pure Mathematics, 14, 807-816.[CrossRef]
[9]	Volin, Y.M. (2015) On Normal Inference in Arithmetic and the Problem of Consistency. Actual Problems of Contemporary Science, No. 3, pp. 181-2009; No. 6, 146-159. (In Russian)
[10]	Prawitz, D. (2006) Natural Deduction. Dover Publications, Inc.
[11]	Hao, V. and McNaughton, R. (1953) Les systemes axiomatiquies de la theorie des ensembles. Gauthler-Villars.