(No abstract available; you can read the introductory chapter on a separate page instead.)
Hlavním účelem této práce je studium elementárních vnoření univerzální třídy do tranzitivní třídy (stručně nazývaných reflexe) v jisté neregulární teorii množin, kterou budeme ve shodě s [1] označovat jako univerzální teorii (UT). Axiom regularity, který v klasické teorii množin značně omezuje (mimo jiné) možnost konstruovat elementární vnoření množinového univerza, je v UT nahrazen tzv. axiomem superuniverzality, jenž naopak dovoluje sestrojit množství reflexí s rozmanitými vlastnostmi. Reflexe lze s výhodou využít zejména pro modelování prostředků nestandardní analýzy a obecnějších nestandardních principů, my se však zaměříme na obecný popis reflexí a možností jejich konstrukce.
Ústředním pojmem kapitoly 2 jsou tzv. minimální reflexe. V celé kapitole budeme pracovat výhradně v UT. V sekci 2.1 nejprve ukážeme, že studium vlastností minimálních reflexí má mnoho důsledků i pro neminimální reflexe, neboť každá reflexe v jistém smyslu obsahuje určitou minimální reflexi, zde nazývanou jádro. Část tohoto tvrzení dále zobecníme na třídy, které jsou modelem tzv. axiomu kolekce, což nám zpětně umožní ukázat, že nekonečné schéma formulí v definici reflexe lze konečně axiomatizovat, tedy nahradit jedinou formulí.
Sekce 2.2 se krátce zabývá reflexemi vedoucími do kotranzitivních tříd (tedy např. do celé univerzální třídy) — ukážeme, že takové reflexe jsou triviální, tedy že se takřka neliší od identické reflexe.
V sekci 2.3 popíšeme obecnou konstrukci, kterou lze získat všechny minimální reflexe. Ukážeme, že každá minimální reflexe je direktní limitou vhodného usměrněného systému ultramocnin univerzální třídy, a na druhou stranu (téměř) každá taková direktní limita určuje minimální reflexi. Zjistíme také, že určité speciální typy minimálních reflexí (jednoduché reflexe, polojednoduché reflexe a PP-reflexe) lze charakterizovat podmínkami na tvar příslušné direktní limity. Navíc uvidíme, že tyto typy minimálních reflexí jsou uzavřené na některé způsoby konstrukce reflexí (ultraprodukty, skládání, podreflexe, direktní limity).
Sekce 2.4 obsahuje dva příklady minimálních reflexí se zajímavými vlastnostmi, pokusíme se ukázat, že přinejmenším některé z výše zmíněných tříd minimálních reflexí spolu nesplývají.
V kapitole 3 reflexe opustíme a budeme se věnovat axiomu silného výběru, který postuluje existenci vzájemně jednoznačného zobrazení univerzální třídy na třídu všech ordinálních čísel. Pro klasickou teorii množin s axiomem regularity je známo, že axiom silného výběru konzervativně rozšiřuje obyčejný axiom výběru, jeho použitím tedy není možné dokázat pouze o množinách nic nového. Pro neregulární teorii množin však zmíněná konzervativita neplatí. Přesto se nám podaří popsat množinové důsledky axiomu silného výběru pomocí jednoduchého schematu axiomů a dokážeme konzervativitu axiomu silného výběru nad takto modifikovanou teorií množin. Protože UT axiom silného výběru obsahuje, obdržíme jako důsledek také popis fragmentu UT v základním jazyce teorie množin.
Grzegorczyk’s modal logic (Grz) corresponds to the class of upwards well-founded partially ordered Kripke frames, however all known proofs of this fact utilize some form of the Axiom of Choice; G. Boolos asked in [1], whether it is provable in plain ZF. We answer his question negatively: Grz corresponds (in ZF) to a class of frames, which does not provably coincide with upwards well-founded posets in ZF alone.
We study the extension (introduced as BT in [2]) of the theory S21 by instances of the dual (onto) weak pigeonhole principle for p-time functions, dWPHP(PV)xx². We propose a natural framework for formalization of randomized algorithms in bounded arithmetic, and use it to provide a strengthening of Wilkie’s witnessing theorem for S21 + dWPHP(PV). We construct a propositional proof system WF (based on a reformulation of Extended Frege in terms of Boolean circuits), which captures the ∀Πb1-consequences of S21 + dWPHP(PV). We also show that WF p-simulates the Unstructured Extended Nullstellensatz proof system of [1].
We prove that dWPHP(PV) is (over S21) equivalent to a statement asserting the existence of a family of Boolean functions with exponential circuit complexity. Building on this result, we formalize the Nisan–Wigderson construction (derandomization of probabilistic p-time algorithms) in a conservative extension of S21 + dWPHP(PV).
We study groupoids satisfying the identities x·xy = y and x·yz = xy·xz. Particularly, we focus our attention at subdirectly irreducible ones, find a description and characterize small ones.
We introduce a nonstandard arithmetic NQA− based on the theory developed by R. Chuaqui and P. Suppes in [1] (we will denote it by NQA+), with a weakened external open minimization schema. A finitary consistency proof for NQA− formalizable in PRA is presented. We also show interesting facts about the strength of the theories NQA− and NQA+; NQA− is mutually interpretable with IΔ0 + EXP, and on the other hand, NQA+ interprets the theories IΣ1 and WKL0.
We study the extension of the theory S21 by instances of the dual (onto) weak pigeonhole principle for p-time functions, dWPHP(PV)xx². We propose a natural framework for formalization of randomized algorithms in bounded arithmetic, and use it to provide a strengthening of Wilkie’s witnessing theorem for S21 + dWPHP(PV).
Then we show that dWPHP(PV) is (over S21) equivalent to a statement asserting the existence of a family of Boolean functions with exponential circuit complexity. Building on this result, we formalize the Nisan–Wigderson construction (conditional derandomization of probabilistic p-time algorithms) in a conservative extension of S21 + dWPHP(PV). We also develop in S21 the algebraic machinery needed for implicit list-decoding of Reed–Muller error-correcting codes (including some results on a modification of Soltys’ theory ∀LAP), and use it to formalize the Impagliazzo–Wigderson strengthening of the Nisan–Wigderson theorem.
We construct a propositional proof system WF (based on a reformulation of Extended Frege in terms of Boolean circuits), which captures the ∀Πb1-consequences of S21 + dWPHP(PV). As an application, we show that WF and G2 p-simulate the Unstructured Extended Nullstellensatz proof system.
We also consider two theories which have explicit counting facilities in their language. The first one is the Impagliazzo–Kapron logic; we propose a modification of the theory, and prove a generalization of the Impagliazzo–Kapron soundness theorem to ∀∃-consequences of the theory. The second one is a feasible theory of approximate counting, formulated in a variant of Kleene’s 3-valued logic. We introduce the theory, and prove a witnessing theorem for its existential consequences.
We construct explicit bases of admissible rules for a representative class of normal modal logics (including the systems K4, GL, S4, Grz, and GL.3), by extending the methods of S. Ghilardi and R. Iemhoff. We also investigate the notion of admissible multiple conclusion rules.
We investigate the computational complexity of deciding whether a given inference rule is admissible for some modal and superintuitionistic logics. We state a broad condition under which the admissibility problem is coNEXP-hard. We also show that admissibility in several well-known systems (including GL, S4, and IPC) is in coNE, thus obtaining a sharp complexity estimate for admissibility in these systems.
By a well-known result of Cook and Reckhow [1,4], all Frege systems for the Classical Propositional Calculus (CPC) are polynomially equivalent. Mints and Kojevnikov [3] have recently shown p-equivalence of Frege systems for the Intuitionistic Propositional Calculus (IPC) in the standard language, building on a description of admissible rules of IPC by Iemhoff [2]. We prove a similar result for an infinite family of normal modal logics, including K4, GL, S4, and S4Grz.
We develop approximate counting of sets definable by Boolean circuits in bounded arithmetic using the dual weak pigeonhole principle (dWPHP(PV)), as a generalization of results from [1]. We discuss applications to formalization of randomized complexity classes (such as BPP, APP, MA, AM) in PV1 + dWPHP(PV).
We prove that the sharply bounded arithmetic T20 in a language containing the function symbol ⌊x / 2y⌋ (often denoted by MSP) is equivalent to PV1.
The principle sPHPab(PV(α)) states that no oracle circuit can compute a surjection of a onto b. We show that sPHPρ(a)Ρ(a)(PV(α)) is independent of PV1(α) + sPHPπ(a)Π(a)(PV(α)) for various choices of the parameters π, Π, ρ, Ρ. We also improve the known separation of iWPHP(PV) from S21 + sWPHP(PV) under cryptographic assumptions.
We show that IPC, K4, GL, and S4, as well as all logics inheriting their admissible rules, have independent bases of admissible rules.
We investigate the substitution Frege (SF) proof system and its relationship to extended Frege (EF) in the context of modal and superintuitionistic (si) propositional logics. We show that EF is p-equivalent to tree-like SF, and we develop a “normal form” for SF-proofs. We establish connections between SF for a logic L, and EF for certain bimodal expansions of L.
We then turn attention to specific families of modal and si logics. We prove p-equivalence of EF and SF for all extensions of KB, all tabular logics, all logics of finite depth and width, and typical examples of logics of finite width and infinite depth. In most cases, we actually show an equivalence with the usual EF system for classical logic with respect to a naturally defined translation.
On the other hand, we establish exponential speed-up of SF over EF for all modal and si logics of infinite branching, extending recent lower bounds by P. Hrubeš. We develop a model-theoretical characterization of maximal logics of infinite branching to prove this result.
We show how to formalize approximate counting via hash functions in subsystems of bounded arithmetic, using variants of the weak pigeonhole principle. We discuss several applications, including a proof of the tournament principle, and an improvement on the known relationship of the collapse of the bounded arithmetic hierarchy to the collapse of the polynomial-time hierarchy.
We investigate the proof complexity of analytic subsystems of the deep inference proof system SKSg (the calculus of structures). Exploiting the fact that the cut rule (i↑) of SKSg corresponds to the ¬-left rule in the sequent calculus, we establish that the “analytic” system KSg + c↑ has essentially the same complexity as the monotone Gentzen calculus MLK. In particular, KSg + c↑ quasipolynomially simulates SKSg, and admits polynomial-size proofs of some variants of the pigeonhole principle.
We develop canonical rules capable of axiomatizing all systems of multiple-conclusion rules over K4 or IPC, by extension of the method of canonical formulas by Zakharyaschev [1]. We use the framework to give an alternative proof of the known analysis of admissible rules in basic transitive logics, which additionally yields the following dichotomy: any canonical rule is either admissible in the logic, or it is equivalent to an assumption-free rule. Other applications of canonical rules include a generalization of the Blok–Esakia theorem and the theory of modal companions to systems of multiple-conclusion rules or (finitary structural global) consequence relations, and a characterization of splittings in the lattices of consequence relations over monomodal or superintuitionistic logics with the finite model property.
We investigate the provability of some properties of abelian groups and quadratic residues in variants of bounded arithmetic. Specifically, we show that the structure theorem for finite abelian groups is provable in S22 + iWPHP(Σ1b), and use it to derive Fermat’s little theorem and Euler’s criterion for the Legendre symbol in S22 + iWPHP(PV) extended by the pigeonhole principle PHP(PV). We prove the quadratic reciprocity theorem (including the supplementary laws) in the arithmetic theories T20 + Count2(PV) and IΔ0 + Count2(Δ0) with modulo-2 counting principles.
We develop an arithmetical theory VNC1* and its variant VNC1*, corresponding to “slightly nonuniform” NC1. Our theories sit between VNC1 and VL, and allow evaluation of log-depth bounded fan-in circuits under limited conditions. Propositional translations of Σ0B(LVNC1*)-formulas provable in VNC1* admit L-uniform polynomial-size Frege proofs.
We formalize the construction of Paterson’s variant of the Ajtai–Komlós–Szemerédi sorting network of logarithmic depth in the bounded arithmetical theory VNC1* (an extension of VNC1), under the assumption of existence of suitable expander graphs. We derive a conditional p-simulation of the propositional sequent calculus in the monotone sequent calculus MLK.
We investigate admissible rules of Łukasiewicz multi-valued propositional logic. We show that admissibility of multiple-conclusion rules in Łukasiewicz logic, as well as validity of universal sentences in free MV-algebras, is decidable (in PSPACE).
We construct explicit bases of single-conclusion and multiple-conclusion admissible rules of propositional Łukasiewicz logic, and we prove that every formula has an admissibly saturated approximation. We also show that Łukasiewicz logic has no finite basis of admissible rules.
Atserias, Galesi, and Pudlák [1] have shown that the monotone sequent calculus MLK quasipolynomially simulates proofs of monotone sequents in the full sequent calculus LK (or equivalently, in Frege systems). We generalize the simulation to the fragment MCLK of LK which can prove arbitrary sequents, but restricts cut-formulas to be monotone. We also show that MLK as a refutation system for CNFs quasipolynomially simulates LK.
We show that the quantified propositional proof systems Gi are polynomially equivalent to their restricted versions that require all cut formulas to be prenex Σqi (or prenex Πqi). Previously this was known only for the treelike systems Gi*.
D’Aquino et al. [1] have recently shown that every real-closed field with an integer part satisfying the arithmetic theory IΣ4 is recursively saturated, and that this theorem fails if IΣ4 is replaced by IΔ0. We prove that the theorem holds if IΣ4 is replaced by weak subtheories of Buss’ bounded arithmetic: PV or Σb1-IND|x|k. It also holds for IΔ0 (and even its subtheory IE2) under a rather mild assumption on cofinality. On the other hand, it fails for the extension of IOpen by an axiom expressing the Bézout property, even under the same assumption on cofinality.
We study the notion of conservative translation between logics introduced by Feitosa and D’Ottaviano [1]. We show that classical propositional logic (CPC) is universal in the sense that every finitary consequence relation over a countable set of formulas can be conservatively translated into CPC. The translation is computable if the consequence relation is decidable. More generally, we show that one can take instead of CPC a broad class of logics (extensions of a certain fragment of full Lambek calculus FL) including most nonclassical logics studied in the literature, hence in a sense, (almost) any two reasonable deductive systems can be conservatively translated into each other. We also provide some counterexamples, in particular the paraconsistent logic LP is not universal.
We investigate properties of the formula p → □p in the basic modal logic K. We show that K satisfies an infinitary weak variant of the rule of margins, which leads to a description of a complete set of unifiers of p → □p. Using this information, we establish that K has nullary unification type. Moreover, we show that the formula p → □p is admissibly saturated, but not exact.
We investigate the computational complexity of admissibility of inference rules in infinite-valued Łukasiewicz propositional logic (Ł). It was shown in [1] that admissibility in Ł is checkable in PSPACE. We establish that this result is optimal, i.e., admissible rules of Ł are PSPACE-complete. In contrast, derivable rules of Ł are known to be coNP-complete.
We show that for any constant d, complex roots of degree d univariate rational (or Gaussian rational) polynomials—given by a list of coefficients in binary—can be computed to a given accuracy by a uniform TC0 algorithm (a uniform family of constant-depth polynomial-size threshold circuits). The basic idea is to compute the inverse function of the polynomial by a power series. We also discuss an application to the theory VTC0 of bounded arithmetic.
We show that the universally axiomatized, induction-free theory PA− is a sequential theory in the sense of Pudlák [1], in contrast to the closely related Robinson’s arithmetic.
Buresh-Oppenheim proved that the NP search problem to find nontrivial factors of integers of a special form belongs to Papadimitriou’s class PPA, and is probabilistically reducible to a problem in PPP. In this paper, we use ideas from bounded arithmetic to extend these results to arbitrary integers. We show that general integer factoring is reducible in randomized polynomial time to a PPA problem and to the problem WeakPigeon ∈ PPP. Both reductions can be derandomized under the assumption of the generalized Riemann hypothesis. We also show (unconditionally) that PPA contains some related problems, such as square root computation modulo n, and finding quadratic nonresidues modulo n.
