Today I Learned

Some of the things I've learned every day since Oct 10, 2016

174: Decidability of Recursive, Complete, Satisfiable Theories

It’s pretty much in the title. If T is an \mathcal{L}-theory which is recursive, complete, and satisfiable, then T is decidable. That is, there’s an algorithm which takes an \mathcal{L}-sentence \phi and outputs whether or not T \vDash \phi.

(T being recursive means that there’s an algorithm which similarly takes \phi as input but outputs whether \phi \in T.)


173: Vaught’s Test

In model theory, Vaught’s Test (also known as the Łoś–Vaught test) determines whether certain \mathcal{L}-theories T are complete. It states that if T is satisfiable, has no finite models, and is \kappa-categorical for some \kappa \geq |\mathcal{L}|, then T is complete.

Proof outline Assume T isn’t complete. Then there’s a sentence \phi such that T \nvDash \phi, T \nvDash \neg \phi, meaning T \cup \{\phi\}, T \cup \{\neg \phi \} are satisfiable, meaning both have infinite models (since T has no finite models), so by [172] we can find models \mathcal{M}, \mathcal{N} of cardinality \kappa which respectively satisfy these theories. But since \mathcal{M}, \mathcal{N} disagree on \phi, they are not elementarily equivalent and hence not isomorphic, contradicting the assumption that T is \kappa-categorical. Thus T must be complete.

172: Infinite Models of L-Theories (Variation of Lowenheim-Skolem)

Suppose \mathcal{L} is a first-order language and T is an \mathcal{L}-theory with an infinite model. Then for every infinite cardinal \kappa \geq |\mathcal{L}|, T has a model of cardinality \kappa.

This result — a variation of the Löwenheim–Skolem theorem — implies that theories with infinite models can’t have unique models up to isomorphism.

171: More General Cauchy Integral Theorem

Let \Omega \subseteq \mathbb{C} be open, and let \Gamma \subset \Omega be a cycle which is null homologous. (That is, \Gamma is a collection of closed curves the winding number of which is 0.) Then

\int _\Gamma f(z) dz = 0.

170: Dangling Pointers

Dangling pointers are essentially pointers which are “left hanging” after the memory location they point to has become invalid. More specifically, a dangling pointer is a non-NULL pointer which points to memory which has become deallocated or otherwise has become invalid memory for the pointer to be pointing to.

For instance, an example in C (a language prone to this problem) taken from Wikipedia:

   char *dp = NULL;
   /* ... */
       char c;
       dp = &c;
     /* c falls out of scope */
     /* dp is now a dangling pointer */

If a dangling pointer is attempted to be dereferenced, unpredictable (incorrect/garbage) behavior can result.

169: Finiteness of Logical Implication

Suppose T is an \mathcal{L}-theory and T \vDash \phi. Then \Delta \vDash \phi for some finite \Delta \subseteq T.

Proof Let \Delta \subseteq T be finite and suppose \Delta \nvDash \phi. Then \Delta \cup \{\neg \phi\} is satisfiable, so T \cup \{ \neg \phi \} is finitely satisfiable and by the compactness theorem T \nvDash \phi.

168: Memory Leaks

In computing, a memory leak occurs when a program fails to release memory which is no longer required. For instance, a C program where the programmer dynamically allocates memory for a task but forgets to de-allocate it.

In certain circumstances, memory leakage may not cause big problems or might even be asymptomatic, like in programs with a little memory leakage which never actually run for long enough periods of time that memory usage becomes a problem. However, in worse cases memory leakage can lead to the complete failure of a program.

A couple types of programs at high risk for memory leakage are those in embedded systems (which can run continuously for years at a time, giving even small leaks the potential for being problematic) and those where memory is allocated extremely frequently for one-time tasks (such as rendering in a video or game).

While many languages like Java have built-in garbage collection which automatically cleans up unused or unaccessible memory, other languages like C and C++ require the programmer to be on top of making sure these leaks don’t happen in the first place. However, there are memory management libraries and memory debugging tools written to help with these languages. It should also be noted that automatic garbage collection comes with a performance overhead, so whether it’s desirable varies depending on the situation.

167: Zorn’s Lemma

In set theory, Zorn’s Lemma states that if S is a nonempty, partially-ordered set such that every chain (totally ordered subset) has an upper bound, then S has at least one maximal element m. (That is, an element such that m \leq n is not true for any n \in S.

Assuming the axioms of Zermelo-Fraenkel set theory, Zorn’s lemma is equivalent to the axiom of choice and the well-ordering theorem, respectively.

166: Elementary Equivalence and Isomorphism between Finite Structures

Let \mathcal{L} be a first-order language. In general, it is true that if two \mathcal{L}-structures \mathcal{M, N} are isomorphic, then they are elementarily equivalent. However, elementary equivalence does not in general imply isomorphism.

When \mathcal{M, N} are finite structures, however, the two conditions are equivalent. That is,

\mathcal{M} \equiv \mathcal{N} \Leftrightarrow \mathcal{M} \cong \mathcal{N}.

165: The Compactness Theorem (Henkin Construction)

In logic, the Compactness Theorem states that a first-order theory is satisfiable if and only if it is finitely satisfiable. Here we give a sketch of a proof for the Theorem using Henkin construction. (The full proof is very syntax-heavy and I’m too lazy to type that much LaTeX, but this is the overall idea of the method.)

Let \mathcal {L} be a first-order language and T be a finitely satisfiable \mathcal{L}-theory.

We can construct a language \mathcal{L}^* \supseteq \mathcal{L} and a finitely-satisfiable \mathcal{L}^*-theory T^* \supseteq T such that any \mathcal{L}^*-theory extending T^* has the witness property. The way we do this is by first adding a constant symbol c_\varphi to \mathcal{L} for each \mathcal{L}-formula \varphi with a single free variable, calling the result \mathcal{L}_1. For each such \varphi we also add to T the \mathcal{L}_1-sentence

(\exists v \varphi (v)) \rightarrow \varphi (c_\varphi ),

calling the resulting \mathcal{L}_1-theory T_1. We then keep doing this indefinitely and call the unions of all such languages and theories \mathcal{L}^* and T^*, respectively, with the result that T^* is finitely satisfiable and any extension thereof has the witness property.

We then extend T^* to a finitely-satisfiable and maximal \mathcal{L}^*-theory T^\prime which by the above will also have the witness property. The way we do this is by adding either \varphi or \neg \varphi to T^* for each \mathcal{L}^*-sentence \varphi (exactly one of which will keep the theory finitely satisfiable).

Now that we have an extended theory (within an extended language) which is finitely satisfiable, maximal, and has the witness property, we show there is a model \mathcal{M} of it, which will obviously also be a model of our original theory T.

We define the universe of \mathcal{M} to be the set of constant symbols of \mathcal{L}^* modulo \sim, where \sim is the relation such that

c \sim d \Leftrightarrow T^\prime \vDash c = d.

We also define

f^\mathcal{M} (t_1 / \sim \dots t_n / \sim) = f(t_1 \dots t_n) / \sim,

(t_1/\sim \dots t_n/\sim) \in R^\mathcal{M} \Leftrightarrow T^\prime \vDash R(t_1 \dots t_n),

where f is a function symbol and R is a relation symbol of \mathcal{L}^*.

We then proceed to show by induction on terms and formulas that

\mathcal{M} \vDash \varphi \Leftrightarrow T^\prime \vDash \varphi

for all \mathcal{L}^* sentences \varphi. This shows that \mathcal{M} is a model of T^\prime, and thus is a model of T, which is what we wanted.