Halting problem = undecidability of all program properties?

[i]UNDERGRAD QUALITY[/i] incoming: An old thread on /math/ got me thinking about this. We know the typical proof uses
func G(x): if Halts(x, x) then loop forever
else false
and G(G) as a counterexample. Would this
func P(x): if ReturnsOdd(x, x) then 2
else 1
mean you can't prove a program always returns odd numbers because of P(P)? What about any other simple property like ``returns alphanumeric character'' or ``returns a valid s-expression''? You can always construct a function that ends in a contradiction by just returning the opposite thing.

AYYO HOL UP

Yes I understand the proof. But something still bothers me--a human can figure out whether or not a small program halts (or returns odd, etc.) by looking at the source and acceptable inputs. Why can't strong AI solve the halting problem then?