# Questions tagged [formal-proofs]

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

537 questions
Filter by
Sorted by
Tagged with
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 ...
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 ...
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 ...
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 ...
225 views

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 ...
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 ...
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 ...
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 ...
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: ...
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 ...
59 views

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 ...
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.
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 ...
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 ...
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 ...
64 views

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$ ...
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!
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 ...
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 ∈...
### $\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 \...