Questions tagged [lo.logic]
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, theories of truth, truth revision, consistency.
5,154
questions
7
votes
1
answer
968
views
Propositional calculus, first order theories, models, completeness
In the usual context of model theory one studies first order theories: the Gödel completeness theorem asserts that $\varphi$ is a theorem of a theory $T$ (i.e. $\varphi$ is provable from the axioms of ...
- 9,150
6
votes
1
answer
179
views
Consistency in pure type systems
Summary
My question is about how (i) a certain presentation of pure type systems in the $\lambda$-cube, bears on (ii) a standard definition of consistency in pure type systems. In short, I'm ...
- 63
4
votes
2
answers
286
views
Is there a consistent, unsound, $\omega$-inconsistent, effective theory that doesn't prove its own inconsistency?
Can we have a consistent and effective (fulfilling Godel's criteria) first order theory $T$, that is both arithmetically unsound and $\omega$-inconsistent, and yet doesn't prove its own inconsistency (...
- 9,276
18
votes
2
answers
1k
views
What notable theorems cannot be automatically proven without choice using Shoenfield absoluteness?
There have been a couple of recent questions, here and here, regarding the role of the axiom of choice in real-analytic results with applicability to general relativity. This lead me to look at some ...
- 10.3k
8
votes
2
answers
1k
views
Can we effectively axiomatize a theory that proves the negation of its own Gödel's sentence?
For any consistent and effective theory $T$ fulfilling Gödel's criteria, let $G_T$ be the Gödel sentence of $T$, that is: $$ G_T \iff \neg \exists x: \operatorname{Proof}_T(x,\ulcorner G_T \urcorner)$$...
- 9,276
10
votes
2
answers
418
views
The additive structure of clusters of nonstandard models of arithmetic
Given $\frak M$ a countable nonstandard model of $\sf PA$ and let $a\in M$ be a nonstandard element. A "cluster around $a$" is the set of successors and predecessors of $a$, a cluster is a ...
- 1,645
5
votes
2
answers
699
views
What is lost in General Relativity without Hahn-Banach axiom in the ZF+HB set theory?
In the same spirit of this question:
How much of mathematical General Relativity depends on the Axiom of Choice?
I want to go radically further ahead and ask for what remains of mathematical general ...
- 308
4
votes
0
answers
237
views
Cantor-Bernstein phenomena for structures (and a "moderate zigzag" property)
My favorite proof of the Cantor-Bernstein theorem is the one that argues by "histories" - given injections $f:A\rightarrow B$ and $g:B\rightarrow A$, we identify each element of $A$ as ...
- 19.3k
10
votes
2
answers
431
views
Is the set of permissible numbers of models of various cardinalities computable?
This question arose in the comments to this question.
Let $X$ be the set of pairs $(m,k)$ such that there is some (consistent complete countable first-order) theory $T$ with exactly $m$ models of size ...
- 19.3k
53
votes
7
answers
6k
views
Are there any undecidability results that are not known to have a diagonal argument proof?
Is there a problem which is known to be undecidable (in the algorithmic sense), but for which the only known proofs of undecidability do not use some form of the Cantor diagonal argument in any ...
- 109k
6
votes
1
answer
378
views
Thick Canadian trees
A Canadian tree (also called a weak Kurepa tree) is a tree of height $\omega_1$ with levels of cardinality $\leq \omega_1$ and at least $\omega_2$ many uncountable branches. Let's call a Canadian tree ...
- 4,343
6
votes
1
answer
341
views
Quantifier complexity of definition of compactness
This question is inspired by the post on quantifier complexity of
continuity. We work with metric spaces M
considered as two-sorted first-order structures (M,$\mathbb R$,d,+,⋅,<)
where $d:M^2→\...
- 15.4k
4
votes
1
answer
727
views
Why adhere to $\omega$-consistency with respect to Godel's proof of first incompleteness?
On MSE I've asked a question about why did Godel assume the theory in question to be $\omega$ consistent [on top of effectiveness] for his proof [actually the second part of his proof] of first ...
- 9,276
13
votes
1
answer
504
views
Is there a complete uncountable theory with two countable models?
This is a question originally asked at MSE a few years ago; the original poster hasn't been active in a while, so I'm taking the liberty of asking it here:
Is there a complete first-order theory $T$ ...
- 19.3k
8
votes
2
answers
655
views
Is the existence of substructures satisfying a theory absolute?
Given a first-order structure $\mathfrak{A}$ and a first-order theory $T$ one can ask if
$$
\varphi(\mathfrak{A}, T) := ``\text{there is a substructure } \mathfrak{B} \text{ of } \mathfrak{A} \text{ ...
- 1,215
3
votes
1
answer
202
views
Another implication of the Affine Desargues Axiom
Definition 1. An affine plane is a pair $(X,\mathcal L)$ consisting of a set $X$ and a family $\mathcal L$ of subsets of $X$ called lines which satisfy the following axioms:
Any distinct points $x,y\...
- 40.9k
2
votes
1
answer
120
views
Splitting $\Pi^0_2$ Singletons?
Given a (non-computable) $\Pi^0_2$ singleton $Y$ are there Turing incomparable $\Pi^0_2$ singletons $X_0, X_1$ with $Y \equiv_T X_0 \oplus X_1$?
What about the same question for arithmetic ...
- 2,633
14
votes
0
answers
416
views
Which functions have all the common $\forall\exists$-properties of continuous functions?
This is an attempt at partial progress towards this question. Meanwhile, Sam Sanders pointed out that my original term was already in use, as were a couple other back-up terms, so ... oh well.
For a ...
- 19.3k
4
votes
1
answer
224
views
Can a halting oracle determine if a Turing machine is an ordinal?
For the sake of clarity, I am regarding a computable relation on $\mathbb{N}$ as a $2$-symbol ($0$ and $1$) Turing machine $T$ which halts on any initial binary string (which are interpreted as some ...
- 460
4
votes
0
answers
143
views
On self-reference in a weak structure
Below, all structures are countable and in finite languages. This question is motivated by the following: "To what extent is self-reference possible when nothing like the diagonal lemma holds?&...
- 19.3k
6
votes
1
answer
278
views
What is the power of the “anti-halting” oracle?
Let me first ask the question, and then, as it may seem a bit cryptic, explain how it comes up (and whence the “anti-halting oracle” in the title):
Notations: we write $\langle m,n\rangle$ for a ...
- 30.2k
4
votes
0
answers
354
views
Does $e^x$ let the reals build any new ordinal functions?
This question is closely related to this one. Belatedly, it occurred to me that I'd probably picked the wrong test question. I'm leaving that question up because I don't think it's bad per se, but I ...
- 19.3k
5
votes
1
answer
411
views
Uniform strategy on Kastanas' game
I think my question applies to most games, but for the sake of concreteness, I shall consider one specific game in this question. We consider the game posed by Ilias Kastanas in his paper On the ...
- 976
1
vote
0
answers
91
views
Need help unpacking the interdependence of axiomatic set theory and first-order logic
I'm currently self-studying both Von Neumann Set Theory (not ZFC but rather axiomatic set theory with the undefined notion of class) and First-Order Logic.
I've been self-studying the following ...
- 119
21
votes
4
answers
3k
views
Is Bauer–Hanson’s result “there is a topos where the Dedekind reals are countable” novel?
Last year, Andrej Bauer gave a talk showing that there is a topos in which the set of Dedekind reals is (sub)countable, and thus, you cannot prove that $\mathbb{R}$ is uncountable without LEM. He ...
- 415
0
votes
1
answer
380
views
How bad is Coq proving both $T$ and $\lnot T$? [closed]
Question: How bad is Coq proving both $T$ and $\lnot T$? Can it be abused?
Back in 2011 on the coq-club mailing list there was a thread:
Is the Daniel Schepler's inconsistency real?.
In the thread ...
- 24.2k
7
votes
0
answers
246
views
Something like "o-minimal ordinal analysis"
Below, by "nice structure" I mean "o-minimal expansion of $(\mathbb{R};<)$ by countably many continuous functions and open relations."
Suppose $\mathfrak{A}=(\mathbb{R};<,......
- 19.3k
32
votes
2
answers
2k
views
Quantifier complexity of the definition of continuity of functions
This was previously asked at MSE, but I was told to ask it on MO. Consider the structure $(\mathbb{R};+,-,*,0,1,<)$. We adjoin to it a unary function $f$ defined everywhere on the set of real ...
- 2,063
40
votes
3
answers
5k
views
How much of mathematical General Relativity depends on the Axiom of Choice?
One of the cornerstones of the mathematical formulation of General Relativity (GR) is the result (due to Choquet-Bruhat and others) that the initial value problem for the Einstein field equations is ...
- 593
-3
votes
1
answer
159
views
Propositional logic without rules of inference and assumptions (except MP) [closed]
I was wondering whether it would be possible to do propositional logic without any rules of inference and assumptions (except modus ponens).
I have the following axioms:
$ p \to (q \to p) $
$ (p \to (...
1
vote
0
answers
64
views
On known links between convexity and fuzzy logic
The following are thoughts I had during a joint work with P. Olver on maps from spheres to the convex hull of finitely many points in some finite-dimensional vector space. I do not wish to discuss the ...
- 5,011
1
vote
1
answer
159
views
How can implications in Gödel logic be understood as assumptions?
Say we have a (positively) real valued logic, i.e. formulas evaluate to the extended interval $[0,\, \infty]$. Furthermore, we have a Gödel implication $a \rightarrow b$ that evaluates to $\infty$ ...
- 21
-1
votes
1
answer
317
views
Can MK+"Ord is almost-huge"+MM$^{++}$ be new standard foundations instead of ZFC?
I'll try to explain what this looks like to a non-expert in set theory. First, $MK$ is just a second-order $ZFC$, and there are moments when we would like to use second-order statements, for example, ...
- 77
5
votes
0
answers
156
views
How to show that $\omega^\omega$ is well-founded in PA?
By induction on $n$ variables I can show that for any meta-natural number $n$, PA proves well-foundedness of $\omega^n$. However it is well known that PA proves well-foundedness of $\omega^\omega$ ...
- 91
4
votes
0
answers
216
views
On natural examples, how much stronger is this than Löwenheim–Skolem?
Given a logic (= regular logic in the sense of Ebbinghaus/Flum/Thomas) $\mathcal{L}$, let a $\downarrow$-sentence be an $\mathcal{L}$-sentence $\varphi$ such that, whenever $\mathfrak{M}\models\varphi$...
- 19.3k
5
votes
2
answers
408
views
Topos semantics of constructive higher order logic
I would like to find a reference that describes the semantics of constructive higher order logic with function types in toposes. In particular, it seems that if we are to take function types as ...
- 1,031
10
votes
4
answers
614
views
Deciding homomorphic images of De Bruijn graphs
The De Bruijn graph $B_n$ of
dimension $n$ (on the two-letter alphabet) is defined as the directed graph on
$2^n$ vertices and $2^{n+1}$ edges, where for every $w = w_0 \dots w_n \in
2^{n+1}$ we put ...
- 105
3
votes
1
answer
125
views
A $\Pi^0_1$ class of $\alpha$-subgenerics for all $\alpha < w_1^{CK}$
In Harrington's mimeographed notes (see here) solving McLaughlin's conjecture he builds reals $f \in \omega^\omega$ which have the property of being $\alpha$-subgeneric defined as follows. He does ...
- 2,633
5
votes
1
answer
316
views
Primitive recursive bounds for multidimensional polynomial vdW / HJ
In Shelah's paper 679, he proves primitive recursive bounds for the polynomial Hales-Jewett theorem and thus for the polynomial van der Waerden theorem.
How about for the multidimensional polynomial ...
- 383
2
votes
1
answer
129
views
Harrington's notes on McLaughlin/Arithmetically incomparable singletons
At one point I had copies of the handwritten notes Leo created about the McLaughlin conjecture and I know a similar set of notes exist titled Arithmetically incomparable arithmetic singletons. I've ...
- 2,633
4
votes
0
answers
176
views
Status of Problems in 102 problems in mathematical logic
Is there any location that records the current status of the problems in 102 problems in mathematical logic? Or, better yet, serves as a status board for open problems in mathematical logic? ...
- 2,633
4
votes
0
answers
104
views
Coding fourth-order objects in second-order Reverse Mathematics
Reverse Mathematics (RM for short) generally takes place in the language of second-order arithmetic. Thus, higher-order objects need to be "coded" or "represented" indirectly. ...
- 3,969
7
votes
0
answers
104
views
How tightly are decidability and "induction-completeness" linked?
It is known that there are a number of expansions of the structure $\mathfrak{N}:=(\mathbb{N};+)$ which are decidable (= have computable theories); one such example is the expansion by a predicate ...
- 19.3k
7
votes
1
answer
286
views
Dedekind-finite-to-one vs Dedekind-finite
This is a slight variation of this recommended blog post by Asaf Karagila. Let $A$ be a set. Then:
$A$ is said to be Dedekind-finite if every injective map $f:A\to A$ is also surjective.
$A$ is said ...
- 45.5k
-2
votes
1
answer
177
views
Can this Rosser-like trick also work as a proof of the first incompleteness theorem?
The context of this question is related to proving the first incompleteness by alternative ways related to Rosser's trick. So, for a proof by negation, we assume that $T$ is complete, and fulfills ...
- 9,276
12
votes
2
answers
811
views
An overview of mathematical-logical approaches in formalizing natural languages
Crossposted on Mathematics SE
I am an undergraduate mathematics student with a keen interest in pursuing research in the formalization of natural languages (from a more mathematical-logical approach),...
5
votes
1
answer
147
views
Countable closure of quotient forcing
Let us say that a partial order is "countably closed with infima" if every descending $\omega$-sequence has an infimum.
Suppose $P$ and $Q$ are posets that are countably closed with infima, ...
- 18.1k
6
votes
1
answer
478
views
Normal form for terms in language with two ring structures
Suppose I have two different ring structures on the same domain $\langle R,+,\cdot,0,1\rangle$, $\langle R,\oplus,\otimes,\bar 0,\bar 1\rangle$ and I throw the structures together into a single common ...
- 225k
4
votes
0
answers
146
views
The monochromatic principle and the axiom of choice
For any set $A\neq\emptyset$, denote by $[A]^A$ the collection of sets $B\subseteq A$ such that there is a bijection $\varphi:B\to A$. If ${\cal S}\subseteq [A]^A$, we say that $B\in[A]^A$ is ...
- 45.5k
7
votes
0
answers
163
views
"Minimal-ish" Dedekind-finite cardinalities of models
Throughout, we work in $\mathsf{ZF}+$ "There is an infinite Dedekind-finite set."
Say that a Dedekind-finite cardinality $\kappa$ is $\Sigma^1_1$-isolated iff there is some first-order ...
- 19.3k