Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Different types of non-constructive proofs

Jencel Panic (Jul 29 2024 at 10:16):

Non-constructive proofs are proofs that use the law of excluded middle, but it seems interesting to me if there exist some kind of list of different types of non-constructive proofs. Like, how can you prove $P$ non constructively.

We have proof by contradiction which would be something like:

$\lnot P \to (Q \lor \land Q)$

Then, there are many elementary proofs such as this one that work by deriving the statement from a tautology:

$(Q \lor \lnot Q) \to P$

We have proof by contrapositive that use $(A \to B) \leftrightarrow (\lnot A \to \lnot B)$. The general formula of this proof seems to be to to show that $P \leftrightarrow P'$ using excluded middle and then prove $P'$.

I guess there is no way to have an exhaustive categorization, but still it's interesting for me what is the logical forms of constructive proofs?

Nathanael Arkor (Jul 29 2024 at 10:20):

It's worth bearing in mind that LEM is not the only non-constructive axiom. For instance, the axiom of choice is another common non-constructive axiom.

Jencel Panic (Jul 29 2024 at 10:54):

I think that the axiom of choice implies LEM.
https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/S0273-0979-2016-01556-4.pdf

Nathanael Arkor (Jul 29 2024 at 12:54):

Yes, but this doesn't mean that every use of choice is a use of LEM.

Chris Grossack (they/them) (Jul 29 2024 at 15:29):

There are TONS of nonconstructive principles like this! They correspond to "intermediate logics", that is logics which are stronger than full constructive logic, but weaker than full classical logic.

For instance, we can assume De Morgan's Law (recall $\lnot(P \land Q) \to \lnot P \lor \lnot Q$ is not intuitionistically provable, yet we cannot prove LEM using this). This turns out to be equivalent to "Weak Excluded Middle" which says that for every $P$, we have $\lnot P \lor \lnot \lnot P$.

There are other principles too. For instance the Weak Limited Principle of Omniscience which says WLEM only holds in some contexts. You can also ask for Markov's Principle, which says that double negation elimination holds in some contexts.

There are TONS of intermediate logics (indeed, uncountably many. See Bezhanishvili and Bezhanishvili's excellent survey paper Jankov Formulas and Axiomatization Techniques for Intermediate Logics). These have also been studied in the context of topos theory, to recognize when a topos satisfies some intermediate principle and to build a largest subtopos satisfying that principle (analogous to the double negation subtopos). See, for instance, Caramello's Topologies for intermediate logics.

Jencel Panic (Aug 03 2024 at 12:05):

Thanks, that is very interesting. So, the correct way to state it is that non-constructive proofs are proofs that rely on principles that are not valid under the BHK interpretation and constructive proofs are ones that don't rely on such principles.

Chris Grossack (they/them) (Aug 03 2024 at 14:54):

Mmmm... I think "non-constructive proof" is a term whose exact meaning varies slightly depending on who you ask. For instance some people accept MP and some people don't. This is one of the big issues with first getting into this stuff: whenever you're reading the literature you have to be conscious of exactly what the author means by "constructive"!

Chris Grossack (they/them) (Aug 03 2024 at 14:55):

Thankfully I think this is slowly starting to standardize into something like [[neutral constructive mathematics]], but maybe that's just the crowd I hang out with

Jencel Panic (Aug 03 2024 at 15:02):

That's interesting (Markov's principle) I guess the question of what can be constructed and what cannot is debatable.

Chris Grossack (they/them) (Aug 03 2024 at 15:02):

Martín Escardó actually polled a bunch of people on mastodon to see if their thoughts on MP (and constructivity more broadly). Here's the top of the thread:
https://mathstodon.xyz/@MartinEscardo/112633451078625596

Madeleine Birchfield (Aug 03 2024 at 15:36):

Just as an aside, if there is a non-constructive axiom I would accept it would be LPO because then I would get a set of real numbers which behaves very much like the real numbers taught in high school algebra. I find it somewhat hard to tell the average person "all your high school textbooks are wrong because they assume trichotomy and state that Gaussian elimination, the usual quadratic formula, the fundamental theorem of algebra etc hold for the real numbers, and that every real number has an infinite decimal representation". Maybe my opinion on this will change if constructive mathematicians start petitioning school systems around the world to start teaching some neutral constructive analysis in high school algebra, or if school systems no longer end up teaching the real numbers to the general public.

