# Questions tagged [formal-proofs]

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

536 questions
Filter by
Sorted by
Tagged with
2answers
99 views

2answers
115 views

### In proof writing, is it mathematically sound to prove uniqueness before proving existence?

As stated in the title, I'd like to find out is whether or not it is always mathematically sound to prove the uniqueness of something before proving the existence of said something. I am still ...
1answer
88 views

### Predicate Logic Natural Deduction: $∃x P(x) ⊢P(x)$

I am really puzzled right now. To solve the issue, I need to prove this formular: $$\exists x P(x) \vdash P(x)$$ with the natural deduction rules for propositional and predicate logic. I am ...
1answer
106 views

### What logic can express induction on natural numbers?

The induction theorem: $P(0) \land \forall n \in \mathbb{N}\{ P(n) \Rightarrow P(n+1)\} \Rightarrow \forall n \in \mathbb{N} \{P(n)\}$ My understanding is that nature numbers are constructed from ...
1answer
240 views

### How to show $\vdash (\neg\neg p \rightarrow p)$.

Given these axioms: where $\phi, \psi, \theta$ are formulas $$1.:(\psi \rightarrow (\theta \rightarrow \psi))$$ $$2.: ((\neg \psi \rightarrow \neg \theta) \rightarrow (\theta \rightarrow \psi))$$ ...
2answers
653 views

### Fitch style proof of $(\neg B \to \neg A) \leftrightarrow (A \to B)$

I have been stuck on this proof for a while. Here's where I'm at: Goal $(\neg B \to \neg A) \leftrightarrow (A \to B)$ l 1. $A \to B$ ll 2. $\neg B$ lll 3. $A$ lll 4. $B$ Elim 1,3 ...
1answer
37 views

### Proving the theorem $\forall a\in\mathbb{N},\forall m\in\mathbb{N},(m<a\Rightarrow m\leq a-1)$

I want to solve this proof by the method of Contradiction. Though without using the well ordering principle. I don't have any idea how to start. I have found other ways to prove this theorem but only ...
2answers
52 views

### Proof by contradiction - Getting my head around it

Hey there Math community! I have a general question on contradiction and it's getting difficult to get my head around it. Notes: I have some background in math and I have read several proofs by ...
4answers
107 views

### Proof of $(P\to Q) \vee (Q\to P)$ with natural deduction

I need to prove the following statement in natural deduction: $$(P\rightarrow Q) \lor (Q\rightarrow P)$$ I tried assuming not (target statement) and assuming the left hand side, but I don't know ...
2answers
385 views

### Proving that the norm of a Matrix is bigger or equal to it's smallest singular value multiplied by a vector.

I need to prove the following: Let $A \in \mathbf R^{n*n}$ be a real matrix and $x \in \mathbf R^n$ a vector.show that: $$\Vert Ax \Vert_{2} \geq s_{\min}\Vert x \Vert_{2}$$ where $s_{\min}$ is the ...
1answer
534 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? ...
1answer
773 views

### Natural deduction: negation of quantifiers

How can I show that $\lnot \exists x P(x) \vdash \forall x\lnot P(x)$ ? Because I want to show: $\lnot \exists x (P(x) \lor R(x)) \vdash \forall x \lnot R(x)$ My idea: maybe a proof by ...
1answer
122 views

### Tricky predicate logic problem

I'm having a hard time proving that this is a valid argument $Premise 1: (Ǝx)Kx→(\forall x)(Lx→Mx)$ $Premise 2: Kc • Lc$ $Conclusion: Mc$ I am getting confused with all the existential/universal ...
1answer
65 views

2answers
54 views

### Is this proof in natural deduction proof system correct?

Consider a natural deduction proof system. Suppose I know that $\vdash \phi$ (the sentence $\phi$ is provable from no premises). If I'm proving something like $\vdash \psi$, can I just use that $\phi$ ...
1answer
111 views

### When should I use RAA in natural deduction proofs?

I can't understand exactly when should I use RAA (reductio ad absurdum) rule in natural deduction proofs? What situation should "trigger" me to think "Now it's time to use RAA"?
2answers
81 views

### How do we formally define “j-th smallest element”?

Let $A$ be a nonempty finite subset of $\mathbb{R}$. Firstly, let me write down how to define the term "the smallest element of $A$" formally. Suppose 'for every $x\in A$, there exists $y \in A$ ...
2answers
64 views

### Construct a deductive system where $1^n$ is provable iff n is not prime

I'd appreciate some help for the following exercise: Construct a (as simple as possible) deductive system where all sequences of the form 1n (which means 111... n-times) is provable if and only if n ...
1answer
560 views