Questions tagged [formal-proofs]

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

1
vote
4answers
106 views

Prove 𝑃′⋀(𝑃⋁𝑄)→𝑄 - How?

I'm going a course in computer science math, and I came across an exercise that is the following: Use the rules of equivalence and/or inference to prove: $\lnot P \land (P \lor Q)\rightarrow Q$...
0
votes
1answer
49 views

Is this an axiom or does it have to be proved?

a and b are positive integers and x is greater than 1. In Rudin principles of real analysis it is not given as an axiom but proving is seems difficult to me
2
votes
0answers
44 views

Strength of Asymmetric Tautology/Reverse Unit Propagation in proofs

Given a set of disjunctions in propositional logic, they can be said to entail another disjunction D if the negation of D, when added as a set of unit clauses to the original set, yields an ...
1
vote
0answers
70 views

Why, intuitively, are propositional resolution proofs so long?

I'm trying to gain an intuitive understanding of why propositional resolution proofs tend to be so long. As every essential prime implicant can be produced via resolution, intuitively I would have ...
0
votes
2answers
119 views

Let $u$ and $v$ be vectors in $\mathbb R^3$. Let $V=\{au+bv \mid a,b \in \mathbb R\}$. Prove that if $x$ and $y$ are in $V$, then $x+y$ is in $V$.

I'm having trouble writing this a proof for linear algebra. Let $u$ and $v$ be vectors in $\mathbb R^3$. Let $V=\{au+bv \mid a,b \in \mathbb R\}$. Prove that if $x$ and $y$ are in $V$, then $x+y$ ...
1
vote
1answer
390 views

Can we prove if ⊢ (α → β) and ⊢ (¬α → β) then ⊢ β in L0?

The system L0 is defined as follows: Axioms: A1 (α → (β → α)) A2 ((α → (β → γ)) → ((α → β) → (α → γ))) A3 ((¬β → ¬α) → (α → β)) The only rule of inference is Modus Ponens: MP From α and (α → β) ...
4
votes
3answers
434 views

Natural deduction proof of $(\forall x.P(x))\land(\forall y.P(y) \implies Q(y)) \vdash \forall z.Q(z)$

My attempt $(\forall x.P(x))\land(\forall y.P(y) \implies Q(y))$ [premise] $\forall y.P(y) \implies Q(y)$ [$\land$ elim 1] $\forall x.P(x)$ [$\land$ elim 1] $a, P(a)$ [$\forall$ elim 3] $a, P(a) \...
1
vote
0answers
76 views

Formally proving that $a_i\delta_{ij} = a_j$

Using the summation convention and the Kronecker delta ($\delta$), one can show that $$a_i\delta_{ij} = a_j.$$ If one expands the expression, one is looking at $$ a_i\delta_{ij} = a_1\delta_{1j} + ...
1
vote
3answers
149 views

How to prove $n\leq x \rightarrow x = n \vee Sn \leq x$ using Robinson Arithmetic

Given the definition $n \leq x \Leftrightarrow \exists y \ni y+n=x$, how can one prove $n\leq x \rightarrow x = n \vee Sn \leq x$ in Robinson Arithmetic? I think this should be a proof by induction, ...
1
vote
1answer
149 views

Propositional logical equivalence in Lemmon style proof

I am doing a bit of propositional logic and I was wondering does Lemmon style of proofing allows writing logical equivalence of some propositions. There is an example of biconditional that you can ...
1
vote
2answers
90 views

Prove P from B ∨ P when we have proven ¬B

I have the following proof so far: In step 9 I'm not sure how to prove P from the steps I have before. I thought that I could use ∨ Elim but I don't think I can now.
1
vote
2answers
51 views

How to prove A → N from A and (A ∨ B) → N in FOL

I have the following premises: A and (A ∨ B) → N How can I prove A → N from this in a formal proof using FOL?
2
votes
1answer
102 views

Proof of $\forall x \forall y(x+x \neq y+y+1)$ in Peano arithmetic

How to prove $\forall x \forall y(x+x \neq y+y+1)$ using the axioms of Peano arithmetic?
1
vote
6answers
57 views

How do you prove questions of the form: Show that $A\to \text{ B or C or D}$?

