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