Title: Math and science / Theory of Computation / Modal theory

Title: Languages, terms and formulas
This page defines languages, first order languages, terms, formulas and sentences as used in modal theory.
Language
A language is an infinite collection of distinct symbols.
A language in model theory is similar to an alphabet in computation theory. They are both collections of symbols; however, model theory permits a countably infinite set of symbols.
The reverse side discusses the encoding of a language.
First-order language
A first-order language is a language with the following symbols:
1 a. Parentheses
\( \symbolq{(}, \symbolq{)} \)
1 b. Connectives
\( \symbolq{\land}, \symbolq{\lnot} \)
1 c. Quantifier
\( \symbolq{\forall} \)
2. Variables
countable symbols \( \symbolq{v_1}, \symbolq{v_2}, \symbolq{v_3}, ... \)
3. Constant symbols
zero or more (at most countable) symbols \( \symbolq{c_1}, \symbolq{c_2}, ...\)
4. Function symbols
for every natural \( n > 0 \), zero or more (at most countable) \( n \)-arity symbols \( \symbolq{f_1^{n}}, \symbolq{f_2^{n}}, ... \)
5. Relation symbols
for every natural \( n > 0 \), zero or more (at most countable) \( n \)-arity symbols \( \symbolq{R_1^{n}}, \symbolq{R_2^{n}}, ... \)
This definition is a slight alteration of that given by Leary and Kristiansen. There is much to say about this definition in terms of its encoding (covered on the back side).
Modal theory doesn't pause to give a definition for the set of all possible strings formed from symbols of a model theory language. This would be the language in computation theory terms. Instead we go straight to carving out this space to form much smaller sets of strings: terms and formula.
Terms of a first-order language
Let \( \mathcal{L} \) be a first-order language. A term of \( \mathcal{L} \) is defined recursively as:
1. a variable symbol or a constant symbol, or
2. a sequence of symbols where the first symbol is a function symbol and the remaining symbols are terms. The number of terms must match the arity of the function.
To be percise, the above definition is an algorithm for checking if a symbol or sequence of symbols is a term. If instead we wished for a set definition, we could define it as the union of recursively defined sets.
Another recursive definition is employed to define the formulas of a first-order language.
Formulas of a first-order language
Let \( \mathcal{L} \) be a first-order language. A formula of \( \mathcal{L} \) is a sequence of symbols of \( \mathcal{L} \) defined recursively. Each formula must be one of the following:
1. A sequence of symbols where the first symbol is a relation symbol, and the remaining symbols are terms. The number of terms must match the arity of the relation symbol.
2. \( \lnot ( \alpha) \) for some formula \( \alpha \).
3. \( ( \alpha \lor \beta ) \) for some formulas \( \alpha \) and \( \beta \).
4. \( \forall v \; (\alpha) \) for some variable symbol \( v \) and some formula \( \alpha \).
Similar to the definition of terms, the definition for a language reads as an algorithm for checking if a sequence of symbols of \( \mathcal{L} \) is a formula.
BackOnlyText: Decidability
It seems that the symbols of a language can be enumerated. Also, it seems that it can be decided if a symbol sequence is a term or not, and decided if a symbol sequence is a formula or not. I think this is true as if it were not the case, there would be valid formula that can't be decoded in finite time.
Encoding
The definitions of languages above leaves out subtle details about what each symbol must communicate.
Encoding. General language.
In an information theory setting, a symbol could be thought of as being a unique binary sequence. If we wish a machine to read a sequence of such binary sequences, we must either make each symbol encoding prefix free, or we must give the machine an extra symbol to denote the separation. For a binary sequence \( x \), an example prefix free encoding \( \overline{x} \) is the sequence
\[ \overline{x} := 1^{l(x)}0x \]
where \( l(x) \in \mathbb{N} \) and \( 1^{l(x)} \) is \( l(x) \) consecutive '1' symbols.
Encoding. First-order language.
The first-order language inherits the uniquely decodable interpretation above. It seems possible to ignore the semantic labels such as "parentheses", "connectives" etcetera—they are present only to convey to the reader what type of algorithms might rely on these symbols. However, when attempting to do away with these labels, it becomes obvious that we cannot ignore the separation of the 4 collections of symbols. More must be said about them. Implicit in the definition is the condition that if given a symbol, it is possible to determine the collection from which a symbol is part of: whether the symbol is a variable, constant, function or relation. We don't need to worry about the other 5 symbols, as their finite-ness allows a computer to switch on their encoding. But, for the infinite collections, we are forced to encode some additional information along with the symbols. The situation is even more involved for the function and relational symbols. As will be seen later, it is expected that from a symbol we can determine its arity; without this information, we cannot check if a term is valid. One might argue that the variables too should be accompanied by their index.
An argument against the these claims that accompanying information is required is as follows. We could design an enumerator for the symbols of the language in such a way that the index and arity of terms can be deduced by the order in which the symbols are enumerated. This would allow a finite (but horribly slow) method to find this information from a given symbol by pattern matching against every output of the enumerator.
If we had neither accompanying information nor a smartly enumerated language, then it would be possible to encounter a symbol for which no finite computation could determine the type of the symbol or the arity, in the case of function symbols and relation symbols.
Example: The single element set, containing one binary relation symbol, \( \{ \in \} \) is sufficient to form the first-order language of set theory. All other symbols can be build from this one.
Source: A friendly Introduction to Mathematical Logic, Leary and Kristiansen
Context: TODO: graph branching into structure and deductions then merging again with soundness and completeness