How do you prove questions of the form: Show that $A\to \text{ B or C or D}$? For example, suppose the question was: $$\text{(x = 10) $\to$($x+1 = 11$) or ($x+2 = 4$) or ($x-1 = 8$)}$$ I don't know ...
4
votes
1answer
88 views

$\Bbb Q_{\ge 0}$ elementary definable in $\mathfrak A$=($\Bbb Q$, $\cdot$)

I have this exercise which seems very simple, but I am not able to find a solution. Given a structure $\mathfrak A$=($\Bbb Q$, $\cdot$) Is $\Bbb Q_{\ge 0}$ elementary definable in $\mathfrak A$? ...
0
votes
1answer
40 views

If $R\equiv RR$, then $R\equiv \emptyset\text { or } R\equiv \epsilon\text{ or } L(R)\text{ is infinite}$

If $R\equiv RR$, then $R\equiv \emptyset\text { or } R\equiv \epsilon\text{ or } L(R)\text{ is infinite}$ This seems true to me just looking at it. For example if $R\equiv \emptyset$, then this ...
2
votes
3answers
134 views

A rigorous proof of ∀ m ∈ ℕ, 0 < m → 1 < 2 * m

There's a class of problems I struggle to prove by induction/recursion (I'm working in CIC). The best way I can describe this class of problems is "finite cases below m, inductive case above m". An "...
5
votes
2answers
486 views

Are there logics without modus ponens?

The question doesn't go beyond the title. And I don't mean logics that merely just don't have it as a primitive rule - I'm interested in logic where you can't actually use it. I've searched around ...
1
vote
1answer
127 views

The existence of unprovably unprovable statements provable in ZFC [duplicate]

I am aware of Gödel's second incompleteness theorem, the proven existence of several unprovable statements (in ZFC), and the possibility that a formal system may include statements that are unprovably ...
7
votes
1answer
2k views

Which subfields of math are easier or harder to formalize?

This is a follow-up question to Can all math results be formalized and checked by a computer?. Hopefully it's not too broad, but here goes: which subfields of math could be formalized using existing ...
1
vote
2answers
676 views

Are these conditional statements true?

This chapter is brewing in me a dislike for my Math book, sort of. It seems the reasoning applied to solve a particular problem is different from that used to solve another one. I've come with my ...
1
vote
2answers
170 views

Is simplification from 'or' ($\lor$) valid?

The question in my text is : Identify the error or errors in this argument that supposedly shows that if $\forall x (P (x ) \lor Q(x ))$ is true then $\forall x P(x) \lor \forall x Q(x)$ is true. \...
2
votes
1answer
187 views

Proving $C \vdash D \lor \neg D$ using natural deduction, and WITHOUT any additional hypotheses/assumptions?

I proved $(A \land \neg A) \vdash B$ by doing the following: \begin{array}{l l l} 1. & A \land \neg A & (\text{premise}) \\ 2. & A & (1, \text{ simplification}) \\ 3. & A \lor B &...
0
votes
2answers
103 views

formal Proof of an inequality

In trying to prove , $a\leq b\wedge b\leq c\Longrightarrow a\leq c$ I come up with the following: Proof: (intuitively) case 1: $a<b\wedge b<c\Longrightarrow a<c\Longrightarrow a\leq c$ ...
3
votes
1answer
367 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'...
-2
votes
3answers
270 views

Is $f(x, y) = 5x - 4y$ injective or surjective?

Define $f : \Bbb Z\times\Bbb Z \to\Bbb Z$ by $f(x, y) = 5x - 4y$. Is $f$ injective or surjective? How would I go about proving this? Thanks
2
votes
2answers
374 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 ...
3
votes
1answer
375 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 ...
2
votes
4answers
335 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 ...
1
vote
1answer
1k views

Formal proof in Fitch - How to prove contradiction in a biconditional?

I am asked to derive the conclusion $\bot$ from the premise: $P\leftrightarrow \neg P$ This is in the logic system of Fitch, the rules that I am allowed to use can be found here. I may not use ...
11
votes
2answers
331 views

Different proof that $\sqrt{2}$ is irrational

