# Cleaning up confusions in logic and formal theories

There are tons of technicalities in Logic. This leads, occasionally, to confusions. Thus it is instructive to briefly summarize all the basic notions.

## Formal language

In logic one creates, first, a *formal language*,

*formal language*$\mathfrak{L}$ over an alphabet $\Sigma$ is a collection $\Sigma^\ast$ of words (finite sequence of alphabets) over the alphabet $\Sigma$.

Thus to define a formal language, one specifies an alphabet $\Sigma$, then describes the collection $\Sigma^\ast$. The description is often given inductively via a *grammar*.

The simplest example is that of propositional logic.

*formulae*, is given by the following Backus-Naur form $$ M = v_i | \neg A | (A\vee B)| (A\wedge B) | A\to B $$ where $v_i$ is any variable and $A,B$ are all formulae. In particular a formula consisting of just a variable is called an

*atomic formula*. ◀

First order language becomes much more complicated.

- (countable set of) constants $c_1, c_2, ...$,
- predicate symbols of arity $n$, $P^n_1, P^n_2, ...$ for all $n\in\mathbb{N}$,
- function symbols of arity $n$, $f^n_1, f^n_2, ...$ for all $n\in\mathbb{N}$
- quantifiers $\forall,\exists$.

*term*$t$: $$ t = c_i | v_i | f_i^n(t_1,...,t_n), $$ then from terms

*formulae*a word $A$ in the language is defined: $$ A = P_i^n(t_1,...,t_n) | \neg A | A\vee B | A\wedge B | A\to B| \forall v\ A | \exists v\ A $$ where $P_i^n(t_1,...,t_n)$ are atomic formulae. ◀

Remember that a function takes a term to another term, and a predicate takes a term and yields an atomic formula. When a formula $A$ has no free variable, it can then be seen as a *sentence*.

*symbols*, and a word is called a

*formula*, mainly when one is doing logic rather than formal language and grammar per-se. These are just terminological differences. ◈

*formula*is the same as the word

*proposition*. A formula is also called well-formed expression, or well-formed formula when one stipluates a formula to be any sequence of symbols. The differences are purely in conventions used. In type theory one distincts between propositions and general types, but in type theory the notions of formal system and formal language become radically different from those presenting logic. ◈

## Model theory

In model theory one speaks of signatures and structures. Here one exclusively works with functions and sets.

A *signature* of a formal language $\mathfrak{L}$ is just the collection of *non-logical symbols* (letters) in an alphabet $\Sigma$. What constitutes non-logical symbols is subject to stipulation. One can also speak of a signature without mentioning any formal language. In this case it is just a set of $n$-ary function symbols and predicate symbols.

The notion of signature is closely related to that of *structure*, and the definitions are various. The essense here is that a structure is just a set $S$ called *domain* or *universe* together with a signature that is interpreted on $S$.

*structure*is a triple $\mathcal{S} = (S,\sigma, \iota)$ where $S$ is a set called

*domain*, $\sigma$ is a signature, and $\iota$ is a function called

*interpretation*:

- an $n$-ary function symbol $f^n$ is mapped to $\iota(f): S^n \to S$,
- an $n$-ary relation symbol $R^n$ is mapped to $\iota(R) \subseteq S^n$,
- for a constant c, $\iota(c)\in S$ is just an element of the domain.

Given a formal language $\mathfrak{L}$, one speaks of a *theory*. These are just sets $T$ of *sentences* in the formal language $\mathfrak{L}$ (with free variables and notion of formulae). A structure $\Gamma$ is a *model* of a theory $T$ if it satisfies all the sentences (confusingly called axioms but these are not, in general, axioms in a deduction system for a logic) of $T$, namely $\Gamma \vDash \sigma$ for every $\sigma \in T$. Some important theorems then can be formulated in this choice of terminology:

- The
*model existence theorem*says that a consistent theory $T$ always has a model. Meaning that there is always a structure $\Gamma$, s.t. $\Gamma \vDash t$ for all $t\in T$. - The
*soundness theorem*says that what can be proved from a theory $T$ ($\sigma$ s.t. $T\vdash \sigma$) is also valid in any model of $T$ ($T\vDash \sigma$). Here $T\vDash \sigma$ is really an abuse of notation, meaning really given any structure $\mathcal{M}$ s.t. $\mathcal{M}\vDash t$ ($\forall t\in T$), one has $\mathcal{M}\vDash \sigma$. - The
*completeness theorem*says that $T\vDash \sigma$ then $T\vdash \sigma$.

## Deductive/inference systems (Proof theory)

Stipulating a formal language is not enough, since one really wants to achive is to stipulate a system in which rigourous deductions - going from a hypothesis to a conclusion according to some given rules - can be carried out. This is done by introducing the notion of *deductive system*.

There is no general notion that is widely agreed-upon, but we adopt what is given in nLab for some intuition. This is also used in Martin-Lof style dependent type theory.

*deductive system*is a collection of

*judgements*and a collection of

*steps*which has as a sequence of judgements as "hypotheses" and a single judgement as "conclusion". A step is usually written as $$ \frac{ J_1 \quad \cdots \quad J_n }{J} $$

What a judgement means depends on the context. The steps here are usually rules of inference. When $n=0$ in a step, the step is often called an *axiom*. A good practice is *not* to call a step with no hypothesis an axiom, or call it explicitly *logical* axiom, since it is a custom to call sentences in a theory an axiom. The confusion inflates when one works in deductive systems that are not notationally-heavy, e.g. in Hilbert system; these are systems with many logical axiom schemata and few inference rules.

*per se*, its

*meaning*(

**Sinn**) that is invariant, rather than one or many of its formalizations. In Girard's word:

[the syntactic tradition] is always in search of its fundamental concepts, which is to say, an operational distinction between sense and syntax. Or to put tese things more concretely, it aims to find deep geometricalCategory theory might shed some light on the issue. ◈invariantsof syntax: therin is to be found the sense.

In general, a judgement in propositional logic is a

*formula*. The same goes for first order logic. Traditionally, what is called a

*logical system*is a language with a deductive system that looks like propositional and first order logic, in particular, the judgements are formulae. ◀

Hilbert system is a mess, but their conservative extensions are managable.

*judgements*are

*sequents*$\Gamma\vdash \Delta$ where $\Gamma,\Delta$ are finite sequences of formulae ("words") $A_1, A_2,...$. One of the typical steps is the

*cut rule*$$ \frac{\Gamma\vdash A,\Delta\quad \Gamma',A\vdash \Delta'}{\Gamma,\Gamma' \vdash \Delta,\Delta'} \mathsf{Cut}. $$ ◀

*type formation rules*. It is hard to see how type theory can be formulated in a manner similar to "ordinary" logic. ◀

## Remark: typesetting proofs

While I use `\frac`

to write formal proofs, mathjax utilizes Bussproof for sequent and natural deductions. When the proof becomes complicated, this is needed. When using $\LaTeX$ proper mathpartir is a better choice.