Questions tagged [set-theory]
Questions about set theory
39
questions
4
votes
0answers
102 views
On the interpretation of coinduction in type theory
The notion of (co)datatype can be modeled satisfactorily in category theory as fixed-points of polynomial functors. Then, (co)induction principles are derived from initial algebras/terminal ...
0
votes
0answers
58 views
Faster than linear set intersection
Is there a probabilistic data structure, such as the bloom filter, for which we could perform intersection superlinearly (at the cost of false positives)?
(I only know of a O(n) time complexity set ...
5
votes
2answers
414 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 ...
3
votes
1answer
222 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 ...
9
votes
1answer
258 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 / ...
6
votes
1answer
352 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 ...
1
vote
0answers
457 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 ...
1
vote
0answers
80 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 ...
7
votes
2answers
540 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 ...
8
votes
0answers
186 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 ...
7
votes
2answers
336 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$....
4
votes
3answers
312 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 ...
8
votes
3answers
747 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. ...
15
votes
3answers
458 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 ...
1
vote
1answer
209 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 ...
1
vote
1answer
92 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 ...
0
votes
0answers
70 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).
...
-3
votes
1answer
73 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 (...
7
votes
1answer
1k 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 ...
4
votes
3answers
274 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=...
1
vote
1answer
612 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 $\...
2
votes
0answers
371 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 ...
0
votes
1answer
551 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 ...
5
votes
1answer
211 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 ...
4
votes
3answers
768 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 ...
1
vote
2answers
215 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 $...
1
vote
2answers
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?
6
votes
1answer
138 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} ...
2
votes
1answer
100 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 ...
7
votes
1answer
155 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$ ...
11
votes
1answer
400 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 ...
15
votes
4answers
673 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 ...
1
vote
0answers
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-...
9
votes
2answers
1k 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 ...
2
votes
1answer
412 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 ...
11
votes
3answers
1k 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 ...
0
votes
2answers
694 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:
...
37
votes
5answers
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 ...
67
votes
7answers
3k 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 ...
