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

1
vote
1answer
46 views

Recursive definitions in formal logic

A binary tree $T$ is either A single vertex, or A graph formed by taking two binary trees, adding a vertex, and adding an edge directed from the new vertex to the root of each binary tree. Suppose ...
1
vote
1answer
63 views

Is there a definition of the existential quantifier which does not imply the axiom of choice?

The definition of the existential quantifer given in Bourbaki's Theory of Sets is $$(\exists x)R \iff (\tau_x(R)\mid x)R.$$ Here $x$ is a letter, $R$ is a relation, and $(\tau_x(R)\mid x)R$ means ...
0
votes
2answers
66 views

How can Godel's theorem apply to every formal system?

How can Godel's theorem apply to any formal system of logic, if the truth of the theorem itself is only relative to the axioms and rule of inference that were used to generate it. In other words ...
1
vote
2answers
83 views

Analysis and formal proofs.

Ever since I started learning formal logic I've had these kind of doubts: Is analysis ever studied in a completely axiomatic/formal proofy way? What I mean is, given a set of axioms and inference ...
1
vote
2answers
37 views

Peano Arithmetic: How would this formalized statement be correct?

Using Peano Axioms I have formalized the following: x is the square of an odd prime number For some odd prime number x' , x is its square IF x is some odd prime number, THEN x is the square of x' IF ...
0
votes
0answers
33 views

Do we use Z specification language these days?

I am studying organization and properties of CAM (Content Addressable Memory) of a network switch. While searching for applications of Z, I found that there are several formalization projects ...
2
votes
0answers
40 views

Connection between Algebraic structures and Formal Systems

I am a college student with very little mathematics background (up to Calculus 152 at Rutgers University), but have become increasingly interested in computing and mathematics in the last year. I am ...
1
vote
2answers
95 views

Can there exist a definition of 'multiplication' in Presberger Arithmetic?

According to Wikipedia, Presberger Arithmetic is the first-order theory of the natural numbers with addition. It can be proved to be consistent, complete, and decidable. Though it contains no axioms ...
1
vote
1answer
50 views

What's wrong with this proof that ZFC is consistent

If we take ZFC minus all it's axioms, we can easily prove that ZFC's first axiom is independent (because all statements are independent in a formal system without any axioms). We can then prove that ...
1
vote
1answer
29 views

Will assuming an undecidable statement result in a consistent system?

If you assume that an undecidable statement in a consistent axiomatic system is true (or false), will that new system also be consistent? For example, does $\mathsf{ZF}$ being consistent imply that ...
0
votes
3answers
89 views

Rational numbers and leibniz law

Leibniz law says $a = b \implies f(a) = f(b)$. Unfortunately this law seems to fail for rational numbers e.g. ${1 \over 2} = {2 \over 4}$ but $numerator({1 \over 2}) \neq numerator({2 \over 4})$. I ...
0
votes
1answer
58 views

Order of Parentheses is Irrelevant: Metatheorem?

Here was shown by induction that the order of parentheses is irrelevant when associativity is verified. Question: Would this be a metatheorem about the formal language (say, of ZF) where the ...
0
votes
1answer
40 views

Is there a formal system which is generally accepted, and how is it called?

I read the question at Gödel's Incompleteness Theorem -- meta-reasoning "loophole"? about Gödel's incompleteness theorem. My question is little about the contents of that other ...
3
votes
2answers
75 views

Proving the rules of a complicated game are well defined

What strategy could one use to formally model a game and prove that the rules do not lead to any self contradiction? A major example that comes to mind is Magic the Gathering. The card ...
0
votes
0answers
12 views

Logical systems and formal proof

Is there any good book dealing with various formal systems and a book for formal proofs. Or atleast some good notes. This page on wikipedia also says: 'This article needs attention from an expert in ...
3
votes
0answers
79 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
54 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
49 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
64 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 ...
2
votes
1answer
165 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
50 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
193 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
247 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
127 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
76 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
151 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 ? ...
4
votes
0answers
130 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
345 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
418 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 ...
0
votes
2answers
227 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. ...
4
votes
1answer
200 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
54 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
3answers
111 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
112 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
48 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
154 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
51 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
93 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 ...
5
votes
2answers
270 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
127 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
59 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
60 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
168 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
280 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
69 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
129 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
64 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
365 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
101 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
131 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 ...