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)
241
questions
-1
votes
2answers
74 views
Does Godel's theorem only apply to formal systems? [closed]
What I've seen in gathering information about this proof is it's only about this framework of formal systems, plus some intuitions about number.
Math isn't necessarily a formal system, and these ...
0
votes
1answer
34 views
How to write “the set of all walks of a graph” in formal logic notation?
I have this question on the CS stackexchange to figure out how to model "a walk of a graph" in a custom formal language. I think the problem is that there is not just one walk of a graph but ...
1
vote
0answers
77 views
How do you formalize this reasoning?
There is this simple number theory problem which says "how many 4 digit numbers that are divisible by 3 and whose digits exclude 2, 4, 6 and 9 exist?"
the solution is quite intuitive:
each ...
1
vote
1answer
87 views
Axiom scheme for mathematical induction in formal axiom system for Peano Arithmetic
I'm reading the book "Gödel's incompleteness theorems" by Smullyan. (I found it online here: https://isidore.co/calibre/get/pdf/5823). In Chapter III he explains the Axiom System for Peano ...
1
vote
1answer
57 views
What is a precise definition of soundness?
I'm trying to better understand soundness, especially in contrast to semantic consistency. Here is what I've put together so far:
Soundness: A theory is sound if all theorems are true under all ...
1
vote
0answers
46 views
Is it possible to create a “hack-proof” system?
Various organizations, such as DARPA, have purported to create virtually "hack-proof" software systems using mathematical techniques such as formal verification. In short, the idea is ...
0
votes
0answers
22 views
Lindenmayer system for Pólya space filling curve
I am considering the special case of an isosceles right triangle.
The pattern seems that starting with $+F$ for odd depth of recursion and $F$ for even depth of iteration where + means rotate ...
0
votes
0answers
30 views
Is there any technical, mathematical or logical, terminology for a set of propositions, all of which cannot be True at the same time.
As the question states, what is the technical term (if any) for a set of propositions which cannot all be true at the same time.
That is to say,
If there is a set, $A${x1, x2, x3, ... , xn}
for which ...
0
votes
0answers
44 views
Is it possible to list all hidden lemmas of a proof?
I'm studying Imre Lakatos' Proofs and Refutations for my master's thesis. Currently I address the concept of hidden lemmas, which I understand to mean unstated assumptions of a mathematical proof, ...
2
votes
1answer
25 views
Beta Reduction Constraints
The definition of $β$ reduction is the following :
$$(λx.M)N \rightarrow_{β} Μ[x∶=N] $$
So basically we stop treating $x$ as a bound variable and we perform substitution of the now free variable $x$ ...
2
votes
1answer
58 views
Beta Reduction in Lambda Calculus
I came across the definition of beta reduction in Lambda Calculus which is :
$$(λx.M)N \rightarrow_β Μ[\space x:= N \space]$$ under the constraint that the $FV(N)$ are still free after the ...
0
votes
1answer
50 views
Godel Escher Bach: Why is a Godel proof-pair representable in TNT?
On page 441, fundamental fact 2 asserts that:
The property of forming a proof-pair is testable in BlooP, and consequently, it is represented in TNT by some formula having two free variables.
Why is ...
1
vote
2answers
53 views
Formal relationship between rules of inference and the material conditional
I am not $100\%$ clear as to what constitutes the difference between a rule of inference and the material conditional, at least in classical logic. I am using the truth-functional definition of the ...
2
votes
0answers
46 views
Is there a way to study formal systems in general?
I was reading Gödel Escher Bach, and the author explains that mathematics is just an example of something broader: formal systems. So I wonder wether there exists a theory to study formal systems in ...
0
votes
0answers
41 views
Reading Principles of Mathematical Logic by Hilbert
I want to read Principles of Mathematical Logic by Hilbert and Ackermann. However, I don't know if this is an introductory level text. So I was wondering, is there some background one should have ...
0
votes
1answer
72 views
Describing all formal theory theorems problem
I'm having problems understanding how this works so I'll provide detally explained problem but I'd like if someone could explain it somehow simpler or write it out more step by step than what I'll ...
0
votes
1answer
67 views
Is it possible to add computational facilities to otherwise “mathematical” formal systems by adjoining identities to types?
The following thought has been on my mind for years.
Think of $\mathbb{N}$ as the type of all well-formed expressions representing natural numbers. And think of $$\tilde{\mathbb{N}} := \frac{\mathbb{N}...
0
votes
0answers
29 views
What differences and relation are between proof systems and deductive systems? [duplicate]
https://en.wikipedia.org/wiki/Proof_calculus says
A proof system includes the components:
Language: The set of formulas admitted by the system, for example, propositional logic or first-order logic.
...
5
votes
2answers
205 views
What's up with the Sheffer stroke axiom?
While reading some old paper on the foundations of set theory, I came across a symbol $\mid$ that I eventually determined was the Sheffer stroke, which is a fancy word for NAND.
Wikipedia, and also ...
5
votes
2answers
263 views
Implementing sets in $\lambda$-calculus
Both Set theory and $\lambda$-calculus are considered to be valid foundations for mathematics. Since these are both equivalent (in the sense that any structure that can be implemented in set theory ...
1
vote
1answer
57 views
Why doesn't this show that first-order Peano arithmetic is consistent?
SOME PRELIMINARIES: Predicate logic is consistent and complete. In other words, (i) for a closed formula $F$ in predicate calculus with equality and functions, $\vdash F$ if and only if $\,\vDash F$ (...
20
votes
2answers
2k views
What is the definition of a definition?
In mathematical logic or other formal systems, what is the definition of a definition, formally?
If "A" is defined as "B", what is the definition of "A" like?
Does it ...
5
votes
1answer
352 views
Can inconsistent systems be mathematically interesting/useful?
According to the top answer to this question:
Doing mathematics we often have an idea of an object that we wish to represent formally, this is a notion. We then write axioms to describe this notion ...
0
votes
1answer
172 views
What are the relations and differences between formal systems, rewriting systems, formal grammars and automata?
I learned from Herre & Schroeder-Heister's "Formal Languages and Systems" that
A formal system is based on a formal language $L$, endowing it with a consequence
operation $C: 2^L\to 2^...
3
votes
1answer
67 views
Is this property of derivation relation equivalent to idempotence?
In Herre & Schroeder-Heister's "Formal Languages and Systems", on p6,
A formal system is based on a formal language L, endowing it with a consequence
operation C. This operation C can ...
0
votes
1answer
32 views
What is compactness for a deductive system?
In Herre & Schroeder-Heister's "Formal Languages and Systems", on p6,
It (i.e. a consequential operation) is called a deductive system, if the consequences of a set X can be
obtained ...
1
vote
0answers
29 views
Is the semantics of a first order logic system defined as part of the first order logic system?
Does a first order logic system consist only of
a first order language
a first order deductive system?
Is a first order logic system nothing more than a formal system?
Is the semantics of a first ...
1
vote
0answers
64 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 ...
1
vote
1answer
64 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
60 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
45 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
61 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
40 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
49 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
54 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
117 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
39 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
40 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
93 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 ...
1
vote
0answers
50 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 ...
2
votes
2answers
148 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
58 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 ...
1
vote
1answer
56 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
80 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
46 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
25 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....
5
votes
1answer
343 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 ...
8
votes
2answers
168 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 ...
