arXiv subjects

Farida Kachapova

Publications and source records attributed to Farida Kachapova.

7 recordsLinked to original sources

arXiv2022

Formalizing Elements of Probabilistic Mechanics

In this paper we create a model of particle motion on a three-dimensional lattice using discrete random walk with small steps. We rigorously construct a probability space of the particle trajectories. Unlike deterministic approach in classical mechanics, here we use probabilistic properties of particle movement to formally derive analogues of Newton's first and second laws of motion. Similar probabilistic models can potentially be applied to justify laws of thermodynamics in a consistent manner.

math.PR↗

arXiv2021

Formalizing groups in type theory

In this paper we formalize some foundation concepts and theorems of group theory in a variant of type theory called the Calculus of Constructions with Definitions. In this theory we introduce definition of a group, which is both general and simple enough to use in formal proofs. Based on this definition, we formalize the concepts of subgroup, coset, conjugate, normal subgroup, and quotient group, and formally derive some related theorems. We aim to keep these formalizations transparent and concise, and as close as possible to the standard mathematical theory. The results can be implemented in proof assistants that are based on calculus of constructions.

math.LO↗

arXiv2021

Formalizing relations in type theory

Type theory plays an important role in foundations of mathematics as a framework for formalizing mathematics and a base for proof assistants providing semi-automatic proof checking and construction. Derivation of each theorem in type theory results in a formal term encapsulating the whole proof process. In this paper we use a variant of type theory, namely the Calculus of Constructions with Definitions, to formalize the standard theory of binary relations. This includes basic operations on relations, criteria for special properties of relations, invariance of these properties under the basic operations, equivalence relation, well-ordering, and transfinite induction. Definitions and proofs are presented as flag-style derivations.

math.LO↗

arXiv2018

Alternative proof of existence of Gibbs measure at high temperature

Mathematical models in equilibrium statistical mechanics describe physical systems with many particles interacting with an external force and with one another. Gibbs measure is a fundamental concept in this theory. In existing literature infinite-volume models are constructed as limits of finite models and existence of Gibbs measure for them is proven through DLR formalism. The general existence proofs are quite complicated and involve topology and cluster expansion. In this paper we develop a more transparent and more constructive proof of existence of infinite Gibbs measure for a particular case of interaction model at high temperature. The proof is based on a limiting procedure and involves estimates of series of semi-invariants and graph-related estimates.

math.PR↗

arXiv2015

Comparison of constructive multi-typed theory with subsystems of second order arithmetic

This paper describes an axiomatic theory BT for constructive mathematics. BT has a predicative comprehension axiom for a countable number of set types and usual combinatorial operations. BT has intuitionistic logic, is consistent with classical logic and has such constructive features as consistency with formal Church thesis, and existence and disjunction properties. BT is mutually interpretable with a so called theory of arithmetical truth PATr and with a second-order arithmetic SA that contains infinitely many sorts of sets of natural numbers. We compare BT with some standard second-order arithmetics and investigate the proof-theoretical strengths of fragments of BT, PATr and SA.

math.LO↗

arXiv2015

Application of semi-invariants to proof of the central limit theorem on a lattice

Statistical mechanics describes interaction between particles of a physical system. Particle properties of the system can be modelled with a random field on a lattice and studied at different distance scales using renormalization group transformation. Here we consider a thermodynamic limit of Ising model with weak interaction and we use semi-invariants to prove that a random field transformed by renormalization group converges in distribution to an independent field with Gaussian distribution as the distance scale infinitely increases; it is a generalization of the central limit theorem to the Ising model.

math.PR↗

arXiv2014

A strong intuitionistic theory of functionals

In this paper we construct a Beth model for intuitionistic functionals of high types and use it to create a relatively strong theory SLP containg intuitionistic principles for functionals, in particular, the theory of the "creating subject", axioms for lawless functionals and some versions of choice axioms. We prove that the intuitionistic theory SLP is equiconsistent with a classical typed set theory TI, where the comprehension axiom for sets of type n is restricted to formulas with no parameters of types > n. We show that each fragment of SLP with types <= s is equiconsistent with the corresponding fragment of TI and that it is stronger than the previous fragment of SLP. Thus, both SLP and TI are much stronger than the second order arithmetic. By constructing the intuitionistic theory SLP and interpreting in it the classical set theory TI, we contribute to the program of justifying classical mathematics from the intuitionistic point of view.

math.LO↗