>>11365512I studied this stuff extensively a few years ago, but forgot most of it, so take what I am about to write with a grain of salt. If someone knows better feel free to correct me.
1. As far as I am aware Gödel proved two incompleteness theorems for higher order predicate logic, in that every finitely axiomatized formal system using it, is incomplete (which means one cannot deduce all true propositions from it) and cannot proof its own consistency.
Undecidability -I think- was postulated by Turing and Church and constitutes a weaker version of Gödel’s theorem (Gödel implies undecidability, but not the other way around)
2. Gödel also proved a completeness theorem for first order logic. So there are (weak) complete, consistent formal systems (e. g. Euclidean geometry in Hilbert axiomatization). It’s not much, but at least something.
Only if you have a system strong enough to axiomatize arithmetics of natural numbers (e. g. ZFC or Peano axioms), you are lost.
