Skip to main content
Share Your Experience: Take the 2024 Developer Survey

Questions tagged [set-theory]

Questions about set theory

Filter by
Sorted by
Tagged with
71 votes
7 answers
4k views

Which interesting theorems in TCS rely on the Axiom of Choice? (Or alternatively, the Axiom of Determinacy?)

Mathematicians sometimes worry about the Axiom of Choice (AC) and Axiom of Determinancy (AD). Axiom of Choice: Given any collection ${\cal C}$ of nonempty sets, there is a function $f$ that, given a ...
Ryan Williams's user avatar
40 votes
5 answers
1k views

Results in Theoretical CS independent of ZFC

I'm going to ask a quite vague question, since the borderline between theoretical computer science and math is not always easy to distinguish. QUESTION: Are you aware of any interesting result in CS ...
OldFella's user avatar
  • 501
16 votes
3 answers
700 views

Applications for set theory, ordinal theory, infinite combinatorics and general topology in computer science?

I am a mathematician interested in set theory, ordinal theory, infinite combinatorics and general topology. Are there any applications for these subjects in computer science? I have looked a bit, and ...
user135172's user avatar
15 votes
4 answers
801 views

Forcing method used in Baker-Gill-Solovay Relativization paper and Cohen's Proof of Continuum Hypothesis Independence

I am generally interested in the forcing method used by Baker-Gill-Solovay and Cohen. I am looking for as many sources as I can get my hands on concerning either the technique itself or its use. Does ...
djkern's user avatar
  • 533
14 votes
3 answers
2k views

Type system based on naive set theory

As I understand, in computer science data types are not based on set theory because of things like Russell's paradox, but as in real world programming languages we can't express such complex data ...
Nutel's user avatar
  • 381
11 votes
1 answer
472 views

The state of art for sunflower system

I am interesting in the sunflower system and its applications in computer science. Given a Universe $U$ and a collection of $k$ sets $A_i$ is called a k-sunflower system if $A_i \cap A_j = Y $ for ...
Yao Wang's user avatar
  • 329
10 votes
3 answers
1k views

Universal and existential types

I'm trying to wrap my head around the concepts of universal and existential types but everywhere I look, I see either logical or operational intuitions (or implementations) (e.g. TAPL book by B. ...
socumbersome's user avatar
10 votes
2 answers
489 views

What are the issues with a set-like interpretation of quantifiers in type theory?

In his answer to a question that tries to treat universal and existential quantifiers as intersections and unions of sets, Andrej Bauer says: Forget the intersections and unions. People get this idea ...
Jozef Mikušinec's user avatar
9 votes
1 answer
410 views

Cantor's theorem in type theory

Cantor's theorem states that For any set A, the set of all subsets of A has a strictly greater cardinality than A itself. Is it possible to encode something like this using only types / ...
Paula Vega's user avatar
9 votes
2 answers
2k views

Formal Definition/counter part in mathematics for “Objects” of Object Oriented Models

This is a question I asked in mathematics SE forum, and I was referred here. So here is the question- I'm a newbie in both formal mathematics and theoretical computer science, so please bear with me ...
user1260776's user avatar
8 votes
1 answer
2k views

Are there presentations of set theory in terms of lambda-calculus?

I am planning to implement in software a set theory language, based on a binary function, which in set theory is the so called adjunction operation: $f(x, y) = x \cup$ {y}. Therefore, a presentation ...
JoeD's user avatar
  • 81
8 votes
0 answers
231 views

Is there a known automatic proof of the independence of the continuum hypothesis?

In 2002, L.C. Paulson gave a mechanized proof of the consistency of the axiom of choice by formalizing $V=L$ and its consistency. We could ask whether there is a formalized proof of the independence ...
Hanul Jeon's user avatar
7 votes
2 answers
2k views

In the context of regular languages, must the alphabet be finite?