Title: \( \mathcal{L} \)-structure
In model theory, the definition of a language involves syntax only. An \( \mathcal{L} \)-structure moves beyond syntax and gives a first-order language a set theoretic interpretation.
The back side has a recap for concepts referenced in the below definition.
\( \mathcal{L}\)-structure
Let \( \mathcal{L} \) be a language. An \( \mathcal{L} \)-structure consists of the following:
1. A nonempty set \( A \), which is called the universe.
2. A map, from constant symbols → elements of \( A \).
3. A map, from relation symbols → relations over \( A^n \), where \( n \) is the arity of the relation.
4. A map, from function symbols → functions with signature \( A^n \to A \), where \( n \) is the arity of the function.
An \( \mathcal{L} \)-structure is often denoted by the Fraktur symbol \( \mathfrak{U} \).
\( c \) is a symbol often used to represent some "constant" symbol of a language, and \( c^{\mathfrak{U}} \) is often used to represent an element of the universe mapped to by the symbol represented by \( c \). For the similar purposes, the symbols \( f \), \( f^{\mathfrak{U}} \), \( R \) and \( R^{\mathfrak{U}} \) are used.
An \( \mathcal{L} \)-structure doesn't give an interpretation to the variable symbols of a language. Variable symbols are mapped to elements of the universe by a variable assignment function.
Variable assignment function
Let \( \mathcal{L} \) be a language, and let \( \mathfrak{U} \) be an \( \mathcal{L} \)-structure for the language. Let \( A \) be the universe of \( \mathfrak{U} \).
A variable assignment function is a mapping from the variable symbols of \( \mathcal{L} \) to elements of \( A \).
BackOnlyText: Recap some definitions.
Languages, first-order languages and formula
A language in model theory is a collection of symbols.
A first-order language has specific symbols \( \symbolq{(} \), \( \symbolq{)} \), \( \symbolq{\lnot} \), \( \symbolq{\lor} \), and \( \symbolq{\forall} \). There are other symbols split into classes such as variable symbols and function symbols. In can be interpreted as an encoding scheme, which in turn can be seen as just a couple of machines/algorithms that decode certain symbol sequences.
A recursive set of requirements narrows down the valid strings of a first-order language to a smaller set of formulas. Requirements are rules like \( aRb \) is a formula, where \( R \) is a relation symbol and \( a \) and \( b \) are terms. Terms also are defined recursively in a similar way.
Symbols, but not sequences
If a language is given an \( \mathcal{L} \)-structure and a variable assignment function, then almost every symbol of the language is mapped to a set theoretic object. The symbols that do not have such an interpretation are: \( \symbolq{(} \), \( \symbolq{)} \), \( \symbolq{\lnot} \), \( \symbolq{\lor} \), and \( \symbolq{\forall} \). Furthermore, no symbol sequence has been given an interpretation. Specifically, terms and \( \mathcal{L} \)-formula have not yet been given an interpretation.
Source: A Friendly Introduction to Mathematical Logic, Leary and Kristiansen

