Questions about set theory

learn more… | top users | synonyms

2
votes
0answers
246 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
103 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
154 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 ...
3
votes
3answers
198 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
181 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
289 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
128 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 | ...
2
votes
1answer
63 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
142 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
252 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 ...
13
votes
4answers
480 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
86 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, ...
5
votes
2answers
887 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
224 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 ...
6
votes
3answers
735 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
1answer
373 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: ...
34
votes
5answers
890 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 ...
49
votes
5answers
2k 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 ...