Page 4 footnote 8 in the version you saw looks like footnote 9 in mine.
I don’t see how ‘proof-of-bottom → bottom’ makes a system inconsistent. This kind of formula appears all the time in Type Theory, and is interpreted as “not(proof-of-bottom)”.
The ‘principle of explosion’ says ‘forall A, bottom → A’. We can instantiate A to get ‘bottom → not(proof-of-bottom)’, then compose this with “proof-of-bottom → bottom” to get “proof-of-bottom → not(proof-of-bottom)”. This is an inconsistency iff we can show proof-of-bottom. If our system is consistent, we can’t construct a proof of bottom so it remains consistent. If our system is inconsistent then we can construct a proof of bottom and derive bottom, so our system remains inconsistent.
Have I misunderstood this footnote?
[EDIT: Ignore me for now; this is of course Lob’s theorem for bottom. I haven’t convinced myself of the existence of modal fixed points yet though]
Page 4 footnote 8 in the version you saw looks like footnote 9 in mine.
I don’t see how ‘proof-of-bottom → bottom’ makes a system inconsistent. This kind of formula appears all the time in Type Theory, and is interpreted as “not(proof-of-bottom)”.
The ‘principle of explosion’ says ‘forall A, bottom → A’. We can instantiate A to get ‘bottom → not(proof-of-bottom)’, then compose this with “proof-of-bottom → bottom” to get “proof-of-bottom → not(proof-of-bottom)”. This is an inconsistency iff we can show proof-of-bottom. If our system is consistent, we can’t construct a proof of bottom so it remains consistent. If our system is inconsistent then we can construct a proof of bottom and derive bottom, so our system remains inconsistent.
Have I misunderstood this footnote?
[EDIT: Ignore me for now; this is of course Lob’s theorem for bottom. I haven’t convinced myself of the existence of modal fixed points yet though]