# 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
8answers
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 ...
2answers
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 ...
3answers
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 ...
2answers
352 views

1answer
105 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 ...
1answer
205 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,...
5answers
6k views

### Prove that $\vdash p \lor \lnot p$ is true using natural deduction

I'm trying to prove that $p \lor \lnot p$ is true using natural deduction. I want to do this without using any premises. As it's done in a second using a truth table and because it is so intuitive, I ...
2answers
3k views

### 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 ...
3answers
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$ ...
2answers
119 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: ...
2answers
503 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 ...
2answers
156 views

### How can we express “induction is the same as recursion”, formally?

Informally, the connection between induction and recursion is easy to see, especially when using induction to constructively prove the existence of something. For example, when proving that every ...
1answer
486 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 ...
1answer
308 views

1answer
167 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 ...
1answer
118 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 ...
3answers
490 views