Intuitionistic Logic: Formalizing "A is Non-Empty

[disregardthat]

I have recently read about intiuitional logic, and have a question. What is the formal form of the statement "A is non-empty", where A is a set?

Could it be a pair <a,b>, where a is an element of A, and b is a proof of that a is an element of A; i.e. if A = { x | phi(x) }, then a is an object, and b is a proof of phi(a)?

 

[Hurkyl]

One useful interpretation is that "A is non-empty" has truth value equal to the image of the map A --> *.

Here, * is the one-element set, and I'm identifying truth values with subsets of *. (in classical logic, after making this identification, "true" would be * and "false" would be the empty set)

 

[disregardthat]

One useful interpretation is that "A is non-empty" has truth value equal to the image of the map A --> *.

Here, * is the one-element set, and I'm identifying truth values with subsets of *. (in classical logic, after making this identification, "true" would be * and "false" would be the empty set)

I understand how subsets of * can be identified with truth values, but could you elaborate on the map you speak of?

 

[Hurkyl]

Ack, notational snafu. I meant 1, not *, for the set with one element. I meant to use * to denote the element of 1.

For any set S, there is a unique map from S to *. It's graph is the subset

{ (s,*) | s in S }​

of Sx1.

It's a little awkward to talk about it, because the existence and properties of 1 are given as axioms in the formulation of intuitionistic set theory I'm familiar with (i.e. interpreting it as topos theory).

A concrete example: for the inutitionistic set theory whose sets are sheaves on a topological space, the map S --> * is simply the map that sends any section of S to the unique section of * over the same domain.


Another concrete example is that classical set theory is an intuitionistic set theory.

 

[disregardthat]

Are you familiar with the Brouwer–Heyting–Kolmogorov interpretation of intuitionistic logic?
http://en.wikipedia.org/wiki/BHK_interpretation

Do you know how the statement, or your proposal, would be interpreted there?

 

[JSuarez]

What is the formal form of the statement "A is non-empty", where A is a set?

Usually, when one asks for the formal expression of a statement, he wants it translated in a formal language, which in this case I take it to be the one for First-Order Intuitionistic Logic (FOIL); but the syntax of FOIL coincides with the one for the First-Order Classical Calculus, so the set of formulas is the same for both calculi (what changes is their meaning and truth conditions).

If you have a set A in Intuitionistic ZFC (that is, the axioms of FOIL plus the ZFC ones), defined by some sort of comprehension, A=\left\{x:\phi\left(x\right)\right\}, then:

<br /> a\in A\Leftrightarrow\model_I\phi\left(a\right)<br />

