Questions tagged [formal-proofs]
For questions about proofs within a formal system, such as natural deduction or Hilbert system.
855
questions
0
votes
1
answer
81
views
How can a problem with cases be represented formally? [duplicate]
For example, if there are two men A & B.
A says
Both of us always tell the truth
B says
A always lies
Edit: A and B either always tell the truth or lie.
What I know that this can be solved by ...
- 66.3k
5
votes
1
answer
107
views
How to establish this generalization rule in sequent calculus for First Order Logic?
I stumbled across this rule:
$$\frac{\Gamma\vdash q\rightarrow p(a) }{\Gamma \vdash (q \rightarrow \forall x. p(x))}$$
where $a$ also needs to be a fresh constant, so with that in mind you could re-...
- 17.4k
1
vote
1
answer
392
views
Let $S$ a subspace and $V$ a vector space. Show that the additive identity of $S$ is the additive identity of $V$.
Working on the book: Robert Messer. "Linear algebra - The gateway to mathematics" (p. 55)
16. Suppose $S$ is the subspace of a vector space $V$.
a. Show that the additive identity of $S$ is ...
2
votes
2
answers
881
views
Proving $\vdash \neg \neg P \to P$ (double negation elimination) in first order logic, preferrably without deduction theorem
The axiom system used is
$A\to B \to A$
$(A \to B \to C) \to (A \to B) \to A \to C$
$(\neg A \to \neg B)\to (B \to A)$
$(\forall x A) \to A[t/x]$, where $x$ is substitutable with $t$ in $A$.
$\forall ...
- 282
1
vote
2
answers
3k
views
How to make a formal proof with A → (B ∨ C) ⊢ (A → B) ∨ (A → C)
Here is what I've got so far:
I feel like I need an indirect proof for this and so I need to prove a contradiction with one of line 4 or 5. I'm not sure how to approach it. Any hints that can help me ...
- 31.4k
1
vote
2
answers
1k
views
How to prove this using natural deduction
$$⊢ P ∨ ¬P$$
I found this question on the net. I know the solution, but I find it complicated.
How should I approach this sort of question? Or can you provide me with another solution?
CommunityBot
- 1
2
votes
3
answers
169
views
Negation of a Formula is Provable without Including the Formula as an Assumption
The following lemma states that if we can prove negation of a Well Formed Formula (WFF) $\alpha$ by assuming the formula itself, then we can do it without such an assumption.
Lemma. Let $\Sigma$ be a ...
- 15.1k
10
votes
1
answer
3k
views
A simple proof of Descartes's rule of sign
I search all over the Internet for a proof of Descartes's rule of sign.
Found a pdf file which has page-long proof that a high schooler has to no way to understand.
Can somebody talented here give ...
- 62k
16
votes
3
answers
4k
views
Does every proof need an axiom saying it works?
I am wondering whether for every (valid) proof $P$ done in mathematics, at least one of the following statements are true:
There is an axiom guaranteeing that its schema indeed gives us license to ...
- 21.9k
29
votes
5
answers
5k
views
Are there statements so self-evident that writing a proof for them is meaningless? Is this an example of one?
Context: I know nothing about proofs and only a small amount about formal logic used in proofs. I'm trying to learn the basics of how to write a proof.
For example, suppose I wanted to prove that &...
4
votes
4
answers
5k
views
How to prove that $P \rightarrow Q$ is equivalent with $\neg P \lor Q $?
In my book about Logic, which is called 'Language, Proof and Logic', by the way, there is explained that the conditional $ P \rightarrow Q $ is equivalent with $\neg P \lor Q$.
There is another ...
- 557
2
votes
2
answers
688
views
Spivak Calculus 3rd. Edition Chapter 1 Problem 12 (i) and (ii) Proofs Critique
Here are my "proofs" for Spivak's Calculus Chapter 1 Problem 12. I am new to this level of rigour and I am attempting to intimate myself with more advanced topics of mathematics to prepare for next ...
- 11
3
votes
1
answer
176
views
On the limitations(?) of first-order logic in mathematical reasoning
Note: This is a follow-up to this earlier question. Also, for the purpose of this question, I'll use the term "normal mathematics" to refer to topics other than "foundational" ones ...
- 363
1
vote
0
answers
77
views
If proofs can be checked by computers, will we ever mistakenly believe a false proof? [closed]
As I understand, math proofs can be formalized and checked by a computer. Does this mean the math community will never have to deal with believing incorrect proofs?
If not, is the issue with adoption ...
2
votes
1
answer
82
views
Prove $\forall x\forall y \neg R(x,y) \wedge \neg \exists x\forall y\neg R(F(x),y)$ is a contradiction by natural deduction
Problem: Prove by natural deduction that the formula $$\forall x\forall y \neg R(x,y) \wedge \neg \exists x\forall y\neg R(F(x),y)$$ is a contradiction.
So far: Here $R$ is a relation and $F$ a unary ...
- 6,125
4
votes
1
answer
124
views
Prove $\forall x \forall y(xEy \rightarrow \neg x=y)$ in the vocabulary of graphs
Problem: Prove the sentence $\forall x \forall y(xEy \rightarrow \neg x=y)$ in the vocabulary of graphs using the axioms of graph theory.
So far: The axioms of graph theory given are antireflexivity ...
- 131k
2
votes
3
answers
89
views
Proving $\exists x P(x) \rightarrow \forall x P(x)$ from $\forall x\forall y(x=y)$
Problem: Using identity axioms, prove $\exists x P(x) \rightarrow \forall x P(x)$ from $\forall x\forall y \, x=y$.
So far: I'm quite stuck on where to even begin. Working backward, I know we want $P(...
- 14.9k
2
votes
1
answer
3k
views
How to prove ¬P∨Q entails P→Q by Natural deduction
I can easily prove that $P \to Q$ entails $\lnot P \lor Q$ by Natural deduction,
but I cannot find a way to proof $\lnot P \lor Q$ entails $P \to Q$.
Could you show me the way by using Natural ...
- 179k
1
vote
1
answer
205
views
Considering $\Gamma \vdash \varphi$, is $\Gamma$ a set or a list?
As far as I know, most of mathematical logic textbooks state the Weakening Lemma:
Let $L$ be a first-order language.
Then, for any sets $\Gamma_1$ and $\Gamma_2$ of $L$-formulas and any $L$-formula $\...
- 11.9k
1
vote
1
answer
137
views
How to prove that $∀x (p(x) \to ¬ q(x))⊢¬(∃x (p(x)∧q(x)))$ using natural deduction in tree format
I need to prove that using natural deduction in tree format
$(\forall x\ p(x)\to \neg q(x)) \vdash \neg (\exists x (p(x)\land q(x)))$
I have built the following proof which is incomplete and I do not ...
- 131k
3
votes
0
answers
104
views
What kind of principles of reasoning can we use for classes in ZFC?
$\newcommand{\set}[2]{\{\ #1 \mid #2 \ \}}$
Motivation & Context
In ZFC, everything in the domain of discourse is a set and we can only talk about classes in the metatheory. But we still want to ...
- 175
6
votes
2
answers
745
views
Is "first-orderizability" a requirement for "legitimate" mathematical reasoning?
If we take a first-order theory (like $\mathsf{ZFC}$, or $\mathsf{ZFC}$ plus some additional axioms) as the foundation of mathematics, does that imply that mathematical reasoning (theorems, proofs, ...
- 1,090
6
votes
1
answer
538
views
Why typeclasses rather than inductive types to define mathematical structures in Lean?
I am not sure whether this is the right forum for this question, but I am not sure where else to ask (There is no Lean forum afaik).
In the Lean Prover mathlib library, typical mathematical ...
- 875
0
votes
1
answer
141
views
Help with Formal Proof using introduction and elimination rules
I need help with a proof where the premise is $\lnot A \land \lnot B$ and the goal is $\lnot (A \lor B)$. We are allowed to use the introduction and elimination of the following operators: $\lnot$,$\...
- 131k
1
vote
1
answer
72
views
Examples of sequent derivations that uses cut rule that can be modified to not to use cut rule?
The cut-elimination theorem states that any sequent calculus derivation that uses the cut rule also has a derivation that does not use the cut rule. I cannot find any explicit examples of such ...
- 17.4k
1
vote
2
answers
349
views
Prove distributive law in Hilbert system
Using the logical axioms of the Hilbert system
$\phi\to\phi$
$\phi\to(\psi\to\phi)$
$\left( \phi \to \left( \psi \rightarrow \xi \right) \right) \to \left( \left( \phi \to \psi \right) \to \left( \...
- 583
-1
votes
1
answer
89
views
Formal proof of equality of ordered pairs [duplicate]
I am trying to prove with natural deduction the following with the Kuratowski definition of ordered pair:
$$\forall x, y, z, w(\langle x, y\rangle=\langle z, w\rangle\leftrightarrow(x=z\land y=w))$$
I ...
- 3,597
0
votes
2
answers
114
views
Proving $A\to (¬A \to B)$ with Łukasiewicz's axioms and modus ponens?
I am trying to answer the following exercise from Hao's Fundamentals of Logic and Computation: With Practical Automated Reasoning and Verification.
Using only modus ponens and the following axioms:
...
- 583
3
votes
1
answer
225
views
Are there any recent advances in formalizing the undecidability of $\mathit{CH}$?
I'm cross-posting this from Mathoverflow. Since I'm asking for recent developments, it seems best to have answers in both sites.
The website Formalizing 100 Theorems by Freek Wiedijk contains a list ...
- 4,744
4
votes
3
answers
432
views
Axiomatic proof of $⊢(a→b)→(¬b→¬a)$ without using the deduction theorem
I'm trying to prove : $⊢(a→b)→(¬b→¬a)$ , or the contrapositive as a wff, using the following 6 axioms, the Hypothetical Syllogism rule, and Modus Ponens.
...
- 102k
1
vote
1
answer
122
views
Smallest natural deduction proof for Meredith's axiom from basic rules
I tried to find a small natural deduction proof for Meredith's single axiom
Infix notation
Polish notation
((((ψ→φ)→(¬χ→¬ξ))→χ)→τ)→((τ→ψ)→(ξ→ψ))
...
- 282
3
votes
2
answers
142
views
Interpretation Theorem
The Interpretation Theorem is the following excerpt from Kunens old Set Theory
8. Appendix $1$: More on relativization
We sketch here a more formal treatment than that in $\S 2$. There is a general ...
- 95.2k
2
votes
1
answer
80
views
Use sequent calculus to show if $\Gamma\vdash t_1=t_2$ then $\Gamma\vdash f(t_1)=f(t_2)$
Suppose the sequent $\Gamma\vdash t_1=t_2$ where $t_1,t_2$ are closed terms. Let $f$ be a one-place function symbol.
I am trying to find a sequent calculus derivation of $\Gamma\vdash f(t_1)=f(t_2)$ ...
- 17.4k
3
votes
1
answer
101
views
Question about quantifiers in the proof of the cut eliminiation theorem
Lately I have been reading about the cut elimination theorem, I think I get the idea however I have been struggling with some technical details concerning quantifiers.
Consider the following rule:
...
- 17.4k
1
vote
2
answers
100
views
Basis for $V$ containing no elements of the proper subspace $U$
Let $U$ be a proper subspace of a finite-dimensional vector space $V$ . Find a basis for $V$ containing no element of $U$.
We have no answer key for this question which i find annoying since that is ...
- 36.2k
2
votes
1
answer
208
views
What is machine-assisted formalization of proofs good for? And when to do it?
I have been watching Terry Tao's lecture on machine-assisted proofs https://www.youtube.com/watch?v=AayZuuDDKP0&t=1460s.
However in terms of the formalization of proofs via systems like Lean or ...
- 102k
4
votes
1
answer
523
views
Are there axioms in a natural deduction system?
In the Hilbert system, a proof may include some axioms. In a natural deduction system, it seems no axiom is involved, at least from the examples I read in logic books. So, I wonder how axioms such as ...
- 233
2
votes
2
answers
179
views
Natural deduction - prove a theorem
I am currently taking a course in "Introduction to Mathematical Logic" and I have been trying to do this proof, but everything I did just lead me to nowhere... Could anyone give me a ...
- 17.4k
1
vote
2
answers
197
views
Circularity in the argument that Gödel's incompleteness theorems undermine Hilbert's program
I'm only familiar with the very basics of mathematical logic, but over the last few days I have been looking into Gödel's incompleteness theorems and it seems to me (but I might simply be grossly ...
- 1,773
0
votes
1
answer
86
views
adding axioms to K logic [closed]
Let $K$ be the modal logic extending classical propositional logic by adding the necessitation rule
N: if $\vdash A$, then $\vdash \square A$
and the distribution axiom
K: $\square(A \rightarrow B) \...
- 1,084
9
votes
1
answer
570
views
Deriving A, ¬A ⊢ B in a weak Hilbert proof system
I am asked to derive A, ¬A ⊢ B in the following supposedly weaker system:
Axiom 1: $A \rightarrow (B \rightarrow A)$
Axiom 2: $(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \...
- 523
1
vote
0
answers
63
views
Directly verify ring axioms for a ring with $2$ elements [duplicate]
I'm relearning mathematics from the ground up in order to keep up with it's rigor in the university I attend. I'm doing this with serge langs basic mathematics, which thankfully involves writing ...
- 25
2
votes
0
answers
158
views
How to get comfortable with proofs includes algebra and inequalities
I'm self studying Baby Rudin and trying to do exercises, i got stuck at exercise 2.18 then looked up the answer from solution manual but the proof includes so much algebra for me to understand where ...
- 45
2
votes
1
answer
248
views
I don't understand this definition of a derivation
Here is a definition of a derivation
How can we, for the first time, obtain a derivation with a hypothesis to use, for example, $(2\rightarrow)$?
More specifically, to prove, for example, $\vdash\phi\...
- 10.7k
2
votes
3
answers
2k
views
natural deduction proof
Need help with the steps for natural deduction:
P1. $(A \rightarrow B) \rightarrow (C \rightarrow A)$
P2. $A \wedge (C \leftrightarrow B)$
P3. $(A \lor C) \to (A \to B)$
$\therefore B \vee A$
...
- 131k
3
votes
2
answers
389
views
Find a natural deduction proof to show ∃x∃y (S(x,y) ∨ S(y,x)) ⊢ ∃x∃y S(x,y) by predicate logic.
I'm trying to prove $\exists x \exists y (S(x,y) \lor S(y,x)) \vdash \exists x \exists y S(x,y)$ in natural deduction, and I have already applied existential elimination to get $S(x_0,y_0)$, with $x_0$...
5
votes
0
answers
219
views
How do I play type theory? What are the rules?
What I (think) I know:
Type theory is a game where you construct trees from strings. As far as I can tell, the rules of the game are roughly those of a Gentzen system whose "propositions" ...
- 5,070
10
votes
7
answers
6k
views
What is the theorem that has the most proofs?
Classical theorems like the irrationality of $\sqrt{2}$ or the infinitude of the primes have lots of proofs. But one theorem in particular, which I studied years ago in an introductory course of ...
- 3,955
0
votes
0
answers
90
views
Proving that If $\lim_{h \to 0} \frac{a^h-1}{h}=1$, Then $a$ = Euler's Constant
I want to prove that if $$\lim_{h \to 0} \frac{a^h-1}{h}=1$$ then $a$ must equal Euler's constant, denoted as "$e$."
However, I have some specific constraints for this proof:
1.$e$ is ...
- 581
3
votes
3
answers
245
views
What is an example of a proof that uses the principle of explosion/ex falso quodlibet?
I am reading through Mathematical Logic by Ian Chiswell and Wilfrid Hodges. In chapter 2 they introduce natural deduction rules. Before stating a rule, the authors (usually) motivate the rule by ...
- 102k