Reinhard Kahle and Wilfried Keller logo_ttlM. Antonia Huertas, João Marcos,
María Manzano, Sophie Pinchinat,
François Schwarzentruber54th International Conference on Tools for Teaching
Logic1175TTL2015

# Syntax versus Semantics

Reinhard Kahle  CMA and DM, FCT, Universidade Nova de Lisboa
P-2829-526 Caparica, Portugal
<EMAIL_ADDRESS>Wilfried Keller  Universität des Saarlandes
66123 Saarbrücken, Germany
<EMAIL_ADDRESS>
###### Abstract.

We report on the idea to use colours to distinguish syntax and semantics as an
educational tool in logic classes. This distinction gives also reason to
reflect on some philosophical issues concerning semantics.

###### Key words and phrases:

syntax, semantics, colour, philosophy, teaching

###### 1991 Mathematics Subject Classification:

F.4.1, F.4.m

††footnotetext: Acknowledgements. The first author was partially supported by
the Fundação para a Ciência e a Tecnologia (Portuguese Foundation for Science
and Technology) through the projects _The Notion of Mathematical Proof_
(PTDC/MHC-FIL/5363/2012) and UID/MAT/00297/2013 (Centro de Matemática e
Aplicações). We thank the anonymous referees for helpful comments.

##  1\. Introduction

When the first author attended as a first year student a logic course at a
philosophy department, he was wondering why the professor was repeating, after
introducing the relation $\vDash$, “the same” again but using the symbol
‘$\vdash$’. It was, most likely, the negligence of the student, and not the
presentation of the professor, which caused this fundamental misunderstanding.
In retrospect, there is one question which might make one wonder: how was it
possible to miss one of the most fundamental distinctions in modern logic? On
a more mature stage, as third year student, the problem repeated itself on a
different level: speaking about Gödel’s first incompleteness theorem with a
teaching assistant, he refused to continue the discussion when the question
was raised what its meaning is from the perspective of “proper Mathematics”.
Again, the distinction of syntax and semantics wasn’t clearly seen and the
discussion stalled when the participants did not realize that reference of a
term like “proper Mathematics” need to be better specified while entering into
a discussion of Gödel’s theorem.

Based on the experiences above, when starting to teach logic courses by
himself, the first author took it as a particular challenge to present the
problems concerning the distinction of syntax and semantics in a persuasive
way. In this paper, we present the chosen solution: the use of colours to
distinguish the syntactical and semantical role of logical text. We also
report on some of the educational insights one might win with this approach
together with certain philosophical questions which surface (again) in this
context.

We assume that the reader is familiar with first-order logic and has, at
least, an idea of Gödel’s incompleteness theorems. Without formal
introduction, we use the standard notations of first-order logic and Peano
Arithmetic, using typically Greek letters from the end of the alphabet to
denote formulae.

##  2\. First-order logic

Let us go _in media res_ and recall the definition of the satisfiability
relation $\models$ for first-order logic as given by Barwise in [3, p. 21].

######  Definition 2.1.

Let $\mathfrak{M}$ be an L-structure. We define a relation

$\mathfrak{M}\models\varphi[s],$

(read: the assignment $s$ satisfies the formula $\varphi$ in $\mathfrak{M}$)
for all assignments $s$ and all formulae $\varphi$ as follows.

  1. [(i)]

  2. (1)

$\mathfrak{M}\models(t_{1}=t_{2})[s]$ iff
$t_{1}^{\mathfrak{M}}(s)=t_{2}^{\mathfrak{M}}(s)$,

  3. (2)

$\mathfrak{M}\models R(t_{1},\dots,t_{n})[s]$, iff
$(t_{1}^{\mathfrak{M}}(s),\dots,t_{n}^{\mathfrak{M}}(s))\in R^{\mathfrak{M}}$,

  4. (3)

$\mathfrak{M}\models(\neg\varphi)[s]$ iff not $\mathfrak{M}\models\varphi[s]$,

  5. (4)

$\mathfrak{M}\models(\varphi\wedge\psi)[s]$ iff
$\mathfrak{M}\models\varphi[s]$ and $\mathfrak{M}\models\psi[s]$,

  6. (5)

$\mathfrak{M}\models(\varphi\vee\psi)[s]$ iff $\mathfrak{M}\models\varphi[s]$
or $\mathfrak{M}\models\psi[s]$,

  7. (6)

$\mathfrak{M}\models(\varphi\rightarrow\psi)[s]$ iff either not
$\mathfrak{M}\models\varphi[s]$ or else $\mathfrak{M}\models\psi[s]$,

  8. (7)

