Here's a quick proof of Godel's theorem, which can be made as formal as you like:
Theorem: Given any computable deductive system S (with a condition which is best stated afterward), write a computer program GODEL to:
- print it's code into a variable R (computer programs can do that)
- Deduce all consequences of S (computer can do that, by assumption)
- Halt if you see a proof that "R does not halt".
Then S cannot consistently prove that "GODEL does not halt". Informally, GODEL looks for "I do not halt" and halts if it finds it. The construction is basically identical to the informal statement, and the self-reference is by an obvious construction which is an exercize for first-year programming students.
The hidden assumption on S is that if a program P halts after a finite number of steps, then S will follow it step by step, and prove that it halts after a finite number of deductions. This is the main condition in Godel's theorem.
That's it, that's the proof. It is obvious that if GODEL halts, S is inconsistent, and if S is inconsistent, it proves any theorem, including "GODEL does not halt" at which point GODEL halts. So "GODEL halts" iff "S is consistent" and that's Godel's second theorem.
What it means is that a closed computable system of deduction, with no uncomputable method of producing new axioms, cannot produce all mathematical truths, in particular, it cannot prove it's own formal consistency.
This is not a barrier to formalization of mathematics as much as a tool. What it says is that starting with a simple theory S, say PRA, you can add "S is consistent" to produce S+1, then "S+1 is consistent" to produce S+2. After you run out of integers, you have an infinite list of theories, and you can enumerate all the theorems proved by all the theories and take the union, and this is the theory "S+ omega". The iteration continues up over all countable computable ordinals, and this produces higher theories, which eventually complete mathematics.
The only non-computable thing is naming higher and higher computable ordinals. This cannot be done algorithmically, but it can probably be done evolutionarily, using a random number generator. A true random number generator produces an uncomputable number. The goal is to convert this uncomputable number into a scheme for naming countable ordinals that converge onto the Church Kleene ordinal with probability 1 as you get more random digits. I don't know how to do this, but I don't know it's false either. This is a completion of Hilbert's program in a sense--- it shows you how to step up to get higher and higher theories.
That's enough about Godel's theorem.
Logical positivism is something else. It is first the claim that formal languages can describe all of experience, that formal first order predicate logic is sufficiently strong to speak about anything. This is true, because of Turing universality. Computers can simulate anything. Anything you run on a computer you describe in first order logic on integers.
It is also the claim that the understanding of the world is founded first on direct experience, and that all claims must be reduced to experience, and verified or falsified based on experience. Those claims which cannot be reduced to sensory experience are neither true nor false, they are moot.
The way I personally made this statement precise as a child (which, by the way, was also the very last time I ever got confused on any of this) is not by formalizing reduction to sense experience the way Carnap tried to do, but rather by defining the notion of positivistic equivalence classes. Logical theories make deductions, and this is equivalent to computational models. So two computational models are different when their predictions for sense impressions are different. They are equivalent when their predictions for sense impressions are the same. The positivist rule is then to identify any two identified theories as being fundamentally identical in content, and to not consider the question of whether model A or model B is the true as meaningful. It is no more meaningful then asking whether electrodynamics is in Coulomb gauge or in Landau gauge, the question is meaningless, because the sense experience predicted either way is the same.
This does not require you to formally build everything from the ground up starting with sentences about observations, it requires you only to compare formal models using their observational consequences, and when these consequences are identical, to freely switch between either model without considering the two conceptions as different. I do this all the time, all physicists learn to do it, it's the "change of gauge" in gauge theory, or the "change of coordinate systems" in General Relativity, or the "change of basis" in quantum mechanics. If you ask a physicist "which gauge?", "which coordinates?", "which basis?" they laugh. The question is obviously meaningless.
This keeps the basic principle of Mach and Carnap, gives it a formal meaning, gives it precise examples from physics (so that you can't say it's nonsense) and avoids making a formal separator between sensory sentences and non-sensory sentences. All you need is to be able to compare a sensory prediction, a deduction from the formal model, to a sensory input, something which you can program a computer to do, so there is no mystery here.
Further it allows evolution of models, as ones that conflict with data are rejected, ones that match data survive, and ones that don't differ with respect to data are identified with one another. You can implement evolution on the models, and then you can model cognition (poorly).
Technically it also requires an Occam's razor, so that you throw away complicated arbitrary models for simpler ones. You could state this formally in terms of the length of the program involved, but you have to be careful to think of it in terms of the "ultimate program", meaning an idealized total predictive model thing underneath, like your personal theory of everything in life, not in terms of the specific subprogram for any one particular phenomenon. If your smoke alarm consistently goes off every day for 10 years when you cook fish, the simplest program isn't "alarm will go off forever", because it includes the possibility that your battery will one day run out of charge, even though you haven't seen it happen yet. You know what I mean.
That's positivism. It's evolution in the head. It dismisses as meaningless the metaphysical questions in the same way Carnap says, and in a sense, it does reduce everything to sense experience, because if you have a data structure encoding the sense experience that allowed you to evolve the theory, you can describe the evolution from the rejected or accepted experience, and you can do the Carnap manipulations to turn everything into sentences about the sense experience along with sentences that describe the algorithms you are evolving at this particular point.
Anyway, it's not a deep idea today, after Turing, when people know what a computer is. It's just something one sorts out as a child, when one thinks back on early childhood, as you made sense of the world, and say "how the heck did I do that?" It's just what Mach's positivism was all about.
The statements are of the nature of definitions of terms, what does it mean to understand something? What does it mean to have a meaningful question? It just defines the underlying computational processes involved in understanding meaning. These are not things which one can verify in any way, because they define precisely things that have no precise definition otherwise. The same way as you can't ask "How do you prove that F=ma from Newtonian mechanics?", you can't ask "How do you prove that the verification principle is valid" in positivism, it's an axiom, it defines what the word "understanding" means precisely computationally. Once you define this, then you can ask about verifying other statements, statements about the world.
It's also not hard to understand, compared to any nontrivial theorem, or any real science. It's just a founding philosophy. I also don't claim it's any extension of Carnap, because Carnap already understood all the consequences: the elimination of metaphysics, the justification of induction, the computational idea of mind, and so on. It's just an explanation with some hindsight.
