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
1
vote
0answers
38 views

Is linear algebra a formal system?

By a formal system I mean a system for inferring theorems from axioms according to a set of rules. Essentially I wonder, whether a linear algebra could be viewed as some particular set of axioms from ...
0
votes
0answers
57 views

What formally means when physicists say “relativity theory is inconsistent with quantum theory”? [migrated]

I hear this sentence sometimes: "quantum theory is inconsistent with relativity theory". Is it possible interpret this really formal system like? I tried to understand "to be consistent ...
1
vote
1answer
57 views

Does a formal system that proves everything that is provable exists?

The Church thesis states that "a function is computable iff it is computable by a Turing machine." Similarly, I wonder if there exists some thesis that states that "a mathematical truth ...
1
vote
0answers
36 views

Are Real Numbers a Formal System?

I don't know a lot of mathematics but I have noticed that every branch of Mathematics has the same structure: some axioms (For example in Geometry might be Euclid's Axioms, in Probability might be ...
1
vote
2answers
40 views

Question about MU puzzle from GEB

In MU puzzle: https://en.wikipedia.org/wiki/MU_puzzle#The_puzzle, We have "MU" string and 4 rules. Now when compared this to logic the wiki article says "The MI string is akin to a single axiom, and ...
1
vote
0answers
56 views

Is there a point at which you can no longer formally define something in math?

I'll admit this is a bit of a vague question, but I'm having trouble actually formulating it. I understand definitional systems can have recursive definitions however this can turn into nonsense ...
0
votes
1answer
30 views

How weak can a formal system be that codifies most formal systems?

As I understand it, most if not all formal systems can be codified in $\mathsf{ZFC}$, because this theory is sufficiently strong that it allows us to define strings, manipulate them, and talk about ...
1
vote
0answers
40 views

What motivated people like Euclid to create such a general axiomatic systems like the one in the book Elements so early in history?

I think I understand why people wanted (and still wants of course) to prove some mathematical statements. Example of that would be proof of Pythagorean theorem. People noticed earlier than Pythagoras ...
0
votes
2answers
35 views

Are there in mathematics some non-logical axioms which are not obviously true but we accept them as true? [closed]

I have encountered some non-logical axioms (e.g., a + b = b + a) in a linear algebra (field axioms, vector space axioms). For all those non-logical axioms I have encountered, it seems to me that they ...
0
votes
1answer
107 views

Proof of *2.38 in Principia Mathematica (Russell/Whitehead) [closed]

In Bertrand Russell and Alfred Whitehead's Principia Mathematica, they note that "The proofs of *2.37.38 are exactly analogous to that of *2.36." I have found a proof of *2.37, but would like to ...
0
votes
0answers
31 views

How to axiomatize IF logic?

IF logic here refers to Hintkaa's independence - friendly logic. I heard a saying from one of my seniors that Jaakko Hintkaa's independence friendly logic seems to have no good semantics other than ...
0
votes
0answers
38 views

Help interpreting a logical formula

I encountered a formula in a paper, and i need help interpreting it: The original formula as an image, it is in the middle on page 4 of the PDF at the link i am concerned with the second formula in ...
2
votes
1answer
34 views

When does a formal system cease to be able to be complete and consistent?

In Gödel, Escher, Bach , Hofstadler contends that certain formal systems may be both consistent and complete, such as his own pq system. However, for certain "sufficiently powerful" formal systems, ...
6
votes
1answer
79 views

Terms in the lambda calculus

The formal definition of the lambda calculus I am seeing here reads: The class of $\lambda$-terms is defined inductively as follows: Every variable is a $\lambda$-term. If $M$ and $N$ are ...
0
votes
0answers
9 views

Formally State Asymmetry of Information

I am constructing a formal framework for insurance companies. The idea of asymmetry of information by no mean is new to economists but even in textbooks, it is not defined formally. What is meant by ...
1
vote
0answers
48 views

Expected Length of Proof in a given Axiomatic System

Is there some sort of notion of the expected length of proof taken over the space of all theorems in an axiomatic system or something close to that in the far reaches of pure math? What type of math ...
0
votes
0answers
12 views

How do we call a formal system for a propositional logic?

I have been interested in the MU-puzzle lately. I do not have a math background and I have just learnt that a formal system is a collection of symbols and grammar for constructing formulas from these ...
2
votes
2answers
96 views

Is there any easy example of a formal proof in mathematics and an equivalent informal proof to illustrate a difference between those two?

I would really like to see some SHORT example of an informal proof in mathematics side by side with the same proof but formal one to see some clear distinctions between those two. Do you know any such ...
0
votes
1answer
27 views

What is some easy illustrative example of an non-recursive formal system and recursive formal system?

I have a difficulty to relate recursion in to formal systems. Would you please show me some easy example (like for example MU-system) of a recursive formal system and non-recursive formal system so ...
0
votes
1answer
44 views

Gödel's Second Theorem and the Consistency of Robinson's System

In Kleene, Introduction to Metamathematics, $\S42$ (end), it is shown that if formal number theory is simply consistent, then its consistency cannot be proven formally within the system. In other ...
-2
votes
1answer
52 views

Contradictory vacuous truths in consistent formal system [closed]

Can 2 contradictory vacuously true statements be proved in a consistent formal system?
0
votes
0answers
26 views

How to imagine a process of generating theorems from a formal system in a computer?

I'm aware that it is possible to create a formal system in a computer to generate theorems from it. How could I imagine such a system in a computer which generates theorems in a way that would be ...
0
votes
0answers
29 views

What is the difference between a mathematical theory and a formal system?