$\mathfrak{M}\models(\exists v.\varphi)[s]$ iff there is an $a\in M$ such that
$\mathfrak{M}\models\varphi[s(^{a}_{v})]$,

  9. (8)

$\mathfrak{M}\models(\forall v.\varphi)[s]$ iff for all $a\in M$,
$\mathfrak{M}\models\varphi[s(^{a}_{v})]$.

Barwise then states: “There is nothing surprising here. It is just making sure
that each of our symbols means what we want it to mean.”

This is certainly correct, but it might be worth to reflect shortly what this
definition actually does.111Here a disclaimer is in order. In the following we
don’t intend to criticise Barwise’s presentation; first, the citation is taken
from a handbook article and not from a textbook (and we may add: from an
excellent article in an excellent handbook); secondly, mathematically there is
no issue here, the definition is surely the correct one; we are just looking
for aspects which are of interest in an educational perspective. Looking, for
instance, to the clauses for conjunction and disjunction, it simply “lifts”
the symbols ‘$\wedge$’ and ‘$\vee$’ to the _meta-level_ using the natural
language expressions “and” and “or”. Thus, who understands “and” and “or” is
supposed to understand how to obtain the truth value of a formula using
‘$\wedge$’ or ‘$\vee$’. The _meta-level_ comes into play, because the natural
language terms are outside of the $\models$ relation, while the logical
symbols are inside. Nothing surprising here, as said. We will see later in § 6
that the situation for the negation is actually more subtle than it looks (and
this is a first educational pitfall!). But the issue we like to start with is
unambiguously expressed by Barwise (in continuation of the citation above):

> There is one possibly confusing point, in (i), caused by our using $=$ for
> both the real equality (on the right-hand side) and the symbol for equality
> (on the left). Many authors abhor this confusion of use and mention and use
> something like $\equiv$ or $\approx$ for the symbol.

It is this confusion222And it might be doubted, whether the difficulty at hand
is best couched in terms of use and mention. It seems to us rather clear,
however, that it is educationally not best dealt with by introducing
subtleties of quotation theory., which will repeat itself when one comes to
the language of arithmetic, we like to address. As Barwise remarks, many
authors try to resolve the problem by the use of different symbols for
syntactical and semantical equality. This would be a way out, but it comes at
the price that the formal language appears artificial, in particular, if this
is extended to arithmetical terms. Let us mention the clumsy notation
$\textbf{k}_{n}$ for the numeral representing the number $n$ in the classical
textbook of Shoenfield [15]. With respect to equality, Sernadas and Sernadas
[14], for instance, use $\cong$ as special sign on the syntactical side. Cori
and Lascar [5] use, quite generally, a bar over the syntactical symbol to
refer to its _semantic_ interpretation. However, in general (and with good
reasons), the syntactic symbols are chosen to match exactly with their
intended meaning; the resulting “overloading” is just a problem when the
difference of syntax and semantics is the subject under discussion.

Our solution is to use the same symbols, but different colours to distinguish
the use of symbols on the syntactical and semantical side. So, let us choose
red for syntax and blue for semantics.333The particular choice of the colours
is arbitrary; it is, however, known that one should avoid yellow and green for
beamer presentations. After giving a definition of first-order language with
all syntactic expressions in red, and the definition of a structure with blue
for the elements of the structure, the definition above reads as follows:

######  Definition 2.2.

Let $\mathfrak{M}$ be an L-structure. We define a relation

${\color[rgb]{0,0,1}{\mathfrak{M}\models{\color[rgb]{1,0,0}{\varphi}}[s]}},$

(read: the assignment ${\color[rgb]{0,0,1}{s}}$ satisfies the formula
${\color[rgb]{1,0,0}{\varphi}}$ in ${\color[rgb]{0,0,1}{\mathfrak{M}}}$) for
all assignments ${\color[rgb]{0,0,1}{s}}$ and all formulae
${\color[rgb]{1,0,0}{\varphi}}$ as follows.444For sure, as one referee pointed
put, colouring these expressions does not remove entirely the possibility of
misunderstanding: The functional expression
${\color[rgb]{1,0,0}{t_{1}}}^{{\color[rgb]{0,0,1}{\mathfrak{M}}}}$, for
instance, takes the syntactic argument ${\color[rgb]{1,0,0}{t_{1}}}$ and
evaluates it relative to the semantic model
${\color[rgb]{0,0,1}{\mathfrak{M}}}$—so the value of the whole expression of
course denotes a blue item. The interpretation function itself does not appear
in this notation, and therefore, luckily, we do not have to decide on its
colour. However, with interested students we had some interesting discussions
about its colour.

  1. [(i)]

  2. (1)

