# 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
Filter by
Sorted by
Tagged with
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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, ...
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$ ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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}...
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. ...
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 ...
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 ...
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$ (...
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 ...
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 ...
1answer
172 views

1answer
80 views

### Contradictory vacuous truths in consistent formal system [closed]

Can 2 contradictory vacuously true statements be proved in a consistent formal system?
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 ...
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 ...
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....
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 ...
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 ...
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 ...