 Solovay’s completeness theorem provides an alternative way to construct many arithmetical sentences that are not provable in Peano Arithmetic. For example, it is easy to make a possible worlds model to show that GL does not prove \(\Box p \vee \Box\neg\, p\), so by Solovay’s theorem, there is an arithmetical sentence \(f(p)\) such that Peano Arithmetic does not prove \(\Prov(\ulcorner f(p)\urcorner ) \vee \Prov(\ulcorner \neg\, f(p)\urcorner )\). In particular, this implies that neither \(f(p)\) nor \(\neg\, f(p)\) is provable in Peano Arithmetic; for suppose on the contrary that \(\PA \vdash f(p)\), then by Löb’s first condition and propositional logic, \(\PA \vdash \Prov(\ulcorner f(p)\urcorner ) \vee \Prov(\ulcorner \neg\, f(p)\urcorner )\), leading to a contradiction, and similarly if one supposes that \(\PA \vdash \neg\, f(p)\).