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)

5
votes
0answers
209 views

Constructive compactness for countable models?

The compactness theorem for countable (Tarski?) models is equivalent to the weak König's lemma by a result of H. Friedman and others as noted here, in the context of classical logic. The weak König's ...
2
votes
1answer
97 views

Can tests for the convergence and divergence of series be used to create undecidable sentences?

Let f(k) be a recursive function which maps the set of positive integers into itself. Let T be a formalized theory which is axiomatizable and contains Peano's Arithmetic as a sub-theory. For example, ...
2
votes
1answer
114 views

Some very weak statements on choice

This is a follow-up question to Does $|(X\times\{0\}) \cup (X\times\{1\})| \leq |X|$ for $X$ infinite imply ${\sf AC}$? Consider the statements $(\text{S}1)$ For any infinite set $X$ there ...
2
votes
1answer
109 views

Does $|(X\times\{0\}) \cup (X\times\{1\})| \leq |X|$ for $X$ infinite imply ${\sf AC}$?

Consider the statement For any infinite set $X$ there is an injection $\varphi$ from $(X\times\{0\}) \cup (X\times\{1\})$ into $X$. Does this imply the ${\sf AC}$?
37
votes
4answers
2k views

Inconsistent theory with long contradiction

What can one say about an inconsistent theory $T$ which has no contradictions (i.e. deductions of $P \wedge \neg P$) of length shorter than $n$, where $n$ is some huge number? There have been some ...
24
votes
1answer
2k views

Community experiences writing Lamport's structured proofs

About two years ago, I came across this paper by Lamport http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-how-to-write.pdf on writing proofs hierarchically. It changed how I wrote ...
4
votes
0answers
74 views

Ref request: modelling regular theories as an injectivity condition

The background to the following observation is standard material in categorical logic, and I thought this was was too — I don’t remember learning it, but I don’t think it is original — but I can’t now ...
-1
votes
0answers
51 views

Minimal CNF expression [on hold]

Given any propositional form A, I'm interested on finding an equivalent CNF form of minimal length. Length of a formula is defined as the number of atomic statements in the formula. For example, ...
1
vote
1answer
830 views

What is the modern consensus on the difficulty of infinitesimals?

At a related thread at MSE an expert in reverse mathematics noted that "As the modern consensus is that only nonstandard models have infinitesimals, it will be quite challenging to give a concrete ...
21
votes
9answers
2k views

What is… A Grossone?

Y. Sergeyev developed a positional system for representing infinite numbers using a basic unit called a "grossone", as well as what he calls an "infinity computer". The mathematical value of this ...
-1
votes
0answers
69 views

Elementary derivation in a very stingy logical calculus [closed]

