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
193 views

How do I formally prove a universal implication?

A textbook I am reading (Discrete Mathematics and its Applications by Rosen) went from introducing formal propositional and predicate logic (including popular rules of inference like Modus Ponens, ...
3
votes
4answers
693 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
644 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
5answers
229 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
3answers
73 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
293 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
1answer
121 views

What is the reason we usually don't use formal proofs in mathematics?

Is the reason for not using formal proofs very often in mathematics because it is usually too lengthy for a person to make such a proofs or the reason is that it is simply not possible for everything ...
3
votes
3answers
96 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
3answers
56 views

How can I eliminate two conflicting subformulas in two premises in a formal proof?

Problem: Prove that $P \lor S$ follows from the premises: $P \lor (Q \land R)$ and $(\lnot Q \lor \lnot R) \lor S$ So far I have been able to prove that $(\lnot Q \lor \lnot R)$ equates to $\lnot (Q ...
3
votes
2answers
44 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
1answer
85 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
101 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
80 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
155 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
2answers
97 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
88 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
951 views

Given ∃x.¬p(x), use the Fitch System to prove ¬∀x.p(x).

What I am thinking was I need two formulas, AX.p(X) => something AX.p(X) => ~ something I guess something maybe is the p(x) and the other is ~p(x) since we was given EX.~p(x)..But actually it can't ...
3
votes
2answers
33 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
123 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
90 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
77 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
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
173 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
90 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
195 views

Natural deduction proof - I don't' understand the question

I am supposed to give a natural deduction proof of $$(P_1∨P_2), \neg P_1 ⊢ P_2$$ My assumption is $(P_1∨P_2)$ and I am going to derive $P_2$ from $\neg P_1$ or I am wrong? EDIT: Or I am going to ...
3
votes
1answer
86 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
2answers
102 views

Is $A \& B \multimap A$ derivable?

Intuitively, the sentence $A \& B \multimap A$ seems to mean "Using a choice between $A$ and $B$, get an $A$." This feels like it should be derivable for any $A$ and $B$, but I haven't found any ...
3
votes
1answer
583 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
222 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
255 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
574 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
428 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
137 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
4answers
145 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
43 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
1answer
83 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
69 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
431 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
0answers
100 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
215 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
393 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
131 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
594 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
375 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
256 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
2k 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
507 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 ...