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)

3
votes
2answers
36 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 $&...
5
votes
1answer
822 views

Understanding definition of conservative extension of a theory

From Wikipedia In mathematical logic, a logical theory $T_2$ is a (proof theoretic) conservative extension of a theory $T_1$ if the language of $T_2$ extends the language of $T_1$; every ...
0
votes
0answers
34 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
19 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 ...
3
votes
1answer
63 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 ...
3
votes
1answer
124 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 ...
2
votes
1answer
142 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
32 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
56 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 ...
13
votes
4answers
21k views
3
votes
0answers
90 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
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 ...
1
vote
0answers
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 ...
3
votes
1answer
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 ...
1
vote
0answers
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 ...
3
votes
2answers
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. ...
4
votes
1answer
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 ...
0
votes
2answers
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 ...
1
vote
1answer
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 ...
0
votes
0answers
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 ...
3
votes
2answers
290 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
48 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 $\...
0
votes
1answer
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 ...
2
votes
1answer
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? ...
5
votes
1answer
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 ...
5
votes
2answers
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 ...
0
votes
1answer
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 ...
1
vote
1answer
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 ...
3
votes
3answers
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 ...
0
votes
1answer
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....
1
vote
2answers
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 ...
0
votes
2answers
198 views

How to use axioms to prove a derivation in propositional calculus?

Given a formal system called "$P0$" that has 1 rule (Modus Ponens) and 3 axioms: $1.$ $\alpha$ $\rightarrow$$(\beta \rightarrow \alpha)$ --- (Ak) $2.$ $(\alpha \rightarrow (\beta \...
1
vote
2answers
395 views

Can there exist a definition of 'multiplication' in Presberger Arithmetic?

According to Wikipedia, Presberger Arithmetic is the first-order theory of the natural numbers with addition. It can be proved to be consistent, complete, and decidable. Though it contains no axioms ...
2
votes
2answers
239 views

What is the purpose of the Axiom of regularity/foundation?

Besides the axioms of extensionality and regularity, all of the axioms of ZFC either postulate the existence of a set or give a method for generating new sets from existing sets. Extensionality then ...
2
votes
3answers
368 views

Is every true statement about the natural numbers provable in ZFC?

Related questions: Difference between undecidable statements in set-theory and number theory? Is the arithmetic most mathematicans use a modelled within first or a second order logic? Peano's axioms ...
2
votes
1answer
254 views

book recommendation - formal systems

I'm looking for a strict book/pdf about logic which discusses formal systems in great detail. I only know basic stuff. It should cover: definitions (like $(\exists x \varphi\leftrightarrow\lnot\...
9
votes
3answers
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 ...
-1
votes
2answers
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?
2
votes
2answers
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 ...
1
vote
1answer
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 ...
6
votes
1answer
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 ...
1
vote
1answer
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 ...
6
votes
0answers
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, ...
4
votes
6answers
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 ? <...
0
votes
1answer
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 ...
1
vote
2answers
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 ...
2
votes
2answers
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 \_ \}$. ...
1
vote
1answer
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 ...
2
votes
0answers
49 views

Weird analogy between quadratic forms and formal systems

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 $...
0
votes
1answer
87 views

What are “non-trivial formal systems”? [closed]

In Godel’s incompleteness theorem, his two statements relate to “non-trivial formal system”, but how are these determined? Is 1+1=2 one of these? What about P vs NP?