 Hilbert-Bernays-Löb derivability conditions

ID: hilbert-bernays-lob-derivability-conditions

□ A = Pr_{T} (┌ A ┐)

. The conditions are: if

T ⊢ A

then

T ⊢ □ A

;

T ⊢ □ (A \to B) \to (□ A \to □ B)

; and

T ⊢ □ A \to □□ A

. The first is an external rule, while the latter two are internal theorems. They formalize proof verification, closure under modus ponens rule and positive introspection. None licenses reflection from a proved sentence

□ A

A

 New to topics? Read the docs here!