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....
13
That a formula is not provable can essentially be done in two ways. With some luck we might be able to show within type theory that the formula implies one which is already known to be not provable. The other way is to find a model in which the formula is invalid, and this can be quite hard. For example, it took a very long time to find the groupoid model of ...
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 ...
8
The theory of real closed fields (RCF) is complete for the first order theory of real numbers in the language you described. Therefore it is equivalent to checking if RCF proves the formula.
By Tarski's quantifier elimination for RCF this can be computed. Tarski's algorithms complexity is non-elementary and there is a doubly exponential lowerbound for the ...
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
If you look at things from a model-theoretic perspective, the basic ingredients you have are atoms, relations, and functions. Atoms could be modelled using nodes of the graph, and binary relations and single argument functions could be modelled using graphs. If you are willing to allow hyper-edges in your graph, then the remainder of the relations and ...
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 ...
3
I would like to add to Dave Clarke's answer. The binary relations are sufficient to express higher-arity relations and functions (by adding new non-logical symbols if necessary). Hence, if you allow multiple directed edges, which can take on different colors, then this is already sufficient to encode any $L$-structure. Furthermore, this encoding can be ...
Only top voted, non community-wiki answers of a minimum length are eligible
