Suppose proves every specified reflection instance. Use only the instance with . The deduction theorem givesClassical propositional reasoning turns this into : if already holds the implication is true, while otherwise holds and the displayed theorem supplies it. Löb's theorem now yields , making inconsistent. Therefore no sentence consistent with can supply all the local reflection instances in a one-sentence extension. The proof uses just one well-chosen instance, and never applies necessitation to a derivation with the extra assumption still open.
Articles by others on the same topic
There are currently no matching articles.