7
votes
1answer
282 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 ...
1
vote
0answers
51 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 ...
2
votes
1answer
242 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 – ...
0
votes
1answer
656 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 ...
1
vote
3answers
264 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 ...
0
votes
1answer
115 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 ...
4
votes
1answer
490 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) ...
12
votes
1answer
848 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's unclear, in this ...
2
votes
2answers
603 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 ...
1
vote
2answers
261 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 ...
4
votes
3answers
286 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 ...
1
vote
2answers
430 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 ...
3
votes
2answers
804 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 ...
2
votes
1answer
440 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 ...
3
votes
1answer
328 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 ...
0
votes
1answer
261 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 ...
1
vote
4answers
528 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 ...
11
votes
1answer
533 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 ...
2
votes
0answers
329 views

Relations 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. ...
2
votes
3answers
398 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 ...
1
vote
2answers
698 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 ...
3
votes
0answers
275 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} ...
6
votes
1answer
832 views

Using the multiverse approach to decide the law of the exluded middle?

Recently, in response to deciding the Continuum Hypothesis $CH$, Hamkins and Gitman have proposed consider a multiverse of set-theoretic universes, some in which $CH$ is true, some in which $\neg CH$ ...
8
votes
3answers
974 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 ...
5
votes
3answers
642 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 ?
0
votes
2answers
521 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 ...
6
votes
3answers
496 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 ...
10
votes
4answers
2k views

Why do I find Category Theory mostly just a way to make simple things difficult?

I have a basic working knowledge of category thoery since I do research in programming languages and typed lambda-calculus. Indeed, I have refereed many papers in my area based on category theory. ...