Computational and Proof Complexity of Partial String Avoidability

The partial string avoidability problem is stated as follows: given a finite set of strings with possible “holes” (wildcard symbols), determine whether there exists a two-sided infinite string containing no substrings from this set, assuming that a hole matches every symbol. The problem is known to be NP-hard and in PSPACE, and this article establishes its PSPACE-completeness. Next, string avoidability over the binary alphabet is interpreted as a version of conjunctive normal form satisfiability problem, where each clause has infinitely many shifted variants. Non-satisfiability of these formulas can be proved using variants of classical propositional proof systems, augmented with derivation rules for shifting proof lines (such as clauses, inequalities, polynomials, etc.). First, it is proved that there is a particular formula that has a short refutation in Resolution with a shift rule but requires classical proofs of exponential size. At the same time, it is shown that exponential lower bounds for classical proof systems can be translated for their shifted versions. Finally, it is shown that superpolynomial lower bounds on the size of shifted proofs would separate NP from PSPACE; a connection to lower bounds on circuit complexity is also established.

‘Sometime a paradox’, now proof: Yablo is not first order

Interesting as they are by themselves in philosophy and mathematics, paradoxes can be made even more fascinating when turned into proofs and theorems. For example, Russell’s paradox, which overthrew Frege’s logical edifice, is now a classical theorem in set theory, to the effect that no set contains all sets. Paradoxes can be used in proofs of some other theorems—thus Liar’s paradox has been used in the classical proof of Tarski’s theorem on the undefinability of truth in sufficiently rich languages. This paradox (as well as Richard’s paradox) appears implicitly in Gödel’s proof of his celebrated first incompleteness theorem. In this paper, we study Yablo’s paradox from the viewpoint of first- and second-order logics. We prove that a formalization of Yablo’s paradox (which is second order in nature) is non-first-orderizable in the sense of George Boolos (1984). This was sometime a paradox, but now the time gives it proof. —William Shakespeare (Hamlet, Act 3, Scene 1).

On the Intersection of Fields F with F [X]

Summary This is the third part of a four-article series containing a Mizar [3], [1], [2] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field F and every polynomial p ∈ F [X]\F there exists a field extension E of F such that p has a root over E. The formalization follows Kronecker’s classical proof using F [X]/<p> as the desired field extension E [6], [4], [5]. In the first part we show that an irreducible polynomial p ∈ F [X]\F has a root over F [X]/<p>. Note, however, that this statement cannot be true in a rigid formal sense: We do not have F ⊆ F [X]/ < p > as sets, so F is not a subfield of F [X]/<p>, and hence formally p is not even a polynomial over F [X]/ < p >. Consequently, we translate p along the canonical monomorphism ϕ: F → F [X]/<p> and show that the translated polynomial ϕ (p) has a root over F [X]/<p>. Because F is not a subfield of F [X]/<p> we construct in the second part the field (E \ ϕF)∪F for a given monomorphism ϕ: F → E and show that this field both is isomorphic to F and includes F as a subfield. In the literature this part of the proof usually consists of saying that “one can identify F with its image ϕF in F [X]/<p> and therefore consider F as a subfield of F [X]/<p>”. Interestingly, to do so we need to assume that F ∩ E = ∅, in particular Kronecker’s construction can be formalized for fields F with F ∩ F [X] = ∅. Surprisingly, as we show in this third part, this condition is not automatically true for arbitrary fields F : With the exception of ℤ2 we construct for every field F an isomorphic copy F′ of F with F′ ∩ F′ [X] ≠ ∅. We also prove that for Mizar’s representations of ℤn, ℚ and ℝ we have ℤn ∩ ℤn[X] = ∅, ℚ ∩ ℚ[X] = ∅ and ℝ ∩ ℝ[X] = ∅, respectively. In the fourth part we finally define field extensions: E is a field extension of F iff F is a subfield of E. Note, that in this case we have F ⊆ E as sets, and thus a polynomial p over F is also a polynomial over E. We then apply the construction of the second part to F [X]/<p> with the canonical monomorphism ϕ: F → F [X]/<p>. Together with the first part this gives – for fields F with F ∩ F [X] = ∅ – a field extension E of F in which p ∈ F [X]\F has a root.

