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. > > > Similarely, -x /\ x is false, but your tables give ?. > > > > I wonder from which source you took your definitions? > > Various on-line sources such as: > http://en.wikipedia.org/wiki/Intuitionistic_logic > (I don't have acess to a university library) > > >From which source do you get your definitions? We are obviously > working with very different assumptions. Can you give an on-line > source that we can both agree on? > Actually Wikipedia looks correct (but gives only little detail). For example, Wikipedia sends you to http://en.wikipedia.org/wiki/Gödel-Gentzen_negative_translation and on that page you have: The easiest double-negation translation to describe comes from Glivenko's theorem. It maps each classical formula to its double negation. Glivenko's theorem states: If T is a set of propositional formulas and phi a propositional formula, then T proves phi using classical logic if and only if T proves --phi using intuitionistic logic. Now, true is proved classicaly from empty set, so --true is proved using intuitionistic logic from empty set, which means that --true is true in intuitionistic logic. Similarely, for x /\ x beeing equivalent to x look at axioms: AND-1 gives (x /\ x) -> x so by modus ponens x is conseqence of x /\ x. In the opposite direction: AND-3 gives x -> (x -> (x /\ x)). Using x as starting point by modus ponens we get x -> (x /\ x). Again by modus ponens we get x /\ x, so x /\ x is a conseqence of x. In other words x and x /\ x are equivalent in sense of having the same conseqences. Also, in section 'Relation to many-valued logic' Wikipedia says: Kurt Gödel in 1932 showed that intuitionistic logic is not a finitely-many valued logic. (See the section titled Heyting algebra semantics below for a sort of "infinitely-many valued logic" interpretation of intuitionistic logic.) If you look at 'Heyting algebra semantics' you see: It can be shown that to recognize valid formulas, it is sufficient to consider a single Heyting algebra whose elements are the open subsets of the real line R. In this algebra, the /\ and \/ operations correspond to set intersection and union, and the value assigned to a formula A -> B is int(A^c \cup B), the interior of the union of the value of B and the complement of the value of A. The bottom element is the empty set 0, and the top element is the entire line R. The negation -A of a formula A is (as usual) defined to be A -> 0. The value of -A then reduces to int(A^c), the interior of the complement of the value of A, also known as the exterior of A. With these assignments, intuitionistically valid formulas are precisely those that are assigned the value of the entire line. According to this true corresponds to the whole R, negation of true is interior of complement of R. Complement of R is empty set, so negation of true corresponds to empty set. Conseqently negation of true is false. Similarely you can check that negation of false is true. You see difference with classical logic if you look at A = R - {0}, that is R minus one point. Complement of A is one point, so interior of complement of A is is empty and consequently negation of A is false (and double negation is true). So in intuitionistic logic there are things which are not true, but their negation is false (so double negation is true). -- 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.
