# 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 about smallest (lexicly first if several) representitive of an equivalence class as the cannonical form?

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:

• Is such a logic strong enough to define a proof CHECKER? (This would give a proof checker with a formal proof of correctness) [I suspect it can]
• Is such a logic strong enough to define any theorem provers? [I suspect not] (This would give a theorem prover with a proof of correctness...).
• If the prior item were possible, could a condensed detachment theorem prover for a D-Complete system be done? [I suspect this is pure fantasy]