# 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
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(...
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)...
400 views

27 views

51 views

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 ...
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 ...
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 ...
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 ...
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?