The Stack Overflow podcast is back! Listen to an interview with our new CEO.

Questions tagged [formal-systems]

A formal system is broadly defined as any well-defined system of abstract thought based on the model of mathematics. (Def: http://en.m.wikipedia.org/wiki/Formal_system)

Filter by
Sorted by
Tagged with
1
vote
1answer
95 views

In a string rewriting system, does rewriting consume the string?

In string rewriting system, does rewriting 'consume' the string? For instance, suppose $101$ is written down and there's a rule $1x1 \rightarrow 11x11,$ we can apply this rule to write down $11011,$ ...
8
votes
2answers
721 views

How do we derive new inference rules?

I've been toying with a system of inference rules for propositional logic. I can use the system to prove theorems; but my question is, can I use the system to obtain new inference rules? Here are the ...
1
vote
0answers
206 views

A question about the analogy between formal systems and Turing machines

It is well known the analogy between formal systems and Turing machines. If I am not wrong, you can code any formal system of language L in first order logic into a Turing machine, and there is a ...
5
votes
2answers
155 views

Would it be possible to concoct a “harmful” axiom?

Suppose I run an automated theorem prover. It begins with the axioms of ZFC, and using a random number generator, it proves more theorems, and it runs for two days. At the end of the second day, it ...
12
votes
1answer
917 views

Understanding the syntactical completeness

A formal system is syntactically complete if for each sentence (closed formula) $\varphi$ either $\varphi$ or $\lnot \varphi$ is provable. A formal system is semantically complete if every ...
4
votes
3answers
232 views

Are PA and ZFC examples of logical systems?

Wikipedia says A logical system or, for short, logic, is a formal system together with a form of semantics, usually in the form of model-theoretic interpretation, which assigns truth values to ...
7
votes
2answers
391 views

Symbols and terminology for distinguishing derivability from sequents

First some definitions to make it clear what I'm talking about: A deductive system is a set $J$ of judgments together with a set $R$ of inference rules each of the form $$ j_0 \leftarrow j_1, j_2,...
13
votes
1answer
734 views

Some different versions of completeness of a formal system, of a logic and of a theory

I have seen people talking about Gödel's complete theorems and Gödel's incomplete theorems on math.SE. I am curious what they are really about, so I try to understand the meaning of completeness first....
5
votes
3answers
574 views

Aftermath of the incompletness theorem proof

This is somewhat of a minor point about the incompletness theorem, but I'm always a little unsure: So one proves that there is a formula which is unprovable in the theory of consideration. Okay, at ...
5
votes
3answers
803 views

Why can't we use memoization to parse unambiguous context-free grammars in linear time?

This is a follow-up question to Why is it hard to parse unambiguous context-free grammar in linear time? I know that Parsing Expression Grammars (PEG) can be parsed in linear time using a packrat ...
1
vote
1answer
96 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 ...
3
votes
1answer
560 views

Definition and meaning of “Proof Schema”, “Class Sign”

I'm a newbie in advanced mathematics, and I'm trying to understand Godel's theorem. I came across these two words which I couldn't understand clearly. "Proof Schema" and "Class-Sign" Can anybody ...
2
votes
2answers
834 views

Why is it hard to parse unambiguous context-free grammar in linear time?

From this question, I gather that whether unambiguous CF grammar can be parsed in linear time is an open problem. I'd like to know what the major roadblocks to achieve this are. That is, what made the ...
5
votes
2answers
1k views

Determining if a grammar can be converted to LL(1)/LL(k)

(This is a cross-post of https://cstheory.stackexchange.com/questions/11676/determining-if-a-grammar-can-be-converted-to-ll1-llk in the hopes of gaining a wider audience.) I'd like to know if there ...
1
vote
1answer
769 views

Differences between the formal grammar, formation rules and automaton for a formal language

Added: A formal grammar is a set of formation rules for strings in a formal language. Formation rules are rules for describing which strings of symbols formed from the alphabet of a formal language ...
2
votes
0answers
466 views

Summation notation and a negative sign of some elements

Having sequence like $$ \beta_1 \cos\theta_1 + \beta_2 \cos\theta_2 + \beta_3 \cos\theta_3 + \dots + \beta_n \cos\theta_n$$ it is possible to present it using summation notation as follows: $$ \sum_{...
1
vote
1answer
197 views

How it is possible that sound system is inconsistent

We have some sound deduction system (every provable sentence is true), which has property of principle of explosion and some theory T described in that system. Lets assume that theory T is ...
6
votes
2answers
948 views

How it is posible that $\omega$-inconsistency does not lead to inconsistency

After wikipedia: Theory is $\omega$-inconsistent if, for some property P of natural numbers, T proves P(0), P(1), P(2), and so on (that is, for every standard natural number n, T proves that P(n) ...
5
votes
1answer
664 views

What are metatheory, metalanguage and meta-…

I have been reading the Wiki articles for metatheory and metalanguage, but not sure if I have understood what they are about. Some accessible examples may help clarify a bit, I guess. Do metatheory ...
0
votes
2answers
228 views

Does a formal system having inference rules imply that it is a logic system?

From Wikipedia Formal systems in mathematics consist of the following elements: A finite set of symbols (i.e. the alphabet), that can be used for constructing formulas (i.e. finite ...
3
votes
1answer
156 views

What is the minimal axiomatization of a set of structures?

I wonder what the minimal axiomatization of a set of structures mean? I came across this term from Wikipedia: For a theory $T\in A,$ let $F(T)$ be the set of all structures that satisfy the ...
0
votes
1answer
41 views

Are interpretation and formalization inverse to each other?

I am not sure if I understand this correctly. Please correct me. In a formal system, an interpretation is a mapping from its formal language to one of its structures ie models. an ...
6
votes
1answer
829 views

Understanding definition of conservative extension of a theory

From Wikipedia In mathematical logic, a logical theory $T_2$ is a (proof theoretic) conservative extension of a theory $T_1$ if the language of $T_2$ extends the language of $T_1$; every ...
6
votes
4answers
3k views

Hofstadter's TNT: b is a power of 2 - is my formula doing what it is supposed to?

If you've read Hofstadter's Gödel, Escher, Bach, you must have come across the problem of expressing 'b is a power of 2' in Typographical Number Theory. An alternative way to say this is that every ...
3
votes
1answer
129 views

Axiom and concept

Is there a concept called "concept" defined in a formal system? Can concepts always be treated as axioms? Can axioms always be used to define concepts? For example, in ZFC set theory, I think the ...
4
votes
2answers
888 views

How does a recursive definition fit into a formal proof?

I understand a proof as a series of statements that are either axioms or follow from previous statements by a small set of rules of inference. I understand a recursive definition to be something like ...
1
vote
0answers
77 views

Differential fields and rings

If one is to compute the derivative of $$ y=3x+2 $$ by $$ \frac{\mathrm{d}(3x+2)}{\mathrm{d} x} $$ Would I be working with differential fields? Since differential fields is a first-order ...
4
votes
1answer
163 views

Computing square roots and calculus

If one were to verify that $$ \sqrt{2} < 3 $$ would the underlying formalisation require a logic more expressive than first-order? Or, is FOL sufficient since real numbers can be formalised in ...
1
vote
1answer
310 views

Expressing P = NP as a first order formula

I want to express P = NP in a completely formal way. My first try: There exists an algorithm A and a polynomial bound p such that for all input i, A(i) = true iff i is a satisfiable formula and the ...
5
votes
5answers
342 views

Periodic sequences on finite alphabet

Let $\Sigma=\{A,B,C\}$ be an alphabet, and let $\Sigma^{\mathbb{N}}$ be the set of infinite sequences on $\Sigma$ (ie $ABCBCCCBABC...$). By outside conditions, I have several subsequences that are ...
1
vote
1answer
114 views

Understanding recursion in λ calculus

In recursion for λ calculus, I was wondering why the following two are equal (λx.g (x x)) (λx.g (x x)) g ((λx.g (x x)) (λx.g (x x))) How shall I understand g ((λx.g (x x)) (λx.g (x x)))? I ...
0
votes
1answer
251 views

The way that a regular expression describes a regular language

A formal language is a set of words in some alphabet. It may be defined as being generated by a formal grammar or as being recognized by an automaton. For a regular language, it can also be described ...
2
votes
2answers
459 views

Can a formal language always be generated by a formal grammar?

A formal language is often defined by means of a formal grammar. I wonder for a formal language if there is always a formal grammar that generates the language? Does this answer have something to do ...
0
votes
3answers
215 views

Is a regular expression a string or a set of strings?

Quoted from Introduction to the Theory of Computation by Sipser, a regular expression is defined as: Say that R is a regular expression if R is a for some a in the alphabet $\Sigma$, $\...
2
votes
2answers
199 views

Accessible formal specification and explanation of First Order Logic?

I am trying to get good at proofs by working through How To Prove It. Unfortunately I am very bothered by the fact that I do not understand all the formalities in First Order Logic + set theory (FOL+...
1
vote
1answer
268 views

What formal mathematical models exist for digital hardware?

What formal mathematical models exist for digital hardware? I am familiar with several non-formal models that are used as the basis of several hardware description language simulators and ...
1
vote
1answer
101 views

How to show that a set does not contain a specific string

If I have a set $S$ defined as the smallest set $S$ over an alphabet $A=\left\{ \star, \urcorner,(,), a_0,a_1, \dots \right\}$ ( $S\subseteq \cup_{k \in \mathbb{N}} A^k$) satisfying: $\bullet \ a_0, ...
2
votes
2answers
176 views

Informal Equivalents of Mathematica “Set” and “SetDelayed”

How would one distinguish between what is meant by Mathematica's "Set" and "SetDelayed" functions in informal mathematical notation? Is there a way to make this distinction any any reasonably standard ...
2
votes
1answer
1k views

Generating all words in a language from CFG

I have a non-ambiguous context-free grammar. Is there some standard algorithm to create list of all the words in the language the CFG defines? This can be done with an abvious brute-force search by ...
0
votes
2answers
175 views

Formal language problem

I’m new to formal language and searching for the solution for the following task: $\Sigma$ is an alphabet with $\lvert \Sigma\rvert = 5$ and $k \in \mathbb{N}_0$. I’m searching for $\lvert \Sigma^k\...
0
votes
3answers
208 views

Formal language problem

Hello I´m new to formal language and searching the solution for the following task: Language: $L = \{0^{2i+1}|i\in\mathbb{N}_0\}$ Alphabet: $\Sigma = \{0\}$ I'm searching the resultion (sic) for: $\...
2
votes
2answers
337 views

Recognizing language using Turing machine

Given integers $a, b, c$ construct a single-tape Turing machine recognizing the language $\{w \in \{0,1\}^{*}: a*\#_{0}w+b*\#_{1}w+c=0\}$ in time $O(n*logn)$, where $n=|w|$. $\#_{x}w$ denotes the ...
2
votes
1answer
609 views

Detecting cycles in off-line Turing machines

Let $M$ be an off-line Turing machine over the input alphabet $\{0,1\}^{*}$, that uses only one working tape in addition to the input tape. Construct a Turing machine $M'$, such that: $L(M) = L(M&...
8
votes
1answer
408 views

is this language context free? [closed]

I need an NPDA for the following language if it is context-free, and if it isn't I need a proof using the pumping lemma that it is not a CFL: $$L_1=\{w_1w_2 \in \{a,b\}^* : |w_1| = |w_2|,w_1\neq w_2\}...
4
votes
1answer
201 views

Help understand $\text{handle}$ in parsing problem

The BNF is defined as followed: S -> aAb | bBA A -> ab | aAB B -> bB | b The sentence is: aaAbBb And this is the ...
4
votes
1answer
144 views

Do there exists permutations $\pi_1,\pi_2$ and polynomial size CFG that describe the finite language $\{w \pi_1(w) \pi_2(w)\}$ over alphabet {0,1}?

Do there exists permutations $\pi_1,\pi_2$ and polynomial size CFG that describe the finite language {$w \pi_1(w) \pi_2(w)$} over alphabet {0,1}? Polynomial size in $|w|=n$
3
votes
3answers
392 views

Software/algorithm for the smallest context free grammar describing a set of words?

I am looking for software/algorithm for the smallest context free grammar describing a finite set of words (and no other words). For a single word I found sequitur Related to this seems: given a CFG ...
13
votes
4answers
21k views

What makes a context free grammar ambiguous?

What makes a context free grammar ambiguous?
15
votes
1answer
5k views

Formal System and Formal Logical System

I was reading the Wikipedia article for Mathematical_logic. When reaching Formal_logical_systems, I was curious about its definition and clicked into its own article Logical_system, which redirected ...
4
votes
1answer
268 views

Can a polynomial size CFG over large alphabet describe any of these languages:

Can a polynomial size CFG over large alphabet describe any of these languages: Each terminal appears $0$ or $2$ times Word repetition $\{www^* \mid w \in \Sigma^*\}$ (word repetition of an arbitrary ...