Questions about mathematical logic, including model theory, proof theory, computability theory (a.k.a. recursion theory), and non-standard logics. Consider using one of the following tags: (model-theory), (set-theory), (computability), (proof-theory) if they fit the question.

learn more… | top users | synonyms (1)

39
votes
0answers
1k views

What does it take to divide by $2$?

Theorem 1 [ZFC, classical logic]: If $A,B$ are sets such that $\textbf{2}\times A\cong \textbf{2}\times B$, then $A\cong B$. That's because the axiom of choice allows for the definition of ...
16
votes
0answers
329 views

How much set theory does the category of sets remember?

Question. Let $M$ be a model of enough set theory. Then we can form a category $\mathbf{Set}_M$ whose objects are the elements of $M$ and whose morphisms are the functions in $M$. To what extent is ...
13
votes
0answers
308 views

complete, finitely axiomatizable, theory with 3 countable models

Does it exist a complete, finitely axiomatizable, first-order theory $T$ with exactly 3 countable non-isomorphic models? A few relevant comments: There is a classical example of a complete theory ...
12
votes
0answers
423 views

Non-axiomatisability and ultraproducts

Let $T$ be a first-order theory over a language $L$, and let $\mathcal{M}$ be a subclass of the class of models of $T$. As I understand it, if there is no theory $\hat{T}$ over $L$ whose class of ...
11
votes
0answers
166 views

References on filter quantifiers

This post is primarily a reference request. In combinatorics and other areas, we use filter quantifiers to simplify the statements of various definitions, theorems and proofs. The general idea is ...
11
votes
0answers
194 views

Reference on standard types

This question is about what I presume is a basic construction in type theory. The finite types are defined as follows: 0 is a finite type; if $\sigma, \tau$ are finite types, then so is ...
10
votes
0answers
181 views

The ethics of Borel determinacy

I was speaking with a friend the other day, and I happened to say "morally, Borel determinacy is as strong as ZF." I was riffing on the well-known result of Harvey Friedman, that we need ...
9
votes
0answers
158 views

A consequence of zero sharp (successor cardinals having countable cofinality)

