21

One major application of topology in semantics is the topological approach to computability. The basic idea of the topology of computability comes from the observation that termination and nontermination are not symmetric. It is possible to observe whether a black-box program terminates (simply wait long enough), but it's not possible to observe whether it ...


17

For more uses of forcing (via so-called generic oracles) in complexity theory, see The Oracle Builder's Toolkit (freely available from Fortnow's homepage) by Fenner, Fortnow, Kurtz, and Li. They give a general theory of generic oracles, and show its many applications in complexity. If you're interested in how oracles in complexity are like independence ...


16

The communication complexity of the set disjointness problem is $\Omega(n)$. The communication complexity is a lower bound on the time complexity of testing whether the two instances are disjoint. Imagine Alice stores the data structure for the first set, and Bob stores the data structure for the second set; since they'll have to communicate $\Omega(n)$ ...


14

Our goal is to prove that $\aleph_1 < 2^{\aleph_0}$ in the model $M[G]$, and therefore the Continuum Hypothesis is not true in $M[G]$. This is equivalent to saying that $\aleph_2 \leq 2^{\aleph_0}$. So we need to construct a model $M[G]$ such that there is an injective map $f$ from $\aleph_2$ to $2^{\aleph_0}$ in $M[G]$. Note that each element of $2^{\...


11

For an excellent introduction to forcing in set theory, there's Timothy Chow's famous USENET post "Forcing for dummies" as well as the more formal paper that arose from it, "A beginner's guide to forcing".


9

Set theory is doing you some harm here and the sooner you liberate yourself from it the better it will be for your understanding of computer science. Forget the intersections and unions. People get this idea that $\forall$ and $\exists$ are like $\bigcap$ and $\bigcup$, which is the sort of thing the Polish school was doing a long time ago with Boolean ...


9

For uses of forcing like techniques in proof complexity you might want to look at: M. Ajtai. The complexity of the pigeonhole principle. In Proceedings of the 29th Annual IEEE Symposium on Foundations of Computer Science, White Plains, NY, 1988, pp. 346–355; and M. Ajtai. The complexity of the pigeonhole principle. Combinatorica 14 (1994), no. 4, 417–433. ...


9

It makes sense in some contexts in mathematics to consider strings or languages over infinite alphabets. For instance, this concept is used in the strong version of Higman's lemma. But a finite automaton requires a finite alphabet, and only finitely many symbols can actually appear in a single regular expression. So, specifically for the context of regular ...


9

Short answer: yes! You don't need that much machinery to get the proof to go through. One subtlety: it seems on the face of it that there is a use of the excluded middle: one builds a set $D$ and a number $d$, and shows that either $d\in D$ or $d\not\in D$ which leads to a contradiction. But there is a lemma, true in intuitionistic logic, that states: $$ \...


8

The usual convention in formal languages and automata theory is that an alphabet is finite. However, there are certainly some cases where it's useful to think of an alphabet being infinite. For example, if one wants to define a universal Turing machine that can simulate the computations of any other Turing machine, then it's useful to have in mind some ...


7

the Erdos sunflower conjecture seems to be very difficult after now over a half century(!) of being open. youve already listed some of the very best and most recent refs on the subj that would be very hard to beat (Alons recent paper, Juknas book on combinatorics). the Alon paper is highly notable for newly linking the conjecture to lower bounds on matrix ...


6

You did not say why you want a formalization, but presumably you want to do things with it, for instance prove properties of dictionaries and operations on them. In fact, your question can be understood in two ways: you want a mathematical description of dictionaries, or you want a computer formalization of dictionaries. For a computer formalization have a ...


6

There are numerous ways of formalizing set theory: ZFC uses first-order logic and a primitive relation $\in$ NBG uses first-order logic, a primitive relation $\in$, and a primitive predicate $S$ Church's type theory is multi-sorted and uses infintely many types Type theory is similar to set theory, but not quite the same Second-order arithmetic, through ...


6

There is a really interesting approach to a set theory-like foundational system that I am rather fond of: Grue's Map Theory. The basic idea is to take the (untyped!) $\lambda$-calculus as a base foundation, and to represent a set $S$ as a term $f$ such that $$ S=\{f(x)\mid x\in\Phi\}$$ where $\Phi$ represents the well founded functions ($x\neq\bot$ in the ...


6

This is not an answer to the exact question you pose, because the $n$ is different and the set instances are not separate. But there's a data structure for representing subsets of an $n$-element universe that allows addition of another subset $S$ in time $\tilde O(|S|)$ time and finding the smallest element at which two sets differ in time $O(\log n)$, in my ...


5

Some of the work of Olivier Finkel seems related to the question---though not necessarily explicitly about the Axiom of Choice itself---and in line with Timothy Chow's answer. For instance, quoting the abstract of Incompleteness Theorems, Large Cardinals, and Automata over Finite Words, TAMC 2017, one can construct various kinds of automata over finite ...


5

(Note: This answer works for most any consistient theory, not just $ZFC$.) We will define a machine $p$ based on the universal algorithm. $p$ does a search, looking for a string that represents a proof of a statement of the form "not ($p$ halts and outputs $n$)" (note that this requires quining, since it is self-referential), for some numeral $n$, such that ...


4

see also Forcing in proof theory by Avigad, 30pp, 2004. he cites BGS75 but not in detail. there is some reference to Scott/Solovay as a rephrasing of forcing into boolean-valued models. Ideas in forcing have been influential in computational complexity; for example, the separation of complexity classes relavitized to an oracle (e.g., as in BGS75) can ...


4

If I read you correctly, the intuition you have in mind goes like this: Suppose we have a program $P$, which takes a function as an argument. Further suppose that we have two functions $f$ and $g$, such that $f$ terminates on a subset of the inputs $g$ terminates on, but agrees with $g$ whenever they both terminate. Now, if $P\;g$ is partially correct, ...


4

I interpret your question as follows: Let $M$ be a minimal dominating set (MDS). Then there exists a minimal vertex cover (MVC) $C$ such that $M \subseteq C$. The answer is negative. Consider the line $a - b - c - d$ and the MDS $M=\{a,d\}$. The edge $(b,c)$ isn't covered so either $b$ or $c$ need to be added to $M$ to yield an MVC. However, minimality ...


4

Since there is no single minimal dominating set nor minimal vertex cover, I interpret your question as: There exist one minimal dominating set $D$ and one minimal vertex cover $C$ such that $D \subseteq C$. No. If by any graph you also consider non-connected graphs, then you have a trivial counterexample in $G=(V,E)$ with $V\neq\emptyset$ and $E=\...


4

If I'm not mistaken, the case you specify (with $k =2$, $k_i = 3$) is in P. Note that the condition $|S \cup S'| \le 3$ is equivalent to saying that $S, S'$ intersect (since $k=2$). Thus, if you think of the $S_i$ as vertices, then the constraints specify a graph $G$, and your problem reduces to finding a graph $H$ such that $G$ is the line graph of $H$. ...


4

The 2004 Gödel Prize was shared between the papers: The Topological Structure of Asynchronous Computation. By Maurice Herlihy and Nir Shavit, Journal of the ACM, Vol. 46 (1999), 858-923 Wait-Free k-Set Agreement Is Impossible: The Topology of Public Knowledge. By Michael Saks and Fotios Zaharoglou, SIAM J. on Computing, Vol. 29 (2000), 1449-1483. Quotes ...


4

Behavior of a reactive system is often modeled using infinite structures ( infinite traced and infinite computation trees) and their Temporal properties (safety and liveness properties) have also been characterized using topology. Defining Liveness Alpern and Schneider Safety and Liveness in Branching time Manolios et. al.


4

This answers question (2): The greedy heuristic for Set Cover / Maximum Coverage always picks the set which contains the maximal number of uncovered elements. Assuming your modification for the heuristic is picking the set which greedily increases the solution profit, you might end up in a lousy approximation ratio. Consider the following example: $$A = \{...


3

I am not sure if these results are known. If you define the $t$-thick upper (or lower, does not matter) shadow of $A_k$ as the sets of one level higher (resp. lower) that contain (resp. are contained in) at least $t$ sets from $A_k$, then what you ask for is the $(k+1)/2$-thick upper shadow. As far as I know it is open to determine the size of the smallest $...


3

I will attempt to write the same answer as Neel with fewer technicalities (and therefore not really correct). By the way, you are using very strange terminology, which I will avoid. For each type $T$ appearing in a programming language we can define a partial order $\leq_T$ as follows: on the integers we define $p \leq_{\mathtt{int}} q$ to mean: "if $p$ ...


3

Regarding question 1): the variable $Y$ must not appear in $Y$, indeed it needs to be unconstrained. If you want to have any hope of the lhs being equal to the rhs, certainly you should have the same number of free variables on each side, which is impossible if $Y$ gets captured in $T$. The intuition is that $\exists T$ should be equal to the infinite ...


2

My impression reading this question is that no suitable example of a problem that requires more than just PA (let alone ZF) has been given, and the excellent answer by Timothy Chow explains why it's so hard to find examples. However, there are some examples of TCS extending beyond the realm of arithmetic, so I thought I would give a theorem that requires ...


Only top voted, non community-wiki answers of a minimum length are eligible