# Questions tagged [formal-proofs]

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

524 questions
5k views

### Should a mathematical proof be 'convincing'?

I just read a description of what is a mathematical proof in my mathematical logic textbook, and I'm a bit puzzled by it. It goes like this: A mathematical proof is a finite sequence of mathematical ...
2k views

### When writing proofs, is logical notation a crutch?

I'm near the end of Velleman's How to Prove It, self-studying and learning a lot about proofs. This book teaches you how to express ideas rigorously in logic notation, prove the theorem logically, and ...
2k views

### Each person has at most 3 enemies in a group. Show that we can separate them into two groups where a person will have at most one enemy in the group.

The question that I saw is as follows: In the Parliament of Sikinia, each member has at most three enemies. Prove that the house can be separated into two houses, so that each member has at most ...
329 views

95 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 ...
201 views

### Associativity of concatenation

Prove that the following operator is associative for $b\in \Bbb N$ $$x||y = x\cdot b^{1+\lfloor\log_{b}{y}\rfloor}+y$$ One thing that you can notice is that it is the concatenation operator. However,...
2k views

### Natural Deduction Tautology

I'm trying to prove the following tautologies: \begin{align} & ⊢ (A \to (B \to A)) \\ & ⊢ ((A \to B) \to A) \to A \end{align} For the first one, what I did was: $A$ assumption $B$ ...
111 views

### Natural Deduction with identity: two distinct elements proof

Here's an argument that's quite clearly valid, but which I'm having trouble proving in Natural Deduction: $\exists x~\exists y~\lnot x=y \vdash\forall x~\exists y~\lnot x=y$ The informal reasoning: ...
485 views

### Are there logics without modus ponens?

The question doesn't go beyond the title. And I don't mean logics that merely just don't have it as a primitive rule - I'm interested in logic where you can't actually use it. I've searched around ...
450 views

### Natural Deduction First Order Logic $∃y∀x(P(x) ∨ Q(y))↔∀x∃y(P(x) ∨ Q(y))$

I'm working on some of my logic exercises for my end term exam in Predicate Logic. One of these exercises is "Show with natural deduction that $\vdash ∃y∀x(P(x) ∨ Q(y))↔∀x∃y(P(x) ∨ Q(y))$" I'm ...
306 views

163 views

### Formalize a set theory argumentation from a short story fiction

This problem may be interesting. A writer Raymond Queneau wrote in his "Exercises in Style" a series of stories depicting the same event. One of them was in set theory. I'm wondering if anyone might ...
115 views

### Why is the assumption needed in this conditional introduction?

In the first derivation detailed here, why must we include a subderivation with $P$ as an assumption? We can derive $Q$ (4) from $S \land Q$ (2) without the help of $P$ (3); and then since we have ...
431 views

### Proof that for any $16$ digit number there is at least one sequence of $1$ or more digits which its product is a perfect square
I came across this problem where one is asked to proof that, for any $16$ digit number there is at least a sequence of $1$ or more digits which its product is a perfect square. For example, in the ...
### How to prove that $P \rightarrow Q$ is equivalent with $\neg P \lor Q$?
In my book about Logic, which is called 'Language, Proof and Logic', by the way, there is explained that the conditional $P \rightarrow Q$ is equivalent with $\neg P \lor Q$. There is another ...