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
27
votes
9answers
3k views

Is formal truth in mathematical logic a generalization of everyday, intuitive truth?

I'm trying to wrap my head around the relationship between truth in formal logic, as the value a formal expression can take on, as opposed to commonplace notions of truth. Personal background: When I ...
14
votes
1answer
4k 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 ...
14
votes
1answer
2k views

The Power of Lambda Calculi

A simple question here, which likely demands a somewhat complex answer... Or rather, a set of related questions. What are the advantages of typed lambda calculus over untyped lambda calculus in terms ...
13
votes
4answers
21k views

What makes a context free grammar ambiguous?

What makes a context free grammar ambiguous?
13
votes
1answer
712 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....
11
votes
1answer
897 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 ...
10
votes
0answers
210 views

Is it possible to formalize all mathematics in terms of ordinals only?

Our experience shows that all finitary mathematical objects could be encoded using the natural numbers, and all operations on those objects could be expressed in terms of a few basic operations on ...
9
votes
3answers
2k views

Why is establishing absolute consistency of ZFC impossible?

Why is establishing the absolute consistency of ZFC impossible? What are the fundamental limitations that prohibit us with coming up with a proof? EDIT: This post seems to make the most sense. In ...
9
votes
5answers
2k views

Resources for learning formal math?

I'd like to learn formal math. Preferably, though not necessarily, starting with predicate logic/first order logic rather than higher order logic. I am trying to find resources (papers, books etc.) ...
9
votes
2answers
231 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" $...
9
votes
3answers
540 views

How do you go about formalizing a concept?

I am reading Godel Escher Bach. 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 represents ...
8
votes
4answers
403 views

Calculus of Natural Deduction That Works for Empty Structures

Currently, I am dealing with the calculus of natural deduction by Gentzen. This calculus gives us rules to manipulate so-called sequents. Definition. If $\Gamma$ is a set of formulas and $\phi$ a ...
8
votes
2answers
696 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 ...
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\}...
7
votes
2answers
382 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,...
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 ...
6
votes
2answers
934 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) ...
6
votes
1answer
169 views

Can one-element set be considered equal to its element?

Are there "interesting" (that is non-trivial, for example not containing only one set) set theories with one element set being equal to their element ($\{x\}=x$ for every $x$)? This question arose ...
6
votes
2answers
740 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 ...
6
votes
2answers
136 views

Formal systems in which $\forall x \in \mathbb{R}(x \neq 0 \rightarrow x^{-1} \neq 0)$ is true, but the contrapositive is disallowed.

Question. Are there any formal systems out there for which $$\forall x \in \mathbb{R}(x \neq 0 \rightarrow x^{-1} \neq 0)$$ is true, but the contrapositive $$\forall x \in \mathbb{R}(x^{-1} =...
6
votes
1answer
824 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
0answers
107 views

Does introducing a new type create a different extension, and is it still conservative?

In this comment on Terry Tao's page about his Analysis I textbook, he writes, If one wanted to do things by the book, what one should actually do each time one introduces a new mathematical object, ...
5
votes
5answers
340 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 ...
5
votes
3answers
568 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
5answers
784 views

Can a polynomial size CFG over large alphabet describe a language, where each terminal appears even number of times?

Can a CFG over large alphabet describe a language, where each terminal appears even number of times? If yes, would the Chomsky Normal Form be polynomial in |Σ| ? EDIT: What about a language where ...
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 ...
5
votes
3answers
150 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 ...
5
votes
3answers
792 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 ...
5
votes
2answers
554 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 ...
5
votes
2answers
497 views

Are there logics without modus ponens?

The question doesn't go beyond the title. And I don't mean logics that merely just don't have it as a primitive rule - I'm interested in logic where you can't actually use it. I've searched around ...
5
votes
1answer
653 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 ...
5
votes
1answer
158 views

Every Turing machine corresponds to a formal system

Solomon Feferman, at page 138 of his 2006 paper "Are there absolutely unsolvable problems" says that each formal system of axioms can be made to correspond to a suitably designed Turing machine so ...
5
votes
1answer
144 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 ...
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 ...
5
votes
0answers
117 views

Which formal system (aka platform) is the best for selfstudying Category Theory?

I was planning to learn category theory with coq's aid and its category theory implementation, but a stackoverflow user told me in the comments (of other question) that it may be too difficult. So, ...
5
votes
0answers
234 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 ...
4
votes
2answers
864 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 ...
4
votes
3answers
228 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 ...
4
votes
1answer
74 views

How it makes sense to talk about consistency of theories?

So I was reading this post Probability axioms (Kolmogorov) and so in the answer there was said that it doesn't make sense to talk about consistency of probability axioms because it is not a formal ...
4
votes
1answer
214 views

Why can't we keep adding axioms forever?

Let F be a formal system falling prey to Gödel's incompleteness theorems, implyng there is a true but unprovable statement, call it $G_1$. Of course, adding $G_1$ to the axioms of F doesn't solve the ...
4
votes
1answer
1k 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$ are ...
4
votes
1answer
66 views

Codification of a formal language in set theory.

Starting with an arbitrary class of sets $\Gamma$, can you generate a free semigroup $\Gamma^*$ over $\Gamma$ with the group operation of concatenation ($\frown$)? The goal here is to codify a formal ...
4
votes
6answers
402 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
1answer
307 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 (well-...
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$
4
votes
1answer
160 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 ...
4
votes
1answer
199 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
266 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 ...
4
votes
1answer
240 views

The monadic second order theory with $<$ and Presburger arithmetic

Consider the monadic second order logic over the natural numbers with $<$ as a predicate, i.e. the second order logic over $(\mathbb N, 1, <)$, where we can quantify over sets and individual ...
3
votes
4answers
1k views

natural deduction: introduction of universal quantifier and elimination of existential quantifier explained

Currently, I am dealing with the calculus of natural deduction by Gentzen. This calculus gives us rules to manipulate so-called sequents. Definition. If $\phi_1,\dots, \phi_n,\phi$ are formulas, then ...