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)

learn more… | top users | synonyms

3
votes
1answer
39 views

Incompleteness of formal systems as opposed to completeness of a non-formal theory

I have read that Gödel's incompleteness theorem does not apply to real closed field theory. But the incompleteness theorem applies only to formal systems, that is systems whose alphabet of symbols and ...
0
votes
0answers
47 views

Strong logical system without principle of explosion

Are there some logical systems strong enough to contain theorems of first/second order Peano Arithmetic but constructed in such way that principle of explosion does not hold for them?
0
votes
1answer
32 views

Regular Expression of alternative 0's and 1's?

Let $L$ be the language of $0$'s and $1$'s in alternate positions, where $$ L = \{ \epsilon, 0, 1, 01, 10, 01010,\ldots\}. $$ Is $(0)*$ + $(1)*$ a valid regular expression that represents this ...
1
vote
1answer
79 views

Difference between Hilbert program and Russel & Whitehead's Principia Mathematica

May some one explain me what is difference between Hilbert program and Russel & Whitehead's Principia Mathematica? I know both of them wanted to reduce the mathematics into a set of axioms and ...
0
votes
1answer
46 views

prove this theorem $\vdash (\exists x_i (A\to B)\to (A\to \exists x_i B))$

Here is my thought to prove the theorem we should get $\{\exists x_i (A \to B), A\} \vdash \exists x_i B $ then, I don't know how to process...
0
votes
1answer
187 views

True or false? If $\eta$ is an explicitly defined incomputable number, then no formal system can pin down the value $\eta$ to arbitrary precision.

Let $\eta$ denote an explicitly defined incomputable real number (the bounty text is faulty, and does not mention incomputability of $\eta$). Then I think that no (recursively ennumerable) formal ...
2
votes
1answer
104 views

How can a proof by formula induction in a formal language be formalized?

From a set of not-so-rigorous lecture notes on Metalogic: Formulas of $L$: (i) Each sentence letter is a formula. (ii) If $A$ is a formula, then so is $\neg A$. (iii) If $A$ and $B$ ...
5
votes
3answers
114 views

Is there such a thing as the number of axioms?

This question was inspired by this question. Does it really make sense to say that a formal system has some number of axioms, say three, or ten, etc? E.g., take a formal system that admits ...
0
votes
2answers
59 views

Help with semi-formal logic

How do I write semi-formally 'there are only 2 objects in the universe'? My hypothesis is: ∃x∃y(x≠y) Any ideas?
4
votes
5answers
93 views

semantics(truth) vs formal system?

my first question is can we just define semantics in logic and not define a formal system ? why do we need a formal system to prove a proposition when for example we know the proposition is true ? ...
3
votes
0answers
98 views

Intuition for the choice of background (set) theory

Problem From the formalist point of view, any mathematical statement should ultimately be an assertion about the derivability of a certain formula in a certain formal system, call it the background ...
9
votes
3answers
299 views

How do you go about formalizing a concept?

I am reading Godel Escher Bach. I love it. In the first few chapters, the author shows what a formal system is and gives examples that eventually lead to a typographical formal system of strings that ...
3
votes
1answer
179 views

how to prove : there are an infinite number of points on the circle

I think the follow problem is equal to the problem set 1.16.(a) in Principles of Mathematical Analysis (walter ruldin), And we take (a, b) in $R^2$, X in $R^i$ how to prove : there are an infinite ...
1
vote
2answers
195 views

How many undecidable statements are there in ZFC?

There are several statements known to be undecidable in ZFC, with the continuum hypothesis probably being the most "popular" one. Is it known how many undecidable statements are there in ZFC? I.e. ...
0
votes
0answers
27 views

Do automatons and formal grammars belong to formal systems

A formal system consists of a formal language, a formal grammar that generates the language, a set of axioms, and a set of inference rules. Are automatons also formal systems? Is an automaton ...
4
votes
1answer
165 views

What does “calculus” mean?

"calculus" and "formal system" From http://en.wikipedia.org/wiki/Propositional_calculus#Terminology a calculus is a formal system that consists of a set of syntactic expressions ...
0
votes
1answer
44 views

theory, theorems and axioms

According to Wikipedia In mathematical logic, a theory (also called a formal theory) is a set of sentences in a formal language. Usually a deductive system is understood from context. An ...
0
votes
0answers
80 views

Meaning of abstractness and concreteness

