Questions tagged [formal-proofs]

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

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
329 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
270 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
346 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
428 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
1answer
134 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
585 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
400 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
312 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
702 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
402 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
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 ...
6
votes
1answer
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,...
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
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: ...
5
votes
2answers
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 ...
5
votes
1answer
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 ...
5
votes
1answer
306 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
615 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
2answers
95 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
398 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
664 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
88 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
535 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
208 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
80 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
96 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
212 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
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 ...
4
votes
1answer
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 ...
4
votes
3answers
431 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
341 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 ...
3
votes
4answers
178 views

How do I formally prove a universal implication?

A textbook I am reading (Discrete Mathematics and its Applications by Rosen) went from introducing formal propositional and predicate logic (including popular rules of inference like Modus Ponens, ...
3
votes
4answers
671 views

Using the Intermediate Value Theorem to prove the existence of a number$\;$

I'm having a bit of trouble with something most everyone might find trivial, and I feel rather silly asking, but here it goes. The premise is as follows: "Use the Intermediate Value Theorem to prove ...
3
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 ...
3
votes
3answers
614 views

Prove that there are no positive integers $a$ and $b$, such that $b^4 + b + 1 = a^4$

So I've been trying to solve this problem for a couple of days now. What I've come up with is this: By way of contradiction, assume that there are positive integers a and b such that $b^4 + b + 1 = a^...
3
votes
1answer
129 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 ...
3
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 ...