All Questions
Tagged with formal-languages lo.logic
51 questions
1
vote
0
answers
94
views
Determine equivalences in the generated collection of subgroups and quotients
Let $A$ be an abelian group, and $B_1, B_2, \dots, B_m$ be subgroups of $A$. Define the family of subgroups $\mathcal{D}_0 = \{ \{0\}, A, B_1, B_2, \dots, B_m \}$.
Let $\mathcal{C}_1$ be the ...
- 807
-3
votes
1
answer
188
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 (...
12
votes
2
answers
926
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),...
7
votes
1
answer
494
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 ...
- 236k
17
votes
0
answers
540
views
Are there more true statements than false ones?
It is a nontrivial fact that half the primes are $\equiv 1 \pmod{4}$ and the other half are $\equiv 3\pmod{4}$. The Chebyshev bias suggests, however, that the latter class of primes is winning the ...
- 18.7k
13
votes
1
answer
2k
views
Are 100% of statements undecidable, in Gödel's numbering? [duplicate]
Gödel's incompleteness theorem shows that there are undecidable statements, i.e., formal logical claims which neither have proofs nor disproofs.
In doing so, Gödel famously enumerated all well-formed ...
- 2,902
4
votes
0
answers
121
views
Are semilinear sets piecewise periodic?
I wanted to check my understanding of semilinear sets before I give a talk on them, and I haven't been able to find this exact perspective in any of the sources I've read through. Is it correct, and ...
- 429
4
votes
0
answers
170
views
Corollaries of Kleene's Theorem (Regular Languages)
Kleene's theorem that finite automata (specifically, nondeterministic) are expressively equivalent to regular expressions seems to be a powerful and not immediately obvious tool for untangling the ...
- 429
0
votes
0
answers
113
views
Empty context-sensitive language independent of ZFC?
Is there a simple context-sensitive grammar $G$ such that $L(G)=\emptyset$ is independent of ZFC?
$L(G)$ is the formal language generated by $G$.
- 11
3
votes
1
answer
485
views
Is there an equivalent of the incompleteness theorems/halting problem in category theory?
Taking the doctrine of computational trinitarianism ( https://ncatlab.org/nlab/show/computational+trinitarianism ), if one understands the incompleteness theorems as the "logic" version, and ...
- 141
5
votes
1
answer
464
views
Computational complexity of proof verification
Let $\mathcal{L}$ be a recursive first-order theory, with a deductive system $\Xi$ (for instance, Hilbert-Ackerman proof system). Let $\phi$ be a formula and let $l=(\psi_1, \ldots, \psi_n=\phi)$ be a ...
- 3,318
3
votes
0
answers
722
views
Can third-order arithmetic prove the consistency of second-order arithmetic?
I'm trying to get a deeper understanding of Buss's version of Gödel's speedup proof. In short, if we assume that $Z_0$ is first-order arithmetic, $Z_1$ is second-order arithmetic, and so on, then for $...
- 31
0
votes
1
answer
208
views
Does the fixed point lemma / diagonalization require capturing or not?
Peter Smith's formulation of the diagonalization lemma is essentially as follows, from Theorem 47 of his (fantastic) online book:
If theory T extends Robinson Arithmetic, and P is an one-place open
...
- 31
1
vote
0
answers
206
views
Is it possible to construct a formal language that allows to refer to specific real numbers that encode ordinals accidentally writable by an ITTM?
Let $A$ denote a particular (fixed) algorithm to encode ordinals as real numbers. The exact technical description of $A$ is irrelevant for this question: it can be any algorithm that is mathematically ...
- 959
27
votes
5
answers
3k
views
Formalizations of the idea that something is a function of something else?
I'll state my questions upfront and attempt to motivate/explain them afterwards.
Q1: Is there a direct way of expressing the relation "$y$ is a function of $x$" inside set theory?
More ...
- 5,343
8
votes
1
answer
403
views
Can ETCC/ETCS talk about 'size issues'?
In material set theories (like ZFC), one can prove that there is no set of all sets. Can one prove a similar statement in ETCS? This exact statement "there is no set x such that y in x for every set y"...
- 81
10
votes
2
answers
2k
views
What exactly is a judgement?
Before formulating my question, let me briefly sum up what I know about the topic (feel free to correct me if something I claimed is false!). This is for you good to see what my state of knowledge is, ...
user99916
4
votes
1
answer
401
views
What do we call this quantifier ("binder")?
There's a quantifier ("binder", whatever), call it $\alpha$, defined as follows: $\alpha x.\tau$ is the (usually infinite) expression obtained by applying the substitution $\{x \mapsto \tau\}$ to the ...
- 3,793
10
votes
1
answer
692
views
Coherence and rewriting
In category theory there are numerous coherence theorems (https://ncatlab.org/nlab/show/coherence+theorem). One example is the Mac Lane's coherence theorem for monoidal categories. This and probably ...
- 2,312
3
votes
1
answer
1k
views
How to get $\omega$-regular expression from buchi automaton
Is there an algorithm or a trick on how to get $\omega$-regular expressions from Buchi automatons? If yes, is there also some way to do create minimal such regular expressions?
It is extremely ...
- 33
0
votes
0
answers
197
views
Is the positive existential theory undecidable?
Could you tell if the positive existential theory of $\mathbb{C}[e^{\mu x} \mid \mu \in \mathbb{C}]$ is undecidable in the language $\{+, \cdot , \frac{d}{dx} , 0, 1, e^x\}$ ?
How can we prove the (...
- 309
6
votes
1
answer
485
views
Show that the positive existential theory is undecidable
To show that the positive existential theory of $\mathbb{C}[t, e^{\lambda t} \mid \lambda \in \mathbb{C}]$ in the language $\{+, \cdot , ' , 0 , 1, t\}$ is undecidable we have to prove the following: $...
- 309
2
votes
0
answers
47
views
Relation between indexed languages (OI-macro or context-free tree) and scattered context languages
I'm not sure about the relation between indexed languages (generated by indexed grammars--Aho) and scattered context languages (generated by
scattered context grammars--J Hopcroft).
I think that ...
- 21
5
votes
2
answers
266
views
Formal languages with non-unique interpretations of terms
In mathematical logic and model theory, one considers interpretations of syntactic expressions: terms without free variables are interpreted as elements of some structure, formulas without free ...
- 1,481
9
votes
1
answer
443
views
Is there a name for infinite words containing every finite words?
Apparently, the closest thing I've found would be normal number http://mathworld.wolfram.com/NormalNumber.html
But requiring that every finite words occurs is weaker than this property. So I'm ...
- 93
1
vote
0
answers
66
views
Is it possible to classify all the inequivalent classes of first order sentence with quantifier rank fixed
It is known that for symbols with finite many relations, the number of inequivalent class of first order sentence with quantifier rank $m$ is finite. But is it possible to list (classify) them? At ...
- 11
5
votes
1
answer
592
views
Expressive power of first-order category theory
Given the signature $\lbrace \mathsf{dom}, \mathsf{cod}, \mathsf{id},\circ \rbrace$ and the axioms of category theory – which are expressible in the signature's first-order (FO) language – ...
- 9,720
1
vote
1
answer
772
views
Is there any danger far from home? (Edited & Revised Version) [closed]
The notion of formal proof is defined by finite sequences ($<\omega$ - sequences) of sentences. In some sense if a sentence $\sigma$ is (finitely) provable from the theory $T$ it is very "near" to ...
user42090
1
vote
3
answers
301
views
Is there an recursively axiomatized system with infinitely many proofs for some propositions or a proposition [closed]
Is there any recursively axiomized system with infinitely many proofs for some propositions or a proposition? So we will have at least one proposition which is deduced from the recursively axiomatic ...
- 3,084
0
votes
1
answer
187
views
Can decidability results for monadic second-order logic be extended to monadic higher-order logics?
Call a higher-order logic fully monadic if and only if all of its predicate constants (at any order) and higher-order variables (at any order) are monadic (and it has no function symbols). In /...
- 1
4
votes
1
answer
2k
views
Deciding equivalence of regular languages
Given two regular expressions $R$ and $S$ on an alphabet $\Sigma$ it is possible to decide their equivalence as follows:
build two finite automata $M_R$ and $M_S$ such that $L(R) = L(M_R)$ and $L(S) =...
- 105
23
votes
1
answer
3k
views
What's the difference between ZFC+Grothendieck, ZFC+inaccessible cardinals and Tarski-Grothendieck set theory?
Say that "U" is the axiom that "For each set x, there exists a Grothendieck universe U such that x $\in$ U", where Grothendieck universes are defined in the usual way (or, if that'...
- 4,897
2
votes
2
answers
745
views
All properties of a mathematical object
This is primarily a question about related literature. I am looking for specific references, or terminology that I can use to search for references.
Let A a well defined mathematical structure of ...
- 313
1
vote
2
answers
480
views
Satisfiability problem for FOL[<,R]
Let FOL[<,R] be the fragment of first-order logic enriched with two relational symbols < and R and the first-order axioms that say:
< is a strict partial order and R is an irreflexive and ...
- 105
4
votes
3
answers
459
views
Existential quantification over regular predicates
A regular language over an alphabet $\Sigma$ is a subset of the set of all words over $\Sigma$ that can be accepted by some finite automaton. A regular language identifies a certain property of ...
- 105
1
vote
2
answers
2k
views
Translate a buchi automaton to LTL
How can I translate a Büchi automaton A to LTL(linear temporal logic) if $L(A)$ is definable in the LTL?
MY idea is : Büchi automaton $A$ ===> QPTL ===> LTL
I know that given any Buchi ...
- 73
4
votes
2
answers
2k
views
Are context-free languages with context-free complements necessarily deterministic context-free?
Let $L \subseteq A^\star$ be a formal language over $A$ generated by a context-free grammar, and $L' = A^\star - L$ be the relative complement in $A^\star$.
If $L$ and $L'$ are both context-free, are ...
- 387
3
votes
1
answer
528
views
Study of free monoids of the recursive S. Eilenberg.
Compared to the usual treatises on recursion (eg, Rogers H. "Computability and Undecidability." McGraw-Hill, New York) the book of Samuel Eilenberg & Calvin C. Elgot "Recursiveness" treats such ...
- 4,165
3
votes
1
answer
411
views
density of formal language？
let $\sum_0^n l_i x^i$ and $\sum_0^n 2^i x^i$ be generating function of L a given language and the closure over alphabet $\Sigma= \{0,1 \}$ when $n\to\infty$.
let$$D=\frac{\sum_0^n l_i }{\sum_0^n 2^...
- 3,084
0
votes
1
answer
280
views
What is the conditional probability or probablity of classes of languages?
What is the conditional probability or probability of classes of languages?
Let $E,C,S,F,R $ be the class of computably enumerable languages,computable languagesl,context-sensitive anguages,context-...
- 3,084
2
votes
4
answers
1k
views
Are inference laws consistent?
Please forgive me if this question sounds too naive... Well, in mathematics a formal theory consists of a collection of axioms $T$ (such as Peano arithmetics, or Group Theory, or ZFC), which ...
- 23.3k
12
votes
3
answers
877
views
Complementation of $\omega$-regular languages in reverse mathematics
Does anyone know where Büchi's theorem that $\omega$-regular languages are closed under complementation fits into the reverse-mathematics classification scheme? That is, is it equivalent over $\...
- 866
12
votes
5
answers
1k
views
Predicates of infinite arity
Infinitary logic considers languages being infinite by infinite conjunctions and disjunctions.
I wonder why it not considers languages being infinite by relations and functions of infinite arity.
...
- 9,720
1
vote
3
answers
576
views
Graph properties: definability and decidability
[This is a side question to Supervenience in mathematics.]
There are graph properties that are not FO-definable, but MSO-, TC-, or LFP-definable. There may be other graph properties that are not MSO-,...
- 9,720
4
votes
2
answers
1k
views
Semantics of Higher-Order Logics
I've been trying to get to grips with the various semantics commonly discussed in formal logic. Specifically, the nature and role of interpretations of first and higher-order logics is slightly ...
- 820
4
votes
0
answers
306
views
To what extent MSO = WS1S, when adding relations?
Let me first clarify my definitions. For a word $w \in \Sigma^*$, with $\Sigma=\{a_1, \ldots, a_n\}$, I define two structures:
$${\mathbb{N}}(w) = \langle {\mathbb{N}}, <, Q_{a_1}, \ldots, Q_{a_n} ...
- 786
10
votes
3
answers
1k
views
Is there a formal notion of what we do when we 'Let X be ...'?
This is likely an elementary question to logicians or theoretical computer scientists, but I'm less than adequately informed on either topic and don't know where to find the answer. Please excuse the ...
- 1,376
6
votes
3
answers
1k
views
Proof formalization
I read some time ago some papers about proof formalization. Typically, I began whith this one, from Lamport.
Are there more recent works in this field ?
3
votes
2
answers
989
views
Theory interpreted in non-set domain of discourse may be consistent?
Following the blow. I will try to ask question in order to check if I well understand what was pointed. I decide to ask another question, because mathoverflow is not projected to be good environment ...
- 1,626
8
votes
3
answers
739
views
What assumptions and methodology do metaproofs of logic theorems use and employ?
In logic modules, theorems like Soundness and completeness of first order logic are proved. Later, Godel's incompleteness theorem is proved. May I ask what are assumed at the metalevel to prove such ...
user2529