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
0answers
71 views

What do the ZFC axioms look like in terms of subset?

I'm reasonably familiar with the ZFC axioms. I know they can be formalized in many different ways. However, I usually see them presented in terms of the elementary "propositional calculus primitives" ...
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
48 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
34 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
94 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
109 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
116 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
61 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
97 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
103 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
305 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
195 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
201 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
169 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
45 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
89 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
97 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
93 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
41 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
89 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 ...
3
votes
0answers
49 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
88 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
197 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
121 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
134 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
232 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
61 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 ...
4
votes
1answer
126 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
61 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
329 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
88 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
129 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
296 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 ...
2
votes
3answers
123 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
242 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
234 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
345 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
204 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
401 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
829 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
414 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
297 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 ...