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
1
vote
2answers
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 ...
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
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 ...
-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
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 ...
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
300 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 ...
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 ...
-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
49 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 ...
2
votes
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
97 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 ...
4
votes
3answers
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 ...
2
votes
1answer
93 views

Proving $∀x (x ≠ 0 → gcd(x, 0) = x)$ formally attempt

I have proved $a≤gcd(a,0)$ in my attempt to prove $∀x (x ≠ 0 → gcd(x, 0) = x)$ but I am having trouble proving $gcd(a,0)≤a$ see below: I have access to the normal rules of natural deduction and the ...
9
votes
7answers
4k views

What is the theorem that has the most proofs?

Classical theorems like the irrationality of $\sqrt{2}$ or the infinitude of the primes have lots of proofs. But one theorem in particular, which I studied years ago in an introductory course of ...
1
vote
1answer
53 views

Attempt to prove the $∀d∀x∀y (d | x ∧ d | y ∧ x ≤ y → d | y- x)$ property of the “divides” relation for non-negative integers

I am attempting to prove the $∀d∀x∀y (d | x ∧ d | y ∧ x ≤ y → d | y- x)$ property of the “divides” relation for non-negative integers, but am having a little difficulty and am hoping someone can help. ...
8
votes
5answers
628 views

What are some good proofs to read? [closed]

I have just started my second year in a maths degrees and I am interested in reading mathematical proofs, I find the proofs to everything I do in class fascinating so I'm looking for some proofs to ...
0
votes
2answers
58 views

Different kind of proofs.

In mathematics the four color theorem have been proved by letting a computer checking each case, thus proving that each map can be colored by only four colors. However, this made me think about the ...
0
votes
3answers
123 views

Prove $\sqrt{n+1} < \sqrt{n} + 1 $ [duplicate]

Prove $\sqrt{n+1} < \sqrt{n} + 1 $ for all $n \ge 1$. I have proven the base step for $n = 1$. $\sqrt{2}$ is less than $2$. The inductive hypothesis is $\sqrt{n+1} < \sqrt{n} + 1$. From here, I ...
2
votes
0answers
135 views

Are there any recent advances in formalizing the undecidability of $\mathit{CH}$?

I'm cross-posting this from Mathoverflow. Since I'm asking for recent developments, it seems best to have answers in both sites. The website Formalizing 100 Theorems by Freek Wiedijk contains a list ...
-1
votes
1answer
52 views

The product of any nonzero irrational number and any integer constant is irrational. [closed]

Can anyone help me find the counterexample to this problem?
2
votes
1answer
542 views

Prove commutative law of multiplication using peano axioms.

That is, prove $∀x∀y(x \cdot y=y \cdot x)$. I have tried induction but it seems not work well. It may require the rule of additive cancellation to be proved. could someone please prove it please? ...
0
votes
2answers
273 views

Prove cancellation law using peano axioms.

Using Peano axioms, prove $∀x∀y∀z(x+y=x+z→y=z)$. I have been stuck on it for some time, could someone please give a proof? Thanks!
1
vote
2answers
106 views

How do I find the contradition in this indirect proof?

I'm utterly stuck with no where to go. The assignment is to complete the indirect proof. I'm stuck on the following step, and have no clue how to proceed. Where do I go? Also, pardon the poor ...
2
votes
1answer
55 views

Are $A, B, C \vdash D$ and $A, B\vdash C \rightarrow D$ interchangeable?

For an assignment we have to make a proof in the Hilbert system. And my proof hinges on the following operation being allowed: $A, B, C \vdash D\tag 1$ Becomming: $A, B\vdash C \rightarrow D\tag 2$ ...
1
vote
1answer
111 views

peano arithmetic - PA sentences

In using the non-logical axiom sentences of PA, I was trying a practice problem to get the hang of using the PA sentences: $((S0 * S0) = S0)$ And so my approach was the following: $\forall x_1((x_1 ...
0
votes
1answer
48 views

Isabelle — Strange proof under Formal_Power_Series

While working towards the Lagrange Inversion theorem in Isabelle to do some formal combinatorics I am following: http://users.math.msu.edu/users/magyar/Math880/Lagrange.pdf I get to Lemma 1, ii . $\...
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 ...
-2
votes
1answer
125 views

Prove disjoint number of subsets of pairs of a set is $3^n$. [closed]

I've been having a a lot of trouble trying to prove the size of the set of disjoint subsets of pairs of a set ($DP(n)$) is $3^n$ using induction. $S(n) = {0, 1, ..., n-1}$, $S(0)$ is the empty set. ...
-1
votes
1answer
76 views

Show that two lines intersect if and only if $a_1b_2 \ne a_2b_1$? [closed]

Could anyone help me with this proof? Thanks Show that two distinct lines given by the equations $a_ix+b_iy+c_i=0$ for $i=1,2$ in $\mathbb R^2$ intersect if and only if $a_1b_2\ne a_2b_1$, and ...
1
vote
2answers
103 views

Deduction of $(\exists x Px \rightarrow \forall y Qy)\rightarrow \forall z(Pz \rightarrow Qz)$

Deduction of $(\exists x Px \rightarrow \forall y Qy)\rightarrow \forall z(Pz \rightarrow Qz)$ My try: There exists a deduction as follows. The Deduction and Generalization Theorems together imply ...
-1
votes
1answer
69 views

Difference between EF and EX in CTL

I don't understand the difference between EF and EX in CTL. The tutorial says almost the same about the two (but they do give ...
4
votes
1answer
167 views

Formalize a set theory argumentation from a short story fiction

This problem may be interesting. A writer Raymond Queneau wrote in his "Exercises in Style" a series of stories depicting the same event. One of them was in set theory. I'm wondering if anyone might ...
0
votes
2answers
200 views

Proving $(p \to q) \to ((q \to r) \to (p \to r))$ from Hilbert formal system for positive implicational formal system?

How to prove suffixing $(p \to q) \to ((q \to r) \to (p \to r))$ from weakening and self-distribution axioms and MP. So, in system with axioms $$A1. p \to (q \to p))$$ $$A2. (p \to (q \to r)) \...
1
vote
0answers
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 ...
1
vote
1answer
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$...
1
vote
1answer
276 views

Sequent calculus, how to prove double negation introduction and conjunction

I want to prove double negation introduction in sequent calculus using the most basic rule set. That is what I want to prove: from the sequent $$\Gamma \rightarrow\Phi,$$ the sequent $$\Gamma \...
6
votes
1answer
208 views

Associativity of concatenation

Prove that the following operator is associative for $b\in \Bbb N$ $$x||y = x\cdot b^{1+\lfloor\log_{b}{y}\rfloor}+y$$ One thing that you can notice is that it is the concatenation operator. However,...
1
vote
1answer
35 views

Proof of the equation of a surface

In Ian N. Sneddon's Elements of Partial Differential Equations, there is the following text: If the rectangular Cartesian co-ordinates of any point $P(x,y,z)$ in space satisfies the relation $$f(x,...
1
vote
1answer
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. ...
2
votes
1answer
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 ...
1
vote
3answers
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 ...
0
votes
2answers
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 ...
1
vote
3answers
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 ...
3
votes
2answers
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. ...
1
vote
2answers
53 views

Question about reading proof notation

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 ...
1
vote
2answers
148 views

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? ...
0
votes
2answers
77 views

How shall I prove the given statement?

How to prove this statement- "If in a quadrilateral only one pair of opposite angles are known to be equal then,prove that it is not necessarily a parallelogram."?