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
0
votes
1answer
54 views

Formal proof that if $a-b = \frac{a-b}{ab}$, $a-b$ has to be zero.

Just out of interest, how would I provide a proof that if $a-b = \frac{a-b}{ab}$, then $a$ has to be equal to $b$? It appears really logical, I just want to know how to formally prove it. Thanks for ...
0
votes
0answers
28 views

Formalising sequence generator / optimisation problem

I am a CS student and would like to kindly ask you for help to rigorously formalise an optimisation problem for my research (not a coursework or textbook problem). I massively appreciate any help and ...
0
votes
0answers
30 views

What is the proof for the factorization criterion?

** The Factorization Criterion ** Let $U$ be a statistic based on the random sample $Y_1, Y_2,...Y_n$. Then $U$ is a sufficient statistics for the estimation of a parameter $\theta$ if and only if ...
1
vote
4answers
3k views

Propositional Logic Proof of DeMorgan's Law

This problem was recently posed to me that I prove it. $\vdash (A \land B ) \iff \neg(\neg A \lor \neg B) $ We are only allowed to use derivation rules. It is obviously just the statement of ...
3
votes
5answers
225 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 ...
0
votes
4answers
232 views

Construct formal proofs using the natural deduction

So I'm currently studying First Order Logic, and I'm really struggling with constructing formal proofs. I managed to solve some of the basic problems, but can't seem to understand this one. Can you ...
3
votes
4answers
140 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 ...
1
vote
2answers
147 views

Inference Proof for Biconditional

