Questions tagged [formal-proofs]

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

Filter by
Sorted by
Tagged with
3
votes
4answers
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 ...
3
votes
3answers
620 views

Prove that there are no positive integers $a$ and $b$, such that $b^4 + b + 1 = a^4$

So I've been trying to solve this problem for a couple of days now. What I've come up with is this: By way of contradiction, assume that there are positive integers a and b such that $b^4 + b + 1 = a^...
3
votes
1answer
129 views

Proof that for any $16$ digit number there is at least one sequence of $1$ or more digits which its product is a perfect square

I came across this problem where one is asked to proof that, for any $16$ digit number there is at least a sequence of $1$ or more digits which its product is a perfect square. For example, in the ...
3
votes
3answers
71 views

Natural deduction proof: $C, (C \land D)↔F \vdash (D \land E) \to F$

I'm having trouble with proving C, (C Λ D) ↔ F |- (D Λ E) → F If it were $\lor$ instead of $\land$, then I would be able to do it. If I can prove that $(C ...
3
votes
2answers
291 views

The intuitive meaning of “or” and “implies” in axiom schemes of a logical theory

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 $\...
3
votes
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 ...
3
votes
2answers
42 views

Could provide some further detail about this step in a proof

$((𝑃 \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 ...
3
votes
3answers
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 ...
3
votes
1answer
83 views

Is there a proof of $\lnot \forall x, P(x) \iff \exists x, \lnot P(x)$

I am interested in how one would formally prove: $\lnot \forall x, P(x) \iff \exists x, \lnot P(x)$ I realize that it's basically saying that: $\lnot(P(x_0) \land P(x_1) \land ... \land P(x_n)) \...
3
votes
2answers
95 views

How to use natural deduction to show $\neg (P \land Q) \vdash \neg P \lor \neg Q$?

How to use natural deduction to show $\lnot (P \land Q) \vdash \lnot P \lor \lnot Q$? I think I need to first assume $\neg(\neg P \lor \neg Q)$ and then find a contradiction but I cannot see how to do ...
3
votes
2answers
76 views

Using a Hilbert system to show the correctness of a few logical arguments

I have system: $(A1)\qquad A → (B → A)$ $(A2)\qquad (A → B) → ((A → (B → C)) → (A → C))$ $(A3)\qquad (A → B) → ((A → \neg B) → \neg A)$ $(A4)\qquad \neg \neg A → A $ $(MP)\qquad \frac{A \quad A ...
3
votes
3answers
154 views

A Natural-Deduction proof of $ \{ \neg N,\neg N \to L,D \leftrightarrow \neg N \} \vdash (L \lor A) \land D $.

I would like to prove $\{ \neg N,\neg N \to L,D \leftrightarrow \neg N \} \vdash (L \lor A) \land D $. My work until now is as follows: $$ \begin{array}{l|ll} 1 & \neg N ...
3
votes
1answer
79 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$...
3
votes
2answers
32 views

Formal proof of distributivity of conjuction

I'm trying to prove that $\vdash p\land (q\lor r)\to(p\land q)\lor (p\land r)$ in natural deduction. ...
3
votes
3answers
92 views

Formal proof of one of De Morgan's laws

How to give a formal proof of $\vdash \neg (p\land q)\to\neg p\lor \neg q$ in the natural deduction proof system? Here is what I have: ...
3
votes
3answers
86 views

Equivalence in natural deduction in First-order logic

Task $\vdash \exists x (P(x)\lor Q(x)) \iff \exists xP(x) \lor \exists xQ(x) $ My answer If we have $A \iff B$ then $A\vdash B$ and $B \vdash A$. So I started trying to see if I could prove $B$ ...
3
votes
2answers
71 views

How would I show that X is equivalent to ((¬X ↔ X ) ∨ X )?

I use the https://en.wikipedia.org/wiki/Fitch_notation, or fitch notation, for logical deduction systems. I don't know how to derive a contradiction in the other half of the biconditional where $X \...
3
votes
2answers
82 views

Propositional Logic: Prove $(p \land \lnot q) \to \lnot p \vdash p \to q$.

I'm having a lot of trouble trying to solve this. Any help would be greatly appreciated, I just can't seem to go any further! "Give syntactic proofs for the following sequent using only propositional ...
3
votes
2answers
1k views

Formal proof with first order logic axioms.

How do I formally prove the following: $$[\forall y Gy \wedge \exists x Hx] \iff \exists x[\forall y Gy \wedge Hx]$$ and by formally I mean using premises and whatever other first order logical ...
3
votes
1answer
165 views

Should $x$ be not free in $\beta$ to prove $\vdash [ \forall x(\beta\rightarrow \alpha)\rightarrow (\exists x\beta\rightarrow \alpha)]$?

Should $x$ be not free in $\beta$ to prove $\vdash [ \forall x(\beta\rightarrow \alpha)\rightarrow (\exists x\beta\rightarrow \alpha)]$? In "Mathematical Introduction to Logic, Enderton" This is an ...
3
votes
2answers
89 views

Proof, is $\lnot p \land \lnot q \vdash p \iff q$?

I have derived the proof to some extent, mentioned below:- $$\begin{array}{rll} 1. &\lnot p \land \lnot q &\text{Premise} \\ 2. &\lnot p &\land\text{elim}...
3
votes
1answer
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 ...
3
votes
1answer
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 ...
3
votes
1answer
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 ...
3
votes
2answers
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.
3
votes
2answers
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. ...
3
votes
3answers
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 ...
3
votes
1answer
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 ...
3
votes
3answers
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
3
votes
2answers
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,...
3
votes
3answers
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 ...
3
votes
1answer
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 ...
3
votes
1answer
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 ...
3
votes
1answer
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 ...
3
votes
1answer
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∃...
3
votes
0answers
91 views

Formal proof of $\exists x (\exists y P(y) \rightarrow P(x))$ and $(\forall x \exists y R(x,y))\rightarrow (\forall y \exists x R(y,x))$

within the following axiomatic system I've beeb trying to proof the formulas (1) $\forall x \exists y R(x,y) \rightarrow \forall y \exists x R(y,x) \\$ and (2) $\\ \exists x (\exists y P(y) \...
3
votes
1answer
196 views

Conditional Statements/ Implication statements within a proof specifically linear algebra

I am sort of new to the mathstackexchange so excuse me for any mistakes that I make while writing this post. I've been working on proofs and ran into a conflicted view of how to prove conditional ...
3
votes
1answer
372 views

Proof with disjunctive conclusion

I'm after a natural deduction proof of the following sequent: (P & Q) → R : (P → R) ∨ (Q → R) The textbook I'm using says there is a 24 line proof, but the shortest I've managed is 29 lines. I'...
3
votes
0answers
124 views

Is there an intuitive way to understand the split between additive and multiplicative connectives?

For example, where $\otimes$ is multiplicative conjunction, our rules are: $$ \frac { \Gamma ,\: A,\: B\: \Rightarrow \Delta }{ \Gamma ,\: A\otimes B\Rightarrow \Delta } \quad \quad \frac { \Gamma \:...
3
votes
0answers
591 views

A simple proof of Descartes's rule of sign

I search all over the Internet for a proof of Descartes's rule of sign. Found a pdf file which has page-long proof that a high schooler has to no way to understand. Can somebody talented here give ...
2
votes
4answers
353 views

Direct Proof for sum of $n$ integers equation?

I am trying to prove by direct proof that $$3+5+7+\ldots+(2n+1)=n(n+2)$$ for all natural numbers $n$. I figured out how to do it by induction, but I know it can be done directly and I can't ...
2
votes
5answers
248 views

Prove that $(p \to q) \land (q \to r)$ is equivalent to $p \to r$

$(P\implies Q)\land(Q\implies R)$ is equivalent to $P\implies R$. Is this true? How to prove this directly, not using truth tables?
2
votes
2answers
1k views

Proof of FOIL Modern Algebra

I am trying to work through Birkhoff's A Survey of Modern Algebra independently, but am having difficulty getting off the ground with the proofs based on laws, rules, etc. I come from mostly soft ...
2
votes
4answers
336 views

Direct proof using summation

I'm trying to provide a general proof for the following theorem. Let $0 < n < 1000$ be an integer. If the sum of the digits of $n$ is divisible by $9$, then $n$ is divisible by $9$. The book ...
2
votes
3answers
495 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 ...
2
votes
1answer
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 ...
2
votes
3answers
159 views

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.
2
votes
2answers
98 views

Prove using Hilbert calculus $\forall x(Px\rightarrow x\equiv a)\vdash Pb\rightarrow Pa$, formal proof.

Prove: $\forall x(Px\rightarrow x\equiv a)\vdash Pb\rightarrow Pa$ Using Hilbert Calculus Format of solution: Step (my understanding) Solution: (1) $\forall x(Px\rightarrow x\equiv a)\vdash Pb\...
2
votes
1answer
762 views

How to proof ¬P∨Q entails P→Q by Natural deduction

I can easily proof 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 ...
2
votes
1answer
109 views

Strange sum of random variables

So guys, I'm having this hard proof to solve in probability. I don't really know how to tackle it! Hope that someone can help. Let $\{Z_i\}_{i\in\mathbb{Z}}$ be i.i.d. random variables with zero mean ...