I don't have a problem with not accepting the full excluded middle, or the fan theorem, etc because formal logic, set theory, locales, topological spaces, formal topologies, uniformly continuous functions, the Heine-Borel theorem, etc aren't taught to the general public in high school algebra.

Morgan Rogers (he/him) (Aug 08 2024 at 10:44):

@Madeleine Birchfield it's fascinating to me that your attitude to non-constructive axioms is determined by sociological considerations like this. I haven't seen enough people think about that kind of influence on their reasoning principles.

Notification Bot (Aug 09 2024 at 09:08):

5 messages were moved from this topic to #theory: philosophy > epistemology and non-constructive principles by Morgan Rogers (he/him).

James E Hanson (Aug 09 2024 at 18:31):

Jencel Panic said:

Thanks, that is very interesting. So, the correct way to state it is that non-constructive proofs are proofs that rely on principles that are not valid under the BHK interpretation and constructive proofs are ones that don't rely on such principles.

The problem I have with citing the BHK interpretation is that I haven't seen what I would consider to be a solid mathematical justification of the rules of intuitionistic logic in particular from something that intuitively resembles the BHK interpretation. BHK doesn't really give a complete account of what statements like $P \to Q$ and $\forall x P(x)$ mean. It says that a proof of $P \to Q$ is a procedure that converts a proof of $P$ to a proof of $Q$, but what is the justification for how we know that a given procedure actually accomplishes this? Presumably one would need to prove it constructively, but BHK is supposed to be the explanation of what it means to prove something constructively.

I feel like this is most acute in the context of negation. In BHK, a proof of $P \to \bot$ is really just a promise (justified in some unspecified way) that there will never be a proof of $P$. If I'm a constructive mathematician, then I both believe that $\mathsf{LEM}$ is never going to have a constructive proof and know formal justifications of this, so why can't I then conclude $\neg \mathsf{LEM}$ under the BHK interpretation? Why isn't that a permitted justification?

Obviously there are answers to this in practice (like wanting to have a system that can handle various, possibly classical semantics), but that's shifting to a different justification for deciding what should or shouldn't be considered constructive.

Patrick Nicodemus (Aug 09 2024 at 19:19):

That's an interesting point. After thinking about this my conclusion is that some formal separation between theory and metatheory is necessary to get out of this. If you are working in an intuitionistic formal logic, there is no reason to think that "Assume $A$" should be taken to mean "Assume that we have proved $A$". Intuitionistic mathematicians refer to "evidence for $A$" or "proofs for $A$" so I can understand why you call this contradictory, but I think if we take what you are saying to its logical endpoint then it amounts to denying people the ability to reason about hypotheticals. In this case you would be trying to do a gymnastic leap out of your system of deduction in order to pass to the metatheory, where you reason that your system cannot prove this, and so it should be false.

Patrick Nicodemus (Aug 09 2024 at 19:26):

The BHK interpretation justifies certain proof rules on the grounds that they can be interpreted as manipulation of evidence, but I don't think it follows from this that any proposition which does not follow from the proof rules is false, only that we should not assert it. For example, it would be weird for a constructivist to claim that the Continuum hypothesis is both false and not false as neither it nor its negation can be proven. It seems like not a very reasonable philosophical position to say that someone should affirm the negation of everything they cannot prove. There is a difference here between hypothetical evidence for a proposition and actual evidence for a proposition.

Patrick Nicodemus (Aug 09 2024 at 19:30):

The kind of reasoning you're describing is more like what happens in logic programming with the negation - https://arxiv.org/pdf/cs/9301109

Patrick Nicodemus (Aug 09 2024 at 19:35):

It's a very informal explanation so it's easy to find holes in it. What would be your justification for intuitionistic logic?

James E Hanson (Aug 09 2024 at 21:02):