I found the following proof arguing for the irrationality of $\sqrt{2}$. Suppose for the sake of contradiction that $\sqrt{2}$ is rational, and choose the least integer $q > 0$ such that $(\sqrt{...
0
votes
1answer
306 views

Concerning Symmetric Transitive closure

Please Comment on the validity of presented proof of the given theorem. Theorem. Given that $R$ is a relation on $A$, and $S$ is the transitive closure of $R$, If $R$ is symmetric, then so is $S$. ...
0
votes
1answer
286 views

Fitch Notation Set Theory

I am wanting to show that $(A\cup B)-B\subseteq A$ by using Fitch Notation. I think it would be as follows. Would this be correct? I am unsure as to to label the assumption step and conditional ...
1
vote
1answer
105 views

Proving that this statement is a theorem of our proof system

So I need to produce a proof tree of the below statement using the introduction and elimination rules. $$ \begin{array}{c} x \in a &q \\ \hline \exists x \colon a \bullet q \\ \hline ((\exists ...
0
votes
1answer
72 views

Triangulation proofs

How can I prove that: $a)$ In every triangulation with $n$ nodes there is a node Degree $\leq 5$ $b)$ Each triangulation with $n$ nodes has at least $\frac{n}{27}$ pairs of non-adjacent nodes of ...
0
votes
2answers
134 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 ...
1
vote
2answers
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 ...
0
votes
2answers
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 ...
3
votes
4answers
671 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 ...
-1
votes
1answer
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 ...
4
votes
1answer
535 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 ...
2
votes
0answers
67 views

Elementary Hoare logic proof

I would like to prove that the following Hoare triple is correct by giving a full Hoare logic proof. (Assuming all variables are real.) How can I do so? $$\{c = 0\} ~ a := −c; ~ b := a + c; ~ c := a ~...
0
votes
0answers
39 views

Elementary proof that $\Bbb Z[\sqrt d]$ is an ordered ring

I'm trying to show that $\Bbb Z[\sqrt d]$ is an ordered ring, where $d$ is a positive non-square integer. This is obviously true given that $\Bbb Z[\sqrt d]\subseteq\Bbb R$, but here the catch is that ...
1
vote
3answers
290 views

Giving a formal proof of p ⇒(q ⇒ r) $\vdash$ (p ⇒ r)∨(q ⇒ r) using the rules of inference.

I can prove this with semantic equivalences and truth tables but I'm struggling on the formal proof using rules of inference front. Given its format I would assume it must finish on V-introduction ...
2
votes
2answers
911 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 ...
-2
votes
1answer
55 views

Consider the following proof on equivalence relations [closed]

Consider the following incorrect statement and flawed argument. False Statement. Let $A$ be a set and let $R$ be a relation on $A$. If $R$ is symmetric and transitive, then $R$ is reflexive. ...
1
vote
1answer
48 views

Let $Y = \{y_n\}$ be defined inductively by $y_1=1$ , $y_{n+1} = \frac 14\left(2y_n +3\right)$. Show that $\lim_{n\to \infty}y_n=\frac 32$

Let $Y = \{y_n\}$ be defined inductively by $y_1=1$ , $y_{n+1} = \frac 14\left(2y_n +3\right)$. Show that $$\lim_{n\to \infty}y_n=\frac 32$$ This is a problem from Bartle's Introduction to Real ...
1
vote
1answer
1k views

Given ∃y.∀x.p(x,y), use the Fitch system to prove ∀x.∃y.p(x,y).

I have a problem to solve this question. I thought I should eliminate the existential first but it seems not work..Not sure how to use the existential condition to prove the later one. Here's the ...
1
vote
2answers
96 views

Implication Introduction in reverse way

In Gentzen system, there is an inference rule such that one can deduce $\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B}$ from $\Gamma, \mathfrak{A} \to \Delta, \mathfrak{B}$. Can we, in ...
3
votes
1answer
3k views

Use Fitch system to proof ((p ⇒ q) ⇒ p) ⇒ p without any premise. ONLY FOR FITCH SYSTEM.

I know here has few similar questions, but I cannot figure out with those answer. Since for Fitch system, I can only use And Intro, And Elim, Or Inro, Or Elim, Neg Intro, Neg Elim, Impl Intro, Impl ...