2022 Developer Survey is open! Take survey.

# Tag Info

Accepted

### To what extent can the mathematics of Reals be applied to Computable Reals?

The real numbers may be characterized in a couple of ways, let us work with the Cauchy-complete archimedean ordered field. (We need to be a bit careful how exactly we say this, see Definition 11.2.7 ...
• 26.4k

### What is the axiomatic (set theory) context of the P vs NP and NP=EXPTIME conjectures?

It's not specified. When there is a serious enough candidate paper purporting to resolve P ≟ NP, a Special Advisory Committee will be formed to decide whether (and to whom) to award the prize. I ...
• 23.5k
Accepted

### Standard reference for basic model theory definitions

Here is one possibility, but other people might use different words. I will use first-order logic as a running example. Language The language is a collection of expressions, which are syntactic ...
• 26.4k
Accepted

### Is it decidable that a computable analytic function over $\mathbb{R,C} ,$ equals $0$

No, it is not decidable. A good heuristic to answer such questions is the following: every computable map is continuous. If you could decide whether $f(x) = 0$ for all $x \in \mathbb{C}$, then the ...
• 26.4k
Accepted

### Decidability of first-order theory of real closed fields with functions

It's undecidable because we can interpret natural numbers (with addition and multiplication). For example, let $Ind(f)$ be the formula: $$f(0)=1 \land \forall x \ \big(f(x)=1 \to f(x+1)=1\big)$$ Now ...
• 21.3k

• 2,470
Accepted

### Is there a way to define dependent types without explicit substitutions internally within agda?

The thing is, the definition is "too" dependent. In order to define the type of substitution or renaming, you need to something like ...
• 231