16

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 and Defintion 11.2.10 of the HoTT book.) The following theorem is valid in any topos (a model of higher-order intuitionistic logic): Theorem: There is a ...


15

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 presume that the Special Advisory Committee will decide whether your system of axioms is acceptable. If you assume Z-F with choice, I guarantee you they will take it....


11

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 entities, i.e., finite configurations without any a priori meaning. A language is described by the grammar, which determines which finite configurations are valid ...


7

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 characteristic map $d$ of such a decision procedure, namely $$d : f \mapsto \begin{cases} 1 & \text{if $\forall x \in \mathbb{C} . f(x) = 0$}\\ 0 & \text{...


5

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 we can define the characteristic function of the set of natural numbers using its universality property as a minimal inductive function: $$Ind(h) \land \forall ...


5

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)}}]$, first-order logic with exponentially iterated quantifier blocks. $SO[n^{O(1)}]$, second-order logic with polynomially iterated quantifier blocks. $SO[TC]$, ...


4

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 between $p$ and $q$ are also in $S_F$. Now suppose that $F\Rightarrow G$, where $G$ is a disjunction of equations $x_1=y_1\vee\ldots\vee x_n=y_n$ (note that ...


2

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. Papadimitriou, Santosh S. Vempala, Daniel Mitropolsky, Michael Collins, Wolfgang Maass Proceedings of the National Academy of Sciences Jun 2020, 117 (25) 14464-14472;...


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