Showing 1–5 of 5 results for author: Günther, E

The formal verification of the ctm approach to forcing

Authors: Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, Matías Steinberg

Abstract: We discuss some highlights of our computer-verified proof of the construction, given a countable transitive set-model $M$ of $\mathit{ZFC}$, of generic extensions satisfying $\mathit{ZFC}+\neg\mathit{CH}$ and $\mathit{ZFC}+\mathit{CH}$. Moreover, let $\mathcal{R}$ be the set of instances of the Axiom of Replacement. We isolated a 21-element subset $Ω\subseteq\mathcal{R}$ and defined… ▽ More We discuss some highlights of our computer-verified proof of the construction, given a countable transitive set-model $M$ of $\mathit{ZFC}$, of generic extensions satisfying $\mathit{ZFC}+\neg\mathit{CH}$ and $\mathit{ZFC}+\mathit{CH}$. Moreover, let $\mathcal{R}$ be the set of instances of the Axiom of Replacement. We isolated a 21-element subset $Ω\subseteq\mathcal{R}$ and defined $\mathcal{F}:\mathcal{R}\to\mathcal{R}$ such that for every $Φ\subseteq\mathcal{R}$ and $M$-generic $G$, $M\models \mathit{ZC} \cup \mathcal{F}\text{``}Φ\cup Ω$ implies $M[G]\models \mathit{ZC} \cup Φ\cup \{ \neg \mathit{CH} \}$, where $\mathit{ZC}$ is Zermelo set theory with Choice. To achieve this, we worked in the proof assistant Isabelle, basing our development on the Isabelle/ZF library by L. Paulson and others. △ Less

Submitted 14 December, 2023; v1 submitted 27 October, 2022; originally announced October 2022.

Comments: 20pp + 14pp in bibliography & appendices, 2 tables. v2: Added details to Delta System Lemma appendix, updated acknowledgments

MSC Class: 68V20 (Primary) 03E35; 03E30 (Secondary) ACM Class: F.4.1; I.2.3

Formalization of Forcing in Isabelle/ZF

Authors: Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf

Abstract: We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct a proper generic extension and show that the latter also satisfies ZFC. In doing so, we remodularized Paulson's ZF-Constructibility library. We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct a proper generic extension and show that the latter also satisfies ZFC. In doing so, we remodularized Paulson's ZF-Constructibility library. △ Less

Submitted 18 April, 2020; v1 submitted 27 January, 2020; originally announced January 2020.

Comments: 15 pages. Accepted at the 10th International Joint Conference on Automated Reasoning (IJCAR 2020). v2: Added expanded section on related work

MSC Class: 03B35 (Primary) 03E40; 03B70; 68T15 (Secondary) ACM Class: F.4.1

Mechanization of Separation in Generic Extensions

Authors: Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf

Abstract: We mechanize, in the proof assistant Isabelle, a proof of the axiom-scheme of Separation in generic extensions of models of set theory by using the fundamental theorems of forcing. We also formalize the satisfaction of the axioms of Extensionality, Foundation, Union, and Powerset. The axiom of Infinity is likewise treated, under additional assumptions on the ground model. In order to achieve these… ▽ More We mechanize, in the proof assistant Isabelle, a proof of the axiom-scheme of Separation in generic extensions of models of set theory by using the fundamental theorems of forcing. We also formalize the satisfaction of the axioms of Extensionality, Foundation, Union, and Powerset. The axiom of Infinity is likewise treated, under additional assumptions on the ground model. In order to achieve these goals, we extended Paulson's library on constructibility with renaming of variables for internalized formulas, improved results on definitions by recursion on well-founded relations, and sharpened hypotheses in his development of relativization and absoluteness. △ Less

Submitted 10 January, 2019; originally announced January 2019.

Comments: 23 pages, 1 figure

MSC Class: 03B35 (Primary) 03E40; 03B70; 68T15 (Secondary) ACM Class: F.4.1

First steps towards a formalization of Forcing

Authors: Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf

Abstract: We lay the ground for an Isabelle/ZF formalization of Cohen's technique of forcing. We formalize the definition of forcing notions as preorders with top, dense subsets, and generic filters. We formalize the definition of forcing notions as preorders with top, dense subsets, and generic filters. We formalize a version of the principle of Dependent Choices and using it we prove the Rasiowa-Sikorski… ▽ More We lay the ground for an Isabelle/ZF formalization of Cohen's technique of forcing. We formalize the definition of forcing notions as preorders with top, dense subsets, and generic filters. We formalize the definition of forcing notions as preorders with top, dense subsets, and generic filters. We formalize a version of the principle of Dependent Choices and using it we prove the Rasiowa-Sikorski lemma on the existence of generic filters. Given a transitive set $M$, we define its generic extension $M[G]$, the canonical names for elements of $M$, and finally show that if $M$ satisfies the axiom of pairing, then $M[G]$ also does. We also prove $M[G]$ is transitive. △ Less

Submitted 27 November, 2018; v1 submitted 13 July, 2018; originally announced July 2018.

Comments: 18 pages. Isabelle proofs can be found among the source files of this submission. v2: Added discussion of related work and of details of implementation. Proof that G belongs to M[G] and that the latter is transitive

MSC Class: 03B35 (Primary) 03E40; 03B70; 68T15 (Secondary) ACM Class: F.4.1

A New Approach to Online Scheduling: Approximating the Optimal Competitive Ratio

Authors: Elisabeth Günther, Olaf Maurer, Nicole Megow, Andreas Wiese

Abstract: We propose a new approach to competitive analysis in online scheduling by introducing the novel concept of competitive-ratio approximation schemes. Such a scheme algorithmically constructs an online algorithm with a competitive ratio arbitrarily close to the best possible competitive ratio for any online algorithm. We study the problem of scheduling jobs online to minimize the weighted sum of comp… ▽ More We propose a new approach to competitive analysis in online scheduling by introducing the novel concept of competitive-ratio approximation schemes. Such a scheme algorithmically constructs an online algorithm with a competitive ratio arbitrarily close to the best possible competitive ratio for any online algorithm. We study the problem of scheduling jobs online to minimize the weighted sum of completion times on parallel, related, and unrelated machines, and we derive both deterministic and randomized algorithms which are almost best possible among all online algorithms of the respective settings. We also generalize our techniques to arbitrary monomial cost functions and apply them to the makespan objective. Our method relies on an abstract characterization of online algorithms combined with various simplifications and transformations. We also contribute algorithmic means to compute the actual value of the best possi- ble competitive ratio up to an arbitrary accuracy. This strongly contrasts all previous manually obtained competitiveness results for algorithms and, most importantly, it reduces the search for the optimal com- petitive ratio to a question that a computer can answer. We believe that our concept can also be applied to many other problems and yields a new perspective on online algorithms in general. △ Less

Submitted 31 October, 2012; v1 submitted 4 April, 2012; originally announced April 2012.

Comments: 24 pages; short version to appear in SODA 2013