Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

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)

0
votes
0answers
29 views

Formalization of a Predicate in Intro to Metamathematics, Kleene (Gödel Numbering)

In Introduction to Metamathematics $\S$51, Kleene defines fourteen predicates for a generalized arithmetic with each of $$\supset\,\,\&\,\,\vee\,\,\neg\,\,\forall\,\,\exists\,\,=\,\,+\,\,\cdot\,\,'...
3
votes
1answer
58 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 ...
4
votes
1answer
119 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
123 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
31 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
42 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 ...
3
votes
0answers
79 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
193 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
29 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 ...
1
vote
0answers
46 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
101 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
68 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 ...
1
vote
1answer
54 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
50 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
1answer
91 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 ...
0
votes
1answer
42 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 $\...
3
votes
2answers
283 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
89 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
59 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
117 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 ...
0
votes
1answer
53 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
86 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 ...
0
votes
1answer
59 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....
3
votes
3answers
343 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
2answers
173 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
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 ...
2
votes
2answers
209 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 ...
0
votes
2answers
52 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 ...
2
votes
3answers
328 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 ...
-1
votes
2answers
642 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
149 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
161 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 ...
5
votes
2answers
446 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 ...
1
vote
1answer
108 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, ...
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
58 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
153 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
51 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
77 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?
2
votes
1answer
212 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\...
2
votes
1answer
54 views

Find Theorems of a Formal Theory

Going through a book on formal logic, I have encountered the following problem. Since I am somewhat new to formal logic, I am confused about how to approach it. A certain formal theory has exactly ...
1
vote
0answers
40 views

What is the easiest way to show that a type theory is consistent?

I'm working on presenting an extension of MLTT which uses a (from what I can tell) novel conception of type universes which I believe is not equivalent to the standard Russell/Tarski-style approaches. ...
1
vote
0answers
45 views

Kolmogorov complexity measure of a formal system

Each formal system can be encoded in a binary string. For instance, you can use the input string that a pre-specified Turing machine needs in order to enumerate all the theorems in a theory in the ...
0
votes
2answers
43 views

How to state the “unsolvability of quintic by radicals” in 2nd and higher order logic?

I am attempting to express the sentence "There does not exist a general solution for the 5th degree polynomial equation in radicals" In 2nd order logic. So I made the statement clearer by going ...
0
votes
0answers
50 views

Is there a standard notion of a “theory of Turing machines”?

Of course, there are more-or-less standard definitions of Turing machines as a certain type of mathematical object formalized in some theory (Say, ZFC), but what I am looking for is a first order ...
1
vote
0answers
27 views

Formal verification of function contract?

How could I formally reason about the following function: function f(x){ if(x>=0){ return 1; }else{ return 0; } return 2; } ...
0
votes
1answer
48 views

Given an axiom in a formal system, can we always find another formal system in which this axiom is a theorem?

As an example, when set theory was created, it seems people tried to write the mathematical concepts they had using set theory, I guess that after this, what were previously axioms became theorems in ...