Questions tagged [formal-proofs]

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

Filter by
Sorted by
Tagged with
37
votes
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 ...
30
votes
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 ...
21
votes
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 ...
11
votes
2answers
352 views

Different proof that $\sqrt{2}$ is irrational

I found the following proof arguing for the irrationality of $\sqrt{2}$. Suppose for the sake of contradiction that $\sqrt{2}$ is rational, and choose the least integer $q > 0$ such that $(\sqrt{...
9
votes
7answers
4k views

What is the theorem that has the most proofs?

Classical theorems like the irrationality of $\sqrt{2}$ or the infinitude of the primes have lots of proofs. But one theorem in particular, which I studied years ago in an introductory course of ...
9
votes
4answers
1k views

Motivation for natural deduction

I've been learning natural deduction recently. I've seen many problems and am starting to be able to solve problems more easily. For some reason I feel the need to ask what high school math students ...
9
votes
1answer
285 views

What is “magic” about the combination of addition and multiplication in formal arithmetic?

Goedel's incompleteness tells us that any system containing Robinson arithmetic is incomplete. OTOH, Presburger Arithmetic, which contains only the successor and addition, is complete. I'm pretty ...
9
votes
1answer
357 views

Status of declarative proof languages in proof assistants

I'm interested in formalising mathematics and logics in a proof assistant, both to get to know a proof assistant and to make an archive of proofs for myself (nothing too fancy, mainly first order ...
8
votes
3answers
429 views

Why isn't Modus Ponens valid here

I have the following: $(\neg A \lor B) \rightarrow (\neg A \lor B) \\ (\neg A \lor B) \\ \vdash \neg A \lor B $ And in my mind this seems like a legitimate use of the Modus Ponens rule. But the ...
8
votes
3answers
84 views

How to formally prove that index renaming doesn’t change sum

How do we formally prove (e.g. in type theory) that $$\sum _ix_i=\sum_ix_{f(i)}$$ For any bijection $f:I\to I$ for any finite set $I$? I might be overcomplicating things, but I’m having trouble ...
8
votes
1answer
144 views

Semantic proofs to syntactic proofs

Given a first-order logic theory $T$ and and a formula $F$, suppose I have semantically proved that $T\vdash F$. That is, I have proved that any model $M$ of $T$ satisfies $F$ and I conclude by Gödel'...
8
votes
5answers
622 views

What are some good proofs to read? [closed]

I have just started my second year in a maths degrees and I am interested in reading mathematical proofs, I find the proofs to everything I do in class fascinating so I'm looking for some proofs to ...
8
votes
4answers
410 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 ...
7
votes
4answers
317 views

Show that $(p \to q) \lor (q \to p)$ is a tautology

I tried to prove that $(p \to q) \lor (q \to p)$ is a tautology. I used $p$ and $¬q$ as conditions. (Premises 1 and 5) I managed to get to a solution, but I'm not sure if it's right. Can you please ...
7
votes
1answer
2k views

Which subfields of math are easier or harder to formalize?

This is a follow-up question to Can all math results be formalized and checked by a computer?. Hopefully it's not too broad, but here goes: which subfields of math could be formalized using existing ...
6
votes
4answers
707 views

Is this proof correct? (natural deduction)

I'm working through The Science of Programming by David Gries. This question is #18 in section 3.3. Prove $((P \land \lnot Q) \to Q) \to (P \to Q)$ Using the natural deduction system here is my ...
6
votes
2answers
405 views

Propositional Logic Help: $(\neg p \wedge (p \vee q)) \rightarrow q $ is a tautology

I need to prove that $(\neg p \wedge (p \vee q)) \rightarrow q $ is a tautology using Laws of Logic (not truth tables). This is what I tried: $\equiv (( \neg p \wedge p) \vee (\neg p \wedge q)) \...
6
votes
1answer
103 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 ...
6
votes
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,...
5
votes
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 ...
5
votes
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 ...
5
votes
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$ ...
5
votes
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: ...
5
votes
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 ...
5
votes
2answers
155 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 ...
5
votes
1answer
476 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 ...
5
votes
1answer
308 views

Formal proof of $(A\lor B)∨C \leftrightarrow A\lor(B\lor C)$

$A\lor B$ by definition $\neg A\implies B$ Deduction rules: $A\implies (B\implies A)$ $(A\implies (B\implies C))\implies ((A\implies B)\implies(A\implies C))$ $(\neg B\implies \neg A)\implies(A\...
5
votes
2answers
156 views

Formal proof of $P\to Q, (P\to Q)\to (T\to S), \neg Q, P\lor T\vdash S$

This is an example exam question that I'm wondering if I did right? We weren't given an answer key, so I'm checking to make sure I'm comprehending the material and if my answer is correct? Premises: ...
4
votes
3answers
620 views

Is an axiom a proof?

From this comments discussion on Philosophy.SE: "Check out formal logic resources - I'm not going to dig them out for you. Alternatively ask on Math.SE. An 'axiom is a proof' is a definition in ...
4
votes
3answers
2k views

Proving using axioms of propositional logic

As part of my upcoming exam in Mathematical Logic we are supposed to be able to prove a given statement using a list of given $axioms$, $M.P.$ and $H.S.$ My question is, how do I approach these kinds ...
4
votes
4answers
190 views

Find propositional formulas $\phi$ and $\psi$ such that $(\phi \rightarrow (\psi \rightarrow (¬\psi)))$ is a theorem of L.

Find propositional formulas $\phi$ and $\psi$ such that $(\phi \rightarrow (\psi \rightarrow (¬\psi)))$ is a theorem of L. So every axiom is a theorem of L so I thought there would be some way to ...
4
votes
3answers
2k views

Proof of transitivity in Hilbert Style

We can use the following axioms: $$\begin{align} &A\to(B\to A)&\tag{A1}\\ &[A\to(B\to C)]\to[(A\to B)\to(A\to C)]&\tag{A2}\\ &(\lnot A\to\lnot B)\to(B\to A)&\tag{A3} \end{align}...
4
votes
3answers
3k views

Use Fitch system to proof ((p ⇒ q) ⇒ p) ⇒ p without any premise. ONLY FOR FITCH SYSTEM.

I know here has few similar questions, but I cannot figure out with those answer. Since for Fitch system, I can only use And Intro, And Elim, Or Inro, Or Elim, Neg Intro, Neg Elim, Impl Intro, Impl ...
4
votes
2answers
96 views

Formalizing $na$ for $n\in\mathbb{Z}$ and $a\in R$ where $R$ is a ring.

Let $R$ be a ring and let $n\in\mathbb{Z}$. Given $a\in R$, I've seen $na$ defined as $$ na:=\begin{cases}0&\text{if }n=0,\\\underbrace{a+a+\cdots+a}_{n\text{ times}}&\text{if }n>0,\\\...
4
votes
2answers
2k views

equivalence between formal and informal proof

I'm reading Cohen's book on the independence of the continuum hypothesis, and I see that all the proofs that he gives when he's defining the basic notions of set theory (ordinals, cardinals, ...
4
votes
2answers
401 views

Deducing $(\lnot B) \to A$ from $\lnot A \to B$ using Hilbert deductive system

As the title says, I've been trying to prove this: $(\lnot A \to B) \vdash (\lnot B) \to A)$ but unfortunately keep winding up with crazy long steps and then I have no idea where to go. The only ...
4
votes
1answer
56 views

Why typeclasses rather than inductive types to define mathematical structures in Lean?

I am not sure whether this is the right forum for this question, but I am not sure where else to ask (There is no Lean forum afaik). In the Lean Prover mathlib library, typical mathematical ...
4
votes
1answer
691 views

Why, precisely, do mathematicians think the Collatz conjecture is true? [closed]

I noticed Wikipedia says that most mathematicians who have looked into the problem think the conjecture is true because experimental evidence and heuristic arguments support it (seen on Wikipedia, ...
4
votes
1answer
90 views

$\Bbb Q_{\ge 0}$ elementary definable in $\mathfrak A$=($\Bbb Q$, $\cdot$)

I have this exercise which seems very simple, but I am not able to find a solution. Given a structure $\mathfrak A$=($\Bbb Q$, $\cdot$) Is $\Bbb Q_{\ge 0}$ elementary definable in $\mathfrak A$? ...
4
votes
1answer
540 views

Fitch proof for $(p \implies (q \implies r)) \implies ((p \implies q) \implies (p \implies r))$ with no premises

I'm having trouble solving this problem using the Fitch system. As I understand Fitch, if the goal has the form $(φ \implies ψ)$, it is often good to assume $φ$ and prove $ψ$ and then use Implication ...
4
votes
3answers
212 views

Is the following a correct logical proof?

A → (F ∧ P) ~A → (S ∧ R) ~R ∴ P     assume ~P         assume A         F ∧ P (1, ...
4
votes
1answer
1k views

How to prove math theorems in formal logic or at least in the style of natural deduction?

I have become rather interested lately in proofs in mathematics, and I discovered at first to my surprise that they are written in paragraph form using natural language. Although this seemed out of ...
4
votes
1answer
82 views

Predicate logic, proof of validity of sequent.

The goal is to prove that $\forall x (P(x) \land Q(x)) \vdash \forall x (P(x) \to Q(x))$ in natural deduction. Would like to find out if I did this natural deduction correctly and if not where did I ...
4
votes
2answers
100 views

Natural Deduction Proof that irreflexive, transitive relations on a Set S are not three-cycles

I am looking for a natural deduction proof for above question. I have formalized the argument in the following way: $$ \forall x \neg Rxx, \ \forall x\forall y \forall z (Rxy\land Ryz \rightarrow Rxz)...
4
votes
1answer
215 views

Deduction of “Disjunction elimination”

I have at my disposal Modus Ponens (MP) and the three axioms: A1: $(\alpha\to(\beta\to\alpha))$, A2: $((\alpha\to(\beta \to\gamma))\to ((\alpha\to\beta)\to(\alpha\to\gamma)))$, A3: $(((\lnot\beta)\to(...
4
votes
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 ...
4
votes
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 ...
4
votes
3answers
480 views

Natural deduction proof of $(\forall x.P(x))\land(\forall y.P(y) \implies Q(y)) \vdash \forall z.Q(z)$

My attempt $(\forall x.P(x))\land(\forall y.P(y) \implies Q(y))$ [premise] $\forall y.P(y) \implies Q(y)$ [$\land$ elim 1] $\forall x.P(x)$ [$\land$ elim 1] $a, P(a)$ [$\forall$ elim 3] $a, P(a) \...
4
votes
0answers
371 views

Axioms of Newtonian Mechanics

Axiomatically speaking, could Newton's laws be derived (as theorems) from the conservation of momentum and energy -- along with a few suitable definitions of things like an inertia frame and force? ...
3
votes
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 ...