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
1answer
27 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
36 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
65 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
174 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
28 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
99 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
42 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
88 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
39 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
274 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
76 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
57 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
95 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
41 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
85 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
56 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
322 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
144 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
44 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
190 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
49 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
304 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
553 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
59 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
136 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
156 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
385 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
102 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
61 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
54 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
145 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
48 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
74 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
190 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
53 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
43 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
49 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 ...
0
votes
0answers
35 views
Efficiently Verifying “identities” in Arithmetic
So suppose I have two expressions $A,B$ both consisting of some combination of parenthesis $()$, addition $+$, multiplication $\times$, exponentiation $ \text{^}$.
What is an efficient way to check ...
5
votes
0answers
109 views
Which formal system (aka platform) is the best for selfstudying Category Theory?
I was planning to learn category theory with coq's aid and its category theory implementation, but a stackoverflow user told me in the comments (of other question) that it may be too difficult. So, ...
1
vote
1answer
70 views
Show that a given formula is not provable without the associative rule
This question is from Shoenfield's "Mathematical Logic", an exercise on page 25.
Show that the formula $((x \neq x) \vee \neg(x \neq x \vee x \neq x)) \vee (x \neq x \vee x \neq x)$ is a theorem, ...
2
votes
1answer
547 views
What is the difference between a formal system and first order logic?
Can someone explain the connection between them? For example i have read about Hofstadter's MIU System and don't know how it relates to first order logic. What do formal systems and first order logic ...
