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)
220
questions
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?
...
