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)

1
vote
2answers
47 views

What is a gross-looking formal axiomatic proof for a relatively simple proposition?

I'm looking for long and hard to follow derivations or symbolic proofs to motivate how tedious it is to actually reason within a formal system. I'm hoping there is an image of the proof, with few if ...
5
votes
1answer
821 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 ...
4
votes
1answer
235 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 ...
1
vote
1answer
71 views

Show that a given formula is not provable without the associative rule

This question is from Shoenfield's "Mathematical Logic", an exercise on page 25. Show that the formula $((x \neq x) \vee \neg(x \neq x \vee x \neq x)) \vee (x \neq x \vee x \neq x)$ is a theorem, ...
1
vote
1answer
91 views

Can Left Conjunction Elimination Get Proven in M in Less Than 30 lines?

Peter Smith writes in his Types of Proof System: "How do you get from: $\lnot$(P -> $\lnot$ Q) to the desired conclusion P? It can be done, but as far as I know it takes well over fifty lines (if done ...
1
vote
1answer
152 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
1answer
66 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 element $...
0
votes
1answer
368 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 ...
10
votes
0answers
209 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 ...
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
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
229 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 ...
3
votes
0answers
90 views

Formal proof of $\exists x (\exists y P(y) \rightarrow P(x))$ and $(\forall x \exists y R(x,y))\rightarrow (\forall y \exists x R(y,x))$

within the following axiomatic system I've beeb trying to proof the formulas (1) $\forall x \exists y R(x,y) \rightarrow \forall y \exists x R(y,x) \\$ and (2) $\\ \exists x (\exists y P(y) \...
3
votes
0answers
112 views

What is the root of first class object in programming languages?

What is the root of "first class object" of programming languages? (Also see https://en.wikipedia.org/wiki/First-class_function, and https://stackoverflow.com/questions/245192/what-are-first-class-...
3
votes
0answers
184 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 ...
3
votes
0answers
64 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?
2
votes
0answers
49 views

Weird analogy between quadratic forms and formal systems

A fundamental connection between provability and consistency for formal systems is that, if $Q$ is a formal system and $A$ is a sentence in the language of $S$, then $Q$ proves $A$ if and only if $...
2
votes
0answers
54 views

Why is \mathsf{} used for formal systems?

A lot of times I have seen well-respected members of this community edit posts (including mine) changing things like "ZFC" into "$\mathsf{ZFC}$". It kind of makes sense, because formal systems like ...
2
votes
0answers
67 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" ...
2
votes
0answers
456 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: $$ \sum_{...
1
vote
0answers
19 views

Intro to Metamathematics Kleene $\S54$ Lemma IId

In this section, Kleene builds a formal system for primitive recursive functions. The beginning of the proof for lemma IId is skipped because it comes for general properties, but I must be missing ...
1
vote
0answers
32 views

Is there correspondence between vector spaces and independent theories?

I'm not a mathematician, but I have this idea. A vector space is defined by a basis, that is a set of linearly independent vectors. On the other hand, an independent theory is defined by a set of ...
1
vote
0answers
59 views

On the notion of semantic completeness

I have some doubts regarding this concept. DEF1: Given a formal language L, an interpretation of L is a mechanism that allow the ascription of a truth value to every sentence of L. If E is a set of ...
1
vote
0answers
41 views

What is the easiest way to show that a type theory is consistent?

I'm working on presenting an extension of MLTT which uses a (from what I can tell) novel conception of type universes which I believe is not equivalent to the standard Russell/Tarski-style approaches. ...
1
vote
0answers
50 views

Kolmogorov complexity measure of a formal system

Each formal system can be encoded in a binary string. For instance, you can use the input string that a pre-specified Turing machine needs in order to enumerate all the theorems in a theory in the ...
1
vote
0answers
27 views

Formal verification of function contract?

How could I formally reason about the following function: function f(x){ if(x>=0){ return 1; }else{ return 0; } return 2; } ...
1
vote
0answers
79 views

Is there a formal class theory that suffices to formalize the basic notions of category theory?

Is there a formal class theory that suffices to formalize the basic notions of category theory? I think the usual formalizations of class theory like Neumann-Bernays-Gödel or Morse-Kelley don't ...
1
vote
0answers
36 views

How Does the Number of Lines of a Proof Change If Expanding a Condensed Detachment Proof into a Simultaneous Substitution and Detachment Proof?

For every condensed detachment proof, there exists a substitution and detachment proof. If both the antecedent of the major premise, e. g. one having form C$\alpha$$\beta$ or (p $\rightarrow$ q) ...
1
vote
0answers
23 views

Can I effeciently check whether the inverse of a semantic function exists?

I'm relatively new to the fields of formal semantics/systems/languages or even model theory and therefore I miss some knowledge and experience. I try to boil the question down to the core essence of ...
1
vote
0answers
35 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 ...
1
vote
0answers
200 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 ...
1
vote
0answers
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 ...
0
votes
0answers
34 views

What happens when we introduce a third 'paradox' possibility to the Halting Machine?

Thanks to Turing, we know that it is impossible to construct a machine that can prove for all machines whether they halt or not. This then has mayor implications on many other fields and theorems, ...
0
votes
0answers
57 views

Creating a formal system which corresponds to multiplication (of natural numbers)

I've begun studying mathematical logic with Hodel's 'An Introduction to Mathematical Logic', and have just learnt about formal systems and their components. In the textbook, Hodel gives as an example ...
0
votes
0answers
52 views

Is there a standard notion of a “theory of Turing machines”?

Of course, there are more-or-less standard definitions of Turing machines as a certain type of mathematical object formalized in some theory (Say, ZFC), but what I am looking for is a first order ...
0
votes
0answers
35 views

Efficiently Verifying “identities” in Arithmetic

So suppose I have two expressions $A,B$ both consisting of some combination of parenthesis $()$, addition $+$, multiplication $\times$, exponentiation $ \text{^}$. What is an efficient way to check ...
0
votes
0answers
64 views

Can there be true but unprovable statements about object other than numbers?

In ZFC, everything is a pure set, and because the necessary amount of arithmetic for the Gödel's incompleteness theorems to go through is interpretable within ZFC, there are undecidable statements ...
0
votes
0answers
28 views

Simplest way to say “$\varphi$ is a wff of formal system $\mathbf{F}$”?

What is the simplest way to say "$\varphi$ is a well-formed formula of formal system $\mathbf{F}$" in symbols? The only thing that comes to mind is: $$\varphi \in \mathbf{F}$$ Am I right? I.e., ...
0
votes
0answers
15 views

Metamathematic: Cover the case if X=Y

I want to formalize: "If X is less than Y, Then U is equal to Y ", and have been told that $$ \bf [\forall V \sim X=(Y+V)]U=Y $$ does not cover the case X=Y. Therefore I have rewritten it as $$ \bf [\...
0
votes
0answers
65 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?