Inferentialism and the completeness of geometry

The Quinean criterion for existential commitment is that we incur existential commitment precisely by affirming existentially quantified sentences. But what’s an existential quantifier?

The inferentialist answer is that an existential quantifier is anything that behaves logically like an existential quantifier by obeying the rules of inference associated with quantifiers in classical logic.

Here is a fun little problem with the pairing of the above views. Tarski proved that, with an appropriate axiomatization, Euclidean geometry is complete and consistent, i.e., for every geometric sentence ϕ, exactly one of ϕ and its negation is provable from the axioms. Now let us stipulate a philosophically curious language L^*. Syntactically, the symbols of L^* are the symbols of L but with asterisks added after every logical connective, and the sentences are of L^* are the sentences of L with an asterisk added after every connective and predicate. The semantics of L^* are as follows: the sentence ϕ of L^* means that the sentence of L formed by dropping the asterisks from ϕ is provable from the axioms of Euclidean geometry.

Inferentially, the asterisked connectives of L^* behave exactly like the corresponding non-asterisked connectives of L.

Consider the sentence ϕ of L^* that is written ∃^*x(x=^*x). This sentence, by stipulation, means that ∃x(x=x) is provable from the axioms of Euclidean geometry. According to the Quinean criterion plus inferentialism, it incurs existential commitment, because ∃^*x, since it behaves inferentially just like an existential quantifier, is an existential quantifier. Now, it is intuitively correct that ∃^*x(x=^*x) does incur existential commitment: it claims that there is a proof of ∃x(x=x), so it incurs existential commitment to the existence of a proof. So in this case, the inferentialist Quinean gets right that there is existential commitment. But rather clearly only coincidentally so! For now consider the sentence ψ that is written ∀^*x(x=^*x). Since ∀^*x behaves inferentially just like ∀x, by inferentialist Quineanism it incurs no existential commitment. But ψ means that there is a proof of ∀x(x=x), and hence incurs exactly the same kind of existential commitment as ϕ did, which said that there was a proof of ∃x(x=x).

What can the inferentialist Quinean respond? Perhaps this: The language L^* is syntactically and inferentially compositional, but not semantically so. The meaning of p∨^*q, namely that the unasterisked version of p∨^*q has a proof, is not composed from the meanings of p and of q, which respectively mean that p has a proof and that q has a proof. But that’s not quite right. For meaning-composition is just a function from meanings to meanings, and there is a function from the meanings of p and of q to the meaning of p∨^*q—it’s just a messy function, rather than the nice function we normally associate with disjunction.

Perhaps what the inferentialist Quinean should do is to insist on the intuitive non-inferentialist semantic compositional meanings for the truth-functional connectives, but not for the quantifiers. This feels ad hoc.

Even apart from Quineanism, I think the above constitutes an argument against inferentialism about logical connectives. For the asterisked connectives of L^* do not mean the same thing as their unasterisked variants in L.

A new kind of project

I did something new and fun this fall: I wrote a computer science paper. It's an analysis of the conditions under which a device equipped with a camera and an accelerometer can identify its position relative to two observed landmarks with known positions. Except for a measure zero set of singular cases with infinitely many solutions, there are always at most two solutions for device positions (this was previously known), and I found necessary and sufficient conditions for there to be a single solution. In particular, if the two landmarks are at the same altitude, there is always a single solution, unless the device is at the same altitude as the landmarks.

I implemented the algorithm on a phone (code here). In the screenshot, the markers 1 and 2 are landmarks, identified and outlined in green with OpenCV library code, and then the phone uses their positions and the accelerometer data to predict where the control markers 3 and 4 are on the screen, outlining them in red.

For someone like me who does some philosophy of science, it was an interesting experience to actually do a real experiment and collect data from it.

I am planning at some point to try to implement the algorithm using infrared LEDs under a TV and the accelerometer and infrared camera inside a right Nintendo Switch joycon. To that end, over the last couple of days I've reverse-engineered two of the joycon infrared camera blob identification modes.

Greek mathematics

I think it is sometimes said that it is anachronistic to attribute to the ancient Greeks the discovery that the square root of two is irrational, because what they discovered was a properly geometrical fact, that the side and diagonal of a square are incommensurable, rather than a fact about real numbers.

It is correct to say that the Greeks discovered an incommensurability fact. But it is, I think, worth noting that this incommensurability fact is not really geometric fact: it is a geometric-cum-arithmetical fact. Here is why. The claim that two line segments are commensurable says that there are positive integers m and n such that m copies of the first segment have the same length as n copies of the second. This claim is essentially arithmetical in that it quantifies over positive integers.

And because pure (Tarskian) geometry is decidable, while the theory of the positive integers is not decidable, the positive integers are not definable in terms of pure geometry, so we cannot eliminate the quantification over positive integers. In fact, it is known that the rational numbers are not definable in terms of pure geometry either, so neither the incommensurability formulation nor theory irrationality formulation is a purely geometric claim.

I think. All this decidability and definability stuff confuses me often.