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 = ? > > > - ? = ? > > > > > > however in intutionistic logic - T is false and -(- T) = 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 → ¬¬p and also ¬¬p → 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? Martin -- 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.