${\color[rgb]{0,0,1}{\mathfrak{M}\models{\color[rgb]{1,0,0}{(t_{1}=t_{2})}}[s]}}$
iff
${\color[rgb]{0,0,1}{{\color[rgb]{1,0,0}{t_{1}}}^{\mathfrak{M}}(s)={\color[rgb]{1,0,0}{t_{2}}}^{\mathfrak{M}}(s)}}$,

  3. (2)

${\color[rgb]{0,0,1}{\mathfrak{M}\models{\color[rgb]{1,0,0}{R(t_{1},\dots,t_{n})}}[s]}}$,
iff
${\color[rgb]{0,0,1}{({\color[rgb]{1,0,0}{t_{1}}}^{\mathfrak{M}}(s),\dots,{\color[rgb]{1,0,0}{t_{n}}}^{\mathfrak{M}}(s))\in{\color[rgb]{1,0,0}{R}}^{\mathfrak{M}}}}$,

  4. (3)

${\color[rgb]{0,0,1}{\mathfrak{M}\models{\color[rgb]{1,0,0}{(\neg\varphi)}}[s]}}$
iff not
${\color[rgb]{0,0,1}{\mathfrak{M}\models{\color[rgb]{1,0,0}{\varphi}}[s]}}$,

  5. (4)

${\color[rgb]{0,0,1}{\mathfrak{M}\models{\color[rgb]{1,0,0}{(\varphi\wedge\psi)}}[s]}}$
iff
${\color[rgb]{0,0,1}{\mathfrak{M}\models{\color[rgb]{1,0,0}{\varphi}}[s]}}$
and ${\color[rgb]{0,0,1}{\mathfrak{M}\models{\color[rgb]{1,0,0}{\psi}}[s]}}$,

  6. (5)

${\color[rgb]{0,0,1}{\mathfrak{M}\models{\color[rgb]{1,0,0}{(\varphi\vee\psi)}}[s]}}$
iff
${\color[rgb]{0,0,1}{\mathfrak{M}\models{\color[rgb]{1,0,0}{\varphi}}[s]}}$ or
${\color[rgb]{0,0,1}{\mathfrak{M}\models{\color[rgb]{1,0,0}{\psi}}[s]}}$,

  7. (6)

${\color[rgb]{0,0,1}{\mathfrak{M}\models{\color[rgb]{1,0,0}{(\varphi\rightarrow\psi)}}[s]}}$
iff either not
${\color[rgb]{0,0,1}{\mathfrak{M}\models{\color[rgb]{1,0,0}{\varphi}}[s]}}$ or
else ${\color[rgb]{0,0,1}{\mathfrak{M}\models{\color[rgb]{1,0,0}{\psi}}[s]}}$,

  8. (7)

${\color[rgb]{0,0,1}{\mathfrak{M}\models{\color[rgb]{1,0,0}{(\exists
v.\varphi)}}[s]}}$ iff there is an ${\color[rgb]{0,0,1}{a\in M}}$ such that
${\color[rgb]{0,0,1}{\mathfrak{M}\models{\color[rgb]{1,0,0}{\varphi}}[s(^{{\color[rgb]{0,0,1}{a}}}_{{\color[rgb]{1,0,0}{v}}})]}}$,

  9. (8)

${\color[rgb]{0,0,1}{\mathfrak{M}\models{\color[rgb]{1,0,0}{(\forall
v.\varphi)}}[s]}}$ iff for all ${\color[rgb]{0,0,1}{a\in M}}$,
${\color[rgb]{0,0,1}{\mathfrak{M}\models{\color[rgb]{1,0,0}{\varphi}}[s(^{{\color[rgb]{0,0,1}{a}}}_{{\color[rgb]{1,0,0}{v}}})]}}$.

Now, the difference of ${\color[rgb]{1,0,0}{=}}$ and ${\color[rgb]{0,0,1}{=}}$
is obvious; the “possible confusion” will even catch the student’s eye, and
this is of particular educational value. In addition, the quantifier clauses
allow to distinguish better between the syntactical object variable
${\color[rgb]{1,0,0}{v}}$ and the semantical _element_
${\color[rgb]{0,0,1}{a}}$—even if ${\color[rgb]{0,0,1}{a}}$ is here, of
course, a meta-variable for “real elements” of ${\color[rgb]{0,0,1}{M}}$.