Following up on my previous question, I am trying to understand the logical calculus defined here (p.183) by Buchholz and Weiner. I want to prove $0=0+0$. (I can prove $0+0=0$: I start with ...
2
votes
1answer
123 views

A derivation in Tait calculus

I have seen in at least two different places (here, p. 183; and here, last slide) the Tait calculus defined the following way. Here $\Gamma$ denotes a set of formulas $\{A_1, \ldots, A_k\}$, which is ...
6
votes
5answers
972 views

A book explaining power and limitations of Peano Axioms?

Are there books or survey articles explaining the subject to a non-expert? To clarify what I mean, here is a couple of issues that I would like to read about. (I am mainly interested in references but ...
13
votes
3answers
1k views

How would calculus be possible in a finitist axiom system?

I am interested in learning a little more about finitism, currently about which I only know a few encyclopedic paragraphs. I know that during some time, some mathematicians like Kronecker thought ...
16
votes
1answer
1k views

Analogues of Primitive Recursive Functions

Let $\mathbf{A}$ be an admissible set (possibly with urelements). I am wondering if there is some good notion of "primitive recursive arithmetic" relative to $\mathbf{A}$. More precisely, I would like ...
1
vote
0answers
152 views

Reference request: Models of isomorphic languages result into isomorphic categories

This is basically a reference request by someone who has not been educated as a logician and would like to be rigorous about certain preliminary aspects of model theory. Fix an uncountable universe ...
6
votes
1answer
352 views

Taller models of ZFC

This question is somewhat related to a previous one, where I asked for new forms of infinite beyond the cardinal hierarchy. Using forcing techniques, at least the ones I know of, one starts from a ...
16
votes
2answers
654 views

Which graphs are elementarily equivalent to their own disjoint sums?

In Stefan Geschke's recent question, one of the solutions observed that the graph consisting of a single infinite beaded chain, a $\mathbb{Z}$-chain where each integer is connected to its nearest ...
1
vote
1answer
140 views

What restriction(s) of Goedel's primitive recursive functionals is (are) necessary and sufficient to prove the consistency of $PRA$

It is well known that one can use Goedel's primitive recursive functionals of finite type to prove the consistency of $PA$ (Peano Arithmetic). As such, one can certainly use them to prove the ...
1
vote
1answer
284 views

Was “arithmetical translation” (coding in the Goedel sense) ever a part of Hilbert's Program?

Was "arithmetical translation" (that is, coding in the Goedel sense) ever a part of Hilbert's Program? I ask this question for several reasons: i) it gives the numerals |, ||, |||,.... an ersatz ...
9
votes
1answer
308 views

Every measure on a set $X$ extends to the power set of $X$: Consistent or not with ZF?

Question. Is it consistent with ZF that every (countably additive, non-negative) measure $\mu: \Sigma \to \bf R$, where $\Sigma$ is a sigma-algebra on a given set $X$, extends to a (countably ...
6
votes
2answers
1k views

Are all the theorems true?

The title sounds a bit philosophical, but it is about mathematics. Let me explain. Consider a first order theory $T$, which is an extension of Peano Arithmetic. Call this theory "good" if it is ...
4
votes
2answers
138 views

first order languages over graphs (and other discrete models)

A lot of research has been devoted to the study of first order language of graphs (FO). Formulas in this language are constructed using variables $x, y,\dots$ ranging over the vertices of a graph, the ...
6
votes
1answer
165 views

Adding a truth-like predicate to PA

It is well known that adding a truth predicate to arithmetic in the most natural way leads to a contradiction. Suppose as usual that we add a one place relation T to the language of arithmetic, and ...
7
votes
2answers
213 views

How can any theory prove well-foundedness of ordinals above $\omega_1^{\text{CK}}$?

$\newcommand{\omegaoneck}{\omega_1^{\text{CK}}}$ Pardon the extremely basic question - this isn't quite my area - but I'm confused about the definition of proof theoretic ordinals. The proof ...
3
votes
1answer
168 views

Reference request: eliminating function symbols in predicate logic

Here is a basic technique in logic which seems well-known in folklore, but which I haven’t managed to find written down anywhere. $\newcommand{\T}{\mathbf{T}}$ Fact. Let $\Sigma$ be a signature (in ...
17
votes
1answer
533 views

Dual Borel conjecture in Laver's model

A set $X\subseteq 2^\omega$ of reals is of strong measure zero (smz) if $X+M\not=2^\omega$ for every meager set $M$. (This is a theorem of Galvin-Mycielski-Solovay, but for the question I am going to ...
6
votes
2answers
140 views

a variant of the Kleene tree

The (a?) Kleene tree is a computable (a.k.a. decidable) sub-tree of the full binary tree with no computable path. It is well-known. I need a variant. (For those in the know, I need a c-bar which is ...
4
votes
0answers
135 views

Set theory and forcing from the point of view of a formal system $G^+$ of Gentzen type

There are four papers by Vladimir Alfeevich Kuznetsov, which discuss the above titled topic: (1) Some problems in set theory from the standpoint of a formal system G+ of Gentzen type. (Russian) Akad. ...
4
votes
1answer
198 views

When does an infinite model have a proper class-sized elementary extension?

Suppose that a set of sentences of a 1st order language has an infinite model $M$. Under what conditions is there is a proper class-sized elementary extension of $M$? How does the answer change if ...
10
votes
4answers
341 views

A well-founded relation on lists

Let $A$ be a set equipped with a well-founded relation $<$, let $LA$ be the set of finite lists of elements of $A$, and define a relation $\prec$ on $LA$ such that $\ell \prec m$ if $\ell$ is ...
3
votes
2answers
235 views

References for the Keisler Order

Are there any good/modern references on the Keisler order. I have been reading Keisler's original paper, "Ultraproducts which are not Saturated", which introduces the order. However it is somewhat ...
7
votes
7answers
370 views

Strength of Bishop style constructive mathematics vs $\mathsf{RCA}_0$

This question came out of this other MO question of mine. My question is Is there a formal comparison between $\mathsf{RCA}_0$ and $\mathsf{BISH}$ (Bishop style constructive mathematics as used ...
9
votes
0answers
314 views

Riemann hypothesis in Zilber's field

Question. What is known about the situation (truth or falsity) of Riemann hypothesis in the Zilber's field?
2
votes
2answers
281 views

Non-Formal Applications: Higman and Kruskal

After looking through many papers, I noticed that most of the discussions and proofs for Higman's Lemma and Kruskal's Tree Theorem only have formal applications in set theory, logic, and type theory. ...
3
votes
0answers
141 views

Reducing Consistency of $PA$ [closed]

By godel translation consistency of $PA$ is equivalent to consistency of $HA$. I want to know any similar theorems for $PA$. 1.What is the minimal theory $T\subsetneq PA$ such that the proof of ...
2
votes
2answers
421 views

Is there a countable pseudocharacter Hausdorff space,such that…?

Let X be a Hausdorff space and Difine the Property A as following: if $\mathscr{U}$ is a collection of open sets of X that witnesses Hausdorff property of X (= $\forall x,y \in X$, there exist two ...
21
votes
8answers
2k views

Between mu- and primitive recursion

It is well known that primitive recursion is not powerful enough to express all functions, Ackermann function being probably the best known example. Now, in the logic courses (that I have had look ...
2
votes
2answers
164 views

Compactness for countable models?

How and where is it proved that WKL$_0$ proves the compactness theorem for countable models? (This is a follow-up to a comment of F. Dorais.)
28
votes
2answers
1k views

The logic of convex sets

Let me start with Helly's theorem: Let $A_1$, $A_2$, ..., $A_{n+2}$ be $n+2$ convex subsets of $\mathbb R^n$. If any $n+1$ of these subsets intersect (this means: have nonempty intersection), the so ...
7
votes
3answers
879 views

About the axiom of choice, the fundamental theorem of algebra, and real numbers

About fundamental theorem of algebra, there is a large collection different demonstrations. I ask: is there some proof that avoids AC (choice axiom)? In a general topos (with natural number object) ...
14
votes
1answer
229 views

Is the Martin's axiom number $\mathfrak m$ regular

The Martin's axiom number $\mathfrak m$ is the least cardinal $\kappa$ for which $\text{MA}_\kappa(\text{ccc})$ is false, i.e. the least cardinal such that there exists a ccc poset $P$ and a family ...
5
votes
3answers
603 views

What does the axiom of replacement mean and why should I believe it?

Here Professor Blass describes the following cumulative hierarchy of sets: Begin with some non-set entities called atoms ("some" could be "none" if you want a world consisting exclusively of ...
6
votes
1answer
187 views

Does “$|{\cal P}_2(X)| = |X|$ for $X$ infinite” imply ${\sf (AC)}$?

This comes from a comment made by user bof in this thread. Let $X$ be a set, define ${\cal P}_2(X) = \big\{\{a, b\}: a\neq b\in X\big\}$. Consider the statement ${\sf (S)}$ If $X$ is an ...
12
votes
1answer
764 views

Reverse-engineer forcing: am I reinventing the wheel?

In the course of a project I’m working on, I’ve started playing around with a sort of “reverse-engineering” forcing. It seems interesting, but I have a sinking feeling I’m reinventing the wheel; does ...
20
votes
9answers
3k views

Was the early calculus inconsistent?

This question does NOT concern the RIGOR, or lack thereof, of the early calculus. Rather the question is of its CONSISTENCY. George Berkeley wrote in 1734 with reference to the early calculus that ...
4
votes
0answers
157 views

Finding limit-nondecreasing sets for certain functions

This is a question that arose a while ago in work with Damir Dzhafarov on some pieces of reverse mathematics. As far as I know, it has no deep significance; however, it feels like the sort of thing we ...
3
votes
0answers
323 views

“Nicely” strong measure zero sets

This question is essentially an expanded version of the unanswered half of Two strengthenings of "strong measure zero". A set $X$ of reals is strong measure zero if, for any $f: ...
21
votes
4answers
1k views

What are the advantages of the more abstract approaches to nonstandard analysis?

This question does not concern the comparative merits of standard (SA) and nonstandard (NSA) analysis but rather a comparison of different approaches to NSA. What are the concrete advantages of the ...
24
votes
2answers
1k views

A set that can be covered by arbitrarily small intervals

Let $X$ be a subset of the real line and $S=\{s_i\}$ an infinite sequence of positive numbers. Let me say that $X$ is $S$-small if there is a collection $\{I_i\}$ of intervals such that the length of ...