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 ...
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 ...
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))...
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 ...
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,...
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 ...
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 ...
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
94 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 ...
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
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
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
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 (...
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
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
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+...
-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.
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 $\...
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
0answers
29 views

How can I prove that $n \sqrt{\frac{x}{n^2}} = \sqrt{x} | n \in \mathbb{N}$?

I came across this observation in an exam today, and thought that this might be useful in making certain algorithms run faster, but first I want a way to prove that this is true. How can I do this? ...
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 \...
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$ ...
6
votes
1answer
103 views

Higher inductive type: what for?

The typical example of higher inductive type (HIT) is the circle $S^1$ that is nicely described here. I understand HITs are convenient if you want to do homotopy theory within type theory. But what ...
0
votes
0answers
32 views

How do I prove using an $\epsilon - \delta$ proof that $\lim_{x\rightarrow \frac{1}{e}}(e^{x^{x^x}})<2$?

Not a homework question. Just wanting to refresh my epsilon delta proofs, and came up with this - struggled for an hour, no idea where to start.
2
votes
1answer
67 views

Showing $\vdash \phi\to \square \diamond \phi$

I'm trying to prove the converse of what was shown here. Namely, I'm trying to prove B-axioms of modal logic ($\vdash \phi\to \square \diamond \phi$ or $\vdash\diamond\square\phi\to\phi$, whatever is ...
1
vote
1answer
34 views

$\vdash\phi \land \diamond\psi \to \diamond(\psi\land\diamond\phi)$ in KB

I've been trying to prove $\vdash\phi \land \diamond\psi \to \diamond(\psi\land\diamond \phi)$ in natural deduction where it's allowed to use $\phi\to \square \diamond \phi$ and/or $\diamond\square\...
0
votes
1answer
40 views

Formalising the equivalence of a (countably) infinite chain of “or”s and exists

I have a countably infinite set $A$ with elements $\{a_0, a_1, ... \}$. I've also been given $P(n) := (b = a_n) \lor P(n+1)$ and that $P(0)$ is true. I could expand this out to a chain of "ors" for ...
2
votes
1answer
105 views

Formalizing the deduction theorem in the metatheory

Here is the deduction theorem, in the "$\Leftrightarrow$" version (I'm considering it for first order logic): $$\Delta \cup \lbrace A \rbrace \vdash \lbrace B \rbrace \Longleftrightarrow \Delta \vdash ...
2
votes
3answers
62 views

Prove that $n^2\in \mathcal O(n^2-1)$.

Prove that $$\smash { n^2\in\mathcal{O}(n^2 -1)}$$ I don't quite understand what strategy I should use when trying to prove the following big $\mathcal{O}$ notation that doesn't include the use of ...
2
votes
2answers
51 views

Proof by contradiction - Getting my head around it

Hey there Math community! I have a general question on contradiction and it's getting difficult to get my head around it. Notes: I have some background in math and I have read several proofs by ...
1
vote
2answers
55 views

Prove distribution of or over implies knowing the implication is always true

I was given a task to construct a Hilbert-style proof for the following: $A → B ⊢ C ∨ A → C ∨ B$ I figured I could use the axiom $A→B≡A∨B≡B$, but this leads me nowhere since I don't think I can use ...
0
votes
1answer
38 views

prove commuting quadratic functions of real numbers are equal

Suppose that $$f(x) = ax^2 +b$$ is a quadratic function, where $ (a, b) \in \mathbb R^2$ and $a \neq 0. $ If $$g(x) = cx^2 +d,$$ where $(c, d) \in \mathbb R^2$ and $c \neq 0,$ is another quadratic ...
0
votes
0answers
32 views

Reasons for formalizing mathematics

What is the motivation behind formalizing a piece of mathematics in a system like Mizar? I ask as someone interested in the process. I mean it's not like anyone is going to read those formal proofs. ...
3
votes
1answer
84 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)) \...
0
votes
1answer
88 views

Metalanguage of mathematics

What excactly is the matalanguage of mathematics? I mean, the predicate calculus admits the formal language of mathematics, right? Then we add set axioms to it et voilá: mathematics. But what does ...
0
votes
0answers
51 views

Prove $\vdash ((p\to q)\to p)\to p$ [duplicate]

I'm trying to prove $\vdash ((p\to q)\to p)\to p$: ...