2022 Developer Survey is open! Take survey.
16 votes
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 ...
user avatar
  • 26.4k
15 votes

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 ...
user avatar
11 votes
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 ...
user avatar
  • 26.4k
7 votes
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 ...
user avatar
  • 26.4k
5 votes
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 ...
user avatar
  • 21.3k
5 votes

Descriptive model theory classification of Counting hierarchy

This is only a partial answer (to the $PSPACE$ characterization), but I don't have the reputation to comment. $PSPACE$ has the following (equivalent) descriptive characterizations: $FO[2^{n^{O(1)}}]...
user avatar
4 votes
Accepted

Proof that the theory of rationals is convex

The key idea here is that for any conjunction of equations $F\equiv u_1=v_1\wedge\ldots\wedge u_k=v_k$, the set $S_F$ is convex in the geometric sense, i.e. for any two points $p,q\in S_F$, all points ...
user avatar
4 votes
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 ...
user avatar
  • 231
2 votes
Accepted

What kind of computational model is the brain?

This is pretty much an open problem and subject to active research. There are a few proposals available. Here are some of the latest ones: Brain computation by assemblies of neurons Christos H. ...
user avatar

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