| Summary: | The increasing use of artificial intelligence algorithms, smart contracts, the internet of things, cryptocurrencies, and digital money highlights the need for secure and sustainable decentralized solutions. Currently, the blockchain technology serves as the backbone for most decentralized systems. However, the question of axiomatization of the blockchain theory in the first-order logic has been open until today, despite the efficient computational implementations of these systems. This did not allow one to formalize the blockchain structure, as well as to model and verify it using logical methods. This work introduces a finitely axiomatizable blockchain theory <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mi mathvariant="double-struck">T</mi></semantics></math></inline-formula> that defines a class of blockchain structures <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mi mathvariant="double-struck">K</mi></semantics></math></inline-formula> using the axioms of the first-order logic. The models of the theory <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mi mathvariant="double-struck">T</mi></semantics></math></inline-formula> are well-known blockchain implementations with the proof of work consensus algorithm, including Bitcoin, Ethereum (PoW version), Ethereum Classic, and some others. By utilizing mathematical logic, we can study these models and derive new theorems of the theory <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mi mathvariant="double-struck">T</mi></semantics></math></inline-formula> through automatic proofs. Also, the axiomatization of blockchain opens up new opportunities to develop blockchain-based systems that can help solve some of the open problems in the fields of artificial intelligence, robotics, cryptocurrencies, etc.
|
|---|