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)
192
questions
0
votes
0answers
20 views
Is $I\Delta_0+\Omega_1$ globally interpretable in Q?
Alex Wilkie found a single formula $J(x)$ for an inductive cut of the natural numbers such that the axioms of Robinson arithmetic are sufficient to prove every instance of the induction scheme $\phi(0)...
3
votes
2answers
44 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 $&...
0
votes
0answers
36 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 ...
4
votes
1answer
66 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
125 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
143 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
33 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
57 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
91 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
233 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 ...
1
vote
0answers
61 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
74 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
61 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
60 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
102 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
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 $\...
3
votes
2answers
291 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
113 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
65 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
155 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
68 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 ...
0
votes
1answer
69 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
386 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
199 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
241 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
62 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
369 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
719 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
170 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 ...
5
votes
2answers
495 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
129 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
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
158 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?
2
votes
1answer
258 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
41 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
50 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 ...
