# 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
Filter by
Sorted by
Tagged with
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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, ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
52 views

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

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

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, ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
118 views

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 \$\...