Cleaning up confusions in logic and formal theories

Mar 10 2023 · LastMod: Mar 10 2023
Philosophiae · Essays
Quadrivium · Trivium

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,

Definition(Formal language) . A 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.

Example(Propositional language) . The propositional language, or zeroth-order language, $\mathfrak{L}_0$. The alphabet $\Sigma_0$ consists of 1. $\neg,\vee,\wedge,\to$, 2. countable set of variables $v_1,v_2,...$, 3. parentheses $( , )$. The collection of words $\Sigma_0^\ast$, called 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.

Example(First-order language) . The first order language $\mathfrak{L}_1$. The alphabet $\Sigma_1$ consists of all the letters in $\Sigma_0$, together with
  1. (countable set of) constants $c_1, c_2, ...$,
  2. predicate symbols of arity $n$, $P^n_1, P^n_2, ...$ for all $n\in\mathbb{N}$,
  3. function symbols of arity $n$, $f^n_1, f^n_2, ...$ for all $n\in\mathbb{N}$
  4. quantifiers $\forall,\exists$.
In first order language the words of the language are also defined inductively, but via some intermediate definitions. First one has a 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.

Remark(Terminology: letter vs symbol, word vs formula) . A finite sequence of letters in an alphabet is called a word. Alternatively, one says that an alphabet is a collection of 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. ◈

Remark(Terminology: formula vs proposition) . Again, when working in mathematical logic, the word 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$.

Definition(Structure) . A 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:
  1. an $n$-ary function symbol $f^n$ is mapped to $\iota(f): S^n \to S$,
  2. an $n$-ary relation symbol $R^n$ is mapped to $\iota(R) \subseteq S^n$,
  3. 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:

  1. 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$.
  2. 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$.
  3. 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.

Definition. A 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.

Remark(Freedom in formalization) . Even inside a given logic and a kind of deductive systems (say, Hilbert systems), there can be various ways to formalize a logic, since there is freedom for a logic in choosing rules of inferences. This can be seen as a deficiency of syntax, since one really wants to focus on is, for example, first-order logic 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 geometrical invariants of syntax: therin is to be found the sense.
Category theory might shed some light on the issue. ◈

Example(Logic) . The propositional logic is the propositional language $\mathfrak{L}_0$ together with a deductive system. There are many formulations of deductive systems for propositional logic: Hilbert system, natural deduction, sequent calculus, etc.
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.

Example(Gentzen sequent) . In a Gentzen sequent the 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}. $$ ◀

Example(Natural deduction) . In natural deduction systems the judgements are just formulae. A typical step is $$ \frac{A\quad B}{A\wedge B}\wedge $$ ◀

Example(Martin-Lof type theory) . A judgement in Martin-Lof type theory is one the following $$ \Gamma \vdash A:\operatorname{Type},\quad \Gamma\vdash A\doteq B:\operatorname{Type},\quad \Gamma\vdash a:A,\quad \Gamma\vdash a\doteq b:A $$ where $A$ are types and $a$ are elements of type $A$. The types $A$ are formed by 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.