That is, the question of a belonging to A is equivalent to the intuitionistic truth of \phi\left(a\right). In the informal BHK semantics (we don't have a fully rigorous formalization of BHK) this means that you must either provide a proof for \phi\left(a\right), or a countermodel for it.

For exemple, if:

<br /> \phi\left(x\right)\leftrightarrow \left(x=0\right)\vee \left(x=1\right)<br />

Then, assuming the intended interpretations for 0 and 1, if you want to prove, for example, \phi\left(1\right), you must either provide a proof that 1 = 0 or 1 = 1 (these are atomic formulas, so the proof is immediate).

 

[disregardthat]

Thanks. But suppose we have no specific element to question, is it not so that a proof of "A is non-empty", is an element 'a' together with a proof 'b' of phi(a); the pair <a,b>?

I am very curious of whether a proof of the general property of non-emptyness must be a specific element in addition to a proof of that it is in the BHK interpretation.

That is, the question of a belonging to A is equivalent to the intuitionistic truth of \phi\left(a\right). In the informal BHK semantics (we don't have a fully rigorous formalization of BHK) this means that you must either provide a proof for \phi\left(a\right), or a countermodel for it.

What exactly to you mean by a 'countermodel'?

 

[JSuarez]

A pair <a,b> such as you describe would be a proof that A is non-empty. In a more formal manner, note that the statement "A is non-empty" can be formalized as:

\exists x\left(x\in A\right)

And a proof of it (in BHK) would be, again, a pair whose first component is a and the second an "algorithm" b that, given a as input, would output a proof of \phi\left(a\right).

EDIT: just saw the second part now. The semantics for which FOIL is complete are the so-called "Kripke models", which have a more complicated structure than the interpretations for the classical first-order logic. A "countermodel" in FOIL is simply a Kripke model in which the statement is false.

 

[disregardthat]

The semantics for which FOIL is complete are the so-called "Kripke models", which have a more complicated structure than the interpretations for the classical first-order logic. A "countermodel" in FOIL is simply a Kripke model in which the statement is false.

I am not familiar to kripke models. But I suppose a countermodel of \phi(a) is (more or less) equivalent to a proof of \phi(a) \Rightarrow absurdity?

A pair <a,b> such as you describe would be a proof that A is non-empty. In a more formal manner, note that the statement "A is non-empty" can be formalized as:

\exists x\left(x\in A\right)

And a proof of it (in BHK) would be, again, a pair whose first component is a and the second an "algorithm" b that, given a as input, would output a proof of \phi\left(a\right).

Excellent. And in BHK, the statement P \Rightarrow Q is equivalent to providing a function f which takes a proof of P and generates a proof of Q (more or less). Now, what I had in mind was this:

The axiom of choice (or an equivalent of it) is: Given a set A of non-empty sets, then there exists a function c defined on A such that s \in A \Rightarrow c(s) \in s.

A proof of "Given a set A of non-empty sets" is a proof of

\forall s \in A \ : \ s is non-empty. And further, a proof of "s is non-empty" is a pair <a,b>, where a is an element and b is a proof of that a is an element of s.

So a proof of the initial conditions really provides a specific pair &lt;a,b&gt; for each s \in A. In other words, for the initial conditions to be fulfilled (A is a set of non-empty sets), we actually have, for each s \in A, provided an element a of s.

This enables us to define the function c on A by returning the associated element a: s \in A \Rightarrow c(s) = a, where a is the first element in the pair &lt;a,b&gt; \Leftrightarrow "s is non-empty".

There is no need for an infinite choice, as the very assumptions of the axiom (the conditions) are (more or less) on the form of a specific "selection" of elements from each s.

Do you see a flaw in this? Can it not be said that the axiom of choice does not need the status as axiom in the BHK interpretation?

 

[Hurkyl]

What if you have more than one proof? How do you choose which one? And if you can, how do you turn the function you described into a function of the set theory you're studying?

As an FYI, a convenient (IMO) version of the axiom of choice is that every surjective function is split; that is given any surjection X --> Y, there is an injection Y --> X such that the composite is the identity function on Y.

 

[disregardthat]

What if you have more than one proof? How do you choose which one? And if you can, how do you turn the function you described into a function of the set theory you're studying?

Well, my answer to your first question would be that the BHK interpretation of P \Rightarrow Q is (as far as I have understood) a proof of that given a proof of P, you can generate a proof of Q. So given any proof of the conditions, we can generate a choice function. Q is the "output" of P. The choice function always depends on the (necessarily) given proof of the initial conditions.

So in any application of the axiom of choice, you will have to give an explicit proof of the initial conditions. Having found such a proof, you can go on defining your function. (EDIT: the crucial point is that 'a proof of "s is non-empty"' is a pair '<a,b>' as previously described.)

I don't really understand your second question.

 

[Hurkyl]

In a more formal manner, note that the statement "A is non-empty" can be formalized as:

\exists x\left(x\in A\right)

In the presentation in Wikipedia, only bounded quantifers are allowed. Does that make a difference? I don't know how unbounded intuitionistic set theory differs from the bounded version.

So given any proof of the conditions, we can generate a choice function.

Okay, I believe this, although I'm a little skeptical because I've made similar arguments in error before.


However:

I don't really understand your second question.

Have you seen Skolem's paradox?

• There is a countable model of first-order set theory.
• The real numbers in this model have countably many elements.
• The natural numbers in this model have countably many elements.
• There is a bijection between the sets of real and natural numbers of this model.
• Cantor proved there does not exist a bijection between the real and natural numbers.

Surprise -- this isn't a contradiction! The bijection so constructed is not a function in this model of first-order set theory, and thus does not provide a counterexample to Cantor's theorem.

I'm asking the similar question here: you have constructed a function -- an "external "function -- that acts as a choice function not through set theoretic means, but by cheating: it is defined in terms of proofs and interpretations.

So, now we have to ask just what is a function in this version of set theory, and is the function we just defined one of them?

 

[disregardthat]

I am not sufficiently familiar with set theory nor the BHK interpretation to be able to judge this. By searching on it now I came to the web page http://plato.stanford.edu/entries/mathematics-constructive/ which provided the following fact:

"However, there is one further technical matter we would like to mention: the axiom of choice is derivable in ML. ... In Martin-Löf's type theory, every set is completely presented and, in keeping with what we wrote above about the BHK interpretation of (1), the axiom of choice is derivable therein."

Are you familiar with ML?

This is written under the section 3.4 together with the technicalities. It appears that it is possible for the choice function to satisfy the necessary conditions for being a function. Whether or not I have done so correctly is another matter.

 

[JSuarez]

In the presentation in Wikipedia, only bounded quantifers are allowed. Does that make a difference? I don't know how unbounded intuitionistic set theory differs from the bounded version.

Where? I can't recall any presentation of intuitionistic or constructive set theory that allows only bounded quantifiers, but I may be wrong.

I suppose a countermodel of \phi\left(a\right) is (more or less) equivalent to a proof of \phi\left(a\right)\rightarrow\bot?

Not exactly. FOIL is sound and complete relative to Kripke semantics, so a countermodel of \phi\left(a\right) means that it's not provable, but

\neg\phi\left(a\right)\Leftrightarrow\phi\left(a\right)\rightarrow\bot

may also not be provable, which means that it has a countermodel too.

I'll post again tomorrow regarding your claim about the axiom of choice, but let me make a few brief comments now:

(1) It cannot be right; in fact, most versions of AC are incompatible with Intuitionistic Set Theory, because they imply strong instances of the Principle of Excluded Middle, that are false in FOIL.

(2) Remember that the BHK semantics is not rigorous; it cannot be used in a formal demonstration, beyond providing an heuristic for a more rigorous proof.

(3) Regarding Set Theory and given that you already quoted SEP, check this entry as well:

http://plato.stanford.edu/entries/set-theory-constructive/"

This review by Laura Crosilla is not elementary but is, in my opinion, the best one around.

 

[Hurkyl]

Where? I can't recall any presentation of intuitionistic or constructive set theory that allows only bounded quantifiers, but I may be wrong.

I'm used to understanding them in terms of category-theoretic semantics, so that every variable is bound to a type which is interpreted as an object of a topos.

Therefore, I have very little intuition about what can go wrong if we allow unbounded quantifiers. I recall once seeing unbound quantifiers treated in this way, but I don't remember how it worked.

 

[disregardthat]

(1) It cannot be right; in fact, most versions of AC are incompatible with Intuitionistic Set Theory, because they imply strong instances of the Principle of Excluded Middle, that are false in FOIL.

(2) Remember that the BHK semantics is not rigorous; it cannot be used in a formal demonstration, beyond providing an heuristic for a more rigorous proof.

(3) Regarding Set Theory and given that you already quoted SEP, check this entry as well:

http://plato.stanford.edu/entries/set-theory-constructive/"

This review by Laura Crosilla is not elementary but is, in my opinion, the best one around.

I can see how this might be so within the formal intuitionistic set theory, but this was proven(?) 'within' the BHK-interpretation. How does BHK fit into all of this? I am not contradicting your claim, but why is not this interpretation considered a satisfactory way of proving results? (I guess what I am fishing for here is an elaboration)

Let me air my current understanding:
In order to have a rigorous (or so is the common opinion) mathematical theory you must provide (1) a logical foundation (like classical or intuitionistic logic) and (2) a model in which to apply these logical principles (like a set theory or a type theory). In order to extract (1) and (2) from purely formal operations to language we must employ (3) an interpretation/semantics (like the BHK-interpretation), which must be in perfect accordance with the underlying logical principles and model which it represents, i.e. must be translatable from formal syntax to semantics and back.

As far as I have understood the issue here is that the BHK-interpretation is not a rigorous equivalence (in perfect accordance) to intuitionistic logic together with any model, which makes it unsuitable to prove anything formally as the semantics is not translatable back to any given syntax.

 

[JSuarez]

I can see how this might be so within the formal intuitionistic set theory, but this was proven(?) 'within' the BHK-interpretation.[...] I am not contradicting your claim, but why is not this interpretation considered a satisfactory way of proving results?

But that's the point: a 'proof' in BHK is merely heuristic. What is exactly the 'proof' on BHK arguments? What properties does it have and what rules does it obey? Is it the informal notion of mathematical proof? It can't be, because that will defeat the whole purpose of having a more constructive version of it.

More importantly, without the elucidation of this 'proof' it doesn't even make sense to ask what properties does FOIL have relative to this semantics, like soundness and completness, and this renders it pretty much useless beyond an heuristic.

In fact, it's not even a very good heuristic; for example, it's easy to come up with a BHK-justification of, say, \alpha\rightarrow\neg\neg\alpha, but now try to 'prove' that \neg\neg\alpha\rightarrow\alpha is not intuitionistically valid. Or, without negations, that Peirce's Law \left(\left(\alpha\rightarrow\beta\right)\rightarrow\alpha\right)\rightarrow\alpha is not intuitionistically valid either?

...i.e. must be translatable from formal syntax to semantics and back.

This paragraph is not quite clear, but I take it that you mean that, in order to formalize a mathematical theory, you need a consistent logical system, that is also sound relative to a given semantics.

How does BHK fit into all of this?

BHK was the first attempt to 'interpret' intuitionistic logic, as was proposed by Heyting but at the time, these notions were ill-understood. There are theories that attempt to give a sound and complete semantics to intuitionistic logic that more in the spirit of BHK, like Kleene's Realizability, Gödel's dialetica interpretation, the no-counterexamples interpretation, etc. and they are beeing studied actively because, given a formal proof in FOIL they allow, in principle, to extract information about the objects ocurring in the proof, but they also have problems.

so that every variable is bound to a type which is interpreted as an object of a topos.

Ok, so when you say "bounded", it's bounded to a type, not a range of quantification?

 

[Hurkyl]

Ok, so when you say "bounded", it's bounded to a type, not a range of quantification?

I'll rephrase to make sure I'm not using the wrong words here.

In the language of a topos, to each object there is a type symbol. And to each type there is an (infinite) collection of variable symbols.

A formula such as \exists x: x \in S doesn't make sense because the variables are unbound. But, if S is of type \mathcal{P}(A), then the formula \exists x \in A: x \in S does make sense. (Well, I suppose the first formula makes sense if you specify elsewhere the type of x)

I took the term "bounded" from Sheaves in Geometry and Logic -- they describe a set theory called "Bounded Zermelo set theory" which differed from ordinary Zermelo set theory in that unbounded quantifiers were not allowed; only quantifiers of the form \exists x \in S were allowed.

 

[disregardthat]

In fact, it's not even a very good heuristic; for example, it's easy to come up with a BHK-justification of, say, \alpha\rightarrow\neg\neg\alpha, but now try to 'prove' that \neg\neg\alpha\rightarrow\alpha is not intuitionistically valid.

That's interesting, could you provide a demonstration of this? I cannot immediately see how it is so. In BHK (not A) is a function which reduces any proof of A into absurdity. not (not A) would be a function which reduces any function of the previously mentioned sort into absurdity. How does this provide a proof of A? I.e. how can ((A \to \bot) \to \bot ) \to A be established in BHK?

EDIT: I realize might have misunderstood you, did you mean that in BHK it would be possible to 'prove' that \neg \neg \alpha \to \alpha? If not, what was your point of "...but now try to 'prove' ..."?

Could you elaborate on your comment on Pierce's law?

Do you agree that if one could develop an interpretation akin to BHK while also being consistent with intuitionistic logic, that would provide a suitable way to prove things formally but semantically? You say that they run into problems, but what problems are these?

 

[JSuarez]

I took the term "bounded" from Sheaves in Geometry and Logic -- they describe a set theory called "Bounded Zermelo set theory"...

Ok, you are talking about a typed set theory. I'll check MacLane's book then. My rudiments of Category Theory are so scant and rusty that I'll probably won't understand him, but I would like to learn more about the category-theoretic viewpoint anyway, so perhaps I'll take the opportunity to do so.

That's interesting, could you provide a demonstration of this?

To see how BHK "justifies" \alpha\rightarrow\neg\neg\alpha, you need "something" that, given a proof of \alpha, will output a proof of \neg\neg\alpha; but this is another "something" that, given a proof of \neg\alpha, outputs a proof of \bot. Let a be a "proof" of \alpha and ~a a "proof" of \neg\alpha and consider the pair <a,x>; if x is substituted by ~a it will be a "proof" of \alpha\wedge\neg\alpha, which is equivalent to \bot.

...did you mean that in BHK it would be possible to 'prove' that...

What I meant is that it's very difficult (if not impossible) to prove, using BHK, that \neg\neg\alpha\rightarrow\alpha is not intuitionistically valid; the point being the limitations of BHK.

The same goes for Peirce's Law: I mentioned it because almost all examples of classically valid formulas that are not intuitionistically valid involve negations, giving the (false) impression that what distinguishes the two is the semantics for the negation operator; this is one of the simplest that doesn't have any negations.

 

[disregardthat]

To see how BHK "justifies" \alpha\rightarrow\neg\neg\alpha, you need "something" that, given a proof of \alpha, will output a proof of \neg\neg\alpha; but this is another "something" that, given a proof of \neg\alpha, outputs a proof of \bot. Let a be a "proof" of \alpha and ~a a "proof" of \neg\alpha and consider the pair <a,x>; if x is substituted by ~a it will be a "proof" of \alpha\wedge\neg\alpha, which is equivalent to \bot.

Yes, but what about the other way? Did you mean one could provide a justification of this in BHK? And is really \alpha\rightarrow\neg\neg\alpha invalid intuitionistically?

 

[JSuarez]

Yes, but what about the other way?

I take it that for "the other way" you mean \alpha\rightarrow\neg\neg\alpha. This expression is not valid in intuitionistic logic, but the only information provided by BHK are vague statements like "the antecedent doesn't ask for a proof of \alpha, so there is no way to construct one from it".

On the other hand, \alpha\rightarrow\neg\neg\alpha is intuitionistically valid, and you could prove it deductively with any presentation of the system (axiomatic, natural deduction, etc.), or semantically, by proving that it's true in all Kripke models.

 

[disregardthat]

On the other hand, \alpha\rightarrow\neg\neg\alpha is intuitionistically valid, and you could prove it deductively with any presentation of the system (axiomatic, natural deduction, etc.), or semantically, by proving that it's true in all Kripke models.

Exactly, this was the "the other way" i asked about, and which I wrote of in my comment. But now I can't see the issue. \alpha\rightarrow\neg\neg\alpha is true intuitionistically and follows naturally in BHK, while \neg\neg\alpha\rightarrow\alpha does not hold intuitionistically, and does not (as far as I can see) follow in BHK. This has gotten me confused. How is this an example of how bad of a heuristic BHK is?

 

[JSuarez]

It's an example to show that BHK might be a reasonable heuristic, but not a good semantics, because you can't use to prove that \neg\neg\alpha\rightarrow\alpha is not intuitionistically valid.

 

[disregardthat]

It's an example to show that BHK might be a reasonable heuristic, but not a good semantics, because you can't use to prove that \alpha\rightarrow\neg\neg\alpha is not intuitionistically valid.

You just said it was!

EDIT: though I assume you meant \neg\neg\alpha\rightarrow\alpha.

However, there are certainly examples in which \neg\neg\alpha\rightarrow\alpha can be proven in BHK not to be a valid principle.

 

[JSuarez]

That's true; if the \alpha's are atomic formulas, then you can do it. The same goes for the Law of the Excluded Middle, that may be justified using BHK in this case.