Title: Term and formula assignment
In a previous card, it was described how an \( \mathcal{L} \)-structure and a variable assignment fuction act together to identify a set theoretic interpretation for every symbol of a language. For terms and formulas, they have an interpretation assigned to them by a term assignment function and a formula assignment function. Terms get assigned to elements while (some) formulas get assigned "truth" (also called "satisfaction").
Term assignment function
Let \( \mathcal{L} \) be a language, and let \( \mathfrak{U} \) be an \( \mathcal{L} \)-structure for the language. Let \( A \) be the universe of \( \mathfrak{U} \) and let \( s \) be a variable assignment function.
The term assignment function, denoted \( \bar{s} \), is a mapping of terms to elements of \( A \). It is defined recursively and is fully determined by the combination of the \( \mathcal{L} \)-structure and the variable assignment function.
Let \( t \) be a term, then:
- if \( t \) is a variable symbol, \( \bar{s}(t) = s(t) \)
- if \( t \) is a constant symbol \( c \), \( \bar{s}(t) = c^{\mathfrak{U} } \)
- if \( t \) is \( ft_1t_2...t_n \) for some function and term symbols, then \( \bar{s}(t) = f^{ \mathfrak{U} }(\bar{s}(t_1) \bar{s}(t_2) ... \bar{s}(t_n)) \)
Formulas get a very different mapping.
Formula assignment: truth/satisfaction
Let \( \mathcal{L} \) be a language, and let \( \mathfrak{U} \) be an \( \mathcal{L} \)-structure for the language. Let \( A \) be the universe of \( \mathfrak{U} \) and let \( s \) be a variable assignment function (and \( \bar{s} \) the resulting term assignment function).
Let \( \phi \) be a formula valid in \( \mathcal{L} \). We say that \( \phi \) is true in \( \mathfrak{U} \), or that \( \mathfrak{U} \) satisfies \( \phi \), and we write \( \mathfrak{U} \vDash \phi \), iff one of the following conditions holds:
1. \( \phi :\equiv Rt_1t_2...t_n \) and \( (\bar{s}(t_1), \bar{s}(t_2), ..., \bar{s}(t_n) ) \in R^{\mathfrak{u} } \).
2. \( \phi :\equiv (\alpha \lor \beta) \) and \( \mathfrak{U} \vDash \alpha \) or \( \mathfrak{U} \vDash \beta \).
3. \( \phi :\equiv \forall x \; (\alpha) \) and for each element \( a \in A, \; \mathfrak{U} \vDash \alpha[s(x|a)] \; \).
4. \( \phi :\lnot (\alpha) \) and \( \mathfrak{U} \nvDash \alpha[s] \).
\( \mathfrak{U} \nvDash \phi \) means it's not the case that \( \mathfrak{U} \vDash \phi \).
There is a discussion about the meaning of \( \nvDash \) on the back side.
BackOnlyText: Extension: satisfaction for sets of \( \mathcal{L} \)-formula
Let \( \Gamma \) be a sequence of \( \mathcal{L} \)-formulas, let \( \mathfrak{U} \) be an \( \mathcal{L} \)-structure and let \( s \) be a variable assignment function.
We say that \( \mathfrak{U} \) and \( s \) satisfy \( \Gamma \) iff \( \mathfrak{U} \) and \( s \) satisfy all formula in \( \Gamma \).
We write \( \mathfrak{U} \vDash \Gamma \)
Meaning of \( \nvDash \)
Condition 4 introduces \( \nvDash \) without much comment, specifically, without mentioning the excluded-middle. Does this condition work only for classical logic, and not for any logic that prohibits the excluded middle?
An argument supporting the cases that excluded-middle is not an issue: given that formulas are finite sequences of symbols (I think), it should surely be the case that an algorithm to check if a formula is satisfied by an \( \mathcal{L} \)-structure will finish in finite time. Having such a decider would allow us to define the negation without worry of an infinite loop. This seems like a reasonable justification for the definition of \( \nvDash \).
Source: A Friendly Introduction to Mathematical Logic, Leary and Kristiansen

