intuitionism, LEM and infinity
eposse
about intuitionistic logic and I'm confused about its foundations.
Brower eschewed the law of the excluded middle (LEM) arguing that it
had been generalized from finite domains to infinite domains without
proper justification. But at the same time, Brower denied the notion
of actual infinity (e.g. there's no such thing as the complete set of
natural numbers), only accepting potential infinity (e.g. a rule to
build any finite set of natural numbers). Now, here's my confusion: if
LEM is problematic for truly infinite domains and truly infinite
entities do not exist, then why throw away LEM? after all, if we can
only talk sensibly about what we can construct, and we can construct
only finite domains, then we should be able to use LEM on those
entities that we can sensibly talk about, no? How are these ideas
reconciled in intuitionism?
Thanks
Abram Demski
I'm no expert on those particular arguments, but I'd guess something roughly like this:
Think of "finite" as meaning "explicitly bounded" or "closed-off", and "potentially infinite" as "explicitly not bounded" (for example, we know we can keep adding to the list of integers, since we've got a constructive procedure for increasing the size of any finite list).
We'd then say that LEM apparently does not always apply to these "unbounded" domains, since we know examples where both a sentence and its negation fail to lead to a contradiction (so neither are refutable in the intuitionist sense).
Does that sound roughly like the stuff you've been reading? (Comments appreciated.)
My position has been that, since classical and intuitionistic logic interpret each other, the question of which is correct is not fundamental; if you know of any attacks on such a position, that'd be awesome. :)
--Abram
--
You received this message because you are subscribed to the Google Groups "One Logic" group.
To post to this group, send email to one-...@googlegroups.com.
To unsubscribe from this group, send email to one-logic+...@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/one-logic?hl=en.
--
Abram Demski
http://lo-tho.blogspot.com/
http://groups.google.com/group/one-logic
Ernesto Posse
On Sat, Jul 3, 2010 at 6:01 PM, Abram Demski <abram...@gmail.com> wrote:
> Hi,
>
> I'm no expert on those particular arguments, but I'd guess something roughly
> like this:
>
> Think of "finite" as meaning "explicitly bounded" or "closed-off", and
> "potentially infinite" as "explicitly not bounded" (for example, we know we
> can keep adding to the list of integers, since we've got a constructive
> procedure for increasing the size of any finite list).
>
> We'd then say that LEM apparently does not always apply to these "unbounded"
> domains,
I'm not sure I follow. What you are saying is that LEM fails, not only
for the "actual infinite" but also for the "potential infinite"? Could
you illustrate with an example?
> since we know examples where both a sentence and its negation fail
> to lead to a contradiction (so neither are refutable in the intuitionist
> sense).
I don't think I understand this. LEM is not the same as the
principle/rule of non-contradiction, which still holds for
intuitionistic logic. Could you clarify?
> Does that sound roughly like the stuff you've been reading? (Comments
> appreciated.)
Not quite. I have read that there are "weak" and "strong"
counterexamples to LEM, which are based on sets defined
"intuitionistically", but I do not know what that means. None of these
show a sentence which together with its negation fail to entail a
contradiction. (see
http://plato.stanford.edu/entries/brouwer/strongcounterex.html)
> My position has been that, since classical and intuitionistic logic
> interpret each other, the question of which is correct is not fundamental;
> if you know of any attacks on such a position, that'd be awesome. :)
Well, I am aware that anything provable intuitionistically is provable
classically, and I am aware of Glivenko's Theorem, but this simple
states that "an arbitrary propositional formula A is classically
provable, if and only if ¬¬A is intuitionistically provable." But I
think that concluding from these that they are equivalent seems a bit
premature (at least as far as my knowledge on the subject is
concerned). This equivalence is about the proof theory, but
semantically, are they equivalent? My understanding is that this is
not the case (e.g. not every Heyting algebra is a Boolean algebra).
Furthermore, when we consider predicate calculus, there seems to be a
gap between proving ¬¬∃x.P(x) and ∃x.P(x). For intuitionists, to prove
∃x.P(x) you must give an x0 such that P(x0) holds, but for
classisists, it is enough to prove ¬¬∃x.P(x). To me, that seems pretty
fundamental, for allowing to prove existentials without witnesses
requires some additional (epistemic or metaphysical) commitments. In
any case, it might not be too easy to brush aside this issue, since
there is a considerable number of people (well, mathematicians), who
favour either classical or intuitionistic logic, and the distinction
does seem to have consequences in mathematics, as far as I know.
> --Abram
Thanks
--
Ernesto Posse
Applied Formal Methods Group - Software Technology Lab
School of Computing
Queen's University - Kingston, Ontario, Canada
Abram Demski
Thanks for the response. My follow up comments and questions are below.
I'm not sure I follow. What you are saying is that LEM fails, not only
On Sat, Jul 3, 2010 at 6:01 PM, Abram Demski <abram...@gmail.com> wrote:
> Hi,
>
> I'm no expert on those particular arguments, but I'd guess something roughly
> like this:
>
> Think of "finite" as meaning "explicitly bounded" or "closed-off", and
> "potentially infinite" as "explicitly not bounded" (for example, we know we
> can keep adding to the list of integers, since we've got a constructive
> procedure for increasing the size of any finite list).
>
> We'd then say that LEM apparently does not always apply to these "unbounded"
> domains,
for the "actual infinite" but also for the "potential infinite"? Could
you illustrate with an example?
Well, since an intuitionist only recognizes the existence of "potential infinite", I'm assuming an intuitionist would only assert the failure of LEM for that case!
I don't think I understand this. LEM is not the same as the
> since we know examples where both a sentence and its negation fail
> to lead to a contradiction (so neither are refutable in the intuitionist
> sense).
principle/rule of non-contradiction, which still holds for
intuitionistic logic. Could you clarify?
As I understand it, an intuitionist says that "not-A" means "If I assume A, I get a contradiction." So, the law of excluded middle says "For every A, either A leads to a contradiction or not-A does." This is known to be false; for example, the continuum hypothesis is a statement in set theory which we know does not lead to a contradiction, but we also know that its negation doesn't lead to a contradiction! Thus LEM is (apparently) false, with explicit counterexamples in hand.
Not quite. I have read that there are "weak" and "strong"
> Does that sound roughly like the stuff you've been reading? (Comments
> appreciated.)
counterexamples to LEM, which are based on sets defined
"intuitionistically", but I do not know what that means. None of these
show a sentence which together with its negation fail to entail a
contradiction. (see
http://plato.stanford.edu/entries/brouwer/strongcounterex.html)
I did not know of that; thanks. :) My "counterexample" is of a different nature, and I do not know for sure if intuitionists use it.
Well, I am aware that anything provable intuitionistically is provable
> My position has been that, since classical and intuitionistic logic
> interpret each other, the question of which is correct is not fundamental;
> if you know of any attacks on such a position, that'd be awesome. :)
classically, and I am aware of Glivenko's Theorem, but this simple
states that "an arbitrary propositional formula A is classically
provable, if and only if ¬¬A is intuitionistically provable." But I
think that concluding from these that they are equivalent seems a bit
premature (at least as far as my knowledge on the subject is
concerned). This equivalence is about the proof theory, but
semantically, are they equivalent? My understanding is that this is
not the case (e.g. not every Heyting algebra is a Boolean algebra).
Furthermore, when we consider predicate calculus, there seems to be a
gap between proving ¬¬∃x.P(x) and ∃x.P(x). For intuitionists, to prove
∃x.P(x) you must give an x0 such that P(x0) holds, but for
classisists, it is enough to prove ¬¬∃x.P(x). To me, that seems pretty
fundamental, for allowing to prove existentials without witnesses
requires some additional (epistemic or metaphysical) commitments. In
any case, it might not be too easy to brush aside this issue, since
there is a considerable number of people (well, mathematicians), who
favour either classical or intuitionistic logic, and the distinction
does seem to have consequences in mathematics, as far as I know.
There's a provability interpretation of intuitionistic logic in classical provability theory-- which closes the loop and provides interpretation both ways, making them equivalent. Provability requires at least number theory though, so the pure first-order logics w/o mathematics may not be equivalent (probably the intuitionistic is "stronger".) For semantics, I take the provability interpretation as telling me what intuitionistic logic "really means" (ie, puts it in classical terms). I do not, however, similarly accept the interpretation of classical logic into intuitionistic logic as providing the "real meaning" of classical logic. (So perhaps you can see I'm a classicist at heart.)
However, I'm not totally satisfied with my own account on that problem. ;)
--Abram
Ernesto Posse
> Ernest,
>
>> I'm not sure I follow. What you are saying is that LEM fails, not only
>> for the "actual infinite" but also for the "potential infinite"? Could
>> you illustrate with an example?
>
> Well, since an intuitionist only recognizes the existence of "potential
> infinite", I'm assuming an intuitionist would only assert the failure of LEM
> for that case!
Makes sense.
>> > since we know examples where both a sentence and its negation fail
>> > to lead to a contradiction (so neither are refutable in the intuitionist
>> > sense).
>>
>> I don't think I understand this. LEM is not the same as the
>> principle/rule of non-contradiction, which still holds for
>> intuitionistic logic. Could you clarify?
>
> As I understand it, an intuitionist says that "not-A" means "If I assume A,
> I get a contradiction." So, the law of excluded middle says "For every A,
> either A leads to a contradiction or not-A does."
Ah! I see my confusion. I parsed your sentence "both a sentence and
its negation fail to lead to a contradiction" as "both (a sentence and
its negation) fail to lead to a contradiction" instead of "both a
sentence fails to lead to a contradiction and its negation also fails
to lead to a contradiction". The ambiguities of natural language. So
to be more precise, your phrasing corresponds, symbolically to a
particular case of LEM: ¬A∨¬¬A.
>This is known to be false;
> for example, the continuum hypothesis is a statement in set theory which we
> know does not lead to a contradiction, but we also know that its negation
> doesn't lead to a contradiction! Thus LEM is (apparently) false, with
> explicit counterexamples in hand.
Good to know. I was not aware of this. I suppose there is a proviso to
such argument, which is that the continuum hypothesis is about
infinite sets, and therefore I suppose that there is intuitionist's
version.
Also, I've read that what is known is that the continuum hypothesis is
neither provable nor disprovable in ZFC (Zermelo-Fraenkel+Axiom of
choice). I suppose the question of whether there is a system (other
than ZFC) in which it can be proven or disproven is still open?
These examples certainly sound strong, although I would be interested
in more basic examples, if possible, examples which do not require the
machinery needed to define the continuum hypothesis. To me a very
compelling example is the liar's paradox, but this is a more direct
challenge to the principle of bivalence, than to LEM, and as I
recently found out, there is some controversy about whether bivalence
and LEM correspond to each other (although intuitively they should).
Any thoughts on this?
>> > Does that sound roughly like the stuff you've been reading? (Comments
>> > appreciated.)
>>
>> Not quite. I have read that there are "weak" and "strong"
>> counterexamples to LEM, which are based on sets defined
>> "intuitionistically", but I do not know what that means. None of these
>> show a sentence which together with its negation fail to entail a
>> contradiction. (see
>> http://plato.stanford.edu/entries/brouwer/strongcounterex.html)
>
> I did not know of that; thanks. :) My "counterexample" is of a different
> nature, and I do not know for sure if intuitionists use it.
I wouldn't know myself, but it makes sense to use it, after all, for
an intuitionist, stating P is stating that you have a proof of P.
>> > My position has been that, since classical and intuitionistic logic
>> > interpret each other, the question of which is correct is not
>> > fundamental;
>> > if you know of any attacks on such a position, that'd be awesome. :)
>>
>> Well, I am aware that anything provable intuitionistically is provable
[...]
>
> There's a provability interpretation of intuitionistic logic in classical
> provability theory-- which closes the loop and provides interpretation both
Which is this interpretation? Is it different than the (identity)
embedding of intuitionistic proofs into classical proofs?
> ways, making them equivalent. Provability requires at least number theory
> though, so the pure first-order logics w/o mathematics may not be equivalent
> (probably the intuitionistic is "stronger".) For semantics, I take the
> provability interpretation as telling me what intuitionistic logic "really
> means" (ie, puts it in classical terms). I do not, however, similarly accept
> the interpretation of classical logic into intuitionistic logic as providing
> the "real meaning" of classical logic. (So perhaps you can see I'm a
> classicist at heart.)
I'm not sure if we are talking about the same thing here, when we talk
about "meaning". In particular I'm not sure what is the "provability
interpretation". Is it something different than Glivenko's Theorem?
According to Glivenko's Theorem, if P is classically proven, then ¬¬P
is an intuitionistic theorem. What you are saying is that ¬¬P doesn't
provide the "classical real meaning" of P? Or do you mean something
else?
> However, I'm not totally satisfied with my own account on that problem. ;)
>
> --Abram
Thanks
Abram Demski
On Sat, Jul 3, 2010 at 9:07 PM, Abram Demski <abram...@gmail.com> wrote:
> Ernest,
>Makes sense.
>> I'm not sure I follow. What you are saying is that LEM fails, not only
>> for the "actual infinite" but also for the "potential infinite"? Could
>> you illustrate with an example?
>
> Well, since an intuitionist only recognizes the existence of "potential
> infinite", I'm assuming an intuitionist would only assert the failure of LEM
> for that case!
Ah! I see my confusion. I parsed your sentence "both a sentence and
>> > since we know examples where both a sentence and its negation fail
>> > to lead to a contradiction (so neither are refutable in the intuitionist
>> > sense).
>>
>> I don't think I understand this. LEM is not the same as the
>> principle/rule of non-contradiction, which still holds for
>> intuitionistic logic. Could you clarify?
>
> As I understand it, an intuitionist says that "not-A" means "If I assume A,
> I get a contradiction." So, the law of excluded middle says "For every A,
> either A leads to a contradiction or not-A does."
its negation fail to lead to a contradiction" as "both (a sentence and
its negation) fail to lead to a contradiction" instead of "both a
sentence fails to lead to a contradiction and its negation also fails
to lead to a contradiction". The ambiguities of natural language.
Sounds right.
So
to be more precise, your phrasing corresponds, symbolically to a
particular case of LEM: ¬A∨¬¬A.
Sounds wrong... where do you get that from?
Good to know. I was not aware of this. I suppose there is a proviso to
>This is known to be false;
> for example, the continuum hypothesis is a statement in set theory which we
> know does not lead to a contradiction, but we also know that its negation
> doesn't lead to a contradiction! Thus LEM is (apparently) false, with
> explicit counterexamples in hand.
such argument, which is that the continuum hypothesis is about
infinite sets, and therefore I suppose that there is intuitionist's
version.
Also, I've read that what is known is that the continuum hypothesis is
neither provable nor disprovable in ZFC (Zermelo-Fraenkel+Axiom of
choice). I suppose the question of whether there is a system (other
than ZFC) in which it can be proven or disproven is still open?
That's the result I was referring to, for ZFC. More generally, no, the question of whether there is *any* system in which it's decidable is *not* open... many that go one way or the other are known.
These examples certainly sound strong, although I would be interested
in more basic examples, if possible, examples which do not require the
machinery needed to define the continuum hypothesis.
There are examples from number theory... the Goedel sentence is one.
To me a very
compelling example is the liar's paradox, but this is a more direct
challenge to the principle of bivalence, than to LEM, and as I
recently found out, there is some controversy about whether bivalence
and LEM correspond to each other (although intuitively they should).
Any thoughts on this?
What would you mean about "corresponding" to each other?
I wouldn't know myself, but it makes sense to use it, after all, for
>> > Does that sound roughly like the stuff you've been reading? (Comments
>> > appreciated.)
>>
>> Not quite. I have read that there are "weak" and "strong"
>> counterexamples to LEM, which are based on sets defined
>> "intuitionistically", but I do not know what that means. None of these
>> show a sentence which together with its negation fail to entail a
>> contradiction. (see
>> http://plato.stanford.edu/entries/brouwer/strongcounterex.html)
>
> I did not know of that; thanks. :) My "counterexample" is of a different
> nature, and I do not know for sure if intuitionists use it.
an intuitionist, stating P is stating that you have a proof of P.
[...]
>> > My position has been that, since classical and intuitionistic logic
>> > interpret each other, the question of which is correct is not
>> > fundamental;
>> > if you know of any attacks on such a position, that'd be awesome. :)
>>
>> Well, I am aware that anything provable intuitionistically is provable
>Which is this interpretation? Is it different than the (identity)
> There's a provability interpretation of intuitionistic logic in classical
> provability theory-- which closes the loop and provides interpretation both
embedding of intuitionistic proofs into classical proofs?
Yes, it is different...
I believe this is a good reference...
http://portal.acm.org/citation.cfm?id=1027046
Look on Artemov's publication pages...
http://web.cs.gc.cuny.edu/~sartemov/publ.html
The logic of provability can be interpreted in classical peano arithmetic, so that in some sense peano arithmetic talks about provability (you'll be familiar with it doing this if you know Godel's proof, of course). Thus if provability logic interprets intuitionism, then in some sense peano arithmetic can say anything that intuitionistic logic can.
The interpretation you mention, interpreting A as --A, goes in the other direction. It doesn't require the machinery of peano arith, though.
I'm not sure if we are talking about the same thing here, when we talk
> ways, making them equivalent. Provability requires at least number theory
> though, so the pure first-order logics w/o mathematics may not be equivalent
> (probably the intuitionistic is "stronger".) For semantics, I take the
> provability interpretation as telling me what intuitionistic logic "really
> means" (ie, puts it in classical terms). I do not, however, similarly accept
> the interpretation of classical logic into intuitionistic logic as providing
> the "real meaning" of classical logic. (So perhaps you can see I'm a
> classicist at heart.)
about "meaning". In particular I'm not sure what is the "provability
interpretation". Is it something different than Glivenko's Theorem?
According to Glivenko's Theorem, if P is classically proven, then ¬¬P
is an intuitionistic theorem. What you are saying is that ¬¬P doesn't
provide the "classical real meaning" of P? Or do you mean something
else?
Yes, I'm saying that I don't feel that "refutably refutably P" doesn't feel like a meaning for the classical assertion "P" (where "refutably" is intuitionistic negation).
Thanks
> However, I'm not totally satisfied with my own account on that problem. ;)
>
> --Abram
--
Ernesto Posse
Applied Formal Methods Group - Software Technology Lab
School of Computing
Queen's University - Kingston, Ontario, Canada
--
You received this message because you are subscribed to the Google Groups "One Logic" group.
To post to this group, send email to one-...@googlegroups.com.
To unsubscribe from this group, send email to one-logic+...@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/one-logic?hl=en.
Ernesto Posse
>
>> > As I understand it, an intuitionist says that "not-A" means "If I assume
>> > A,
>> > I get a contradiction." So, the law of excluded middle says "For every
>> > A,
>> > either A leads to a contradiction or not-A does."
>>
>> Ah! I see my confusion. I parsed your sentence "both a sentence and
>> its negation fail to lead to a contradiction" as "both (a sentence and
>> its negation) fail to lead to a contradiction" instead of "both a
>> sentence fails to lead to a contradiction and its negation also fails
>> to lead to a contradiction". The ambiguities of natural language.
>
> Sounds right.
>
>> So
>> to be more precise, your phrasing corresponds, symbolically to a
>> particular case of LEM: ¬A∨¬¬A.
>
> Sounds wrong... where do you get that from?
As you stated above, for an intuitionist, ¬A means that assuming A
leads to a contradiction, A⊢⊥, which is equivalent to ⊢A→⊥ (which I
think is the same for classical propositional logic). So I interpreted
"A fails to lead to a contradiction" as ⊬A→⊥ or ⊬¬A, and "A's negation
also fails to lead to a contradiction" as ⊬¬¬A, hence we cannot obtain
¬A∨¬¬A.
>> Also, I've read that what is known is that the continuum hypothesis is
>> neither provable nor disprovable in ZFC (Zermelo-Fraenkel+Axiom of
>> choice). I suppose the question of whether there is a system (other
>> than ZFC) in which it can be proven or disproven is still open?
>
> That's the result I was referring to, for ZFC. More generally, no, the
> question of whether there is *any* system in which it's decidable is *not*
> open... many that go one way or the other are known.
So there are known axiomatic systems in which the continuum hypothesis
is provable?
>> These examples certainly sound strong, although I would be interested
>> in more basic examples, if possible, examples which do not require the
>> machinery needed to define the continuum hypothesis.
>
> There are examples from number theory... the Goedel sentence is one.
RIght, although I am unsure about how Godel's incompleteness theorem
can be seen as a counter example to LEM. If I recall correctly,
Goedel's sentence is true but unprovable, but its negation is false
and also unprovable?
In any case, Goedel's sentence is basically an arithmetic phrasing of
the liar's paradox, but I wonder if there is an example which doesn't
even require arithmetic's axioms at all.
>> To me a very
>> compelling example is the liar's paradox, but this is a more direct
>> challenge to the principle of bivalence, than to LEM, and as I
>> recently found out, there is some controversy about whether bivalence
>> and LEM correspond to each other (although intuitively they should).
>> Any thoughts on this?
>
> What would you mean about "corresponding" to each other?
I'm not too clear on that myself. The papers I have come across (and
which I haven't finished reading) deal with the question of whether
"LEM requires bivalence", which I interpret as "bivalence is a
necessary condition of LEM", or "LEM implies bivalence". But I am
unclear about what that means precisely.
I think this is related to the relation between the proof theory and
the semantics, soundness and completeness. But I wonder how exactly.
>> Which is this interpretation? Is it different than the (identity)
>> embedding of intuitionistic proofs into classical proofs?
>
> Yes, it is different...
>
> I believe this is a good reference...
>
> http://portal.acm.org/citation.cfm?id=1027046
>
> Look on Artemov's publication pages...
>
> http://web.cs.gc.cuny.edu/~sartemov/publ.html
Thanks for the references.
> The logic of provability can be interpreted in classical peano arithmetic,
> so that in some sense peano arithmetic talks about provability (you'll be
> familiar with it doing this if you know Godel's proof, of course). Thus if
> provability logic interprets intuitionism, then in some sense peano
> arithmetic can say anything that intuitionistic logic can.
Some sort of encoding of intuitionistic proofs as Goedel's numbers, I presume?
I have to read the references, but at first sight I wonder why such a
result would be necessary in the first place, since every
intuitionistic proof is automatically a classical proof as well...
> The interpretation you mention, interpreting A as --A, goes in the other
> direction. It doesn't require the machinery of peano arith, though.
Right.
> Yes, I'm saying that I don't feel that "refutably refutably P" doesn't feel
> like a meaning for the classical assertion "P" (where "refutably" is
> intuitionistic negation).
Fair enough. Although it does sound like an intuitionist would agree
to that (maybe you are an intuitionist after all ;)) It does sound
more as an argument stating that classical logic is somehow more
expressive than intuitionistic logic, in the sense that some classical
formulas are not captured (i.e. provable) in intuitionistic logic. But
this begs the question of how "expressiveness" is related to the
question of which is the "correct" logic (if there is such a thing).
Is a more expressive logic more likely to be the "correct" logic, or a
less expressive one?