# 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
58 views

### Stuck on formal proofs. Not sure how to continue

I'm stuck on what how to continue. I know I'm missing a few steps but this is what I have so far. Thank you in advance! ¬Cube(b) → Small(b) Small(c) → (Small(d) ∨ Small(e)) Small(d) → ¬Small(c) Cube(...
1answer
1k views

### Prove ⊢(a→b)→(¬b→¬a) in HPC proof system

As stated in the title, I am asked to give a proof that: ⊢(a→b)→(¬b→¬a) Using a system with the Modus Ponens rule, and the following axioms: A1: a→(b→a) A2: (a→(b→c))→((a→b)→(a→c)) A3: (¬b→¬a)→(a→b)...
0answers
400 views

1answer
27 views

1answer
51 views

1answer
421 views

### Differences between constructivism and formalism

What are the main differences between the formalism and constructivism in mathematics? Is there some theorem or axiom valid in formalism which isn't valid in constructivism and vice versa? Is the ...
4answers
411 views

### Calculus of Natural Deduction That Works for Empty Structures

Currently, I am dealing with the calculus of natural deduction by Gentzen. This calculus gives us rules to manipulate so-called sequents. Definition. If $\Gamma$ is a set of formulas and $\phi$ a ...
4answers
1k views

### natural deduction: introduction of universal quantifier and elimination of existential quantifier explained

Currently, I am dealing with the calculus of natural deduction by Gentzen. This calculus gives us rules to manipulate so-called sequents. Definition. If $\phi_1,\dots, \phi_n,\phi$ are formulas, then ...
1answer
236 views

### Correct notation for presenting solutions to equations

Let's say I have a cubic equation $(x-a)(x+b)(x-c) = 0$, and I want to represent the solutions to this equation, what is the formal/conventional way that one would arrive and state the solution to the ...
5answers
249 views

### Prove that $(p \to q) \land (q \to r)$ is equivalent to $p \to r$

$(P\implies Q)\land(Q\implies R)$ is equivalent to $P\implies R$. Is this true? How to prove this directly, not using truth tables?
2answers
21 views

### why this part of a statement is not in the hypothesis

The question basically is For each of the following problems, identify the hypothesis (what you can assume is true) and the conclusion (what you are trying to show is true). Let \$f(x) = 2^...
1answer
63 views

### Can we write formal (mechanical) proof of any theorem?

why formal proofs are not widely used? sometimes non formal proofs are cumbersome. are there any "important" theorems that have been proved formally