# Questions tagged [formal-proofs]

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

855 questions
Filter by
Sorted by
Tagged with
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 ...
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-...
1 vote
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 ...
881 views

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 ...
1 vote
205 views

1 vote
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 ...
1 vote
349 views

570 views

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$ ...
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$...
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" ...
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 ...
### 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 ...