These two terms seems almost interchangeable to me. Is there any difference?
0
votes
0answers
41 views

Are theorems (not axioms) listed as a part of a formal system?

Are theorems derived from a formal system a part of that formal system? In other words, do we view a formal system as a shorter way of listing all the theorems that flow from such a system? In other ...
0
votes
1answer
24 views

Could formal systems be viewed as a short version of saying what I believe in without necessary listing all theorems which flow from that system?

Lets say that I tell to a person "A" that I believe that the Got exists. For the person "A" it seems therefore obvious to imagine that I also believe in a lot of things that flow from such a statement....
4
votes
1answer
180 views

What is the reason we usually don't use formal proofs in mathematics?

Is the reason for not using formal proofs very often in mathematics because it is usually too lengthy for a person to make such a proofs or the reason is that it is simply not possible for everything ...
0
votes
0answers
41 views

How do I find out effectively what particular formal system I'm using in any particular moment when doing math in school?

I would like to know: How to find out in what particular formal system I am working (what axioms, rules of inference and formal language am I assuming) when they don't specify me in a school? For ...
7
votes
2answers
157 views

Why is it impossible nowadays for a computer to derive all the possible theorems that flow from a particular formal system?

I am just learning about formal systems and mathematical logic. It seems to me that it could be relatively easy to generate all the possible theorems that flow from a particular formal system (set of ...
1
vote
0answers
32 views

Is $I\Delta_0+\Omega_1$ globally interpretable in Q?

Alex Wilkie found a single formula $J(x)$ for an inductive cut of the natural numbers such that the axioms of Robinson arithmetic are sufficient to prove every instance of the induction scheme $\phi(0)...
3
votes
2answers
73 views

Is this a proper rendering for “$b$ is a power of 2” using TNT from Gödel, Escher, Bach

In the book "Gödel, Escher, Bach" by Hofstadter introduces the system of "Typographical Number Theory". One of the exercises is to write 'b is a power of 2', I ended up coming up with the following $&...
0
votes
0answers
37 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, ...
1
vote
0answers
23 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 ...
4
votes
1answer
120 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 ...
2
votes
1answer
128 views

Reducing number of sorts in formal theory

In Kleene ''Introduction to Metamathematics'' 1971 on pp.420 he shows that if we have a formal system which for some formula $M(x)$ can prove the statement $\exists x M(x)$ then one can introduce a ...
3
votes
1answer
218 views

What is the purpose of Semantics/Model theory in Mathematical Foundations?

First off I know very little model theory so apologies if I say anything very dumb or offensive to logicians/model theorists. Second I should note that a lot of what I am saying here is motivated by ...
0
votes
1answer
43 views

Adding constants to formal system

I wonder how can we formalize in logic the fact that we sometimes add additional constants for the sake of readability. Consider, for example, that in some formal system we prove that if $a,i$ are ...
0
votes
1answer
71 views

Infimum and Supremum (of sets) - Formal Concept Analysis

I am taking a course of Introduction to Formal Concept Analysis and I have an uncertainty about the definition of supremum (least comum superconcept) and infimum (greatest comum subconcept) of formal ...
3
votes
0answers
118 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) \...
1
vote
3answers
404 views

Formalization of mathematics? [closed]

I've recently taken an interest in the foundation of mathematics and have read a tiny bit about various type systems, Principia Mathematica, and logic. Personally, I'm not a big believer in the idea ...
1
vote
0answers
35 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
89 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 ...
3
votes
2answers
109 views

Logic - Member of an inductive set that is not a member of the set of theorems in a formal system?

First question on this site. Hope to ask/answer many more in the future. I'm currently self-studying An Introduction to Mathematical Logic by Richard E. Hodel and came across an interesting exercise. ...
4
votes
1answer
80 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 ...
1
vote
1answer
63 views

Independence and Consistence of Formal Systems

Let $S$ be a formal system with axioms $A,A_1,\dots,A_n$. The system $S$ is said to be consistent if no contradiction can be proved (i.e. we can’t prove both a formula and its negation). If $S$ is ...
1
vote
2answers
151 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 ...
3
votes
1answer
125 views

Why must $x$ be not free in $\psi$ in order for $(\psi\to\phi)\vDash[\psi\to(\forall x\phi)]$?

In the PDF textbook "A Friendly Introduction to Mathematical Logic 2nd Edition" by Christopher C. Leary and Lars Kristiansen, page 53, the first quantifier inference rule (QR) is defined by the ...
0
votes
1answer
57 views

Proof explanation of invalidity implying a non-tautology

In the PDF textbook, "A Friendly Introduction to Mathematical Logic 2nd Edition" by Christopher C. Leary and Lars Kristiansen, on page 54, exercise 6, I am asked to do the following: Given that $\...
3
votes
2answers
299 views

The intuitive meaning of “or” and “implies” in axiom schemes of a logical theory

In a Hilbert-style system, the axiom schemes can be written as (From Bourbaki, Book I): S1. If $A$ is a relation in $\mathscr C$, the relation $(A\text{ or }A) \Rightarrow A$ is an axiom of $\...
0
votes
1answer
213 views

GEB Why is it necessary for TNT-PROOF-PAIR{a,a'} to be represented in TNT?

In Hofstadter's Gödel, Escher, Bach there is the predicate TNT-PROOF-PAIR{a,a'} which is used in constructing the Gödel string. He then explains that it is a ...
2
votes
1answer
72 views

Choosing axiom schemes for a logical theory

In a Hilbert system, there are many ways that we can choose axiom schemes. My question is: 1- How do we know that we have defined enough schemes? What would happen if I remove a scheme from the list? ...

1
2 3 4 5