Title: \( \mathcal{L} \)-formula implication
We wish to introduce an idea of implication between sets of \( \mathcal{L} \)-formula.
First, we must generalize the idea of truth/satisfaction that was introduced for \( \mathcal{L} \)-formula.
The idea of truth/satisfaction is recapped on the back side.
Model
Let \( \mathcal{L} \) be a first-order language. Let \( \mathfrak{U} \) be an \( \mathcal{L} \)-structure for \( \mathcal{L} \) and let \( \phi \) be an \( \mathcal{L} \)-formula of \( \mathcal{L} \).
If \( \mathfrak{U} \vDash \phi[s] \) for every variable assignment function \( s \), then we say that \( \mathfrak{U} \) is a model of \( \phi \) (or \( \mathfrak{U} \) models \( \phi \)). We write \( \mathfrak{U} \vDash \phi \).
Extendion to sets of \( \mathcal{L} \)-formula: if \( \mathfrak{U} \) is a model for every \( \mathcal{L} \)-formula in a set of \( \mathcal{L} \)-formulas, \( \Phi \), then we say \( \mathfrak{U} \) is a model of \( \Phi \), and we write \( \mathfrak{U} \vDash \Phi \).
If we compare two sets of \( \mathcal{L} \)-formula we arrive at a type of implication.
Logical implication, under a structure
Let \( \Delta \) and \( \Gamma \) be two sets of \( \mathcal{L} \)-formulas from the same language \( \mathcal{L} \). Let \( \mathfrak{U} \) be an \( \mathcal{L} \)-structure for \( \mathcal{L} \).
If \( \mathfrak{U} \vDash \Delta \) implies \( \mathfrak{U} \vDash \Gamma \), we say that \( \Delta \) logically implies \( \Gamma \) under \( \mathfrak{U} \).
In other words, if whenever all the \( \mathcal{L} \)-formulas of \( \Delta \) are satisfied by \( \mathfrak{U} \) so too are the \( \mathcal{L} \)-formulas of \( \Gamma \).
Finally, we remove the dependency on a specific structure.
Logical implication
Let \( \Delta \) and \( \Gamma \) be two sets of \( \mathcal{L} \)-formulas from the same language \( \mathcal{L} \).
If \( \Delta \) logically implies \( \Gamma \) under \( \mathfrak{U} \) for any \( \mathcal{L} \)-structure \( \mathfrak{U} \) of \( \mathcal{L} \), then we say that \( \Delta \) logically implies \( \Gamma \). We write this as \( \Delta \vDash \Gamma \).
BackOnlyText: Zooming out
In the presence of an \( \mathcal{L} \)-structure and a variable assignment function, the terms and formulas of a first-order language have been assigned meaning. Terms are mapped to elements of the universe, and formulas are assigned to the idea of being true or false. In this setting, if we compare two formulas and observe a truth table implication, we can call this implication between formulas within the setting of the semantic assignments. This implication is strengthened if it is independent of the variable assignment function, and it is strengthened again if it is independent of any particular structure. If our implication is independent of structure, then we have achieved an implication that is not tied to the semantic structure of sets, instead the syntax is sufficient to conclude implication. This isn't quite true! The implication is still tied to the assumption that truth is decided relative to some \( \mathcal{L} \)-structure.
Recap
Recap of formula assignment.
Formula assignment: truth/satisfaction
Let \( \mathcal{L} \) be a first-order language, and let \( \mathfrak{U} \) be an \( \mathcal{L} \)-structure for the language. Let \( A \) be the universe of \( \mathfrak{U} \) and let \( s \) be a variable assignment function (and \( \bar{s} \) the resulting term assignment function). Let \( \phi \) be a formula valid in \( \mathcal{L} \).
We say that \( \phi \) is true in \( \mathfrak{U} \), or that \( \mathfrak{U} \) satisfies \( \phi \), and we write \( \mathfrak{U} \vDash \phi \), iff one of the following recursive condition holds:
1. \( \phi :\equiv Rt_1t_2...t_n \) and the \( (\bar{s}(t_1), \bar{s}(t_2), ..., \bar{s}(t_n)) \in R^{\mathfrak{u}} \).
2. \( \phi :\equiv (\alpha \lor \beta) \) and \( \mathfrak{U} \vDash \alpha \) or \( \mathfrak{U} \vDash \beta \).
3. \( \phi :\equiv \forall x \; (\alpha) \) and for each element \( a \in A \), \( \mathfrak{U} \vDash \alpha[s(x|a)] \).
4. \( \phi :\equiv \lnot \alpha (\lnot \alpha) \) and \( \mathfrak{U} \nvDash \alpha[s] \).
\( \mathfrak{U} \nvDash \phi \) means it's not the case that \( \mathfrak{U} \vDash \phi \).
Source: A Friendly Introduction to Mathematical Logic, by Leary and Kristiansen