In The Theory of Parsing, Translation, and Compiling, Volume I, Section 0.2.1 (p.15 / 1972), Aho and Ullman casually write that "[a]n alphabet need not be finite or even countable, but for all ...
sam's user avatar
  • 71
7 votes
1 answer
172 views

Trying understand a move in Cohen's proof of the independence of the continuum hypothesis

I've read a few different presentations of Cohen's proof. All of them (that I've seen) eventually make a move where a Cartesian product (call it CP) between the (M-form of) $\aleph_2$ and $\aleph_0$ ...
djkern's user avatar
  • 533
7 votes
1 answer
180 views

Order notation quirk

Is it true that $$O(n) = \bigcap \{ O(g) \mid g \in \omega(n) \}?$$ This appears to be a straighforward question about sets of functions, but on closer examination leads to some murky waters. I would ...
András Salamon's user avatar
7 votes
2 answers
351 views

A Combinatorial Problem on Extremal Set Theory

Given a ground set $[n]$, under what condition of parameters $a,b,c$ does a family of subsets $\mathcal{F}\subseteq 2^{[n]}$ with the following property exist? (i) $\forall S\in \mathcal{F}$, $|S|=a$....
Zihan Tan's user avatar
  • 437
6 votes
1 answer
455 views

Do we know a specific $L_{ZFC}$ such that $K(s) \ge L_{ZFC}$ is unprovable in ZFC for all strings $s$?

Chaitin's incompleteness theorem states for any formal system $F$ (which satisfies various criteria), there is a $L$ such that for any $s$ the statement $$K(s) \ge L_F$$ is unprovable in that formal ...
Christopher King's user avatar
6 votes
1 answer
143 views

What's complexity of this set problem which looks like "Linear Programming"?

I came up with a problem below, which looks like a linear programming problem: Given $n$ sets $S_{1}, S_{2},..., S_{n}$, with constraints of : $$ \forall i=1, 2, 3,...,n\space\space \left | S_{i} ...
RIC_Eien's user avatar
  • 439
5 votes
2 answers
655 views

Data structure to determine if sets are disjoint in o(n) time

My initial question was exactly the title of this post, but after feedback from commenters I have formulated a more precise version of the question that attempts to capture its essence. Does there ...
pre-kidney's user avatar
5 votes
3 answers
449 views

Variation on partial Set Cover with penalties

I'm looking at the following problem, which I'm hoping is perhaps a known variant of the Set Cover problem: Input: We're given a universe $U$ and two disjoint subsets $A$ and $B$ such that $A \cup B=...
sammy34's user avatar
  • 171
5 votes
1 answer
240 views

Kruskal-Katona Theorem with Majority?

I am interested in the following problem which seems like an extension of the Kruskal-Katona Theorem. Let $A_k \subseteq \{0,1\}^n$ be a subset of the hypercube such that every element in $A$ has ...
NAg's user avatar
  • 666
4 votes
3 answers
1k views

How to construct a special data structure that allows for "fast" subset operation?

If I have a set S = {1,2,3,4,5} that represents a universe and the following subsets of S: U1 = {1,2} U2 = {3,4,5} C1 = {3,5} C2 = {2} The above sets are guaranteed to be subsets of S, however ...
user1068636's user avatar
4 votes
4 answers
1k views

Is there a set theoretic way to look at SQL?

I have been learning about SQL and at times it feels like set theory. A statement like SELECT * FROM myTable is like a set $\{ x: x \in \text{myTable} \}$. A ...
john mangual's user avatar
2 votes
2 answers
880 views

Which formalism is best suited for automated theorem proving in set theory?

Abbreviations - FOL is first-order logic; NBG is Von Neumann–Bernays–Gödel set theory; SEP is Stanford Encyclopedia of Philosophy; HOL is higher-order logic; ATP is automated theorem proving. Context ...
Atriya's user avatar
  • 279
2 votes
1 answer
422 views

Bloom filter for storage

I am reading about the Bloom filter, and I must say I am fascinated by the idea. I would like to know if it is possible to use it for storage. The problem with the Bloom filter is that, even if we ...
zzzbbx's user avatar
  • 203
2 votes
1 answer
327 views

Is any computational complexity question solved by injury priority method except Post problem?

As we know, there are many questions of Turing Degree closed by injury priority method. Is any computational complexity question solved by injury priority method except Post problem or Turing Degree? ...
XL _At_Here_There's user avatar
2 votes
1 answer
121 views

partition to min the max number of intersections

Given $n$ items and $m$ customers, each of whom is interested in some subset of the items, partition the set of items among $k$ different stores so that the maximum number of customers visiting any ...
user16035's user avatar
2 votes
0 answers
107 views

Faster algorithms to estimate the subset sizes

Lemma: Consider two sets $B ⊆ U$, where $n = |U|$. Let $ξ, γ ∈ (0, 1)$ be parameters, such that $γ < 1/ \log n$. Assume that one is given an access to a membership oracle that, given an element $x ∈...
Com's user avatar
  • 41
2 votes
0 answers
162 views

Set-theoretic encoding of functions in type theory

Functions usually get encoded in set theory as follows. A function $A\to B$ is a subset $f\subset A\times B$ such that $\pi_1:f\to A$ is a bijection. In type theory to give a function $A\to B$ is to ...
user avatar
2 votes
1 answer
251 views

Optimal partition according to partition cardinality

Given $N$ sets of integers $S_1, \ldots,S_N$ with $|S_i| \le K$. We want to partition those sets such that the union of all sets in any given partition doesn't contain more than $K$ elements. Can ...
user avatar
2 votes
0 answers
390 views

Theorem prover fails to find simple set theory proof?

I am trying to use an automated theorem prover (SNARK) to prove a theorem in first-order logic. Tarski claims in his "a work on mereology" that the goal is provable from assertions 1-3 but he does ...
Atriya's user avatar
  • 279
1 vote
2 answers
3k views

What's the relation between the dominating set and vertex cover?

I wonder if the minimal dominating set is always a subset of the minimal vertex cover in any graph. If so, what's the proof?
Yob's user avatar
  • 121
1 vote
2 answers
246 views

Using partial functions to prove correctness

I'm interested in proving that a program (which may or may not terminate) will give the correct answer if it terminates. Given: $P$ is a family of programs, parameterized by a function $f$. Write $...
Jodag's user avatar
  • 45
1 vote
2 answers
823 views

Proving that inclusion is antisymmetric in Coq

I'm a Coq newbie and I'd like to prove that the inclusion relation is antisymmetric, that is: $\forall x\forall y(x\subseteq y\land y\subseteq x\rightarrow x=y)$. I wrote the following thing: ...
gbo4's user avatar
  • 31
1 vote
1 answer
315 views

How can I formalize key value stores with set theory? [closed]

I'm currently developing a simple key-value NoSQL store and want to build its formal model. I'm interested in knowing if there some work about formalization of key-value stores outside of category ...
MainstreamDeveloper00's user avatar
1 vote
2 answers
126 views

Do realizable systems always have some non-well-founded sets?

Suppose we are standing outside a realizable system which admits CZF or a similar constructive set theory. Then consider the following: LEM is not realized (e.g. this MSE answer) The traditional ...
Corbin's user avatar
  • 271
1 vote
1 answer
106 views

Minimum order of partite in a bipartite graph

I want to create a bipartite graph where the first partite $U$ contains $L$ vertices with degree $k$ and the second partite $V$ contains $N$ other vertices with degree $a$. I need to find the minimum ...
Cantfindname's user avatar
1 vote
1 answer
755 views

Rings and the set of all minimum s-t-cuts

Let $N$ be a flow network with nodes $V$ and edges $E$. For technical reasons, the source side of a minimum $s$-$t$ cut $(A,B)$ with $s \in A$ and $t \in B$ is defined as $A - \{s\}$. Now, let $\...
Oliver Witt's user avatar
1 vote
0 answers
54 views

Better approximation of the subset in the membership oracle

A standard tool for estimating the size of a subset via membership oracle queries is given below. Lemma 2.8: . Consider two (finite) sets $B ⊆ U$, where $n = |U|$. Let $ε ∈ (0, 1)$ and $γ ∈ (0, 1/2)$ ...
Com's user avatar
  • 41
1 vote
0 answers
57 views

Is this a variant of the set cover problem?

$\textbf{Decision Problem:}$ Given a finite set of elements $E$ and a collection $C$ of non empty sets, $C=\{E_1,...,E_n\}$, such that each $E_i$ covers at least one element of $E$. The goal is to ...
mahou_2019's user avatar
1 vote
0 answers
483 views

Equality Constraints over Sets with Tree Automata

Tree Automata can be used to model sets of values of a Herbrand Universe, for example, to model possible values in a functional program. Systems of subtype constraints over set expressions have ...
Joey Eremondi's user avatar
1 vote
0 answers
86 views

Equality Theorems with Type Theoretic Proof

I am investigating how I might be able to translate even commonplace equalities/ inequalities via the so-called Curry-Howard Correspondance - from a generic, set theoretic plus AOC foundation - into a ...
Krpcannon's user avatar
1 vote
0 answers
94 views

Is there a name for this property in set-valued analysis or combinatorics?

I asked this question a few days ago on MO, but I haven't received an answer. So I thought I would ask here. I have also added a relaxed version of the question here. Let $F$ be a set-valued, finite-...
Ankur's user avatar
  • 779
0 votes
1 answer
73 views

Given a partition and an element, find the subset that includes this element

I am interested in the following simple problem: Let $X$ be a set and $X_1\cup X_2\cup\cdots\cup X_k$ be a finite partition of $X$. Given $x\in X$, find the subset $X_i$ for which $x\in X_i$. I am ...
user77463's user avatar
0 votes
0 answers
53 views

Data structure for storing set of sets

Let key space $K_n =$ { $1, 2,...,n$ } Let Data Structure $D$ implementing a set $S$ of sets such that All sets in $S$ are of same size $l$, $1 \le l \le n$ All sets in $S$ contain keys belonging to $...
Yolov4's user avatar
  • 1
0 votes
0 answers
47 views

Proving the Equivalence of REGEX r^n and r^{..n} when r Is Nullable

Im seeking clarification and a rigorous proof regarding the equivalence of r^n and r^{..n} in the context of formal languages, particularly when r is nullable. To clarify the terminology: r denotes ...
J.Doe's user avatar
  • 1
0 votes
0 answers
88 views

Can lambda-calculus, or other formal systems / calculi, be represented using set theory?

Background: I'm a fresh grad student looking into interesting ideas I have. I do not have any theoretical computer science background beyond basic Theory of Computation stuff from undergrad. If I have ...
The Pointer's user avatar
0 votes
0 answers
87 views

Existence of a family of size 2^Ω(n) of subsets of {1,...,n} each of cardinality n/4 where two subsets have at most n/8 elements in common

Let $\mathcal{G}$ be a family of $t=2^{\Omega(n)}$ subsets of $N=\{1,2,...,n\}$, each of cardinality $n / 4$ so that any two distinct members of $\mathcal{G}$ have at most $n / 8$ elements in common. ...
C. Mürtz's user avatar
  • 101
0 votes
0 answers
73 views

Finding exact value with a quotients of products of random values

Sorry for the haphazard title: really not sure what this should be called Suppose we have a set of $z$ random values $S = r_1, \dots, r_z$ drawn from $\mathbb{Z}_N$ (where $N$ is some large prime). ...
Dave's user avatar
  • 149
-3 votes
1 answer
78 views

Explanation of Cantor's diagonal argument? [closed]

I struggled to understand the Cantor's diagonal argument, but I have some problems comprehending the following: By construction, $s$ differs from each $s_n$, since their $n^{th}$ digits differ (...
Ivaylo Toskov's user avatar