Questions tagged [formal-proofs]
For questions about proofs within a formal system, such as natural deduction or Hilbert system.
823
questions
0
votes
1
answer
30
views
Proving an if and only if statement using two contrapositive statements
I'm currently working on proving an iff statement and was wondering is it allowed for me to prove the two statements required to prove an iff statement using two contrapositive statements.
(for ...
- 11
0
votes
1
answer
72
views
Examples of in ZFC, rules of inference and logical axioms
I was reading an introduction of ZFC set theory I found:
https://ia803008.us.archive.org/31/items/A_C_WalczakTypke___Axiomatic_Set_Theory/Lecturenotes2006-2007eng.pdf
Chaper 1 covers the idea of "...
- 553
1
vote
3
answers
73
views
How to write it formally? Convergence of an infinite sum
I know that the following sum $$\sum_{n=1}^{\infty} \frac{1}{\sqrt{1+2n}} e^{-\sqrt{n}}$$ converges because it's basically looking at $$\sum_{n=1}^{\infty} \frac{1}{\sqrt{n}} e^{-\sqrt{n}} \sim \int_{...
- 146
0
votes
0
answers
38
views
How to generate iid random variables?
Suppose I want countable many $X_i$ that are iid to e.g the Gamma distribution $\Gamma(k,\theta)$. How do I actually construct these, given the usual definitions of random variables/measureable ...
- 3,038
0
votes
1
answer
45
views
Are there any ternary inference rules in propositional logic?
Every transformation rule I've seen in the context of propositional logic proofs have an arity of 1-2, with citations looking like
...
- 21
0
votes
0
answers
57
views
Do order of lines matter when applying inference rules?
The wikipedia shows the form of Modus ponens as
1. If P, then Q.
2. P.
3. Therefore, Q.
With 1 being the implication and ...
- 21
1
vote
2
answers
85
views
Why is Simplification considered an inference rule instead of a replacement rule?
The wiki entry for Conjunction Elimination, sometimes called simplification elsewhere
$$
{\frac {P\land Q}{\therefore P}}
$$
is classified as an inference rule, rather than replacement rule.
This ...
- 21
2
votes
1
answer
245
views
Is my proof of $1+1=2$ correct?
Here is the proof:
Note: I will denote the successor of a natural number $n$ by $(n++)$
If one assumes the Peano axioms then they may define addition as follows:
$0+m:=m$
$(n++)+m=(n+m)(++)$
$\forall ...
- 1,113
1
vote
0
answers
26
views
Interpretation of a proof by contrapositive in a small subset of the integers
So, i'm having a little problem on interpretating a result that i'm obtaining regarding a proof by contrapositive. Suppose we want to prove, by contrapositive, the following statements:
Let $S$ = $\{2,...
0
votes
0
answers
71
views
Is this formal proof of the "Proof by Contradiction" derivation rule correct?
I started out with Shawn Hedman's "A First Course in Logic: An Introduction to Model Theory, Proof Theory, Computatibility, and Complexity" to learn the very basics. When I got to "...
- 163
0
votes
0
answers
19
views
first order logic - Fitch Formal Proof Question
I'm doing this by myself over the summer and I'm really confused about construct formal proof with Fitch. Currently stucked on a problem that is asking me to derive
Dodec(f) from Dodec(e), ¬Small(e), ...
2
votes
0
answers
79
views
Is the contradiction 1=0 a valid contradiction for a proof?
I am new to proper mathematical proofs and was attempting to prove:
A prime number cannot be a perfect number.
Here is my go:
suppose n is a prime number.
Therefore the only divisors of n, are n and 1 ...
- 1,113
1
vote
1
answer
70
views
What is the difference between proving an equation versus verifying LHS = RHS?
I am referring to the book Mathematical Proofs: A Transition to Advanced Mathematics (3rd Edition) . In the chapter 4.4, I came across the following example -
Prove ...
- 23
0
votes
0
answers
48
views
If $\Sigma\vdash A \lor B$ then $\Sigma \vdash A$ or $\Sigma \vdash B$
I'm a new student for Mathematical Logic and I am trying to solve this question:
In Hilbert proof system, prove or disprove the following: if $\Sigma\vdash A \lor B$ then $\Sigma \vdash A$ or $\Sigma \...
- 401
0
votes
1
answer
76
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$,$\...
0
votes
1
answer
73
views
Advice on proof-based exercises and more theoretical math subjects [closed]
i am a soon to be graduate in physics and i am considering to do a master in the theoretical physics area, but i find myself a little bit "unfaithfull" of my mathematical skills.
Let me ...
- 13
1
vote
0
answers
53
views
Reflection principle for finite subsystems of PA.
I would like to clarify the reasoning behind the proof of reflection schema for finite subsystems of PA that I found in "The Blind Spot" book.
To be wore precise, we have a finite subsystem $...
- 328
2
votes
0
answers
51
views
Software Recommendation for Theorem Suggestions
So I am not sure if this software already exists or perhaps this is something that humanity has to embark on to finally have as a product. A bit about myself, I am student training in a sub-area of ...
- 85
1
vote
2
answers
113
views
For any sets $A, B, C$ within a universal $U$ set, prove that $A\cup B \subseteq C$ iff $(A \cup C)\cap (B \cup C) = U$ [closed]
For any sets $A, B, C$ within a universal $U$ set, prove that $A\cup B \subseteq C$ iff $(A \cup C)\cap (B \cup C) = U$
Confused on how to do this, any help would be great.
Correction: Accidentally ...
- 75
4
votes
1
answer
158
views
Reasoning in natural language vs. reasoning in formal language
In ZFC set theory, we first used axioms to prove the existence of the set of natural numbers based on its definition, and after proving uniqueness, we introduced $\mathbb{N}$ in a new symbolic system ...
- 1,786
0
votes
0
answers
106
views
How to derive $ \forall x \exists y \forall z \exists w \;\; (Q(x, y) \lor \lnot Q(w, z))$?
I have to give a natural deduction proof of the statement:
$$ \emptyset \;\; \vdash \;\; \forall x \exists y \forall z \exists w \;\; (Q(x, y) \lor \lnot Q(w, z)) $$
This is a valid formula as per ...
- 2,098
0
votes
0
answers
73
views
Divergent subsequence of a divergent sequence
If a real sequence $X$ is divergent, then does a divergent subsequence $X'\neq X$ exist.
I know how to prove this for a specific limit. That is if X does not converge to L then there exist a ...
- 19
0
votes
0
answers
115
views
Prove the recurrence relation $T(n) = 2T(n/2) + n$ is equal to $n\log(n) + n$ using induction
Question
Given the recurrence relation for the Merge Sort algorithm:
$T(n) = 1$, if $n = 1$
$T(n) = 2T(n/2) + n$, if $n > 1$
Prove by induction that $T(n) = n\log(n) + n$ and hence $O(n\log(n))$
My ...
2
votes
1
answer
71
views
Proof of distributivity of $\land$ over $\lor$ using disjE in natural deduction
I'm learning about natural deduction from https://www.inf.ed.ac.uk/teaching/courses/ar//slides02.pdf
I'm trying to understand its proof of
$$
P \land (Q \lor R) \vDash (P \land Q) \lor (P \wedge R)
$$
...
0
votes
1
answer
49
views
How to prove an inequality through induction
I am taking real analysis this semester and am confused on how to prove this inequality. It is
$\sqrt{2k+1} - 1 < 1 + \frac{1}{\sqrt{3}} + \cdots + \frac{1}{\sqrt{2k-1}} \leq \sqrt{2k-1} $
I was ...
2
votes
2
answers
118
views
How to derive a function that maps a list to its possible "bracketings"? Recursion?
Let $[n] = \{m \in \mathbb{N}: m < n\}$.
Suppose $\Sigma$ is a set and $\Sigma^*$ is the set of sequences on $\Sigma$. That is $\sigma \in \Sigma^*$ means there exists $n\in \mathbb{N}$ such that $\...
- 1,200
5
votes
0
answers
80
views
How to enforce no abuse of definitions?
I am writing a proof assistant, in which a user can define a propositional calculus, and start creating theorems, which are automatically verified.
The problem I have ran into, comes from that I want ...
- 4,448
3
votes
3
answers
184
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.
...
- 31
2
votes
1
answer
57
views
When can we safely treat $dx$ like it were a real number during integration by substitution
$\def\R{\mathbf{R}}$
Disclaimer. I am aware that this is similar to this post, but the difference here is I'm asking, when can we safely treat these 'infinitesimal' quantities as though they were real ...
- 399
0
votes
0
answers
34
views
Logic-Provide a formal proof (A ∨ B) ∨ C , A → E , B ↔ E , C → E ⊢ E
Prove (AvB)vC,A->E, B<->E,C->E|=E
My work so far: enter image description here
1.) (AvB)vC :PR
2.) A>E :PR
3.) B<->E :PR
4.) C>E :PR
5.) A:AS
6.) E:->E2,5
7.) --
8.) ...
- 1
0
votes
0
answers
14
views
DFS Algorithem and Formallization
Let $G=(V,E)$ be a simple undirected graph with $|V|=4$. Some run of DFS produces a spanning tree in which the root has degree 2.
Claim: $|E|\leq 4$.
Basically I know it's true but I have no idea how ...
- 11
0
votes
0
answers
85
views
Trying a new axiomatization of the real line
Let:
$A$ be a non empty subset of $\mathbb{R}$
$A_U$ be a set of all real upper bounds of $A$
SOME DEFINITIONS:
$A$ is bounded below and $A$ is not bounded above. Then
$A$ has no gap $\iff$
$(\forall ...
- 536
1
vote
0
answers
39
views
Proof by induction involving an inequality and $n!$ [duplicate]
Proposition:
$$
P_n \ : \sqrt[n]{n!} \le \frac{n+1}{2} , \hspace{0.5em}\forall n \in \mathbb{Z}^+
$$
Proof:
$$
P_1 : \text{Let} \ n=1 , \hspace{1em}\sqrt{1!} \le \frac{1+1}{2} \implies 1 = 1 , \ \...
- 55
0
votes
0
answers
23
views
Is there a formal system that proves its consistency while proving the existence of a stronger formal system that can interpret general recursion too?
So looking at theorems like incompleteness, it is clear that such properties cannot be found from within. But when we take a more vague approach like simply requiring existence, do these restrictions ...
- 543
1
vote
2
answers
50
views
Is this predicate logic derivation valid?
Could someone please be so kind as to check the validity of my predicate derivation? I am trying to prove that the set $\{(\forall x)\lnot(\exists y)Gxy,(\forall z)[Hz\implies(\exists z) Gzy],(\exists ...
- 1,377
0
votes
0
answers
19
views
Sources for computer-recognizable first-order logic proofs
When reasoning about proofs, it's tempting to construct them as simply as possible:
A sequence of lines where every line is an axiom or a deduction
Deductions should be very precise: "If a ...
- 2,646
3
votes
3
answers
166
views
Why does natural deduction get its name?
For example, I want to prove $\psi$ from the assumption $\{\varphi,\varphi\to\psi\}$ , the "most natural" proof would be:
$\varphi$
$\varphi\to\psi$
$\psi$(MP)
But using natural deduction, I ...
- 127
0
votes
0
answers
44
views
Please help me to anwser (V)
The functions f(n) and g(n) are defined for positive integers n as follows:
f(n) = 2n + 1, g(n) = 4n.
This question is about the set S of positive integers that can be achieved by applying, in some ...
- 23
0
votes
0
answers
47
views
Why exist two kinds of definition for formal proof?
There are two kinds of definition for formal proof in the logic books I read.
One is:
Let 𝜑 be an ℒ-formula and 𝑇 be an ℒ-theory. A formal proof
of 𝜑 in 𝑇 is a finite sequence of ℒ-formulas (𝜑0, ....
- 127
0
votes
2
answers
346
views
Suppose T ∈ L(U,V) and S ∈ L(V,W) are both invertible linear maps. Prove that ST ∈ L(U,W) is invertible and that $(ST)^{-1} = T^{-1}S^{-1}$.
Suppose T ∈ L(U,V) and S ∈ L(V,W) are both invertible linear maps. Prove that ST ∈ L(U,W) is invertible and that $(ST)^{-1} = T^{-1} S ^{-1}$.
I'm not sure how to solve this proof? I'm stuck now. Is ...
- 1
-1
votes
3
answers
71
views
Can somebody explain quantifier negation equivalence? [closed]
I am unsure of how to prove that the following statement of First Order Logic holds:
$$ ¬∀x¬P(x) ↔ ∃xP(x)$$
The proof scheme available to me is that I cannot use axioms (such as De Morgan's Laws) and ...
- 13
1
vote
1
answer
1k
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 ...
- 29
0
votes
0
answers
66
views
Gödel's Completeness Theorem for uncountable domains
My texts give a proof Gödel's Completeness Theorem for the predicate calculus for countable domains. The theorem briefly says, if a predicate letter formula is valid in the domain of the natural ...
- 1,055
1
vote
0
answers
27
views
Without angle measure, how to I prove that if a ray bisects a vertical angle on one side that it's opposite ray bisects the other side?
Modern Geometry. Here's the question: "Say that ABC and DBE so that angle ABD and angle CBE are vertical angles. Show that if r is a ray emanating from B such that it bisects one of angle ABD or ...
1
vote
1
answer
64
views
Having trouble with this proof
I have to prove the following:
(((p ∨ q) ≡ (r ∨ s) ≡ (p ∨ q ∨ r ∨ s)) ∧ t ∧ u) → (r ∨ s). The proof is supposed to be relatively simple according to the professor but I have no clue where to start. ...
- 13
1
vote
1
answer
75
views
F is a field that contains 4 elements {0,1,a,b} , given ab=1, prove that a^2 = b
How do I prove that a^2 = b using the field axioms of closure, associativity, commutativity, multiplicative and additive identities, negatives and reciprocals, and distributivity?
My current attempt ...
- 51
0
votes
1
answer
50
views
Prove that if P(A) = P(A,B), then A is a subset of B.
I'm struggling a lot on this problem.
This feels intuitionistically true, since if their probabilities are equal, that means that the joint probability did not affect the size of the sample space that ...
1
vote
1
answer
115
views
How do we formally define powers/exponentiation in the theory of the reals?
Assume the second-order theory of the real numbers (it has to be second-order for categoricity) and suppose that we've already gone through the trouble of proving the existence and uniqueness of the ...
- 4,634
0
votes
0
answers
38
views
Proof by Contradiction with Definition of odd Issue with Z domain
I am trying to prove that if $x$ is even, then $x^2 + 4x + 2$ even.
When completing a proof by contradiction I reach this point where I need to use a fraction to get it in the form of the odd ...
user1094246
0
votes
2
answers
50
views
Inductive case choice when proving by induction
Sometimes I see proofs where the induction case is stating that the statement is true for all $x$ smaller than $n$, and that it needs to be proven for $n$.
And sometimes it is true for $n-1$, and ...
- 61