Modal Logic – Initial Reference on Gödel-Löb Axiom in Kripke Semantics of GL

modal-logicreference-request

It seems well known in modal logic society that $\Box(\Box p\to p) \to \Box p$ in Kripke semantics of $GL$ implies well-foundedness of the relation i.e. no infinite ascending chains are allowed.

And validity of $GL$ additionally implies irreflexivity and transitivity of the relation.

But I am wondering what is the initial-like reference for the facts mentioned.

P.S. This question may not make clear anything interesting, this is just reference request to experts.

UPDATE It seems that Segerberg's thesis is tha earliest reference for the fist fact.

Concerning the second fact I reckon Dick de Jongh has proved this one, that said, unfortunately I could not find any reference.

Best Answer

The paper Provability: the emergence of a mathematical modality by Boolos and Sambin says (bottom of page $9$) that the first fact was independently gotten by Kripke and Segerberg, and gives the latter's $1971$ thesis as a reference. However, I can't find a copy of Segerberg's thesis online; the only promising link I found, http://lpcs.math.msu.su/~zolin/ml/pdf/Segerberg_Essay_1971.pdf, seems broken.

The second fact you mention has trivial first conjunct and false second conjunct (non-transitive frames may still be well-founded), and so I doubt there is a citation for it.

Related Question