Martin Baker wrote:
>
> On Monday 20 Jun 2011 17:55:38 Waldek Hebisch wrote:
> > Martin Baker wrote:
> > > On Saturday 18 Jun 2011 13:33:51 Waldek Hebisch wrote:
> > > > Actually, the tables you gave describe something quite different
> > > > that intutionistic logic. For example, you have
> > > >
> > > > - T =3D ?
> > > > - ? =3D ?
> > > >
> > > > however in intutionistic logic - T is false and -(- T) =3D T.
> > >
> > > This looks like the 'law of excluded middle' which I have not been
> > > assuming.
> >
> > No, 'law of excluded middle' is -x \/ x, and of course is _not_
> > valid in intutionistic logic.
>
> Waldek,
>
> There are a couple of statements on the wiki intuitionistic logic page
> that appear to conflict with what you are saying:
> http://en.wikipedia.org/wiki/Intuitionistic_logic
>
> In the 'Syntax' section:
>
> "In classical logic, both p =E2=86=92 =C2=AC=C2=ACp and also =C2=AC=C2=ACp =
> =E2=86=92 p are theorems. In
> intuitionistic logic, only the former is a theorem: double negation
> can be introduced, but it cannot be eliminated"
>
> In the 'Relation to classical logic' section:
>
> start-of-quote
> The system of classical logic is obtained by adding any one of the
> following axioms:
>
> \phi \lor \lnot \phi (Law of the excluded middle. May also be
> formulated as (\phi \to \chi ) \to ((\lnot \phi \to \chi ) \to
> \chi ).)
> \lnot \lnot \phi \to \phi (Double negation elimination)
> ((\phi \to \chi ) \to \phi ) \to \phi (Peirce's law)"
>
> end-of-quote
>
> In other words they seem to be saying that the addition of either Law
> of the excluded middle or Double negation elimination have the same
> effect of converting intuitionistic logic to classical logic.
>
> I remember seeing similar things on various other websites. So this
> gave me a lot of (perhaps misplaced?) confidence that double negation
> elimination should not be assumed.
>
> What do you make of these quotes? Have I misunderstood them?
The quotes look correct. Consider:
x -> --x (Doble negation introduction) means that
T -> --T which in turn means T = --T
OTOH if you know that --x = T you can not infer that x is T
(this is another way of saying that you can not eliminate
double negation).
To say this differently: --T = T but there are x such that
--x ~= x.
--
Waldek Hebisch
[email protected]
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/fricas-devel?hl=en.
