Characterization for unprovable formulas for first-order logic

96 Views Asked by At

Is there any existing work on characterizations of the unprovable formulas in (general) first-order logic? i.e. Gödel's incompletness result constructs an explicit formula that is valid but unprovable: are there other not-so-scary examples of unprovable formulas? are there some attempts/theories to characterize the explicit self-referential trait which prevents these formulas to be proven in any particular calculus?