Are existence proofs outlawed in multi-valued logics?

[nomadreid]

TL;DR

An intuitionist logic (excluding the excluded middle) obeys the existence property (why?) and hence is constructive. That implies that admitting more than two truth values eliminates existence proofs, including axioms allowing for existence proofs by some other means than by contradiction. But I do not see the connection.

First, is my assumption that all consistent multi-valued logics obey the principle of explosion from a false proposition correct?
If so, how would one prove that?

(I assume it is, because if not, then by the definition of intuitionist logic by Wolfram Mathworld http://mathworld.wolfram.com/IntuitionisticLogic.html, the frequently made assertion that a fuzzy logic is automatically intuitionist would be false.)

Therefore, the addition of a third truth value assigned to the interpretation of at least one sentence in a theory would, in itself, be incompatible with an axiom which allowed a conclusion preceded by an existence quantifier (and without the assignment of the variable to a constant).

From the websites that I have looked at, the link between a third truth value and the omission of this class of axioms is apparently supposed to be evident. Sorry, but could someone make this link explicit for me?

(It appears to me that an existence proof need not invoke proof by contradiction; for example, the Power Set Axiom and the Axiom of Choice and a lot of the Large Cardinal Axioms are not constructive, as far as I understand. Or is this way off the mark?)

 

[mathman]

(I read summary only). If you have multivalued logic and prove one value is false, then any other may be true, so you still haven't proved a particular value.

 

[nomadreid]

mathman, thanks for the answer, but as I mentioned in the full text of my question, there are ways to prove existence without using proof by contradiction, which is the only case which your answer covers, and these others ways are not always constructive.

 

[Stephen Tashi]

Therefore, the addition of a third truth value assigned to the interpretation of at least one sentence in a theory would, in itself, be incompatible with an axiom which allowed a conclusion preceded by an existence quantifier (and without the assignment of the variable to a constant).

In modal logic, what's the interpretation of a statement preceeded by an existence quantifier? For example, if the truth values are True, False and Maybe, what does $\exists x: A(x)$ mean? Can that statement have the truth value Maybe? Then it might mean: It is True that there exists an x such that A(x) is Maybe. Or it might mean Maybe it's the case that there exists x such that A(x) is True. Or it might mean other combinations of True and Maybe.

 

[nomadreid]

Good question, Stephen Tashi. I hope that other contributors will chip in, either adding to or correcting my attempt to answer. First, from your other remarks, I infer that you meant "three-valued" rather than "modal" (although a similar question for modal logics would also be interesting; to quote Michael Ende, "But that is another story and shall be told another time.") Secondly, this depends on which logic you adopt: for example, according to https://plato.stanford.edu/entries/logic-manyvalued/, in Łukasiewicz and Gödel logics, the truth value of ∃x A(x) is the supremum of all the relevant truth degrees of A(x).

 

[SSequence]

I don't know the answer to your question ofc since I don't know enough logic. I don't even understand PA rigorously (but hope to at some point later on...). However, I have some rudimentary understanding of these issues, mostly due to thinking of questions that are related to these (over the years).

I don't understand your question fully (and even if I did, likely I wouldn't be able to answer it). However, since the question seems to relate to intuitionistic issues more or less, I think I can give a few remarks (possibly helpful).

To make things concrete, let's take the case of HA. Unless I am mistaken (certainly possible), the questions/problems that can be posed in HA and PA are the same. However, a few things that would be allowed in PA would definitely not be allowed in HA I believe.

For example:
(a) In general, we can't start from the assumption:
A or ~A
and arrive at some conclusion B (using the rules of inference in HA) ... and then assume B to be true.

In PA, we would be able to do this. Because there A is (always) either true or false there.

(b) Similarly, if we started from:
A
and came to the conclusion (using the rules of inference in HA):
~A
then we can't assume A to be false. Again, in PA we would be able to do this.

(c ) As a third example, from:
∃x [P(x)]
we would normally derive:
~∀x [~P(x)]
However, I do not think this would be allowed (as a universally valid inference) in HA.

=====================

Now, to me, one conceptual issue here is why this isn't allowed. From intuitionist perspective (in the given context), the reason is due to "possible" existence of statements that are absolutely unsolvable[*1] (the "third" truth value ... let's write it U). Note the word "possible" in the last sentence (it is mandatory if we are being careful). For example, once again sticking to HA, the reason for the examples (a),(b),(c) above is to account for this possibility. Meaning the person reasoning in this way would say that there might be (first-order) number-theoretic statements that are simply neither provable nor disprovable "by any possible (valid) means" (informal phrase).