Introducing now, as counterpart to the semantic consequence relation, a
derivation relation ${\color[rgb]{1,0,0}{\vdash}}$ which exclusively, deals
with red objects, syntactic and semantic reasoning is already distinguished by
colours. It is our teaching experience, that these colours are of great help
for the students, providing some kind of orientation in rather technical
proofs like these for the compactness and the completeness theorem. As prime
examples for the use of colours we may also mention the Skolem paradox, which,
like the completeness theorem, can be regarded as a corollary of the
compactness theorem.

And so the question of soundness and completeness is the next one to be
addressed. Even in a compact course on Gödel’s incompleteness theorems these
results of Gödel’s dissertation should be discussed.555In introductory logic
courses in philosophy seminars these results will usually not be proven, but,
of course, deserve at least to be mentioned and discussed. Today, they are
usually not proven along the lines of Gödel’s original work, but rather with
the well-known technique introduced by Henkin. This technique is standard for
many completeness proofs for quite a couple of logics and, therefore,
constitute an integral tool in the toolbox of the mathematical logician: it
proceeds by constructing a blue world (validating the negation of a formula,
that cannot be proven in the syntactic calculus) out of the red material
itself. (The situation is somewhat dual to the more demanding case of (set-
theoretic) forcing, where one, so to speak, bestows properties of a language
on certain blue sets, thereby emulating the red world with originally blue
objects.)

##  3\. Arithmetic

The use of the colours exhibits its real potential only, when we study
Arithmetic and want to motivate, for instance, Gödel’s incompleteness theorems
for Peano Arithmetic. In its original form, Gödel’s proof actually entirely
refrains from the semantic realm and in some sense requires only “red”
reasoning. It, indeed, is a theorem about the red world, but one that operates
on a meta-level. It speaks about the axiomatic system, but it does not reason
about its meaning, quite like Hilbert’s attempted consistency proofs do. And
likewise it uses only finitistically acceptable means. In [6, fn. 1, p. 337]
the editors explicitly attribute Gödel’s avoiding of the concept of truth in
his 1931 paper to the “respect for the ‘prejudice’ of the Hilbert school.”
Further reflections can be found in [7].

But, of course, the first incompleteness theorem can—and probably should—be
motivated by the question whether Peano Arithmetic is complete with respect to
the _standard model_. Peano Arithmetic may be defined over the set
$\\{{\color[rgb]{1,0,0}{0}},{\color[rgb]{1,0,0}{S}},{\color[rgb]{1,0,0}{+}},{\color[rgb]{1,0,0}{\cdot}}\\}$
of non-logical symbols. The standard model, as semantic object, can be given
in blue as follows:
${\color[rgb]{0,0,1}{\mathfrak{N}=\langle\mathbb{N},0,S,+,\cdot\rangle}}.$ It
goes without saying that the red symbols should be interpreted by their
respective blue counterparts. Gödel’s first incompleteness theorem tells us,
that the red world, as long as a consistent recursive axiomatic system is
chosen, will miss some formula _and_ its negation666Of course on pain of
inconsistency it should _not_ prove any formula together with its negation.,
it cannot decide all given formulae by proof. However, the blue world so to
speak decides formulae: Either a formula or its negation is satisfied (in a
model by a valuation); this is a direct consequence of clause (iii) in Def.
2.1 (see also §6 below). There is no gap in the blue world—but there will
always be one in the (sensibly chosen, i.e., recursive and consistent) red
one. This then not only entails that no red world (as above) fixes the blue
world of Arithmetic as its only model—this could already be concluded from
Löwenheim–Skolem—but that not all red statements that are true about the blue
world can be proven in the red realm.

So, _how_ are the blue objects in
${\color[rgb]{0,0,1}{\mathfrak{N}=\langle\mathbb{N},0,S,+,\cdot\rangle}}$
actually given? ${\color[rgb]{0,0,1}{\mathbb{N}}}$ as the set of natural
numbers ${\color[rgb]{0,0,1}{\\{0,1,2,\dots\\}}}$ can be taken for granted,
and with it, of course, also the object ${\color[rgb]{0,0,1}{0}}$. But what
_is_ ${\color[rgb]{0,0,1}{+}}$? It should be, of course, the set of all
triples
$({\color[rgb]{0,0,1}{a}},{\color[rgb]{0,0,1}{b}},{\color[rgb]{0,0,1}{c}})$
such that
${\color[rgb]{0,0,1}{a}}+{\color[rgb]{0,0,1}{b}}={\color[rgb]{0,0,1}{c}}$. But
this doesn’t help us, as we just moved the question to another level, writing
$+$ in black (this plus sign can, of course, not be blue if we don’t want to
run into an immediate circle). To avoid it, one could get back to use of dots
and say that ${\color[rgb]{0,0,1}{+}}$ is the set:

