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 ...
- 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 ...
- 23.5k
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 ...
- 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 ...
- 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 ...
- 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)}}]...
- 136
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 ...
- 2,470
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
...
- 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. ...
- 4,011
Only top scored, non community-wiki answers of a minimum length are eligible