# Graphing Calculator via Quantifier Elimination
I think it would be interesting to create a graphing calculator (like Desmos)
where you can type expressions including quantifiers. For example:
\\[\\not\\exists z. zz + xz + y = 0\\]
This one would plot a filled parabola.
Evaluation would proceed by quantifier elimination. 
The example simplifies to this: \\[xx - 4y < 0\\]
And that can be easily plotted by a fragment shader.
There are some problems with this idea, of course. Quantifier elimination is known to be in the complexity class DEXPTIME!
And you can't add many features without the problem becoming undecidable.
But even so, I think this is a cool idea.
## Specifics
If I choose to implement this, I will make the equation description language be a simple typed functional language.
The available types would be described by `τ := number | bool | τ -> τ`. (Optionally, add tuples.)
Quantifiers would be higher-order functions of type `(number -> bool) -> bool`, though syntax sugar might be useful.
Functions of type `number -> number -> bool` would be renderable.
Recursion would be disallowed.
---
It might also be useful to have an operation like `something_satisfying : (number -> bool) -> number`.
Since everything eventually becomes a `bool`, this operation could be implemented by translating
\\(\\phi(\\text{something_satisfying}(p), ...)\\) to \\(\\exists x. p x \\land \\phi(x, ...)\\)
Sure, this operation doesn't really return *a* number. But it's useful.
## Quantification over functions?
It might seem natural to allow quantification over functions. But this cannot be allowed.
If it were, trig functions could be defined like this:
\\[
    \\begin{align*}
    & \\exists \\sin. \\exists \\cos. \\\\
    & \\quad \\cos 0 = 1 \\ \\land \\\\
    & \\quad \\sin 0 = 0 \\ \\land \\\\
    & \\quad (\\forall x. \\forall \\epsilon. \\epsilon > 0 \\implies \\\\
    & \\qquad \\exists \\delta. \\delta > 0 \\ \\land \\\\
    & \\qquad \\quad \\forall y. |y - x| < \\delta \\implies \\\\
    & \\qquad \\qquad |(\\sin y - \\sin x) / (y - x) - \\cos x| < \\epsilon \\ \\land \\\\
    & \\qquad \\qquad |(\\cos y - \\cos x) / (y - x) + \\sin x| < \\epsilon \\\\
    & \\quad ) \\ \\land \\\\
    & \\quad \\textit{rest of expression} \\\\
    & \\end{align*}
\\]
(Yes, I'm using the epsilon-delta definition of derivative to describe differential equations.)
If you have trig functions, you can define the natural numbers:
\\[\\text{is_natural}(x) = x \\geq 0 \\land \\exists \\pi. \\pi > 3 \\land \\pi < 4 \\land \\sin \\pi = 0 \\land \\sin \\pi x = 0\\]
And then you can use standard Godelian tricks to create a paradox.
So no, this is not possible.

# Introduction
I tend to be somewhat secretive with the stuff I'm thinking about. 
If I don't feel a project is "ready", I don't share it.
But this tends to mean most of my projects never see the light of day.
So in 2022, I made a resolution to share my ideas more freely. 
Hence this book.
If you want to work on one of these ideas, go for it! But please credit me if it makes sense to do so.
And if one of my programming ideas has already been done, please point me at the project!

# Summary
- [Introduction](./intro.md)
- [Graphing Calculator via Quantifier Elimination](./quant_elim.md)

[book]
authors = ["finegeometer"]
language = "en"
multilingual = false
src = "src"
title = "My Ideas"
[output.html]
mathjax-support = true

.git
.DS_Store
book