$\displaystyle\\{$
$\displaystyle{\color[rgb]{0,0,1}{(0,0,0)}},{\color[rgb]{0,0,1}{(0,1,1)}},{\color[rgb]{0,0,1}{(0,2,2)}},{\color[rgb]{0,0,1}{(0,3,3)}},\dots$
$\displaystyle{\color[rgb]{0,0,1}{(1,0,1)}},{\color[rgb]{0,0,1}{(1,1,2)}},{\color[rgb]{0,0,1}{(1,2,3)}},{\color[rgb]{0,0,1}{(1,3,4)}},\dots$
$\displaystyle{\color[rgb]{0,0,1}{(2,0,2)}},{\color[rgb]{0,0,1}{(2,1,3)}},{\color[rgb]{0,0,1}{(2,2,4)}},{\color[rgb]{0,0,1}{(2,3,5)}},\dots$
$\displaystyle\qquad\vdots\hskip 150.0pt\\}.$

In fact, we see only two ways out of this situation: First, we appeal to the
common platonism in mathematics and stipulate that ${\color[rgb]{0,0,1}{+}}$
exists in the structure ${\color[rgb]{0,0,1}{\mathfrak{N}}}$ in the way we
expect it and with the properties we want it to have. Or, secondly, we treat
${\color[rgb]{0,0,1}{+}}$ as a proper set-theoretic object and construct it
within our favorite axiomatic set theory, let’s say ZFC.

While the second one is a solution concerning the level of Arithmetic, it
simply shifts the problem to set theory. Within ZFC, the defined
${\color[rgb]{0,0,1}{+}}$ would be a red object (relative to ZFC), and we
would have to ask now, how the models of ZFC look like—which is, not
surprising, a much harder question than to look for structures for Arithmetic,
not only in a technical sense, but also in a philosophical one; in particular,
it leads us simply back to the situation we are discussing for
${\color[rgb]{0,0,1}{+}}$ just for other, now set-theoretical, objects.

For the first option, the sheer existence of ${\color[rgb]{0,0,1}{+}}$
presupposes a certain form of platonism. This platonism allows to dispose of
any further technical questions, but one enters a dangerous philosophical
terrain.

We may leave aside here the preferred way out (this is a philosophical
question—but one which is naturally asked in this context and can nicely be
brought out and talked about with the help of our colours); what we consider
as an important lesson for the teaching of logic is, that any discussion of
the syntax/semantics distinction in the context of Arithmetic—and, _a
fortiori_ , in relation to Gödel’s Incompleteness Theorems—has to presuppose
some “blue objects”. And this presupposition is far from being trivial. As a
minimal conclusion, we like to state that an unreflected “identification” of,
for instance, the “syntactical addition” (symbol) ${\color[rgb]{1,0,0}{+}}$
with the “semantical addition” (function) ${\color[rgb]{0,0,1}{+}}$ prevents a
student from any understanding of the problem which is at issue here.

##  4\. Gödel’s Incompleteness Theorems

Gödel’s Incompleteness Theorems are, without doubt, the most important results
in mathematical logic. They are, however, clouded by continuing philosophical
misunderstandings,777For a detailed discussion, in particular in view of
Gentzen’s later results, we refer to [10]. and a pure formal presentation of
the results can easily support such prejudices.888An extreme case was reported
from a philosophical seminar: the participants, after studying carefully—and
probably painfully—a formal presentation of Gödel’s proof, came to the
conclusion that, yes, after all the results seem to be correct _if one has a
language with 7 symbols; but, of course, one doesn’t know whether it still
holds when one would have 8 symbols_.

We like to address only one problem coming from the fact that many
presentations make use of the _Chinese remainder theorem_. Apparently, here
proper mathematics is used to prove something about formal systems for
mathematics and one may wonder whether there is some kind of vicious circle in
the back.999The first author remembers an elaboration of a Math student of a
course presentation of Gödel’s theorems which focussed nearly entirely on the
use of the Chines remainder theorem; apparently it was the only part of the
proof the student was properly understanding based on his Math classes. This
is, of course, not the case; in fact, the use of this theorem is only relevant
for a certain technical step, in particular in the case of Peano Arithmetic,
and it is irrelevant for other axiomatization or codings (see [16, §3.2.6]).
Hao Wang reported this from interviews with Gödel [17, p. 653]: “He enjoyed
much the lectures by Furtw[ä]ngler on number theory and developed an interest
in this subject which was, for example, relevant to his application of the
Chinese remainder theorem in expressing primitive recursive functions in terms
of addition and multiplication.” Thus, what is at issue here is the
representation of primitive recursive functions in the formal arithmetical
theory. Albeit, it is, of course, possible to develop primitive recursion _in_
such theories, a proper educational approach _can_ “outsource” primitive
recursion.

