# Questions tagged [formal-proofs]

For questions about proofs within a formal system, such as natural deduction or Hilbert system.

531 questions
Filter by
Sorted by
Tagged with
48 views

### Let $Y = \{y_n\}$ be defined inductively by $y_1=1$ , $y_{n+1} = \frac 14\left(2y_n +3\right)$. Show that $\lim_{n\to \infty}y_n=\frac 32$

Let $Y = \{y_n\}$ be defined inductively by $y_1=1$ , $y_{n+1} = \frac 14\left(2y_n +3\right)$. Show that $$\lim_{n\to \infty}y_n=\frac 32$$ This is a problem from Bartle's Introduction to Real ...
1k views

### Given ∃y.∀x.p(x,y), use the Fitch system to prove ∀x.∃y.p(x,y).

I have a problem to solve this question. I thought I should eliminate the existential first but it seems not work..Not sure how to use the existential condition to prove the later one. Here's the ...
96 views

### Implication Introduction in reverse way

In Gentzen system, there is an inference rule such that one can deduce $\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B}$ from $\Gamma, \mathfrak{A} \to \Delta, \mathfrak{B}$. Can we, in ...
3k views

### Use Fitch system to proof ((p ⇒ q) ⇒ p) ⇒ p without any premise. ONLY FOR FITCH SYSTEM.

I know here has few similar questions, but I cannot figure out with those answer. Since for Fitch system, I can only use And Intro, And Elim, Or Inro, Or Elim, Neg Intro, Neg Elim, Impl Intro, Impl ...
92 views

### Proving $∀x (x ≠ 0 → gcd(x, 0) = x)$ formally attempt

I have proved $a≤gcd(a,0)$ in my attempt to prove $∀x (x ≠ 0 → gcd(x, 0) = x)$ but I am having trouble proving $gcd(a,0)≤a$ see below: I have access to the normal rules of natural deduction and the ...
4k 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 ...
53 views

### Attempt to prove the $∀d∀x∀y (d | x ∧ d | y ∧ x ≤ y → d | y- x)$ property of the “divides” relation for non-negative integers

I am attempting to prove the $∀d∀x∀y (d | x ∧ d | y ∧ x ≤ y → d | y- x)$ property of the “divides” relation for non-negative integers, but am having a little difficulty and am hoping someone can help. ...
601 views

### What are some good proofs to read? [closed]

I have just started my second year in a maths degrees and I am interested in reading mathematical proofs, I find the proofs to everything I do in class fascinating so I'm looking for some proofs to ...
58 views

### Different kind of proofs.

In mathematics the four color theorem have been proved by letting a computer checking each case, thus proving that each map can be colored by only four colors. However, this made me think about the ...
121 views

### Prove $\sqrt{n+1} < \sqrt{n} + 1$ [duplicate]

Prove $\sqrt{n+1} < \sqrt{n} + 1$ for all $n \ge 1$. I have proven the base step for $n = 1$. $\sqrt{2}$ is less than $2$. The inductive hypothesis is $\sqrt{n+1} < \sqrt{n} + 1$. From here, I ...
131 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 ...
52 views

### The product of any nonzero irrational number and any integer constant is irrational. [closed]

Can anyone help me find the counterexample to this problem?
521 views

### Prove commutative law of multiplication using peano axioms.

That is, prove $∀x∀y(x \cdot y=y \cdot x)$. I have tried induction but it seems not work well. It may require the rule of additive cancellation to be proved. could someone please prove it please? ...
247 views

### Prove cancellation law using peano axioms.

Using Peano axioms, prove $∀x∀y∀z(x+y=x+z→y=z)$. I have been stuck on it for some time, could someone please give a proof? Thanks!
104 views

### How do I find the contradition in this indirect proof?

I'm utterly stuck with no where to go. The assignment is to complete the indirect proof. I'm stuck on the following step, and have no clue how to proceed. Where do I go? Also, pardon the poor ...
55 views

### Are $A, B, C \vdash D$ and $A, B\vdash C \rightarrow D$ interchangeable?

For an assignment we have to make a proof in the Hilbert system. And my proof hinges on the following operation being allowed: $A, B, C \vdash D\tag 1$ Becomming: $A, B\vdash C \rightarrow D\tag 2$ ...
106 views