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
2answers
49 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))...
3
votes
1answer
45 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
43 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
149 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
88 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
52 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
52 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
42 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
79 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
181 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
71 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
46 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
22 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+...
-2
votes
4answers
52 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
64 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
61 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
32 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
79 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
36 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
98 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
72 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
101 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
64 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
102 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
52 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
82 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
78 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$: ...
3
votes
2answers
32 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
2answers
115 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,...
0
votes
2answers
37 views

Can someone give me a hint on how to prove this?

I'm supposed to prove that, for every integer $n > 0,$ it is true that $(1 + 2 + ... + n)$ divides $3(1^2 + 2^2 + ... + n^2)$. Should I use induction? This was given as an exercise in a chapter ...
-1
votes
1answer
30 views

Non contradiction principle

I want to know where do come exactly the contradiction principle and if a formal proof system needs it to work. Have you some books references who talks about it ?