Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [formal-proofs]

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

0
votes
0answers
18 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 ...
4
votes
3answers
47 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
43 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
20 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
47 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
50 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
60 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
58 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
20 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
27 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
75 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
76 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
70 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
90 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
31 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
60 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
33 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
39 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
91 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
61 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
50 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
50 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
37 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
30 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
66 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
66 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
100 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
28 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 ?
3
votes
3answers
77 views

Formal proof of one of De Morgan's laws

How to give a formal proof of $\vdash \neg (p\land q)\to\neg p\lor \neg q$ in the natural deduction proof system? Here is what I have: ...
2
votes
2answers
50 views

Is this proof in natural deduction proof system correct?

Consider a natural deduction proof system. Suppose I know that $\vdash \phi$ (the sentence $\phi$ is provable from no premises). If I'm proving something like $\vdash \psi$, can I just use that $\phi$ ...
2
votes
2answers
35 views

Natural deduction - formal proof troubles

I'm pretty new to the topic of natural deduction using the Fitch method. I found a very helpful site (http://proofs.openlogicproject.org/) in which you can construct your proofs, but I'm having a lot ...
0
votes
1answer
35 views

A 7-formula deduction for $\{\forall x (Px \to Qx), \forall z P z\} \vdash Qc$. Enderton logic page 123.

Enderton claims that it is not hard to show that a deduction for $\{\forall x (Px \to Qx), \forall z P z\} \vdash Qc$ exists, and furthermore that it consists of only seven formulas. I was able to ...
1
vote
1answer
58 views

Proof of Natural Numbers using n+1 = n ∪ {n}

In set theory natural numbers are defined by 0 = ∅ and natural number n+1 = n ∪ {n} I need to prove that for every n ∈ N , n = {k ∈ N | k < n}. I know that natural numbers 1 = {∅} 2 = {∅,{∅}} ...
2
votes
4answers
102 views

Proof of $(P\to Q) \vee (Q\to P)$ with natural deduction

I need to prove the following statement in natural deduction: $$(P\rightarrow Q) \lor (Q\rightarrow P)$$ I tried assuming not (target statement) and assuming the left hand side, but I don't know ...
0
votes
4answers
62 views

Proving Symmetric Difference of A and B

Let A and B be sets. Define the symmetric difference of A and B as A∆B= (A ∪ B) − (A ∩ B). (a) Prove that A∆B = (A − B) ∪ (B − A) I tried to start this but am getting really lost. if someone could ...
1
vote
4answers
75 views

Formal Deduction (logic) Question: $\lnot C, (B \to \lnot C) \to A \vdash (A \to C) \to F$

I've been stuck on this question for around two hours now. I'm trying to prove that: $\lnot C, \ (B \to \lnot C)\to A \vdash (A \to C)\to F $ I'm trying to get my second last step to be: $\lnot C,...
1
vote
2answers
86 views

Proving $\exists ! x (t = x)$ constructively without double negation axiom

I am wondering how one would go about this. I am using Hilbert style proof system as described in Kleene's "Introduction to Metamathematics" or "Mathematical logic". I am pretty sure that if you can ...
0
votes
0answers
41 views

Formal Proof - premises and conclusions

So I'm learning about formal proof and understand the beginning steps. However, after it gives an argument and conclusion. I then don' t understand how to do the actual formal proofing. For example: ...
0
votes
1answer
23 views

Formal proof method for predicate logics

I am looking for the official name for a proof method, The method consists of proving the INconsistency of a theory. This was done using trees. We call it classic-elimination method but I don't know ...
3
votes
3answers
94 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 ...
3
votes
1answer
35 views

How can I prove the following with natural deduction rules? ¬∀x∃yP(x,y) ⊢ ∃x∀y¬P(x,y)

I have been stuck with this problem for a long time, I tried reductio ad absurdum and I got the hypothesys [¬∃x∀y¬P(x,y)], then I try to eliminate the negation of the premise, but I have to prove ∀x∃...
3
votes
2answers
90 views

How to use natural deduction to show $\neg (P \land Q) \vdash \neg P \lor \neg Q$?

How to use natural deduction to show $\lnot (P \land Q) \vdash \lnot P \lor \lnot Q$? I think I need to first assume $\neg(\neg P \lor \neg Q)$ and then find a contradiction but I cannot see how to do ...
2
votes
1answer
63 views

Show that the proof rule is not sound and proof question

I'm asked to show that the proof rule \begin{equation} \dfrac{\varphi \to \psi}{\lnot \varphi \to \lnot \psi} \end{equation} is not sound. To show this would I just make the truth tables for the ...