# 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
675 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 ...
620 views

291 views

In a Hilbert-style system, the axiom schemes can be written as (From Bourbaki, Book I): S1. If $A$ is a relation in $\mathscr C$, the relation $(A\text{ or }A) \Rightarrow A$ is an axiom of $\... 4answers 219 views ### How to prove$C$from$A \leftrightarrow (B \leftrightarrow C)$and$A \leftrightarrow B$? How does one prove$C$from the premises:$A \leftrightarrow (B \leftrightarrow C)$and$A \leftrightarrow B$? I've tried to prove$C$by contradiction, using a sub-proof which presumes$\neg ...
42 views

$((𝑃 \land \lnot 𝑄) \lor (𝑄 \land \lnot 𝑅)) \lor (\lnot 𝑃 \lor 𝑅) \equiv (\lnot P \lor (P \land \lnot Q)) \lor (R \lor (Q \land \lnot R))$ For the equivalence above, I am not sure how we get ...
79 views

### Understanding ex falso quodlibet together with proof by contradiction in a Gentzen style ND Proof

I began studying some formal logic for possible future proof and type theory dives. I am at the very beginning, Gentzen style natural deductions. Some of these proof rules defies my intuition so I ...
83 views

154 views

45 views

### Why typeclasses rather than inductive types to define mathematical structures in Lean?

I am not sure whether this is the right forum for this question, but I am not sure where else to ask (There is no Lean forum afaik). In the Lean Prover mathlib library, typical mathematical ...
84 views

### Proof using natural deduction (Tautology)

I've been asked to prove the following tautology via natural deduction: $\forall x \, (\lnot Px \lor Qx) \rightarrow (\forall y \, Py \rightarrow \forall z \,Qz)$ I normally use tree proofs, but I ...
551 views

### Fitch System For logic proofs

Does anyone know the Fitch program/ system used for logical proofs ? I am stuck with using fitch to construct a proof of¬(¬A∨¬B) from the premises A and B ... This is how it looks like in ...
220 views

### How to prove this sequent using natural deduction?

How do I prove $$S\rightarrow \exists xP(x) \vdash \exists x(S\rightarrow P(x))$$ using natural deduction? Just an alignment of which axioms or rules that one could use would be much appreciated.
248 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. ...
561 views

### Why are auxiliary lines valid in geometric proofs?

This probably seems like a super basic question, but I'm only on the level of an Honors Geometry course right now. Anyways, I don't understand why auxiliary lines are valid in proofs. Wouldn't they ...
410 views

### Differences between constructivism and formalism

What are the main differences between the formalism and constructivism in mathematics? Is there some theorem or axiom valid in formalism which isn't valid in constructivism and vice versa? Is the ...
1k views

### Fitch-Style Proof [closed]

Hi I'm having trouble solving a Fitch Style Proof and I was hoping someone would be able to help me. Premises: $A \land (B \lor C)$ $B \to D$ $C \to E$ Goal: $\neg E \to D$ Thank You
117 views

### Trouble with negation introduction with Fitch natural deduction proof

I've recently posted another question regarding natural deduction proofs and I've definitely made some progress, but I'm now stuck with a proof which seems like it could be flawed. Now as you can see,...
118 views

### How to prove the following formula using an indirect proof

I need to prove that the premise $A \to (B \vee C)$ leads to the conclusion $(A \to B) \vee (A \to C)$. Here's what I have so far. From here I'm stuck (and I'm not even sure if this is correct). My ...
82 views

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

I'd appreciate some help or at least a hint for the following exercise: Construct a (as simple as possible) deductive system where all sequences of the form $1^n$ (which means 111... $n$-times) is ...
67 views

### Equivalence in Natural deduction in First-order logic 2

I would want to check with you guys if I've done the following natural deduction correct. The reason being that I haven't gotten any answer sheet for this task. Task Solve the following with natural ...
384 views

### Diagonal of a Rectangle [duplicate]

The Pythagoreans proved that the length of the diagonal of a square with side length 1 is not a rational number. Prove that the length of the diagonal of a rectangle with sides length 1 and 2 is not a ...
41 views

### How can I prove the following with natural deduction rules? ¬∀x∃yP(x,y) ⊢ ∃x∀y¬P(x,y)

I have been stuck with this problem for a long time, I tried reductio ad absurdum and I got the hypothesys [¬∃x∀y¬P(x,y)], then I try to eliminate the negation of the premise, but I have to prove ∀x∃...
91 views

465 views

### Proving that $ax^2 + bx + c = dx^2 + ex + f$

So given $ax^2 + bx + c = dx^2 + ex + f$ and that it holds true for all values of x: Prove $a = d$, $b = e$, and $c = f$. What I have done so far is set the equation equal to zero and factor ...
### Proof help: Prove that $x^2+y^2+z^2 \geq xy+xz+yz$ [duplicate]
$x^2+y^2+z^2 \geq xy+xz+yz$ for all real numbers, x, y, and z. I'm not very good with working inequality proofs. Can someone help me prove this? The technique doesn't really matter.