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)

1
vote
2answers
327 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 ...
1
vote
1answer
111 views

Does every ultrafilter contain sets of sup-measure $0$?

Let $\mathbb{N}$ be the set of positive integers and for $A\subseteq {\mathbb{N}}$ set $$m(A) = \text{lim sup}_{n\to\infty}\frac{|A\cap\{1,\ldots,n\}|}{n}.$$ Does every ultrafilter ${\cal U}$ on ...
6
votes
1answer
167 views

Proof-theoretic ordinals after liberalizing induction to $RCA_0$

This is kind of a follow-up to this question. For a class $\Gamma$ of second-order formulas (here either $\Sigma_n^0$ or $\Sigma_n^1$), let $X\Gamma$ be a formal theory consisting of $RCA_0$ together ...
6
votes
4answers
423 views

Direct axiomatization of ordinal and cardinal numbers

Again, this question is related (**) to a previous one: in standard books on basic set theory, after stating the axioms of ZFC, ordinal numbers are introduced early on. Afterwards cardinals appear: ...
5
votes
1answer
264 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
110 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
127 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
118 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
85 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
52 views

Minimal CNF expression [closed]

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
838 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
70 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
131 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
973 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
154 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
370 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
143 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 ...
9
votes
1answer
311 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
139 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
168 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
218 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
172 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
141 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
136 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
199 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
371 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
315 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
283 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
423 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
167 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
880 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
230 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
608 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
188 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
767 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
159 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 ...