### Lower and upper bounds for the provability of Herbrand consistency in weak arithmetics

We prove that for i ≥ 1, the arithmetic $I\Delta \u2080+{\Omega}_{i}$ does not prove a variant of its own Herbrand consistency restricted to the terms of depth in $(1+\epsilon )lo{g}^{i+2}$, where ε is an arbitrarily small constant greater than zero. On the other hand, the provability holds for the set of terms of depths in $lo{g}^{i+3}$.

### On rational solution of the state equation of a finite automaton.

### Sequent Calculus, Derivability, Provability. Gödel's Completeness Theorem

Fifth of a series of articles laying down the bases for classical first order model theory. This paper presents multiple themes: first it introduces sequents, rules and sets of rules for a first order language L as L-dependent types. Then defines derivability and provability according to a set of rules, and gives several technical lemmas binding all those concepts. Following that, it introduces a fixed set D of derivation rules, and proceeds to convert them to Mizar functorial cluster registrations...

### Subalgebras of diagonalizable algebras of theories containing arithmetic [Book]

### The Gödel Completeness Theorem for Uncountable Languages

This article is the second in a series of two Mizar articles constituting a formal proof of the Gödel Completeness theorem [15] for uncountably large languages. We follow the proof given in [16]. The present article contains the techniques required to expand a theory such that the expanded theory contains witnesses and is negation faithful. Then the completeness theorem follows immediately.

### Transition of Consistency and Satisfiability under Language Extensions

This article is the first in a series of two Mizar articles constituting a formal proof of the Gödel Completeness theorem [17] for uncountably large languages. We follow the proof given in [18]. The present article contains the techniques required to expand formal languages. We prove that consistent or satisfiable theories retain these properties under changes to the language they are formulated in.

### Континуум нормальных расширений модальной логики доказуемости с интерполяционным свойством.

### Неразрешимые свойства расширений логики доказуемости. II

### О двух расширениях логики доказуемости GL