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)

205 questions
Filter by
Sorted by
Tagged with
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,$ ...
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 ...
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 ...
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 ...
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 ...
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 ...
391 views

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 ...
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) ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
215 views

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 ...
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 ...
175 views

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\... 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:$\...
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 ...