Consider each of the examples above separately. In (a) above if we already knew that A doesn't have the value U, then of course we could assume B to be true. A similar remark applies to (b).

For (c), assuming the quantification to be over natural numbers, the reason for concern is that even if we are sure that every single one of these statements P(i) below is either true or false:
P(0)
P(1)
P(2)
P(3)
...

The point is that how can we be sure that ∃x [P(x)] is not U. One way to think about it might be to consider the (gold-bach like) statements that are independent from current set-theory+LCA. Even if each of the individual P(i)'s have a definitive truth value trivially, determining the truth-value of ∃x [P(x)] can be quite difficult. The perspective here is that how does one know that some of the (independent) statements don't have the value U. But note that this is just one (rough) way of thinking about this.

If we are sure that ∃x [P(x)] either false or true, then indeed we can derive ~∀x [~P(x)] as a conclusion.

=====================

Another thing is that a similar issue occurs on all levels. So, in this sense, the intuitionistic issues have a very general nature. This is a very rough example that I thought of some time ago. Hopefully though, it conveys some of what I am trying to say.

Consider a statement of the form (obviously we can't write it in PA, so we would have to assume something stronger):
∀x<ω_1 [P(x)]
Now under usual classical maths this kind of statement would be taken as either true or false. Once again, even if we know all P(i)'s to be either true or false, one might potentially raise the concern regarding the acceptance of the whole statement ∀x<ω_1 [P(x)] as either true or false.[*1] As I understand, this phrase is used in different contexts at times. In a way this is natural I suppose, since it depends on what collection of questions/problems one considers. For example, in set-theory discussion perhaps one might encounter it in relation to CH (perhaps as a candidate for a possible example of being such a statement, due to its independence).

But anyway, here the given context is very highly restricted.

 

[nomadreid]

Thank you for your reflections, SSequence.

First, to your remarks labeled (a),(b), and (c). I have no problem with the fact that proof by contradiction is not valid in intuitionistic systems except in certain limited cases, or that the relationships between the universal and existential quantifiers through negation, as used in classical systems, are not valid in intuitionistic systems except in certain limited cases. Also it is clear that there are some three valued logics in which the third truth value can essentially be taken as "undecidable" out of classical logic.

More to the point of my question is your example of Heyting Arithmetic. The way the axioms of PA use universal quantifiers except for the existence of 0 , and with outlawing the equivalence of ∃x and ~∀x~ or of ∀x with ~∃x~ ,there seems no way to get a conclusion with the existential quantifier that isn't constructive.

However, departing from HA, I do not see that in every axiom system, all the non-constructive derivations of existence (e.e., with applications of AC or the existence of 0# using a suitable large cardinal axiom) must necessarily use a proof by contradiction or the quantifier equivalences just mentioned, so I do not see why the definition of an intuitionistic system (invalidity of the Excluded Middle) must necessarily lead to a system being constructive.

 

[SSequence]

I think you are much more learned to answer your own question. Anyway, here are few more thoughts after thinking a bit about your reply.

Speaking qualitatively (in a broad/rough sense), apparently it doesn't seem that "constructive" [say in the sense of algorithmic or possibly in even some broader sense] has a direct relation with the non-assumption of LEM. Thinking a bit after your reply, it seems broadly that when you have a system we can pose certain problems/questions within it. In a generic sense, the non-assumption of LEM really seems to be something very broad which, in some way, would be related to the collection of questions that could be posed in this system (call the collection of questions Q). Very roughly, what I mean by previous sentence is that we would expect the following two possibilities for some arbitrarily chosen subset R (of Q):
i-- every statement in R is definitively supposed to be either true or false
ii-- we can not assume every statement in R to be either true or falseCall the collection of answers proved in the system as A (note that A⊆Q by our definition). What this assumption or non-assumption of LEM would seem to affect is how A would vary. By "answers", I just mean the theorems proved in the system when we assume a certain mode of reasoning.

(a) As an example, in the case of PA and HA, the collection of questions Q is the same but collection of answers for HA is a sub-set of collection of answers for PA. It should be a strict sub-set.

(b) For another example, consider three different systems:
1-- PA
2-- ACA_0
3-- current set-theory

I am quite less familiar with (ii) here, but basically if we denote the collection of questions that can be posed in 1,2,3 as Q1,Q2,Q3 respectively ... then I think we would have:
Q1⊂Q2⊂Q3
I am assuming here that when we encode the (finite) numbers with appropriate sets in (3), then the statements about these encoded sets can be considered statements about numbers in (1). Similarly some kind of basic encoding for all questions in (2). Now if we consider the answers we have:
A1⊂A2⊂A3

And furthermore we have:
(Q1 ∩ A1) ⊂ (Q1 ∩ A3)
(Q1 ∩ A1) = (Q1 ∩ A2)
You would obviously be aware about the first. As for second equality, I think I remember reading this (but not fully sure about it ... you might want to check). But anyway, this is kind of besides the point here perhaps.

Now all these systems (1),(2),(3) basically use LEM (I suppose?). However, it seems that one could consider a system that, say, poses a collection of questions Q such that:
Q2⊂Q⊂Q3
A2⊂A⊂A3 [denoting the theorems/answers of the system as A]
and yet the system could still have, on the very least, the non-assumption of LEM (in some possible way) as an essential part (in the way it arrives at answers).

 

[nomadreid]

Thank you for your further reflections, SSequence. Before I comment on them further, I have three questions:
(1) You state

it doesn't seem that "constructive" [say in the sense of algorithmic or possibly in even some broader sense] has a direct relation with the non-assumption of LEM.

Why do you say that? The problem is that apparently it does: intuitive means two things: invalidity of LEM, and constructive. So they are connected, but I am trying to find out why.

(2) I am not very good at acronyms (PA and HA are OK, but ...) Please tell me what ACA_0 is.

(3) How are you defining questions and answers as sets? Domain and codomain of functions, or what? This is not clear in your exposition.

Once I understand your answers to these questions, I can comment on your remarks.

 

[TeethWhitener]

invalidity of LEM, and constructive. So they are connected, but I am trying to find out why.

Caveat: I don't know much about intuitionistic logic.

Gentzen's original proof is in German, but a paywalled English translation is here:
https://www.sciencedirect.com/science/article/pii/S0049237X0870822X
Here's another paper I found that might be of some interest. Check out Theorems 2 and 7. :
https://www.math.ucsd.edu/~sbuss/ResearchWeb/intuitionisticDP/paper.pdf

 

[nomadreid]

Thanks, Teethwhitener. I shall look at them, but if you could tell me where to find Gentzen's original proof in German, that would be great, because I am fluent in German.

 

[SSequence]

I hesitate to add too much, since I think you might not benefit much from further discussion.

But regarding your questions (in case you haven't seen or know about some of this before):
(1) Regarding your comment, I don't know the answer.

If we try to include reasoning about real numbers in some way, then we have a number of strands. I am not familiar with details that much. In a rough way, there seem to be at least two strands (about which there seems to be much literature).

One strand is notion of "fans" which is how Brouwer initially seemed to go by. Once again I don't know the details well. The other strand is really the usual constructive one (perhaps somewhat like Erret Bishop's book). But there are number of easier books too (unfortunately I haven't been able to get the time to read one). The way we represent real numbers (decimals, intervals etc.) definitely becomes important here.

There are further fine-graining here definitely. I re-call reading a description of at least four systems here (relevant to these two strands I presume) while skimming a document. I will have to check exactly which document, but if you are interested I can look-up the names of the four systems.

==========

However, that's definitely not all. The word "intuitionism" definitely has a broad meaning. There is such a thing as "intuitionistic set-theory" (but I have no idea what it really is).

I also suggest reading the first section (second section would be too advanced/technical) of the paper "Axiomatizing Mathematical Conceptualism". In particular the section-1.2 and section-1.4. Well mostly because I largely have/had similar-sounding (but of course fuzzy) thoughts on this topic for some time.

To summarise, basically the author talks about distinction between collections that are "surveyable" and "determinate" in section-1.2. Sorry for the de-tour, but now in section-1.4("Quantifying over the reals") towards the end:
"Classically this law (the author is referring to LEM) can be justified by saying that the truth value of any statement could in principle be determined by a mechanical search (much like the Goldbach conjecture in our discussion above); thus any statement is definitely either true or false. However, when we quantify over real numbers this justification is not available. Since the notion of “all real numbers” is indefinite in the sense that there is no structural amalgamation of all real numbers which could be mechanically surveyed, even in principle, we cannot generally affirm that any statement about arbitrary real numbers has a definite truth value. Or, at least, since there could be statements whose truth value cannot be determined even in principle, such an affirmation would not have any substantive content.

The main point to keep in mind is that we cannot assume that all statements have definite truth values; to a large extent, intuitionistic logic merely codifies the forms of reasoning that one would naturally adopt in such a case."(2) It is one of the systems of reverse math. I am not familiar enough with it though, but it should be quite restricted and natural system (because of only allowing sets in "arithmetical hierarchy"). Mainly much of traditional analysis can be done in it.

(3) At least for PA, ACA_0 why can't we do this easily. I definitely meant doing it in a certain meta-mathematical sense so to speak.

For example, consider the case of PA specifically. We have all possible strings. Then the strings which form a well-formed statement (with a truth value). And then all theorems which can be proved in PA? So, why can't we do this? We can easily make the well-formed statements (with a truth value) correspond with say the natural numbers. And then theorems can be thought of as a subset of natural numbers.

For set-theory, I don't know since I am not well-read enough (and I would hesitate to speculate incoherently). Maybe you know the answer!
[Edit:] On a second thought, aren't there just two (binary) predicates here. So can't we interpret the well-formed statements (with true/false values) theorems, in a similar way, as subsets of natural numbers? Or am I missing something too obvious?[End]

Though what I was just trying to say was what I wrote in first two paragraphs (which was definitely somewhat informal). I think my example wasn't very good [but anyway, you can remove (3) set-theory from that second example completely and it wouldn't change].

Caveat: I don't know much about intuitionistic logic.

Gentzen's original proof is in German, but a paywalled English translation is here:
https://www.sciencedirect.com/science/article/pii/S0049237X0870822X
Here's another paper I found that might be of some interest. Check out Theorems 2 and 7. :
https://www.math.ucsd.edu/~sbuss/ResearchWeb/intuitionisticDP/paper.pdf

Yes, after being expressed appropriately, con(PA) should be equivalent to con(HA) I think [I have read it but I don't know why this is so].

And basically, con(PA) can be thought of as being definitively proved by Gentzen, at least in my view. And similar for all other theories with a similar analysis, as long as it is checked with enough detail/certainty (once again, in my view). This was also discussed in one of the threads here (towards the end of last year).

Though, it should be said, not everyone seems to agree about the first sentence in previous paragraph. The underlying reasoning seems to be related to the issue of expressing the notion of a well-order formally. But anyway, this goes into a digression.

 

[TeethWhitener]

Thanks, Teethwhitener. I shall look at them, but if you could tell me where to find Gentzen's original proof in German, that would be great, because I am fluent in German.

https://link.springer.com/content/pdf/10.1007/BF01201353.pdf
This is part I. Presumably there's a part II as well.

 

[nomadreid]

SSequence, thank you for your answers. To some of your points:

I now know that ACA_0 stands for “Arithmetical comprehension axiom”, a particular subsystem of second-order arithmetic

Yes, there are a lot of different approaches to the real numbers: whoever divided them up into only four must have been talking in very broad terms. Obviously, intuitionism has great importance in the investigation of the reals, not just Brouwer’s fan theorem. But I am not putting this into question. My question remains.

By "Axiomatizing Mathematical Conceptualism" I presume you mean
“Axiomatizing mathematical conceptualism in third order arithmetic” by Nik Weaver
(https://arxiv.org/abs/0905.1675)

Theorems are part of the syntactic structure, and sets are part of the semantics. So, I presume you mean, by representing a theorem as a set, either: (a) given a model, then the set in the model which satisfies it, or (b) given a standard coding of the wffs into the natural numbers, whereby the natural numbers are represented as sets. But this still does not tell me what you mean by “questions” and “answers”.

Gödel proved in 1933 (using a “double negative translation”) con(HA) implies Con(PA). . But it is a bit strong to say order to say that Gentzen “proved Con(PA)”. As Gödel’s second Incompleteness Theorem shows, you need to assume a stronger system (or assume that PA is inconsistent) to be able to prove Con(PA), but of course then that stronger system runs into the same problem, so this assumption never really allows you to make such an unqualified assertion.

 

[nomadreid]

Thanks, TeethWhitener. I have looked at the tantalizing first two pages that your link to the original Gentzen paper allows... 42 Euros is a bit much for the one article, but I will be inquiring among my acquaintances to see if I can get a copy. It looks very interesting. The other article, essentially a bit of extended complexity theory, is also of interest, but it starts with the assumption of the existence property: it is this assumption that I find puzzling. So, while it doesn't answer my question, it looks like a worthwhile read nonetheless.

 

[SSequence]

I do not have enough knowledge/understanding to answer your main question, so I think I will stop here.

However, regarding this point:

Theorems are part of the syntactic structure, and sets are part of the semantics. So, I presume you mean, by representing a theorem as a set, either: (a) given a model, then the set in the model which satisfies it, or (b) given a standard coding of the wffs into the natural numbers, whereby the natural numbers are represented as sets. But this still does not tell me what you mean by “questions” and “answers”.

Sorry I know little to nothing about models. By question I simply meant a well-formed formula [I think that's what it is called] with no free variables I suppose (so it would be either true or false). So in PA, an ordinary statement (true or false) about natural numbers represented in language of PA counts as a question.

By answers I meant the collection of all the theorems. Sorry for using an idiosyncratic terminology.

I think when you wrote:
"(b) given a standard coding of the wffs into the natural numbers,"
that's along the lines I was thinking of. You correspond the wffs (with no free variables so a definite truth value) with natural numbers. Then the theorems proved by the system can be thought of as a subset of natural numbers. Or am I making a very basic mistake?

Edit:
Also when you wrote:
"So, I presume you mean, by representing a theorem as a set ..."
Maybe the way I wrote it was confusing (or maybe there is just a typo in this sentence). I was merely talking about representing the "collection of theorems" as a subset of natural numbers.

I hope this clarifies some confusion (unless I am hopelessly confused myself :P).

Edit2:
One more point (though it is not quite on-topic):

As Gödel’s second Incompleteness Theorem shows, you need to assume a stronger system (or assume that PA is inconsistent) to be able to prove Con(PA), but of course then that stronger system runs into the same problem, so this assumption never really allows you to make such an unqualified assertion.

I think if we are being very precise, this might not be completely accurate? One of the essays I quoted in one of the older threads here makes a point that doesn't quite seem to agree with it.

Here is a quote from section-4 of that essay:
"Where the above argument goes wrong is the claim of circularity. Godel’s theorem does not actually say that the consistency of PA cannot be proved except in a system that is stronger than PA. It does say that Con(PA) cannot be proved in a system that is weaker than PA, in the sense of a system whose theorems are a subset of the theorems of PA—and therefore Hilbert’s original program of proving statements such as Con(PA) or Con(ZFC) in a strictly weaker system such as PRA is doomed. However, the possibility remains open that one could prove Con(PA) in a system that is neither weaker nor stronger than PA, e.g., PRA together with an axiom (or axioms) that cannot be proved in PA but that we can examine on an individual basis, and whose legitimacy we can accept. This is exactly what Gerhard Gentzen accomplished back in the 1930s, and it is to Gentzen’s proof that we turn next."

 

[TeethWhitener]

This looks promising:
https://arxiv.org/ftp/math/papers/0409/0409070.pdf

 

[nomadreid]

First, SSequence, your Edit 2 was not off-topic, as you corrected an omission (that I myself meant to correct earlier and forgot) in my response: yes, I meant "stronger or equi-consistent with" rather than "stronger". Nonetheless, the point remains that PA was not proven consistent without qualification.

 

[nomadreid]

TeethWhitener: Super, thanks! I went through it quickly, in order to come back to it later, but it appears that the last section may give me the flavour of the proof (which is what I am after). It seems to jive with what I read in the meantime about the (full) Axiom of Choice: it is not accepted, because it can be used to prove the principle of the excluded middle. Possibly all other unrestricted axioms with non-constructive existence conclusions either could be used to prove the principle of EM, or have premises that could do so. To be able to apply the branching argument of the last section (hm, no page numbers; thankfully, I can add them ) to such things as, say, the axiom of a measurable cardinal, is going to take some thinking, though. But at least this puts me on the right track.

 

[nomadreid]

PS. For the record, it appears that it would be an incorrect formulation of the intuitionist idea to say that EVERY logical system having more than 2 truth values must invalidate the LEM. For example, consider the lattice of truth values having four values, {0,a,b,1}, which can be envisioned in the obvious way as the four points (0,0), (0,1), (1,0), and (1,1), such that negation is ~0=1, ~a=b, ~b = a, ~1=0, the order is 0<a<1 & 0<b<1, a and b are not comparable, the "and" is the meet and "or" is the join. Then for all cases, "a or not-a" gives the value "1". But the intuitionists say that a logical system need not follow the LEM to be valid; the logical systems which invalidate the LEM are simply more interesting that this example. This is my understanding; I am quite willing to have someone point out the error of my ways.