We did that by setting up a new realm for primitive recursion (formally a
functional algebra, consisting of function symbols and equalities)—and using a
new colour for it, as, for the moment, it can be located outside of the red
and blue world. After providing a sufficient stock of primitive recursive
functions, one simply proves the representation theorem showing that every
such function can be represented in the formal theory under consideration (as
Peano Arithmetic, for instance). In the particular case of Peano Arithmetic,
this proof may use the Chinese remainder theorem—but it is obvious that it is
not relevant if one would provide another proof, in particular for other
theories. In addition, it should become clear that Gödel’s theorems can be
carried out in essentially the same way for all theories allowing for the
appropriate representation theorem.

With respect to the Chinese Remainder Theorem and the like the diagnosis is as
following: The Chinese Remainder Theorem is—as far as Gödel’s first
incompleteness theorem is concerned—at the level of meta theory, but not
necessarily in the blue world. It deals with the recursion-theoretic realm,
concerning codings, and can be outsourced and imported if needed.

The situation changes however, if one wants to proceed to the second
Incompleteness Theorem: There one repeats the proof of the first completely
inside the red theory. For that case it is of vital importance that one uses
codings and theorems that can be reproduced in the object theory itself—this
is the sense in which it is “occasionally not just important [in logic] what
you prove, but how you prove it” [12, p. 190].

##  5\. “Semantics comes first”?

The dictum “Semantics comes first” is attributed to Tarski.101010The well-
known computer software package _Tarski’s World_ [2] illustrates this slogan
quite appropriately when the student can literally manipulate the semantical
objects. And it has some rationale: in first-order logic as well as in
Arithmetic, we presuppose the _meanings_ of the logical and arithmetical
expressions before we start to manipulate them. It is, in general, seen as a
task of the axiomatization to provide calculi which capture such meaning—and
the completeness theorems should show us that the axiomatization was
successful.

As much as completeness theorems are concerned, they give us— _a posteriori_
—the possibility to identify the red with the blue objects. But, to make sense
out of a completeness theorem—and to prove it—the difference of the
syntactical and semantical expression has to be seen clearly. In this
perspective, we could even propose that one could forget of the red and blue
colour for, let say, equality, _after_ the proof of the completeness theorem
for first-order logic.

But there is still an issues to discuss which might call Tarski’s dictum in
question.

First, the dictum makes sense only, if the semantics is _understood before_
the syntax. It is doubtful that semantics could serve its purpose if it is, by
itself, not fully understood. For first-order logic and Arithmetic it should
be the case that their semantics is clear (although we mentioned the problem
to precisely articulate it in the case of ${\color[rgb]{0,0,1}{+}}$, for
instance). And this holds probably also for most of the mathematical theories
we are familiar with.

The situation changed drastically, when Computer Science entered the stage.
Semantics of programming languages is a rather challenging topic in CS. And
here, the syntax is essentially always prior to the semantics. Instead of
finding an axiomatization for a given semantics, now one looks for a semantics
for a given programming language. But it is not only that such a semantics is
no longer “first”, it might be the case that proposed semantics are, in a
technical sense, more complicated than the programming language in itself (as
example, we may refer to [1]). In some cases, one might wonder in which sense
such semantics provide any _meaning_.111111A colleague expressed this in a
sarcastic statement: “They put these brackets $\llbracket\cdot\rrbracket$
around something and believe they have achieved something.”

From the educational perspective, this only means that logic cannot any longer
be taught with Tarski’s dictum as a rock solid starting point. The
differentiation of syntax and semantics becomes even more significant. What it
means to put “syntax first” we will discuss in the next section.

##  6\. Intuitionism

