Logic Musings

[**** THESE PAGES SERIOUSLY UNDER CONSTRUCTION ****]

Why doesn't anyone have a largely complete chart of relationships between logic systems in machine processable form on line? [I have in mind something like the charts at the end of Hughes and Cresswell's Introduction to Modal Logic.] [*** UPDATE ***] I have started one...

Why have the axiomatic methods fallen out of favor for everyone not doing machine proofs? [Because natural deduction is more "natural"?]

Exactly what makes natural deduction feel so natural to everyone but me?

What is the *real* difference between:

How far can use cannonical forms to simplify matching be pushed in a practical automated proof system?

How far can proof sketches be pushed in machine assisted proofs?

How about a learning theorem prover saving its own proof sketches?

[.. Under construction ...]

Research notes

Gödel's theorem does not forbid a system from (correctly) proving its own consistancy. It only forbids a system strong enought to define multiplication and addition and equality from doing so.

There has been some research on systems that are strong enough to prove their own consistancy, but don't run afoul of Gödel because they are too weak to define +, *, and =. A few such systems are known. (Mostly from the papers of Dan Willard such as: ["Self Verifying Axiom Systems, the Incompleteness Theorem and the Tangibility Reflection Principle" in "Journal of Symbolic Logic" 66 (2001) pp. 536-596)]

This raises a few questions for me:

Skimpy unfleshed out papers to go here


Go to ...


This page is http://www.cc.utah.edu/~nahaj/logic/musings/index.html
This page was last modified on November 23rd, 2011.