# Questions tagged [formal-proofs]

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

542 questions
Filter by
Sorted by
Tagged with
137 views

### Solving theorem proof with only primitive rules of logic!

I am having trouble solving the theorem proof of (P-> ~Q)->(Q->~P). I can only use primitive rules and I understand I have to use arrow introduction to introduce my antecedent, but after that I am a ...
59 views

### How to express induction when we just have finitely many instances, but still proceed inductively over them

Let $Q$ be some finite set with $n = |Q|$. Then suppose I want to show that for every nonempty subset $P \subseteq Q$ some property $A$ holds. One natural way to approach this is using induction, and ...
45 views

### Where to start on a basic derivation?

I have a problem I've been banging my head against for this derivation, I'm not really sure where to begin: $P\rightarrow Q, R\rightarrow S \vdash (Q\rightarrow R) \rightarrow (P\rightarrow S)$ I'm ...
692 views

### Using the Intermediate Value Theorem to prove the existence of a number$\;$

I'm having a bit of trouble with something most everyone might find trivial, and I feel rather silly asking, but here it goes. The premise is as follows: "Use the Intermediate Value Theorem to prove ...
44 views

### Prove by the method of Mathematical induction that $(1-0.3)^n \geq 1-0.3n$ for all $n$ in set of positive integers

Here is what I have so far Basis For $n = 0 (1-0.3)^0 \geq 1-0.3(0)$ checks For $n = 1 (1-0.3)^1 \geq 1-0.3(k$) checks I.H. $(1-0.3)^k \geq 1-0.3(k)$ for all k in the set of positive ...
544 views

### Fitch proof for $(p \implies (q \implies r)) \implies ((p \implies q) \implies (p \implies r))$ with no premises

I'm having trouble solving this problem using the Fitch system. As I understand Fitch, if the goal has the form $(φ \implies ψ)$, it is often good to assume $φ$ and prove $ψ$ and then use Implication ...
67 views

130 views

### Stuck on proving ($p \Rightarrow q) \land (q \equiv r) \Rightarrow (p\Rightarrow r)$

I'm in a Foundations of Computer Science course and it's all about logic and proofs. Some proofs are harder than others, and I'm completely stuck on this proof. It comes out of the textbook Texts and ...
178 views

### Deduction of $\vdash \forall x \phi \rightarrow \exists x \phi$

I can show that $\forall x \phi \vdash \exists x \phi$ through a direct deduction as follows, using axioms as defined in Enderton $(\forall x) \phi$ by hypothesis. $(\forall x) \phi \rightarrow \phi$...
276 views

52 views

### Is this an onto function?

Is f(m,n) = m^2 - 4 an onto function for a function that goes from Z x Z -> Z (Where Z means the set of all integers). I think it is an onto function, but I am not sure how to go about proving it. ...
59 views

### Proof by Induction Help: Prove that there are unique integers $a\geq 0$ and $k>0$ such that $n=(3^a)\cdot k$ and $k$ is not divisible by $3$.

Suppose $n$ is a positive integer. Using induction, prove that there are unique integers $a\geq 0$ and $k>0$ such that $n=(3^a)\cdot k$ and $k$ is not divisible by $3$. Note: I have already proven ...
70 views

### Constructing a counterexample

Premises: $p\implies m$, $m\implies t$, $m$. Conclusion: $m\implies p$ My goal is to provide a counter example for the following problem since it is not true. I am familiar with writing ...
112 views

### Basic Mathematics - Proofs - Proving rational numbers are equivalent to 1

I'm reading through Serge Lang's Basic Mathematics and I've fallen into trouble with a particular proof exercise: Let $a = \frac m n$ be a rational number expressed as a quotient of integers m, n ...
526 views

### (¬A ∨ B) is equivalent to B?

Is there any proof that states (¬A ∨ B) is equivalent to B? There was an example in my text book that had a step I didn't understand. It stated (¬A ∨ B) ∧ A → B is equivalent to B ∧ A → B. I don't see ...
254 views

### Constructive proof of Barber Paradox

Q1. Can Barber Paradox be proven false in constructive logic? I am following the lean tutorial by professor Jeremy Avigad et al. One of the exercises in section 4 asks to prove Barber Paradox false. ...
53 views

When reading the following problem, do you assume that each premise is true? So since number 2 states ¬ B am I to assume that ¬ B is true? Which would mean B is false? A ∨ C → D Premise ¬ B ...
### What's the strength of logic without $\neg\neg\exists x P(x) \implies \exists x P(x)$?
As far as I understand, the main idea of constructive logic is that we only allow proof methods that let us show the statement $\exists x:P(x)$ only by constructing an explicit such object $x$, right? ...