first-order and higher-order logic, model theory, set theory, proof theory, computability theory, formal languages, definability, interplay of syntax and semantics, constructive logic, intuitionism, philosophical logic, modal logic, completeness, Gödel incompleteness, decidability, undecidability, ...

learn more… | top users | synonyms (1)

4
votes
2answers
186 views

Conjecture of a subset of Wang tile which might be decidable

From the two papers proving the undecidability of Wang tile in 1966 by Berger and in 1971 by RM Robinson, the tiles used in proving undecidability has a general common feature: The left color and ...
2
votes
1answer
227 views

A variant of Kruskal's theorem

For $X$ and $Y$ finite sequences of finite trees, let us say that $X$ is everywhere contained in $Y$ ($X\subseteq_{ec}Y$) iff, for every $y\in Y$, there is some $x\in X$ such that $x$ is a minor of ...
5
votes
1answer
214 views

Interaction between Turing and many-one reducibility

This is a question about two reducibility notions in computability theory. I suspect the answer is a fairly simple construction, and I'm just not seeing it. For sets $X, Y\subseteq\omega$, we say $X$ ...
9
votes
2answers
424 views

What is the precise notion of “enough arithmetic” in Godel's first Incompleteness theorem?

I'm trying to reconstruct the proof of Godel's first theorem (Rosser's strong version) from the uncomputability of the Halting function. If we just started with the language $\mathcal{L}=\{0, S, +, ...
5
votes
4answers
227 views

Is every Heyting algebra the Lindenbaum algebra of an intuitionistic first order theory?

This question comes after the comments in the recent related question Sigma-complete Lindenbaum algebras?, but in its current form is sufficiently different in my opinion, and so I decided to follow ...
2
votes
1answer
142 views

Sigma-complete Lindenbaum algebras? [closed]

Is there any calculus whose algebraization is a sigma-complete Lindenbaum algebra, i.e., a sigma-complete Boolean algebra after identification of equivalent formulas?
3
votes
1answer
141 views

On a modal correspondence

Is there an intuitive characterization of the correspondence for the modal logical formula $\square (\alpha \rightarrow \square \alpha) \rightarrow (\square \alpha \vee \square \lnot \alpha)$? In ...
13
votes
0answers
553 views

Souslin trees and weakly compact cardinals

In Souslin trees on the first inaccessible cardinal it is asked if it is consistent that there are no $\kappa-$Souslin trees at the least inaccessible cardinal $\kappa$. In this question I would like ...
1
vote
0answers
99 views

On directedness, transitivity and ancestral directedness

Let $\textit{C}$ be the modal logical schema $(\square (\square \alpha \rightarrow \alpha) \wedge \square (\square \lnot\alpha \rightarrow \lnot \alpha))\rightarrow (\square \alpha \vee \square \lnot ...
4
votes
0answers
72 views

$n$th order arithmetic with predicates for orders

Two papers I have looked at lately axiomatize $n$-th order arithmetic in a single sorted language with predicates $Z_1,\dots,Z_n$ and axioms like $\forall x(Z_1(x)\vee\dots\vee Z_n(x))$ to say ...
2
votes
0answers
64 views

Algorithmic quantifier elimination over p-adic fields

It is known that the first-order theory of p-adic fields is decidable, and that the p-adics admit elimination of quantifiers. What is the state of the art in algorithmic aspects of quantifier ...
6
votes
6answers
631 views

practical algorithms for np complete problems

Inspired by: Conjecture on NP-completeness of tesselation of Wang Tile up to finite size And the practicality of this topic (solving tessellation on a lattice): coloring in lattice Computational ...
8
votes
2answers
288 views

The (non-)absoluteness of second-order elementary equivalence

Elementary equivalence is set-theoretically absolute between any two transitive models of set theory; this is also true for the infinitary logics - e.g., $\mathcal{L}_{\omega_1\omega}$ - at least, ...
8
votes
1answer
269 views

Canonical model for $\neg\mathsf{CH}$ and $\Omega$-logic

Recently I found this book by Woodin. In the introduction of it the author writes the following: The main result of this book is the identification of a canonical model in which the Continuum ...
3
votes
1answer
121 views

How do you prove that Q+Con(PA) can't be interpreted in ACA_0?

The theory $\mathrm{ACA}_0$ is not reflexive (because it is finitely axiomatisable and cannot prove its own consistency). So how, if at all, is it possible to prove that $\mathrm{Q+Con(PA)}$ cannot be ...
6
votes
1answer
231 views

Does the totality of Ackermann's function prove the consistency of $\Sigma_1$-induction?

It is well known that Ackermann's function is not primitive recursive. Therefore, the theories of primitive recursive arithmetic (PRA) and of $\Sigma_1$-induction ($I\Sigma_1$) cannot prove the ...
12
votes
0answers
278 views

Do all linear orders in this class have computable copies?

This is a question which has been bothering me now for quite some time. I've talked to a number of people about it, and we've shown that a few basic ideas can't work, but other than that haven't made ...
6
votes
2answers
224 views

Is every non-recursive set in $\Sigma_1$ complete in $\Sigma_1$ (relatively to many-to-one reductions)?

Most well known sets in $\Sigma_1 \setminus\Delta_0$, such as the Halting problem, are complete in $\Sigma_1$, relatively to the many-to-one reduction. In fact I don't know any example of a (non ...
1
vote
0answers
43 views

A question on completeness for quantified temporal logics

Quantified temporal logics have the Barcan formulas and its converses for both G (it will always be the case that) and H (it has always been the case that), so that both $\forall x G \alpha ...
5
votes
1answer
236 views

Woodin Cardinals and Inner Models

I have a few questions I have been thinking about that I could definitely use some insights on: Question 1. Since a Woodin cardinal is a "local" notion, defined with respect to some rank-initial ...
0
votes
1answer
81 views

Preserving Predimension Functions under Functional Convergences

Definition 1. If ‎$‎‎‎\mathcal{L}‎$ ‎is a‎ ‎countable relational ‎language, ‎a ‎predimension ‎class ‎‎‎‎‎$‎C‎$ is a class ‎of $‎‎\mathcal{L}$-structures with ‎the ‎following ‎properties:‎ ‎C1: ...
2
votes
0answers
112 views

Preimages of accessible full subcategories

My question is ultimately about the model theory of $L_{\infty, \omega}$, but it is more convenient to phrase it in terms of category theory. Suppose I have finitely accessible categories ...
5
votes
1answer
164 views

Is a computer program for correspondence theory available?

In the 1990s I some times used a computer program with the Max Planck Institute which helped with calculating complicated correspondences for modal logical formulas. Is some program like that ...
4
votes
1answer
140 views

Stable examples from Algebra such that the model theoretic algebraic closure of a substructre is no model

Let $T$ be a stable theory. Let $A$ be a subset or substructure of a model $M$ of $T$. Now in some theories the (model theoretic) algebraic closure of $A$ is already a (sub)model of $T$. For example, ...
1
vote
0answers
27 views

Completeness results for quantified tense logics with BF?

Modal tense logics or temporal logics are important in that they correspond with partial orders and their extensions. Are there completeness results for quantified temporal logics with the Barcan ...
4
votes
0answers
92 views

Relation between fundamental theorem of Ehrenfeucht-Fraisse games and notions of bisimulation and simulation

Vijay D alluded to the relation between the fundamental theorem of Ehrenfeucht-Fraisse games and notions of bisimulation and simulation in response to the whats-a-magical-theorem-in-logic question. ...
9
votes
3answers
344 views

Is a model of arithmetic contained in a model of arithmetic an initial segment?

It's easy enough to show that if $\mathbb{N}_1$ is a non-standard model of the Peano axioms, then there is a canonical embedding $\mathbb{N} \to \mathbb{N}_1$, and we have a theorem that if $x \in ...
7
votes
3answers
334 views

Decidability of the winning-position problem in an infinity chess with a finite number of short-range pieces only

Definitions Long-range pieces: queens, rooks, bishops. Short-range pieces: pawns, knights, kings. We can extend the definition of short-range pieces to include also fairy pieces like: Berolina ...
16
votes
2answers
455 views

Is the notion of fixed point property for topological spaces an absolute notion?

Recall that a topological space $X$ has the fixed point property (FPP) if any continuous function $f: X\to X$ has a fixed point. Is the notion of FPP for topological spaces an absolute notion? More ...
1
vote
0answers
42 views

A question on the incompleteness of quantified K.2 and S4.2 with the Barcan formula

I have been attempting to come to grips with Max Cresswell's account of this in Journal of Philosophical Logic 24 (4):379 - 403 (1995) where he presents proofs of the incompleteness of QK.2BF as well ...
7
votes
0answers
309 views

Is there a theory of abuse of notation? [closed]

Is there any theory about the different ways notation can be abused and which abuses are ineliminable without complicating the notation in some essential way? We can define "abuse of notation" as any ...
1
vote
2answers
236 views

Infinite play with tape, or covering the integers with prime arithmetic progressions

It is possible that a more technical version of this question has been asked and answered in the literature. If so, then a reference is much appreciated. I will phrase it in terms of colored tapes ...
2
votes
1answer
90 views

A question on the modal logic S4.2

The modal logic S4.2 with the characteristic axioms 4: $\square \alpha \rightarrow \square \square \alpha$ and .2: $\lozenge \square \alpha \rightarrow \square \lozenge \alpha$ and T: ...
10
votes
0answers
140 views

Maximality of linear orders in the Keisler order on theories

Recently Malliaris and Shelah (see their preprint http://math.uchicago.edu/~mem/Malliaris-Shelah-CST.pdf) have shown that theories with $SOP_2$ are maximal in the Keisler order. A preceding result of ...
5
votes
1answer
114 views

Attribution of an equivalence of the existence of omega-models of RCA0

There are many well-known equivalences in reverse mathematics between statements of the form "Every set is contained a countable coded $\omega$-model of $T$" and $S$, where $S, T$ are subsystems of ...
6
votes
1answer
160 views

Is (Z,+,0,1,P2,P3) decidable?

Is Presburger arithmetic, augmented with two unary predicates P2, P3, for powers of 2 and powers of 3 respectively, decidable? I know that adding just one of P2, P3 to Presburger keeps it decidable, ...
1
vote
1answer
343 views

Compactness and completeness in Gödel logic

The standard proof of the completeness theorem in first-order Gödel logic is based on a first-order countable language. I want to know that is there any proof of the completeness theorem in ...
16
votes
2answers
433 views

Internal logic of the topos of simplicial sets

I am looking for a closed statement (i.e. not depending on any parameter objects) which is true in the internal logic of the topos of simplicial sets, but is not an intuitionistic tautology. Ideally, ...
8
votes
3answers
593 views

What set theoretical questions could never be answered by Turing machines of arbitrary cardinality?

Let us assume that there are Turing machines of arbitrary cardinality, by that I mean they can have input tapes of any arbitrarily high cardinality and compute for a number of steps also of ...
12
votes
1answer
186 views

Nontrivial upper bounds on proof-theoretic ordinals of strong theories: do we have any?

Motivated by Consistency of Analysis (second order arithmetic) and Proof-Theoretic Ordinal of ZFC or Consistent ZFC Extensions?, I have the following question: Are there any examples of strong ...
7
votes
4answers
2k views

Interesting meta-meta-mathematical theorems?

The Goedel incompleteness theorems can be considered meta-mathematical theorems, as they are "written" in a meta-theory and "talk" about properties of a class of formal theories. The following may be ...
3
votes
0answers
140 views

Equational theories determined by “identities without variables”

How to characterize equational theories $T$ which have the following property: for any two terms $t(x_1,...,x_n)$ and $t'(x_1,...,x_n)$ in the signature of $T$, if for any closed terms (i. e. terms ...
8
votes
3answers
569 views

Consistency of Analysis (second order arithmetic)

Is there a proof of the consistency of Analysis (second order arithmetic), which is similar to Gentzen's proof of the consistency of arithmetic? Update: Which (different) methods can be used to ...
3
votes
1answer
214 views

Colorful model theory

There are a number of concepts in model theory - often situated around Hrushovski's amalgamation method (see for instance http://math.univ-lyon1.fr/~wagner/nijmegen.pdf) - which are colorfully named: ...
4
votes
1answer
213 views

Perfect set property implies $\omega_1$ is a limit cardinal in $L$

Specker proved in 1957 that if in $V$ every set of real numbers has the perfect set property, than in $L$, $\omega_1^V$ is actually a limit cardinal. The original proof is in German, and I've been ...
2
votes
0answers
102 views

Does the Lévy collapse obey this nice characterization? [duplicate]

This question is related to an issue in my answer to Monroe Eskew's question on the failure of Cantor-Bernstein for the Lévy collapse. Question. Is the Lévy collapse $\text{Coll}(\omega,\lt\kappa)$ ...
6
votes
1answer
169 views

Failure of Cantor-Bernstein for the Levy Collapse

Related to this question, is it possible to give an example of the failure of Cantor-Bernstein for complete embeddings of forcing notions involving the Levy Collapse $Col(\omega,<\kappa)$? Suppose ...
5
votes
1answer
214 views

A model of Krivine

In a paper by J.-L. Krivine, Modèles de ZF+AC dans lesquels tout ensemble de réels définissable en termes d'ordinaux est mesurable-Lebesgue [C. R. Acad. Sci. Paris Sér. A-B 269 (1969), A549–A552, ...
5
votes
1answer
154 views

What do algebraic theories with strictly terminal trivial models look like?

By algebraic theory I mean one in the sense of Lawvere, i.e. a collection of finitary operations, including projections, together with a multi-composition satisfying the obvious axioms. (I believe ...
7
votes
1answer
474 views

Starting Hilbert's Program on the other end

The idea of Hilbert's program was to start with a simple finitary logic and proof the consistency of more complex systems in this system. Of course, this turned out to be problematic. Even when ...