Ilango (FOCS 2025) invented effectively zero-knowledge proofs, a new variant of zero-knowledge. We reformulate it in the language of logic and give simple proofs (under the same assumptions as Ilango (FOCS 2025)) of its existence and of the key property defined in Ilango (FOCS 2025) that it is "indistinguishable from true" (that property is in Ilango (FOCS 2025) a part of the definition of the prover, not its consequence). Using the theory of proof complexity generators we show that the concept can be turned it into a genuinely zero-knowledge proofs, assuming a conjecture from the theory about the existence of a hard generator and allowing the parties to share a common random string.
To cater to the needs of (Zero Knowledge) proofs for (mathematical) proofs, we describe a method to transform formal sentences in 2x2-matrices over multivariate polynomials with integer coefficients, such that usual proof-steps like modus-ponens or the substitution are easy to compute from the matrices corresponding to the terms or formulas used as arguments. By evaluating the polynomial variables in random elements of a suitably chosen finite field, the proof is replaced by a numeric sequence. Only the values corresponding to the axioms have to be computed from scratch. The values corresponding to derived formulas are computed from the values corresponding to their ancestors by applying the homomorphic properties. On such sequences, various Zero Knowledge methods can be applied.
This paper develops a comprehensive framework for artificial intelligence systems that operate under strict epistemic constraints, moving beyond stochastic language prediction to support structured reasoning, propositional commitment, and contradiction detection. It formalises belief representation, metacognitive processes, and normative verification, integrating symbolic inference, knowledge graphs, and blockchain-based justification to ensure truth-preserving, auditably rational epistemic agents.
Non-fungible tokens, NFT, have been used to record ownership of real estate, art, digital assets, and more recently to serve legal notice. They provide an important and accessible non-financial use of cryptocurrency's blockchain but are peculiar because ownership by NFT confers no rights over the asset. This work shows that it is possible to specify that peculiar property by combining functional and epistemic properties. Suitability of the specification is evaluated by proof that the blockchain implementation conforms to it, and by its use in an analysis of serving legal notice.
Abstract We introduce semitopology, a generalization of point-set topology that removes the restriction that intersections of open sets need necessarily be open. The intuition is that points represent participants in a decentralized system, and open sets represent collections of participants that collectively have the authority to collaborate to update their local state; we call this an actionable coalition. Examples of actionable coalition include: majority stakes in proof-of-stake blockchains; communicating peers in peer-to-peer networks; and even pedestrians working together to not bump into one another in the street. Where actionable coalitions exist, they have in common that collaborations are local (updating the states of the participants in the coalition, but not immediately those of the whole system); collaborations are voluntary (up to and including breaking rules); participants may be heterogeneous in their computing power or in their goals (not all pedestrians want to go to the same place); participants can choose with whom to collaborate; and they are not assumed subject to permission or synchronization by a central authority. We develop a topology-flavoured mathematics that goes some way to explaining how and why these complex decentralized systems can exhibit order, and gives us new ways to understand existing practical implementations. Semitopology is also interesting in and of itself, having a rich and interesting theory that quickly deviates from standard accounts on topological spaces. It soon becomes clear that the most interesting semitopologies are rather ill-behaved from the usual viewpoint, as they are never Hausdorff. A notion of ‘transitive open sets’ (topens) becomes central to the story, as topens define subsets of participants who should decide the same value in a distributed system that tries to achieve consensus, and points are called ‘regular’ when they have a topen neighbourhood. The theory is then further developed by introducing intertwined points, closures, closed sets and two interesting characterizations of regularity.
In paper describes the new logic programming language Delta, which have a many good properties. Delta-programs is p-computable, verifiable and can translation on other languages. Also we describe the Delta-methodology for constructing p-computable programs in high-level languages such as PHP, Java, JavaScript, C++, Pascal, Delphi, Python, Solidity and other. We would like to especially note the use of the Delta methodology for creating Smart Contracts and for Internet of things. We change the concept of the formula and define D-formulas(or Delta programs) are special list-formulas. Then we define the execution of a program how is the process of checking truth D-formula on a dynamic model. Main idea our paper consider program how list-formula from another formulas on dynamic models. And we created by iterations new Delta-programs use simple base formulas for this. Also we entered a dynamic models how models where we save final values of variables when check formula on this model.
Miha E. Habič, Joel David Hamkins, Lukas Daniel Klausner, Jonathan L. Verner · 5 authors
Given a countable model of set theory, we study the structure of its generic multiverse, the collection of its forcing extensions and ground models, ordered by inclusion. Mostowski showed that any finite poset embeds into the generic multiverse while preserving the nonexistence of upper bounds. We obtain several improvements of his result, using what we call the blockchain construction to build generic objects with varying degrees of mutual genericity. The method accommodates certain infinite posets, and we can realize these embeddings via a wide variety of forcing notions, while providing control over lower bounds as well. We also give a generalization to class forcing in the context of second-order set theory, and exhibit some further structure in the generic multiverse, such as the existence of exact pairs.