I'm asked to prove $(p\rightarrow (q \vee r)) \leftrightarrow ((p \wedge \neg q)\rightarrow r)$ using inference rules and I'm not quite sure how to do it. This is what I have so far. $1 [(p \wedge \...
0
votes
2answers
52 views

Are two proofs better than one? [closed]

I have proved a simple conjecture two ways, for an essay I need to do for my highschool maths. How do I justify in my essay why I have included two proofs instead of one. Is there any good reason, to ...
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 ...
3
votes
2answers
100 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 ...
1
vote
2answers
248 views

Formal deduction proof of predicates

I am trying to proof equality is transitive, that is, $\emptyset \vdash \forall x \forall y \forall z ((x=y) \land (y=z) \to(x=z))$ using formal deduction (17 rules) and also other rules (ex. To ...
1
vote
1answer
62 views

Formal Proof - premises and conclusions

So I'm learning about formal proof and understand the beginning steps. However, after I'm given an argument and conclusion, I then don't understand how to do the actual formal proving. For example: ...
2
votes
2answers
165 views

Deduce $ \forall x P(x) \vdash \exists xP(x) $

Well it's a little awkward but how can I show this in a natural deduction proof? $ \forall x P(x) \vdash \exists xP(x) $ I think one has too proof that with a proof by contradiction rule but since I ...
1
vote
2answers
59 views

Deduction of $\forall x(\neg p(x)\rightarrow q(x)), \forall z(p(z)\rightarrow r(z))\vdash \forall z(\neg r(z) \rightarrow\exists yq(y))$

I trying to study for my final exam and I can't figure out how to solve this: $\forall x(\neg p(x)\rightarrow q(x)), \forall z(p(z)\rightarrow r(z))\vdash \forall z(\neg r(z) \rightarrow\exists yq(y))...
2
votes
2answers
52 views

Showcases of formalized mathematics in a system like Coq or Lean?

I have been reading about and trying out type theory based proof assistants Lean and Coq, and I have seen a few formalized proofs of basic, isolated propositions. I am looking for examples, showcases,...
4
votes
1answer
56 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 ...
5
votes
2answers
155 views

How can we express “induction is the same as recursion”, formally?

Informally, the connection between induction and recursion is easy to see, especially when using induction to constructively prove the existence of something. For example, when proving that every ...
8
votes
3answers
84 views

How to formally prove that index renaming doesn’t change sum

How do we formally prove (e.g. in type theory) that $$\sum _ix_i=\sum_ix_{f(i)}$$ For any bijection $f:I\to I$ for any finite set $I$? I might be overcomplicating things, but I’m having trouble ...
4
votes
3answers
2k views

Proof of transitivity in Hilbert Style

We can use the following axioms: $$\begin{align} &A\to(B\to A)&\tag{A1}\\ &[A\to(B\to C)]\to[(A\to B)\to(A\to C)]&\tag{A2}\\ &(\lnot A\to\lnot B)\to(B\to A)&\tag{A3} \end{align}...
0
votes
2answers
38 views

Question on how to prove an expression satisfies a quadratic equation

So I stumbled upon a question in a book that goes, "Prove that in any field, if $ax_1^2 + bx_1 + c = 0$ and $a ≠ 0$, then $x_2 = -(\frac {b}{a} + x_1)$ satisfies $ax_2^2 + bx_2 + c = 0$". My question ...
1
vote
1answer
93 views

Trying to understand the difference between metatheory and theory and circularity

First off I just want to say that I understand that a model is not the same as the thing it models. I've already read several answers on this topic so I am looking for a new answer to hopefully ...
1
vote
1answer
30 views

Verification of proof on repeated root for a quadratic polynomial

I'm fairly new to writing proofs so I'd appreciate it if anyone could point out amy holes in this proof, and if there's any comments so I could improve my proof writing! Question: "Let $a ≠ 0$. If ...
2
votes
1answer
58 views

Proof logical statement with interference rules

Proof following statement with interference rules ( without truth table) that $$ (\neg C \wedge B \wedge (A \rightarrow C) \wedge (B \rightarrow D ) )\implies (\neg A \wedge D ) $$ Attempt to proof ...
1
vote
2answers
62 views

Show that $ \forall{x}\exists{y}{(P(x) \to Q(y))} \vdash \exists{y}\forall{x}{(P(x) \to Q(y))} $

I need to show that $$ \forall{x}\exists{y}{(P(x) \to Q(y))} \vdash \exists{y}\forall{x}{(P(x) \to Q(y))} $$ using the natural deduction rules outlined in Logic in Computer Science: Modelling and ...
3
votes
3answers
88 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
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
4answers
183 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, ...
1
vote
1answer
49 views

What is the name of the rule that allows us to infer the truth of an equation from the truth of another equation?

I am wondering if there is a particular named rule or principle in mathematics/formal logic (that can be listed as justification in a formal proof) that allows one to conclude the truth of an equation ...
0
votes
0answers
45 views

how to give a formal prove to $ \vdash \exists x (P(x) \rightarrow P(y)) $

I am struggeling with giving prove for the next statement : $\vdash\exists x (P(x) \rightarrow P(y))$. This is what I have done but it fails because $\alpha$ isn't a logical sentence. $\exists x (...
3
votes
3answers
72 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 ...
0
votes
0answers
21 views

Formal Methods and specification of program

I have command $choose$ that assign one value from array ${x1...xn}$ to variable $x$. Every call it assigns the same value to the variable. I need to create the specification for this program. I ...
3
votes
2answers
84 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 ...
0
votes
2answers
48 views

let a,b,c and d be positive integers such that a/b < c/d. Show that a/b < a+c/b+d < c/d [closed]

Given that ${a\over b} < {c\over d}$ show that $${a\over b} < {a+c\over b+d} < {c\over d}$$
0
votes
1answer
23 views

Proof that Mathematical Induction is legitimate method of proof [duplicate]

The idea of mathematical induction makes perfect sense, because if a statement is true for n=1, and if the statement being true for an arbitrary natural number $m$ implies the statement is true for $m+...
4
votes
3answers
2k views

Proving using axioms of propositional logic

As part of my upcoming exam in Mathematical Logic we are supposed to be able to prove a given statement using a list of given $axioms$, $M.P.$ and $H.S.$ My question is, how do I approach these kinds ...
-1
votes
4answers
56 views

How to prove A → (B ∨ C) given A → B

How to prove A → (B ∨ C) given A → B I know this is a valid argument, I'm just terrible at fitch-style proofs and have no idea how to start, let alone finish.
2
votes
1answer
481 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 ...
0
votes
0answers
71 views

Why is the calculus of constructions called that way, and what is a “construction” in CoC?

I'm reading about the calculus of construction Nederpelt & Geuvers' book "Type theory and formal proof". I can see that CoC allows us to extend the curry howard isomorphism from simply typed ...
1
vote
1answer
62 views

Having trouble figuring out when to use induction or direct proof.

I know for simple induction you generally want to use this technique when the domain of the conjecture is in the Naturals.However, direct-proof approach would sometimes work too. For example, if i ...
2
votes
1answer
64 views

Show $\neg(\forall x\phi)\vdash \exists x(\neg \phi)$ using an ND-derivation

I'm trying to show that $\neg(\forall x\phi)\vdash \exists x(\neg \phi)$ through a natural deduction (ND) derivation. I'm kind of stuck, because I don't see how I can find some $t$ such that we have $...
-1
votes
1answer
22 views

Proof for similarities between two triangles.

We know that if the angles of two triangles are similar, then their sides are proportional. I get the idea. Now, can it be proven rigorously?
0
votes
0answers
34 views

How do I prove relation involving inequalities is transitive?

I have only written proofs that prove relations using equality are transitive. I have no idea how to manipulate equations with inequalities. R = {(x, y) | x − y > 1} is a relation on ℝ Claim: R is ...
2
votes
1answer
80 views

Understanding $\lor~E$ in Natural Deduction?

I'm reading Frank Pfenning's Lecture Notes on Natural Deduction. It's reasonable that the following $\lor$-elimination rule is incorrect since we can have any theorem $\alpha$ given a single theorem $\...
0
votes
1answer
34 views

Composite function is bijective

Suppose $f : X → Y$ and $g : Y → Z$ are functions. If $g ◦ f$ is bijective and $f$ is surjective. Then what would $g$ be? Would it be bijective or invective? I know that $g ◦ f$ is injective then $f$ ...
0
votes
2answers
255 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!
2
votes
1answer
37 views

Proving the theorem $\forall a\in\mathbb{N},\forall m\in\mathbb{N},(m<a\Rightarrow m\leq a-1)$

I want to solve this proof by the method of Contradiction. Though without using the well ordering principle. I don't have any idea how to start. I have found other ways to prove this theorem but only ...
0
votes
1answer
100 views

Landau’s Function

Show that for all L(n)<2^n for all n ∈ N Where Landau’s function L(n) is defined for every n ∈ N to be the largest order of an element of Sn. I have proven by induction, that n<2^n for all n ∈...
1
vote
1answer
73 views

Can axioms be premises in formal proofs?

If I use an axiom to prove a theorem, i.e. use the axioms of equality in FOL to prove the converse of the axiom of extensionality, do I list those axioms as premises in a formal proof? The answer ...
0
votes
1answer
38 views

$\vdash\neg(\square \neg p\land p\land\diamond(p\land\square p\land \diamond p) )$

How to show that $\vdash\neg(\square \neg p\land p\land\diamond(p\land\square p\land \diamond p) )$ in the logic K? First of all, does this proof work? Assume the converse (i.e. that $\vdash\square \...