# 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
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 ...
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 ...
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 ...
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 ...
2answers
59 views

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 ...
3answers
72 views

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

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 ...
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 ∈...
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 ...
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? ...
1answer
38 views

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 ...
1answer
105 views

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. ...
1answer
84 views