When Brouwer conceived his mathematical philosophy of _intuitionism_ he had
definitely nothing formal in mind. However, based on the “successful”
axiomatization of intuitionistic logic by Heyting, today, intuitionism is
often presented in an axiomatic context; for propositional logic, for
instance, just like a calculus for classical logic, but without _tertium-non-
datur_. In this way, it can be recast totally in our red world. An
“additional” semantics, may it be informal or set-theoretically, would be
alien to intuitionism.121212The first author remembers a remark of an author
to the effect that intuitionism was not succeeding due to the lack of a proper
semantics, until this deficit was cured by the introduction of Kripke
semantics. In our view, this sounds like claiming that a protestant church is
not a church as long as it doesn’t have a pope. One could go a step further
and say—instead of that there is no blue world—that the red world should be
its own blue world. This is often paraphrased by saying that, from an
intuitionistic perspective, the meaning of a formula is given by its proof
(better: the set of all its proofs). Today, this idea is reflected in _proof-
theoretic semantics_ , an approach which “attempts to locate the meaning of
propositions and logical connectives not in terms of interpretations …but in
the role that the proposition or logical connective plays within the system of
inference.”131313http://en.wikipedia.org/wiki/Proof-theoretic_semantics,
accessed Febr. 20, 2015. For more on proof-theoretic semantics, see [11, 13].

In view of our discussion above, the formal framework of intuitionism
undermines substantially Tarski’s dictum. In particular, when we go back to
Definition 2.1 of a L-structure, one can easily observe that clause (iii) for
negation _builds in_ classical logic into any structure.

It is worth to reflect a little bit more on this clause; it looks as innocent
as any other clause, that for conjunction and disjunction, for instance, “just
making sure that each of our symbols means what we want it to mean.”, to
repeat the citation from Barwise [3, p. 21]. But it is not only the case, that
Brouwer would not agree that this is what we want negation to mean; it is the
problem that the right-hand side—not
${\color[rgb]{0,0,1}{\mathfrak{M}\models{\color[rgb]{1,0,0}{\varphi}}[s]}}$—can,
in general, not practically be verified. It is the full purpose of an
axiomatization to give a _positive_ approach to negation, i.e., the symbol for
negation ${\color[rgb]{1,0,0}{\neg}}$ has to stay always on the right-hand
side of the derivation sign ${\color[rgb]{1,0,0}{\vdash}}$, and we must not
make use of a “meta-negation” ${\color[rgb]{1,0,0}{\nvdash}}$. That this is
possible is far from being trivial—the complexity is visible in the proof of
Gödel’s completeness theorem—but it makes clear the fundamental difference
between syntax (in form of an axiomatization, providing an—executable, albeit
not decidable—derivation relation) and semantics, which is, in general,
inherently non-constructive.

As much as it comes to Brouwer’s criticism of the usual semantic understanding
of negation, it is worth to cite Bernays [4, p. 4 (our translation)], who
replied to it as follows:

> As one knows, the use of the “tertium-non-datur” in relation to infinite
> sets, in particular in Arithmetic, was disputed by L. E. J. Brouwer, namely
> in the form of an opposition to the traditional logical principle of the
> excluded middle. Against this opposition it is to say that it is just based
> on a reinterpretation of the negation. Brouwer avoids the usual negation
> non-A, and takes instead “A is absurd”. It is then obvious that the general
> alternative “Every sentence A is true or absurd” is not justified.

Following Bernays, the controversy about classical and intuitionistic negation
could even be boiled down to a question of words. What is of importance for us
here, is that the semantic determination of (classical) negation closes the
road to understand Brouwer’s (intuitionistic) negation. To say it differently:
the “standard approach” of teaching logic based on Tarski’s dictum (used for
Tarskian semantics as given in Def. 2.1) blocks a proper transition to
intuitionistic logic, at least, if the students are “semantically biased”. As
a matter of fact, intuitionistic logic can—and maybe: has to—be developed
purely in the red world.141414As said at the beginning, this concerns
intuitionistic logic based on Heyting’s axiomatization; Brouwer’s original
intuitionism, in particular if considered in the mathematical area of
Analysis, should not come in a formal livery at all. It is not our aim to
motivate an approach that exclusively focusses on intuitionism or the
like.151515It is worth mentioning that _dialogical logic_ has a rather
interesting status concerning the syntax and semantics distinction, which
doesn’t seem to be properly explored yet, see Kahle [8, 9]. But it is
important that an introduction to classical logic should not come with a
semantical bias which blocks the road to non-classical logic from the
start.161616For instance, substructural logics are best approached via proof
theory, because—quite like intuitionism—there lies their motivation; on the
other hand their semantics usually turn out to be rather complicated. Here the
colours may help.

##  7\. Conclusion