Do abstractness and concreteness mean for formal systems and their models respectively? Do they relate to how big the theory is? For example, the theory of rings is richer than the theory of ...
0
votes
3answers
95 views

Are axioms assumed to be true in a formal system?

In a logical system, there is assignment of truth values to the sentences in the language, and axioms are assigned the true value. A logical system is a formal system. In a formal system, there is ...
4
votes
2answers
90 views

Are there formal systems that are not logical systems?

From WIkipedia 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 ...
0
votes
1answer
38 views

What do “completely described” and “complete formalisation” mean?

From Wikipedia In mathematics, an axiomatic system is any set of axioms from which some or all axioms can be used in conjunction to logically derive theorems. A mathematical theory consists of ...
0
votes
1answer
78 views

What are the differences between a collation and a rule of formation?

I'm a beginner in mathematical logic, and currently studying(myself, without any colleague, which is sad and so asking in here) basics of formal system. Before asking a question, I'll introduce my ...
2
votes
0answers
46 views

Are there any formal theories that are not axiomatic?

Are there any formal theories that are not axiomatic? Could you give me some examples?
3
votes
1answer
85 views

How do definitions work in Martin-Lof type theory?

The classical viewpoint is that we can found mathematics by specifying a formal system $F$ whose theorems are precisely those of ZFC. However, since $F$ has essentially no support for the concept of a ...
2
votes
2answers
189 views

Precisely, what is a primitive recursive definition?

If I understand correctly, the language of primitive recursive arithmetic has a distinguished function symbol $S$, together with a function symbol for each primitive recursive definition (hereafter ...
3
votes
2answers
120 views

If $T$ proves any incorrect $\forall$-rudimentary sentence, then $T$ is inconsistent

A theory $T$ in the language of arithmetic is called $\omega$-inconsistent if for some formula $F(x)$, $\exists x F(x)$ is a theorem of $T$, but so is $\neg F(n)$ for each natural number $n$. ...
1
vote
1answer
57 views

Prove the admissibility of $\Gamma, A \vdash_N B $, from $\Gamma \vdash_N B$

(This is an assignment) To prove: $$\frac{\Gamma \vdash_N B}{\Gamma, A \vdash_N B}$$ ($\Gamma, A = \Gamma \cup \{A\}$) I have what I think is a proof for this. I would like and be grateful for ...
2
votes
0answers
59 views

Certain sequents as inference rules

Fix a signature $\sigma.$ Then a coherent formula is a first-order formula built using only $\{\wedge,\vee,\top,\bot,\exists\}.$ See the link for more information. Furthermore, by a "special" ...
3
votes
2answers
131 views

Textbook on Basics of Formal Systems

Whilst trying to learn more about logic I came across Smullyan's Theory of Formal Systems on Google Books. What I liked about the book was how clearly it managed to describe (on pages 3-5 in chapter ...
2
votes
2answers
220 views

$\beta$ - conversion and $\alpha$-reduction problem in $\lambda$-calculus

Here is an expression that I am trying to reduce and my operations so far: $$((\lambda x.(x (\lambda z.zy))) (\lambda z.\lambda y. zy) )= (x (\lambda z.zy))[x \to \lambda z.\lambda y. zy ] = ...
0
votes
1answer
59 views

Is this $\beta$-reduction well defined?

Would it be possible to apply $(\lambda x.\lambda y. x)$ to the argument $y$? It seems to me that this must not be possible as it would give a different answer if applied to a constant, call it ...
3
votes
1answer
115 views

From a foundational point of view, what's a good specification language for formal systems?

Suppose you and I are writing a book that develops (classical) mathematics from scratch. In the course of writing this book, we'll need to define a variety of formal systems, like a system for ...
1
vote
1answer
60 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
325 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
87 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 ...
3
votes
2answers
125 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 ...
4
votes
1answer
280 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 ...
1
vote
3answers
120 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 ...
6
votes
2answers
229 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, ...
8
votes
1answer
221 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 ...
4
votes
3answers
389 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 ...
2
votes
3answers
334 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
69 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 ...
1
vote
1answer
197 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 ...
1
vote
2answers
395 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 ...
4
votes
2answers
818 views

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

(This is a cross-post of http://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 is ...
1
vote
1answer
401 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
284 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: $$ ...
1
vote
1answer
131 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 ...
2
votes
2answers
445 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) ...