Title: Deduction
The definition of a deduction tries to capture the essence of proof.
Deduction. Informal definition.
A deduction is a sequence of statements that justifies another mathematical statement. Each statement of the sequence is justified either by definition, or by the previous statements in the sequence. It must be possible for a machine to execute an algorithm to determine the validity of a deduction in finite steps.
The above informal definition does not explain how justification works. The following definition is more concrete.
Deduction. Definition.
A deduction in a first-order language \( \mathcal{L} \) is a finite sequence \( (\phi)_{n=1}^{N} \) of \( \mathcal{L} \)-formulas from \( \mathcal{L} \) such that each \( \phi_i \) in the sequence satisfies one of the following 2 conditions:
1. \( \phi_i \) is an axiom (logical or non-logical).
2. \( \phi_i \) is the second component of some inference rule \( (\Gamma, \phi_i) \), where \( \Gamma \) is a subset of the preceding terms of the sequence (\( \Gamma \subset \{ \phi_n | n \in \mathbb{N} \land 0 \gt n \lt i \} \)).
If \( \Sigma \) is the set of non-logical axioms*, and \( (\phi_i)_{n=1}^{N} \) is a deduction ending in \( \phi_N \), then we call this a deduction from \( \Sigma \) of \( \phi_N \) and we write \( \Sigma \vdash \phi_N \).
*We care most about how the non-logical axioms enable a deduction (the logical axioms and the inference rules are normally the same standard ones).
The back side includes a recap of axioms and rules of inference.
BackOnlyText: Axioms. Logical and non-logical.
An axiom is an \( \mathcal{L} \)-formula.
We generally classify axioms into two categories:
Logical axioms
A very minimal collection of axioms covering equality, and the quantifier \( \forall \) and \( \exists \). Don't change depending on circumstances (any others? are they really the same for modal theory for all first-order languages?)
Non-logical axioms
Axioms that change based on circumstances. For example, axioms for integer summation or axioms for integer summation and multiplication.
For first-order languages, an algorithm is specified that can check if an \( \mathcal{L} \)-formula is a logical axiom. The set of logical axioms is defined implicitly as the \( \mathcal{L} \)-formula for which the algorithm decides are logical axiom.
Rule of inference
A rule of inference is a pair \( (\Gamma, \phi) \) where \( \Gamma \) is a set of \( \mathcal{L}\)-formula and \( \phi \) is an \( \mathcal{L} \)-formula.
Similar to the case for logical axioms, there is an algorithm for checking if a given (\( \mathcal{L} \)-formula set, \( \mathcal{L} \)-formula) pair constitute an inference rule. This algorithm can be broken down into two steps:
1. convert all \( \mathcal{L} \)-formula to propositional forms
2. check for a tautology
Another card discusses axioms and inference rules in more detail.
Source: A friendly Introduction to Mathematical Logic, Leary and Kristiansen
p43