@Patrick Nicodemus Obviously people who identify as constructive mathematicians are not a monolith, but on a couple of occasions I've seen constructive mathematicians justify their belief that LEM is false in some objective sense on the basis of metamathematical considerations like Gödel's incompleteness theorem. Brouwer and Bishop both engaged in this kind of reasoning at times. For instance, Bishop said this in Foundations of constructive analysis:

Of course, if Fermat's last theorem is proved tomorrow, we shall probably still be able to define a fugitive sequence $\{n_k\}$ of integers. Thus it is unlikely that there will ever exist a constructive proof that for every real number $x \geq 0$ either $x > 0$ or $x = 0$. We express this fact by saying that there exists a real number $x \geq 0$ such that it is not true that $x > 0$ or $x = 0$.
In much the same way we can construct a real number $x$ such that it is not true that $x \geq 0$ or $x \leq 0$.

The nLab article about constructive math mentions Bishop's usage of the word not (with italics) and says that it should be interpreted in the sense of talking metamathematically, but I don't really buy this as an explanation of Bishop's philosophy of math or as an explanation of a lot of constructive mathematicians' philosophy of math. A fair number of constructive mathematicians, like Bishop, have a realist bent and some of them will positively assert things like 'LEM is false.' I think that on some level my overly strong interpretation of BHK is a reasonable explanation of the thought process that leads to such statements. At the very least I just think this kind of issue means that BHK by itself can't be cited as a definition of constructive math, which I think you would agree with given your statement about it being an informal explanation, but more specifically it definitely can't be used to resolve questions like 'Is Markov's principle constructive?' All or essentially all constructive mathematicians think that induction on the natural numbers is constructive, but this is not directly justifiable from BHK, which is just about (first-order) logic. If Edward Nelson had been a constructive mathematician, I'm sure he would have gone around saying that induction isn't constructive because of his belief that it isn't predicative.

What would be your justification for intuitionistic logic?

I'm not entirely sure to be honest. I'd have to think about it.

Madeleine Birchfield (Aug 09 2024 at 21:21):

I think Martin Escardo proved that the BHK interpretation of Brouwer's continuity principles is false. So I don't know why the BHK interpretation has Brouwer's name in it, because Brouwer never seemed to have believed in the BHK interpretation like he did in his continuity principles.

James E Hanson (Aug 09 2024 at 21:26):

@Madeleine Birchfield Do you know a reference for this?

Madeleine Birchfield (Aug 09 2024 at 21:26):

Patrick Nicodemus said:

What would be your justification for intuitionistic logic?

It's the internal logic of a Heyting category, and many categories found in the real world are Heyting categories and not Boolean, and it's worth doing mathematics using the internal logic of a category.

Also, for those interested in reverse mathematics, intuitionistic logic would also be interesting, to see the hierarchy of axioms from neutral constructivism all the way to full excluded middle.

Madeleine Birchfield (Aug 09 2024 at 21:27):

James E Hanson said:

Madeleine Birchfield Do you know a reference for this?

Martin Escardo's paper is found here:

https://www.cs.bham.ac.uk/%7Emhe/papers/escardo-xu-inconsistency-continuity.pdf

Madeleine Birchfield (Aug 09 2024 at 21:32):

As for the origin of the BHK interpetation, the nLab credits Kolmogorov (1932), Heyting (1956), and Troelstra (1969) who formulated the BHK interpretation, and it was Troelstra who named it the "BHK interpretation".

Kevin Carlson (Aug 09 2024 at 22:10):

James E Hanson said:

Madeleine Birchfield Do you know a reference for this?

David McCarty definitely said this [depending on what antecedent you intended for "this"] in his lectures on intuitionistic logic, namely that Brouwer never wanted a mechanistic interpretation for his logic at all, but that his successor Heyting finally supplied it (maybe not even while Brouwer was alive? I don't know the dates.)

James E Hanson (Aug 09 2024 at 22:17):

@Kevin Carlson I just meant the Escardó-Xu result, but thanks.

Madeleine Birchfield (Aug 15 2024 at 14:35):

In foundations without the axiom of choice, the BHK interpretation of logic is useful to distinguish between existence of a structure and having a choice of structure; the latter is a stronger condition that is usually not provable from the former without the axiom of choice.