# Tag Info

Accepted

### What concretely does it mean to "do mathematics in a topos X"?

If one is being precise, working a topos $\mathcal{E}$ means that we are going to prove some a statement in some formal system and then interpret that statement/proof into $\mathcal{E}$ to conclude ...

### What concretely does it mean to "do mathematics in a topos X"?

For a quick example, let me present a simple application. The starting point will be that in intuitionistic logic, you have a tautology: $\lnot \lnot \lnot p \leftrightarrow \lnot p$. Now, to see ...
• 21.2k
Accepted

### What is an 'effective' encoding?

Computability is not always defined using natural numbers. For instance Turing machines work with tapes, and the natural contents of those tapes are strings, collections of which are called languages. ...
• 4,223

### What is an 'effective' encoding?

There is no and there cannot be any a formal definition of this. For example, take for $D$ the set of graphs. There are many possible encodings of a graph as a natural number: for example, you could ...
Accepted

### Is ZFC's Wikipedia article accurate about the redundancy of the axiom schema of specification?

Using $\sf{ZFC}$ as a metatheory, we can construct a model of $\sf{ZF}$ minus Specification, where Replacement is formulated as in $\sf{REP}$ which does not immediately imply Specification. Moreover, ...
• 2,191

### 'The' Halting Problem or Many Halting Problems?

There is a straightforward bijection between strings and natural numbers, so any algorithm on natural numbers can also be regarded as an algorithm on strings. Or, to put it another way, while you can ...
• 5,449
### Can $\exists$ be transformed into enumeration in the case of a finite domain?
Keep in mind that all quantifications are unbounded in single-sorted first-order logic (which ZF is based upon): formally, $$\exists w\in\{u, v\}. a \in w$$ is shorthand for \exists w. w \in \{u, v\}...