It is our experience from courses on mathematical logic—regular university
classes, block courses, and summer school courses—that the use of colours
gives the students, indeed, a “tool” at hand to see better the fundamental
distinction of syntax and semantics.171717We have, of course, not developed an
empirical study to “prove” that the use of colours improves the teaching; it
is rather an informed impression backed by feedback from our students. And
although we do not have statistically valid data comparing the effects of this
method with other approaches, the test results of the courses were very
positive (but we had few, but rather good and understanding students).
Although the use of colours requires some additional effort in the preparation
of the student material, it is a rather inexpensive investment to obtain
significant educational added value. At a certain stage—for instance, as
mentioned, after the proof of the completeness theorem—, when the student has
already internalized the difference of syntax and semantics one can even
easily go back to the common identification of the syntactical and semantical
expression using them just in black; it provides even a good test template, as
one can ask the students in all kind of instances whether a certain expression
would have to be coloured red or blue.

In addition, while the colouring can, of course, not solve any philosophical
problem concerning syntax and semantics, it helps to sharpen the sensibility
for the underlying problems. In any case, the success of a logic course will
not only depend on the use of tools, but on the interaction between teacher,
tutor(s) and students. The use of a new dimension—like colour—underlines the
importance of the distinction between syntax and semantics, it brings various
(philosophical) topics into focus and gives a convenient way of talking about
these issues—a way that often is readily accepted by the students.

The message of this paper is not: By all means use colours to distinguish
syntax from semantics! But rather: Distinguish syntax and semantics clearly
and discuss some of the issues related to that distinction—the use of colour
will help you doing so!

## References

  * [1] Th. Altenkirch, P. Morris, F. Nordvall Forsberg, and A. Setzer.  A categorical semantics for inductive-inductive definitions.  In A. Corradini and B. Klin, editors, Algebra and Coalgebra in Computer Science, volume 6859 of Lecture Notes in Computer Science, pages 70–84. Springer, 2011.
  * [2] D. Barker-Plummer, J. Barwise, and J. Etchemendy.  Tarski’s World, volume 169 of CSLI Lecture Notes.  CSLI Publications, 2008.
  * [3] J. Barwise.  An introduction to first-order logic.  In J. Barwise, editor, Handbook of Mathematical Logic, pages 5–46. North-Holland, 1977.
  * [4] P. Bernays.  Bemerkungen zu Lorenzen’s Stellungnahme in der Philosophie der Mathematik.  In K. Lorenz, editor, Konstruktionen versus Positionen, volume 1, pages 3–16. Berlin, 1979.
  * [5] R. Cori and D. Lascar.  Mathematical Logic, Part I.  Oxford University Press, 2000.
  * [6] B. Buldt et al., editor.  Kurt Gödel. Wahrheit und Beweisbarkeit, volume 2: Kompendium zum Werk.  öbv & hpt, 2002.
  * [7] S. Feferman.  Kurt Gödel: Conviction and Caution.  Philosophia Naturalis, 21:546–562, 1984.
  * [8] R. Kahle.  Konstuktivismus und Semantik.  In J. Mittelstraß, editor, Der Konstruktivismus im Ausgang der Philosophie von Wilhelm Kamlah und Paul Lorenzen, pages 197–212. Mentis, 2008.
  * [9] R. Kahle.  Dialoge als Semantik.  In J. Mittelstraß and Chr. von Bülow, editors, Dialogische Logik, pages 43–54. Mentis, 2015.
  * [10] R. Kahle.  Gentzen’s consistency proof in context.  In R. Kahle and M. Rathjen, editors, Gentzen’s Centenary. Springer, 2015, to appear.
  * [11] R. Kahle and P. Schroeder-Heister, editors.  Proof-theoretic semantics, volume 148.  2006\.
  * [12] W. Rautenberg.  A Concise Introduction to Mathematical Logic.  Springer, 2006.
  * [13] P. Schroeder-Heister.  Proof-theoretic semantics.  In E.Ñ. Zalta, editor, The Stanford Encyclopedia of Philosophy. Summer 2014 edition, 2014.
  * [14] A. Sernadas and C. Sernadas.  Foundations of Logic and Theory of Computation, volume 10 of Texts in Computer Science.  College Publication, 2008.
  * [15] J. R. Shoenfield.  Mathematical Logic.  Addison-Wesley, Reading, MA, 1967.  Reprinted: Association for Symbolic Logic and AK Peters, 2001.
  * [16] C. Smorynski.  The incompleteness theorems.  In J. Barwise, editor, Handbook of Mathematical Logic, pages 821–865. North-Holland, 1977.
  * [17] H. Wang.  Some facts about Kurt Gödel.  The Journal of Symbolic Logic, 46:653–659, 1981.