Blog post: ydoaPs: There and Back Again: The long LONG road to Gödel

There was significant interest in this series, so I've decided to go ahead and do it. Bear in mind, this will not be a replacement for a detailed rigorous course in metamathematics, but I hope it will be enough for you to follow along with various formal systems.

To follow the proof, we'll need the tools of metamathematics. This, however, requires formal logic. So, here we begin:

What is logic? How is it different from math? Well, they're both formalisms. Roughly speaking, logics deal with values and maths deal with quantities. That's not a rigorous distinction, but it's enough to just get a working difference. Aside from that, they're virtually identical ideas. They are languages, what they languages mean, and how we use them.

A formal language can be really anything you want. It's formal; you get to make it! All you need for a formal language is a set of allowed "primitive symbols" (think of letters of a word-in fact, they're often called "letters" and are often actually letters) and rules for combining them into what are called "well-formed formulas" ("wffs" for short). That should really make sense. We don't need the meaning or usage to have a language. If aliens visit Earth in ten million years and all of humanity is dead, they could find something like Wikipedia. From this large body of language, they could learn the language. They can learn what letter combinations are permissible to make words and what word combinations are permissible to make sentences. What they couldn't learn, however, is the semantics.

In fact, we don't even need the semantics to use logic. To use it, all we need is to make a formal system. If we're using a language in a system without a semantic, then our system is using an "uninterpreted language". All a system is is the language, a set of axioms, and rules which let us write new wffs from he axioms and any wffs that follow from the use of the rules.

The semantic is what the language means. It's often that wffs have "True" or "False" values, but that need not be the case. Like with mathematical systems, the semantic could be about quantities. Our systems will, however, have Truth Values.

So, to recap: once you have a language, you can do two things either independently or jointly-you can make a formal semantic and/or you can make a formal system. This has been very non-technical and non-rigorous, but we will get more rigorous as we go along. Now, onto application.

We need to start with what is often called "Propositional Calculus". The name kind of gives away the idea behind the semantic and system; it's "the math of ideas". That's actually a pretty good way to think about it. So, let's get to work and define our language:

Our primitive symbols come in two large flavors-connectives and letters.

Our letters can be any english letter or greek letter (the greek letters will stand for entire wffs picked at random). Some letters will be variables and others will be constants, but we need not worry about that now.

The connectives are as follows:

'?', '?', '˜', '•', '?', ')', '('

That's it. We just have letters and five connectives (not counting parenthesis). Not bad, eh? Now, how to we hook these things together to make sense?

Any letter is a wff. For any wffs '?' and '?', the following are wffs:

~?

???

???

?•?

???

(?)

That's it! There's our language. Next up, the semantic!Read and comment on the full post