Field Extensions and Kronecker’s Construction

Summary This is the fourth part of a four-article series containing a Mizar [3], [2], [1] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field F and every polynomial p ∈ F [X]\F there exists a field extension E of F such that p has a root over E. The formalization follows Kronecker’s classical proof using F [X]/<p> as the desired field extension E [6], [4], [5]. In the first part we show that an irreducible polynomial p ∈ F [X]\F has a root over F [X]/<p>. Note, however, that this statement cannot be true in a rigid formal sense: We do not have F ⊆ F [X]/ < p > as sets, so F is not a subfield of F [X]/<p>, and hence formally p is not even a polynomial over F [X]/ < p >. Consequently, we translate p along the canonical monomorphism ϕ: F → F [X]/<p> and show that the translated polynomial ϕ (p) has a root over F [X]/<p>. Because F is not a subfield of F [X]/<p> we construct in the second part the field (E \ ϕF)∪F for a given monomorphism ϕ: F → E and show that this field both is isomorphic to F and includes F as a subfield. In the literature this part of the proof usually consists of saying that “one can identify F with its image ϕF in F [X]/<p> and therefore consider F as a subfield of F [X]/<p>”. Interestingly, to do so we need to assume that F ∩ E = ∅, in particular Kronecker’s construction can be formalized for fields F with F ∩ F [X] = ∅. Surprisingly, as we show in the third part, this condition is not automatically true for arbitrary fields F : With the exception of ℤ2 we construct for every field F an isomorphic copy F′ of F with F′ ∩ F′ [X] ≠ ∅. We also prove that for Mizar’s representations of ℤn, ℚ and ℝ we have ℤn ∩ ℤn[X] = ∅, ℚ ∩ ℚ[X] = ∅ and ℝ ∩ ℝ[X] = ∅, respectively. In this fourth part we finally define field extensions: E is a field extension of F iff F is a subfield of E. Note, that in this case we have F ⊆ E as sets, and thus a polynomial p over F is also a polynomial over E. We then apply the construction of the second part to F [X]/<p> with the canonical monomorphism ϕ: F → F [X]/<p>. Together with the first part this gives – for fields F with F ∩ F [X] = ∅ – a field extension E of F in which p ∈ F [X]\F has a root.

On Monomorphisms and Subfields

Summary This is the second part of a four-article series containing a Mizar [2], [1] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field F and every polynomial p ∈ F [X]\F there exists a field extension E of F such that p has a root over E. The formalization follows Kronecker’s classical proof using F [X]/<p> as the desired field extension E [5], [3], [4]. In the first part we show that an irreducible polynomial p ∈ F [X]\F has a root over F [X]/<p>. Note, however, that this statement cannot be true in a rigid formal sense: We do not have F ⊆ [X]/ < p > as sets, so F is not a subfield of F [X]/<p>, and hence formally p is not even a polynomial over F [X]/ < p >. Consequently, we translate p along the canonical monomorphism ϕ : F → F [X]/<p> and show that the translated polynomial ϕ (p) has a root over F [X]/<p>. Because F is not a subfield of F [X]/<p> we construct in this second part the field (E \ ϕF )∪F for a given monomorphism ϕ : F → E and show that this field both is isomorphic to F and includes F as a subfield. In the literature this part of the proof usually consists of saying that “one can identify F with its image ϕF in F [X]/<p> and therefore consider F as a subfield of F [X]/<p>”. Interestingly, to do so we need to assume that F ∩ E = ∅, in particular Kronecker’s construction can be formalized for fields F with F ∩ F [X] = ∅. Surprisingly, as we show in the third part, this condition is not automatically true for arbitray fields F : With the exception of 𝕑2 we construct for every field F an isomorphic copy F′ of F with F′ ∩ F′ [X] ≠ ∅. We also prove that for Mizar’s representations of 𝕑n, 𝕈 and 𝕉 we have 𝕑n ∩ 𝕑n[X] = ∅, 𝕈 ∩ 𝕈 [X] = ∅ and 𝕉 ∩ 𝕉 [X] = ∅, respectively. In the fourth part we finally define field extensions: E is a field extension of F iff F is a subfield of E. Note, that in this case we have F ⊆ E as sets, and thus a polynomial p over F is also a polynomial over E. We then apply the construction of the second part to F [X]/<p> with the canonical monomorphism ϕ : F → F [X]/<p>. Together with the first part this gives - for fields F with F ∩ F [X] = ∅ - a field extension E of F in which p ∈ F [X]\F has a root.