So the existence of $0^\sharp$ in set theory is really the assertion on the existence of indiscernibles for the constructible universe $L$ that also "generate" $L$ (see ...
9
votes
0answers
147 views

Elementary references on Robinson Arithmetic, Prim. Recursive fns etc.

I'm in the middle of revising my freely available and much-downloaded introductory notes Gödel Without (Too Many) Tears. (They are a sort of cut down version of part of my Gödel book, and I'm ...
8
votes
0answers
279 views

Gödel's Completeness Theorem and logical consequence

At the end of a long process of "rumination" on "old" math log textbooks, I've found the "missing link" - from my personal point of view - between some issues I've raised in the previous months : (i) ...
8
votes
0answers
498 views

How strong is the statement that Thompson F is amenable?

Justin Moore's proof turned out to have an error I just attended Justin Moore's talk on this today. Since I am neither a group theorist nor a combinatorist, and is not familiar with ultrafilters I ...
7
votes
0answers
103 views

On proving the zero-one-law for first order logic

I'm trying to understand the proof of the zero-one-law for first order logic as provided in (Ebbinghaus-Flum, 1995). It goes as follows: Let $\tau$ be a relational signature. Let $r\in\mathbb{N}$, ...
7
votes
0answers
84 views

Infinite palindromes in number of nonisomorphic posets is independent of $\mathsf{ZF}$

The following is an "exercise" in P. Stanley's book "Enumerative Combinatorics": Let $f(n)$ be the number of nonisomorphic $n$-element posets (...) let $\mathcal{P}$ denote the statement that ...
7
votes
0answers
194 views

Fixed points in computability and logic

I asked this question on CS.SE, too: http://cstheory.stackexchange.com/questions/27322/fixed-points-in-computability-and-logic I would like to understand better the relation between fixed point ...
7
votes
0answers
148 views

Skolem Hulls in $H_{\omega_2}$

Consider a model of the form $\mathfrak{A} = (H_{\omega_2}, \epsilon, \prec, f_0, f_1, ...)$, some expansion of $H_{\omega_2}$ in a countable language, with $\prec$ giving a well-order. Does there ...
7
votes
0answers
301 views

Using the compactness theorem to show a set of first-order formula is equivalent to a set of quantifier-free formula

I am going through some theorems in Hodges' ``A shorter model theory'' and I have realized that I do not understand a certain argument regarding compactness. My question has two forms, I am sure that ...
7
votes
0answers
313 views

logic lectures on youtube

Currently I am reading Logic an Structure by Dirk van Dalen (2008). As I am missing some basics I try to find related lectures on youtube. I frequently watch MIT, Stanford, and University of ...
6
votes
0answers
56 views

Primitive recursion and $\Delta^0_0$

Until recently I assumed that primitive recursive relations are exactly $\Delta^0_0$ (i.e. bounded) ones, but I learned they're different (the former is a proper superclass of the latter). I have ...
6
votes
0answers
79 views

Elementary submodels in stationary logic.

In the paper "Stationary Logic" by Barwise, Kaufmann and Makkai the authors prove that stationary Logic L(aa) has Löwenheim number $\aleph_1$, i.e. every satisfiable set of sentences has a model of ...
6
votes
0answers
58 views

Heyting algebras and infinite distributive law

I want to prove that "a complete lattice satisfies the infinite distributive law $a\wedge(\vee{S})=\vee\{a\wedge s|s\in S\}$ iff it is a Heyting algebra". I proved "if" part but can't "only if" part. ...
6
votes
0answers
248 views

Is Kunen's claim about non-equivalent forms of Axiom of Choice, true?

Consider the following forms of the axiom of choice: $AC_1:\forall F\neq \emptyset~~~(\emptyset\notin F~\wedge~\forall x,y\in F~~~(x\neq y\rightarrow x\cap y= \emptyset))\rightarrow \exists C~\forall ...
6
votes
0answers
237 views

Characterization of the First Order Theory of Ordered Abelian Groups via Quantifier Elimination

In the paper "Elimination of Quantifiers in Algebraic Structures" Macintyre, McKenna and van den Dries, proved that every field (ordered field) whose theory admits quantifier elimination in the ...
6
votes
0answers
296 views

Foundation for category theory

Before a little premise: It's well known that we can internalize the notion of category, functor and natural transformation in any category with enough structure: for instance we can define what an ...
5
votes
0answers
62 views

What are some arguments/counterarguments for Zeilberger's “proof certificates”?

Here is the quote I wish to ask about: "I speculate that similar developments will occur elsewhere in mathematics, and will 'trivialize' large parts of mathematics, by reducing mathematical ...
5
votes
0answers
136 views

ZF and weakly inaccessible cardinals

This question should probably have been asked 3 years ago (perhaps it has and was removed for some reason?) In 2011, Alexander Kiselev claimed to have proved in ZF that there are no weakly ...
5
votes
0answers
55 views

Deductive closure of sentence $\forall x \forall y F(x,y) \stackrel{.}{=} F(y,x)$ in language $\mathcal{L}$ is undecidable.

$\mathcal{L}$ is the language that contains a single binary function symbol $F$. In the earlier parts of this question, we were told to take the $\mathcal{L}$-structure $\mathcal{M}$ with universe ...
5
votes
0answers
49 views

Proving $\square(\forall v_1\neg\psi(v_1))\rightarrow\forall v_1\neg\psi(v_1)$ for a particular $\psi$.

I have a formula $\psi(v_1)$ that is equivalent in $\mathrm{PA}$ to $$\exists a\exists b\exists c\left[\neg\exists ...
5
votes
0answers
96 views

Path to categorical realizability theory

I'm trying to understand the sorts of things found on this page: http://ncatlab.org/nlab/show/realizability In particular, I want to read Oosten's Realizability: An Introduction to the Categorical ...
5
votes
0answers
204 views

Gödel's Incompleteness Theorem in “Gödel, Escher, Bach”

Ok, so I'm reading the chapter on Gödel's Incompleteness Theorem in "Gödel, Escher, Bach" and I want to make sure I'm getting this right: the idea of the book's proof is to form the sentence "There ...
5
votes
0answers
51 views

Type-definable Forcing or forcing in a non-first order setting

Roughly speaking, in set forcing the forcing notion is a set from ground model's perspective and in class forcing its a definable subset of the ground model given by solutions of some formula with ...
5
votes
0answers
109 views

Functorial first order theories interpretation

Question will be a bit naive, so please, be kind. Consider first order theories, $\Gamma, \Gamma'$ . Let $\mathcal{M}$ be the category of models for $\Gamma$ and $\mathcal{M}'$ be the category of ...
5
votes
0answers
890 views

which branch of maths studies Standard Logical Matrices

In classical logic you have truthtables like: & | T | F ---|---|--- T | T | F F | F | F In many valued logic you have tables like: (this one is ...
5
votes
0answers
301 views

Logical consequence of Euclid's theorem

Are there any far reaching non-trivial consequences of Euclid's infinitude of primes where theorems make use of it? Wikipedia does not have the list of applications of this theorem, rather modern ...
5
votes
0answers
116 views

Model theory in terms of type spaces/Lindenbaum algebras

Are there any good references that go into some detail of known 'translations' between properties of the type space of a model and the model theoretic properties of the model? All I seem to find are ...
5
votes
0answers
597 views

The Cantor Space as $\{0,1\}^{\mathbb{N}}$ and as $[0,1]$.

The Cantor-Space is defined as the space of all infinite binary sequences, i.e. the space $\{0,1\}^{\mathbb{N}}$. It has a natural metric, $$ d(x,y) = \inf\{ 2^{-|w|} : w \in pref(x) \cap pref(y) \} ...
5
votes
0answers
143 views

Interpretation of impure set theory within pure set theory?

I recently came across this paper, where the author (in section 3.1) gives an interpretation of ZFU within ZF. The author of the paper goes on to show what he calls the "synonymy" (i.e., that ZF and ...
4
votes
0answers
74 views

Can all axioms of mathematical theories be expressed with predicate logic?

The book Roads to Infinity: The Mathematics of Truth and Proof stated that, "All the standard mathematical theories have axioms that can be expressed in predicate logic." Predicate logic generally ...
4
votes
0answers
55 views

Defined negation in intuitionistic linear logic

Is it possible to define a negation in intuitionistic linear logic, the way one does in intuitionistic logic, i.e. $A^{\bot} \equiv A \multimap \mathbf{0}$ (or, as it would be written in ...
4
votes
0answers
71 views

What is the explicit formula (solution) to this recursively defined binary matrix?

My question concerns the following binary matrix (call it matrix $A$). Or rather the entire family of such matrices, for some number of columns $n$ and rows $2^n$. The ellipses indicate that the ...
4
votes
0answers
99 views

Non-Forcing and Independence

Do there exists sentences which are independent of ZFC, cannot be shown to be independent through some method of forcing, and do not increase the consistency strength of ZFC (e.g. so Large Cardinal ...
4
votes
0answers
109 views

Incompleteness theorem

Correct me if I am wrong at any point! Godel's incompleteness theorem allows us to express "PA is consistent" in the language of Peano arithmetic, and shows that this is not provable in PA. Let's ...
4
votes
0answers
105 views

Is there a logic to formalize the concept of “understanding”

The question may seem little bit weird given that philosophers have been struggling to have a full grasp on the concept of "understanding". But I'm wondering if there are any logics (modal-based or ...
4
votes
0answers
113 views

Countable transitive $T \vDash ZFC-P$ with $\approx$ not absolute: why do we need $H(\aleph_3)$?

I am trying to solve Exercise IV.3.31 from Kunen's Foundations of Mathematics. I think I have a solution but I am confused by one of the hints. By request, here is the text of the exercise. ...
4
votes
0answers
127 views

How to think about iterated ultrapowers?

I would like to gain some basic intuition about iterated ultrapowers. I am perfectly happy with accepting the construction and can see that it fits into a fundamental role in many places (for example, ...
4
votes
0answers
117 views

Combinatorial packages of N items [[How many distinct Boolean Expressions can be made using N variables]]

Using just the AND operator, the number of distinct packages that can be built from a set of size $n$, is simply $2^n$. If one adds the operators OR and XOR, how many packages can be built? That is, ...
4
votes
0answers
97 views

Logic in closed symmetric monoidal categories; reference request.

Suppose we want an algebraic theory $T$ to be interpretable in any closed symmetric monoidal category $\mathbf{C}.$ I am thinking in particular of the case where $\mathbf{C}$ is the category of models ...
4
votes
0answers
57 views

Unification in languages without function symbols or with relational terms.

In case a logic formula is mechanically constructed, obtained as the specification of an expression in an imperative programming language for example, the functional constraints could be implicit in ...
4
votes
0answers
207 views

Puzzle - zero knowledge proof

I am solving the following problem : I have edge-matching puzzles, where all pieces are squares and the grid has $n$*$n$ format. There is no global image to guide a puzzle solver. Despite the puzzles ...
4
votes
0answers
88 views

Induction on Primitive Recursive Function

The set $F_{n}$ of primitive recursive function symbols of arity $n$ can be defined inductively as: \begin{align} & Z, \text{Succ} \in F_{1} & \\ &\pi_{j}^{n} \in F_{n} \quad \text{for ...
4
votes
0answers
64 views

The quantifier “most”

It is well known that the quantifier "most", understood as "more than half the ps" is not first-order definable. This is one of the results Barwise and Cooper (1981: p122-3), in "Formal Semantics: the ...