There are two kinds of languages, formal and informal. *Informal languages* rely on both semantics and syntax to construct intelligible thoughts. *Formal languages* have a special property which allows us to use either syntax or semantics to get a sentence. But that’s a long way from a thought expressed in a natural language. Let’s take a little trip through mathematical logic, the linguistics of mathematics.

A formal language is defined by three things:

- A
*lexicon*which unambiguously defines the set of ‘words’ in the language. We call these words*symbols*. A formal lexicon completely defines the symbols allowed in the formal language. - We also need a notion of
*sentences*derived by syntax rules. A sentence of a formal language constructed properly according the the grammar rules of the syntax is called a*formula.* - Finally, we require a
*semantics*which correlates symbols and their meanings.

Mathematical logic considers two fundamental questions about such formal languages.

Suppose we have a formula \varphi of a language \ell. We can ask:

*Is \varphi true?*This explores the semantic structure of \ell. Model Theory is the study of semantic structures.*Can \varphi be proved?*This explores the syntactical structure of \ell. Proof Theory is the study of syntactical structures.

An amazing fact of formal languages is the following:

\varphi \vdash\psi \iff \varphi\models\psi (Soundness and Completeness)

Let’s think about what this means. ‘\varphi \vdash\psi‘ means that the formula \psi can be derived from the formula \varphi by the grammar rules of \ell. When we construct a formula from a finite and valid sequence of grammar transformations, we say we have *inferred* the final formula. So, ‘\varphi \vdash\psi‘ can be read as ‘\varphi syntactically implies \psi‘ or as ‘infer \psi from \varphi‘.

The formula ‘\varphi\models\psi‘ means that the *meaning* of \varphi *entails* \psi. Something is the world makes this so, causality perhaps. Although other things can also entail. Then, ‘\varphi\models\psi‘ can be read as either ‘ \varphi semantically entails \psi‘ or just as ‘from \varphi entail \psi‘.

The `\iff‘ symbol means that when we have syntactical implication we also have syntactic entailment. That is, syntax and semantics are equivalent. Grammar and meaning are the same thing in some basic way. Without this fundamental property mathematics would be impossible, yet informal languages lack this property!

We are perfectly able to create syntactically correct sentences that have no real meaning. A famous example:

Colorless green ideas sleep furiously.

This is grammatically correct according the rules of the parts of speech, but it makes no sense whatsoever.

In a formal language, this can never happen. If the syntax rules are followed, that sentence is true. That’s why this works:

\begin{matrix}3x + 1 & = & 10 \\3x & = & 9 \\x & = & 3\end{matrix}You don’t need to know what the object x is. If you follow the grammar rules of algebra, you are guaranteed to get the right answer.

And that’s how computers do computations – as pure syntax with no reference whatsoever to the meaning of the symbols or formulas. Computers can compute because of the Soundness and Completeness Property of formal languages. Even though they don’t know what they are doing, computers still get the right answer because in these special languages syntax alone can give the right answer.

But thinking in a natural language isn’t like this. We need both syntax and semantics to match up for things to “make sense”. Remember our furiously sleeping colorless green ideas? Makes no sense because the syntax and semantics don’t match up. For us, syntax and semantics are not equivalent. Human insight comes from the requirements that truth places on language.

Computers can never gain that kind of insight, and so they can never really think. They can compute, but they can’t think. This doesn’t take into consideration other problems, like the way we use background knowledge to think. That’ll be the subject of another article.