Pat C and Anonymous, (01)
I had an offline discussion about natural deduction, which led me
to add two slides to the egintro.pdf presentation (copy below). (02)
Pat's comment about NL dialog is also important. (03)
JFS
>> It's very rare for anyone to understand what other people are
>> saying without a dialog. Just look at any thread on Ontolog Forum. (04)
PC
> I completely agree. I am particularly concerned with how knowledge
> creators can put their information into a form understandable by any
> other computer or person, and this tactic seems to me thus far to be
> the only one with much of a chance to work. (05)
I also agree with Pat's concern about a CNL echo as a means of
verifying whether the computer correctly interpreted the input: (06)
PC
> But having that, one still needs to get the knowledge creator
> (or enterer) to sit long enough to verify the FOL interpretation
> (even if presented back in a very natural sounding CNL). (07)
Yes. Whenever you send some info to the computer (by typing, clicking,
speaking, or swiping), you need some feedback to verify that (a) you
entered the correct input and (b) the computer interpreted it the way
you had intended. (08)
Suggestion: During the day today, pay attention to the various
interactions you have with computers and with other people. (09)
Note that you always need to see or hear some response that indicates
that the message was interpreted correctly. For any task of any
complexity, the process usually takes multiple steps (i.e., a dialog).
We really need a lot more R & D on these issues. (010)
Following is the note about natural deduction. (011)
John
___________________________________________________________________ (012)
Dear Anonymous, (013)
I agree that natural deduction is a good method that should be
more widely taught and used. After reading your note, I added
Slides 31 and 38 (copy below). (014)
Slide 38 summarizes a very effective way of teaching logic. I have
been doing that with novices for years, and it works. I have also
presented the one-hour version in logic seminars for advanced groups
-- including Dana Scott's students at Carnegie-Mellon, Jon Barwise's
students at Indiana, and miscellaneous groups at workshops. (015)
John
_________________________________________________________________ (016)
From Slide 31 of http://www.jfsowa.com/talks/egintro.pdf (017)
Role of the Empty Sheet (018)
Both Peirce and Gentzen start a proof from an empty sheet. (019)
In Gentzen’s syntax, a blank sheet is not a well-formed formula.
● Therefore, no rule of inference can be applied to a blank.
● The method of making and discharging an assumption is the only
way to begin a proof. (020)
But in EG syntax, an empty graph is a well-formed formula.
● Therefore, a blank may be enclosed in a double negation.
● Then any assumption may be inserted in the negative area. (021)
Applying Peirce’s rules to predicate calculus:
● Define a blank as a well-formed formula that is true by definition.
● Define the positive and negative areas for each Boolean operator.
● Show that each of Gentzen’s rules is a derived rule of inference
in terms of Peirce’s rules. (022)
Then any proof by Gentzen’s rules is a proof by Peirce’s rules.
_________________________________________________________________ (023)
From Slide 38 (024)
Teaching Logic (025)
EGs are an excellent pedagogical tool for teaching logic at every
level from beginners to the most advanced. (026)
For people who were exposed to predicate calculus and hate it:
● First hour: EG syntax (along the lines of slides 2 to 11).
● Second hour: Theorem proving (with more examples than 20 to 24).
● Third hour: Draw EGs and ask the class how to prove them.
● After 3 hours, they say it’s the first time they understood logic. (027)
For advanced students:
● Cover the content of slides 2 to 37 in a one-hour seminar. (028)
Observation by Don Roberts at the University of Waterloo:
● Students who start with EGs and move to predicate calculus score
higher on exams than students who study only predicate calculus.
● The biggest improvement is in their ability to prove theorems. (029)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (030)
|