Is there a "logical algebraic geometry" based on provability rather than truth?
I have been taking a course in Gödel's Incompleteness Theorems. I have essentially no logical background, but I noticed a striking - although possibly only superficial - similarity between the concept of
enumeration of a relation by a formula in a theory
and the concept of
algebraic varieties being the solutions of polynomial equations.
We say a relation $R\subset \mathbb{N}^r$ is enumerated by an $r+1$-place formula $F(v_1, \dots, v_{r+1})$ in a formal system $S$ iff the following holds:
- If $(n_1,\dots, n_r)\in R$ then there exists $m\in\mathbb{N}$ such that $S\vdash F(n_1, \dots, n_r, m)$;
- If $(n_1,\dots, n_r)\notin R$ then for every $m\in\mathbb{N}$, $S\vdash \sim F(n_1, \dots, n_r,m)$.
This bears a similarity to the case for algebraic varieties, where if $X$ is a hypersurface over any field $k$ (or more generally, perhaps, a scheme) defined by the vanishing of the polynomial $f\in k[x_1, \dots, x_r]$ then for a point $P$ in the larger ambient space,
$$P\in X \iff f(P)=0.$$
There is an important distinction between these cases, however. The case for enumeration is not an "if and only if" statement, as in the case for algebraic geometry; as far as I understand, this is because we're talking about provability of the negation of a formula rather than the negation of provability of a formula (i.e. that the formula is not provable). This seems clearer when e.g. we take
$$F(v_1, \dots, v_{r+1}):= (f(v_1, \dots, v_r) = v_{r+1}).$$
Then $P = (n_1, \dots, n_r)\in X$ (for the geometry case) if and only if $F(P,0)$ is true, whereas $P\in R$ (for the relation case) if and only if $F(P,0)$ is provable in $S$.
Despite these distinctions, it's made me wonder whether this is all just wishful thinking or whether there is some theory of "provability geometry" in the sense that a point $P$ belongs to some kind of "logical geometric object" $X$ when the algebraic formula $f(P) = 0$ is replaced by a logical formula $S\vdash F(P)$ i.e. some kind of "duality" between provability and geometry. Perhaps this can be established using a type of functor of points idea from some category encoding proof-theoretical data into the category of sets.
If such a thing exists,
- Is it a useful thing to study? Does it shed light on any problems, either in algebraic geometry, number theory or logic?
- Do formulas that cannot be proved have any interpretation in this geometric context?
- How does the formal system $S$, and possible replacement of $\mathbb{N}$ with another "environment" (due to my ignorance of logic I'm being a bit vague here) influence such objects?
I would be very grateful for references to anything in a similar vein to this idea. I would also be grateful if anyone can dispel this as idealism!
The concept you describe is a special case of the model-theoretic notion of a definable set. In general, given a language $L$ with a model $M$, a subset $S\subset M^n$ is definable if there exists a formula in $\varphi$ of $n$ free variables such that $M \models \varphi(a_1,...,a_n)$ iff $(a_1,...,a_n)\in S$. Here, you took $S$ to be a relation $R\subset M^n$, and further requied $\varphi$ to be of the form $\exists x \psi (y_1,...,y_n,x)$ for some formula $\psi$.
As for your geometry-provability question the reason in algebraic geometry we have $(a_1,...,a_n)\in S$ iff $f(a_1,...,a_n)=0$ is true, is because we are fixing some ambient model $k$ in which to interpret the sentences. By the completeness theorem, provability means truth in every model, so an algebra-geometric duality between provability and geometry means to ask whether $f$ has solutions over any arbitrary model. This is a very strong requirement, and almost never happens except for very special cases. You will need to fix a set of axioms to restrict what models to consider, and will probably want to extend $f$ to any set of formula than just polynomial equations.
For example over an algebraically closed field, a system of polynomials $f_1,...,f_r$ has a solution iff they do not generated the unit ideal, (this called Hilbert's Nullstellensatz). Generating the unit ideal is equivalent to saying they are consistent in the sense of logic in the language of rings adjoin the constant symbols for $k$ where $k$ is your algebraically closed field, because generating the unit ideal is equivalent to saying the set of formulas $f_1=0,...,f_r=0$ derive the equation $1=0$.
BTW: The notion of a definable set in general is a very important idea in model theory, and there is work aimed at specifically describing the definable sets of specific theories. For example the result that algebraically closed fields have quantifier elimination means every definable set is generated by a finite application of unions, complements and intersections (i.e. definable = constructable). Related to the notion of a definable set is a 'partial type'. If a set is definable, then there is a formula, or if you relax the definition, a set of formulas which cut it out in 'affine space' $M^n$. On the other hand, a partial type $\Sigma$ is a consistent and deductively closed set of sentences. Partial types are so called because they are model theoretic versions of constructions such as ideals in ring theory or Dedekind cuts that describe an 'ideal' element or 'type' of element which may not exist but should exist in some extended setting, e.g. the limit of a Cauchy sequence or a perfect number (which to put in Emmy Noether's original words is) that is the 'greatest common divisor' of that system of elements generating the ideal.
For some exposition of elementary concepts related to this, you may enjoy an expository paper http://math.uchicago.edu/~may/REUDOCS/Zhang,Victor.pdf. Definitely I think model theory is the subject to study if you wish to think about this further.