# 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)

191 questions
36 views

225 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 ...
32 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 ...
100 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 ...
60 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 ...
102 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. ...
72 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 ...
58 views

### Book request - formal logic

Can anyone recommend a good comprehensive introduction to formal logic? I realise the field is enormous. I am particularly interested in books that a) provide historical context, b) cover both first ...
60 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 ...
57 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 ...
290 views

109 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 ...
63 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? ...
152 views

### Every Turing machine corresponds to a formal system

Solomon Feferman, at page 138 of his 2006 paper "Are there absolutely unsolvable problems" says that each formal system of axioms can be made to correspond to a suitably designed Turing machine so ...
486 views

### Are there logics without modus ponens?

The question doesn't go beyond the title. And I don't mean logics that merely just don't have it as a primitive rule - I'm interested in logic where you can't actually use it. I've searched around ...
67 views

### Is the set of formulas equivalent to a bounded formula decidable

In C. Papdimitriou, Computational Complexity a bounded (first order) formula over the signature of the natural numbers with addition and multiplication is defined the following way: We use the ...
88 views

### How much of first order statements can we derive purely from the definitions in arithmetic?

I didn't know how to formulate a more clear title for this question: Take arithmetic to be the structure $\mathcal N= (\mathbb N, \sigma, +,•, 0,1)$ with its standard interpretation. When I use the ...
376 views

### Foundation of Formal Logic

All the books that I’ve read about formal logic either starts assuming the existence of set theory (they talk of countable sets of symbols and define formulae as sequences of symbols), or follow an ...
67 views

### Language of an Axiomatic System in the Incompleteness Theorem

From wikipedia, the statement of Gödel's First Incompleteness Theorem is : "Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e....
47 views

### What is a gross-looking formal axiomatic proof for a relatively simple proposition?

I'm looking for long and hard to follow derivations or symbolic proofs to motivate how tedious it is to actually reason within a formal system. I'm hoping there is an image of the proof, with few if ...
198 views

537 views

### How do you go about formalizing a concept?

I am reading Godel Escher Bach. In the first few chapters, the author shows what a formal system is, and gives examples that eventually lead to a typographical formal system of strings that represents ...
713 views

### Definition of the bound and unbound variable [closed]

What do we mean by bound and unbound variable? I have difficulty to understand their meanings, Could anyone help me with that?
62 views

### A formal language problem

Translated as best I could the problem is stated as follows: Over the set $A=\{\alpha,\beta,\gamma,\delta,\epsilon,\eta\}$ a model $\mathbb{A}$ of language $\mathcal{L}=\{q\}$ ($ar(q)=2$) is defined ...
169 views

### Show that any monotone boolean function can be realize by the following connectives.

Let the following be the set of connectives involving {$\top,\ \bot,\ \land,\ \lor$}. Set $F \leq T$ Show that any monotone Boolean function $f$ can be realize by a wff (well-form formula) using ...
169 views

### Can one-element set be considered equal to its element?

Are there "interesting" (that is non-trivial, for example not containing only one set) set theories with one element set being equal to their element ($\{x\}=x$ for every $x$)? This question arose ...
127 views

### The existence of unprovably unprovable statements provable in ZFC [duplicate]

I am aware of Gödel's second incompleteness theorem, the proven existence of several unprovable statements (in ZFC), and the possibility that a formal system may include statements that are unprovably ...
107 views

### Does introducing a new type create a different extension, and is it still conservative?

In this comment on Terry Tao's page about his Analysis I textbook, he writes, If one wanted to do things by the book, what one should actually do each time one introduces a new mathematical object, ...
398 views

### semantics(truth) vs formal system?

my first question is can we just define semantics in logic and not define a formal system ? why do we need a formal system to prove a proposition when for example we know the proposition is true ? <...
63 views

### Logic -can it possible we derive all theorems in formal system and we can't derive more theorems?

I'm a really beginner in Mathematical Logic.I'm currently reading Shoenfield Mathematical's Logic He say theorems of formal system F should satisfy the two laws : 1) The axioms of F are ...
59 views

### How to express induction when we just have finitely many instances, but still proceed inductively over them

Let $Q$ be some finite set with $n = |Q|$. Then suppose I want to show that for every nonempty subset $P \subseteq Q$ some property $A$ holds. One natural way to approach this is using induction, and ...
157 views

### Axiomatic set theory as a first-order logic theory?

This question is about how accurate is it to say that axiomatic set theory is a first-order logic (FOL) theory? The crux of the matter is the nature of the set comprehension symbol $\{\_ \mid \_ \}$. ...
52 views

### Is there a term for this logical property?

Suppose I am working in a standard formal theory such as ZFC or NBG. Consider this statement: "For all well-formed formulas s, ((there exists a proof p s.t. p is a valid proof of s) --> s)" I'm ...
A fundamental connection between provability and consistency for formal systems is that, if $Q$ is a formal system and $A$ is a sentence in the language of $S$, then $Q$ proves $A$ if and only if \$...