On Roots of Polynomials over F[X]/ 〈p〉

Summary This is the first part of a four-article series containing a Mizar [3], [1], [2] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field F and every polynomial p ∈ F [X]\F there exists a field extension E of F such that p has a root over E. The formalization follows Kronecker’s classical proof using F [X]/<p> as the desired field extension E [9], [4], [6]. In this first part we show that an irreducible polynomial p ∈ F [X]\F has a root over F [X]/<p>. Note, however, that this statement cannot be true in a rigid formal sense: We do not have F ⊆ [X]/ < p > as sets, so F is not a subfield of F [X]/<p>, and hence formally p is not even a polynomial over F [X]/ < p >. Consequently, we translate p along the canonical monomorphism ϕ: F → F [X]/<p> and show that the translated polynomial ϕ(p) has a root over F [X]/<p>. Because F is not a subfield of F [X]/<p> we construct in the second part the field (E \ ϕF )∪F for a given monomorphism ϕ : F → E and show that this field both is isomorphic to F and includes F as a subfield. In the literature this part of the proof usually consists of saying that “one can identify F with its image ϕF in F [X]/<p> and therefore consider F as a subfield of F [X]/<p>”. Interestingly, to do so we need to assume that F ∩ E =∅, in particular Kronecker’s construction can be formalized for fields F with F \ F [X] =∅. Surprisingly, as we show in the third part, this condition is not automatically true for arbitray fields F : With the exception of 𝕑2 we construct for every field F an isomorphic copy F′ of F with F′ ∩ F′ [X] ≠∅. We also prove that for Mizar’s representations of 𝕑n, 𝕈 and 𝕉 we have 𝕑n ∩ 𝕑n[X] = ∅, 𝕈 ∩ 𝕈[X] = ∅and 𝕉 ∩ 𝕉[X] = ∅, respectively. In the fourth part we finally define field extensions: E is a field extension of F i F is a subfield of E. Note, that in this case we have F ⊆ E as sets, and thus a polynomial p over F is also a polynomial over E. We then apply the construction of the second part to F [X]/<p> with the canonical monomorphism ϕ : F → F [X]/<p>. Together with the first part this gives - for fields F with F ∩ F [X] = ∅ - a field extension E of F in which p ∈ F [X]\F has a root.

Quantitative fundamental theorem of algebra

Using subresultants, we modify a real-algebraic proof due to Eisermann of the fundamental theorem of Algebra (FTA) to obtain the following quantitative information: in order to prove the FTA for polynomials of degree d, the intermediate value theorem (IVT) is required to hold only for real polynomials of degree at most d2. We also explain that the classical proof due to Laplace requires IVT for real polynomials of exponential degree. These quantitative results highlight the difference in nature of these two proofs.

Proving uniformity and independence by self-composition and coupling

Proof by coupling is a classical proof technique for establishing probabilistic properties of two probabilistic processes, like stochastic dominance and rapid mixing of Markov chains. More recently, couplings have been investigated as a useful abstraction for formal reasoning about relational properties of probabilistic programs, in particular for modeling reduction-based cryptographic proofs and for verifying differential privacy. In this paper, we demonstrate that probabilistic couplings can be used for verifying non-relational probabilistic properties. Specifically, we show that the program logic pRHL—whose proofs are formal versions of proofs by coupling—can be used for formalizing uniformity and probabilistic independence. We formally verify our main examples using the EasyCrypt proof assistant.