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
2
votes
2answers
52 views

Proof by contradiction - Getting my head around it

Hey there Math community! I have a general question on contradiction and it's getting difficult to get my head around it. Notes: I have some background in math and I have read several proofs by ...
1
vote
2answers
55 views

Prove distribution of or over implies knowing the implication is always true

I was given a task to construct a Hilbert-style proof for the following: $A → B ⊢ C ∨ A → C ∨ B$ I figured I could use the axiom $A→B≡A∨B≡B$, but this leads me nowhere since I don't think I can use ...
0
votes
1answer
39 views

prove commuting quadratic functions of real numbers are equal

Suppose that $$f(x) = ax^2 +b$$ is a quadratic function, where $ (a, b) \in \mathbb R^2$ and $a \neq 0. $ If $$g(x) = cx^2 +d,$$ where $(c, d) \in \mathbb R^2$ and $c \neq 0,$ is another quadratic ...
0
votes
0answers
32 views

Reasons for formalizing mathematics

What is the motivation behind formalizing a piece of mathematics in a system like Mizar? I ask as someone interested in the process. I mean it's not like anyone is going to read those formal proofs. ...
3
votes
1answer
85 views

Is there a proof of $\lnot \forall x, P(x) \iff \exists x, \lnot P(x)$

I am interested in how one would formally prove: $\lnot \forall x, P(x) \iff \exists x, \lnot P(x)$ I realize that it's basically saying that: $\lnot(P(x_0) \land P(x_1) \land ... \land P(x_n)) \...
0
votes
1answer
103 views

Metalanguage of mathematics

What excactly is the matalanguage of mathematics? I mean, the predicate calculus admits the formal language of mathematics, right? Then we add set axioms to it et voilá: mathematics. But what does ...
0
votes
0answers
51 views

Prove $\vdash ((p\to q)\to p)\to p$ [duplicate]

I'm trying to prove $\vdash ((p\to q)\to p)\to p$: ...
3
votes
2answers
33 views

Formal proof of distributivity of conjuction

I'm trying to prove that $\vdash p\land (q\lor r)\to(p\land q)\lor (p\land r)$ in natural deduction. ...
3
votes
2answers
137 views

Trouble with negation introduction with Fitch natural deduction proof

I've recently posted another question regarding natural deduction proofs and I've definitely made some progress, but I'm now stuck with a proof which seems like it could be flawed. Now as you can see,...
0
votes
2answers
37 views

Can someone give me a hint on how to prove this?

I'm supposed to prove that, for every integer $n > 0,$ it is true that $(1 + 2 + ... + n)$ divides $3(1^2 + 2^2 + ... + n^2)$. Should I use induction? This was given as an exercise in a chapter ...
0
votes
1answer
31 views

Non contradiction principle

I want to know where do come exactly the contradiction principle and if a formal proof system needs it to work. Have you some books references who talks about it ?
3
votes
3answers
124 views

Formal proof of one of De Morgan's laws

How to give a formal proof of $\vdash \neg (p\land q)\to\neg p\lor \neg q$ in the natural deduction proof system? Here is what I have: ...
2
votes
2answers
54 views

Is this proof in natural deduction proof system correct?

Consider a natural deduction proof system. Suppose I know that $\vdash \phi$ (the sentence $\phi$ is provable from no premises). If I'm proving something like $\vdash \psi$, can I just use that $\phi$ ...
2
votes
2answers
36 views

Natural deduction - formal proof troubles

I'm pretty new to the topic of natural deduction using the Fitch method. I found a very helpful site (http://proofs.openlogicproject.org/) in which you can construct your proofs, but I'm having a lot ...
0
votes
1answer
37 views

A 7-formula deduction for $\{\forall x (Px \to Qx), \forall z P z\} \vdash Qc$. Enderton logic page 123.

Enderton claims that it is not hard to show that a deduction for $\{\forall x (Px \to Qx), \forall z P z\} \vdash Qc$ exists, and furthermore that it consists of only seven formulas. I was able to ...
1
vote
1answer
59 views

Proof of Natural Numbers using n+1 = n ∪ {n}

In set theory natural numbers are defined by 0 = ∅ and natural number n+1 = n ∪ {n} I need to prove that for every n ∈ N , n = {k ∈ N | k < n}. I know that natural numbers 1 = {∅} 2 = {∅,{∅}} ...
2
votes
4answers
109 views

Proof of $(P\to Q) \vee (Q\to P)$ with natural deduction

I need to prove the following statement in natural deduction: $$(P\rightarrow Q) \lor (Q\rightarrow P)$$ I tried assuming not (target statement) and assuming the left hand side, but I don't know ...
0
votes
4answers
72 views

Proving Symmetric Difference of A and B

Let A and B be sets. Define the symmetric difference of A and B as A∆B= (A ∪ B) − (A ∩ B). (a) Prove that A∆B = (A − B) ∪ (B − A) I tried to start this but am getting really lost. if someone could ...
1
vote
4answers
84 views

Formal Deduction (logic) Question: $\lnot C, (B \to \lnot C) \to A \vdash (A \to C) \to F$

I've been stuck on this question for around two hours now. I'm trying to prove that: $\lnot C, \ (B \to \lnot C)\to A \vdash (A \to C)\to F $ I'm trying to get my second last step to be: $\lnot C,...
1
vote
2answers
95 views

Proving $\exists ! x (t = x)$ constructively without double negation axiom

I am wondering how one would go about this. I am using Hilbert style proof system as described in Kleene's "Introduction to Metamathematics" or "Mathematical logic". I am pretty sure that if you can ...
1
vote
1answer
64 views

Formal Proof - premises and conclusions

So I'm learning about formal proof and understand the beginning steps. However, after I'm given an argument and conclusion, I then don't understand how to do the actual formal proving. For example: ...
1
vote
1answer
28 views

Formal proof method for predicate logics

I am looking for the official name for a proof method, The method consists of proving the INconsistency of a theory. This was done using trees. We call it classic-elimination method but I don't know ...
3
votes
4answers
145 views

How to prove the following formula using an indirect proof

I need to prove that the premise $A \to (B \vee C)$ leads to the conclusion $(A \to B) \vee (A \to C)$. Here's what I have so far. From here I'm stuck (and I'm not even sure if this is correct). My ...
3
votes
1answer
43 views

How can I prove the following with natural deduction rules? ¬∀x∃yP(x,y) ⊢ ∃x∀y¬P(x,y)

I have been stuck with this problem for a long time, I tried reductio ad absurdum and I got the hypothesys [¬∃x∀y¬P(x,y)], then I try to eliminate the negation of the premise, but I have to prove ∀x∃...
3
votes
2answers
102 views

How to use natural deduction to show $\neg (P \land Q) \vdash \neg P \lor \neg Q$?

How to use natural deduction to show $\lnot (P \land Q) \vdash \lnot P \lor \lnot Q$? I think I need to first assume $\neg(\neg P \lor \neg Q)$ and then find a contradiction but I cannot see how to do ...
2
votes
1answer
80 views

Show that the proof rule is not sound and proof question

I'm asked to show that the proof rule \begin{equation} \dfrac{\varphi \to \psi}{\lnot \varphi \to \lnot \psi} \end{equation} is not sound. To show this would I just make the truth tables for the ...
3
votes
1answer
87 views

Proof using natural deduction (Tautology)

I've been asked to prove the following tautology via natural deduction: $\forall x \, (\lnot Px \lor Qx) \rightarrow (\forall y \, Py \rightarrow \forall z \,Qz)$ I normally use tree proofs, but I ...
2
votes
2answers
119 views

In proof writing, is it mathematically sound to prove uniqueness before proving existence?

As stated in the title, I'd like to find out is whether or not it is always mathematically sound to prove the uniqueness of something before proving the existence of said something. I am still ...
2
votes
4answers
65 views

Natural deduction proof of $(A \to \lnot B \lor C), ((\lnot D \land A) \to B), (\lnot E \to A) \vdash D \lor (C \lor E)$

I'm struggling to proof this both if I use or introduction rule $\lor_{I_1}$ (to work on $D$) or or introduction rule $\lor_{I_2}$ (to work on $C \lor E$). Could you help me?
2
votes
1answer
115 views

When should I use RAA in natural deduction proofs?

I can't understand exactly when should I use RAA (reductio ad absurdum) rule in natural deduction proofs? What situation should "trigger" me to think "Now it's time to use RAA"?
2
votes
1answer
88 views

Predicate Logic Natural Deduction: $∃x P(x) ⊢P(x)$

I am really puzzled right now. To solve the issue, I need to prove this formular: $$ \exists x P(x) \vdash P(x) $$ with the natural deduction rules for propositional and predicate logic. I am ...
1
vote
3answers
105 views

Trouble understanding proof to $\vdash ((\neg(\phi\rightarrow \psi))\rightarrow\phi)$?

I am having trouble understanding the natural deduction proof of $\vdash ((\neg(\phi\rightarrow \psi))\rightarrow\phi)$ (question 2.6.2 (b)) in Hodges and Chiswell's Mathemaical Logic. The natural ...
3
votes
2answers
102 views

Is $A \& B \multimap A$ derivable?

Intuitively, the sentence $A \& B \multimap A$ seems to mean "Using a choice between $A$ and $B$, get an $A$." This feels like it should be derivable for any $A$ and $B$, but I haven't found any ...
0
votes
0answers
34 views

Proving a logical implication using modus ponens and metatheorems [duplicate]

Using the law of inference the axiomatic system and metatheorems prove that $${(\neg A > B),(A > C),(B > D)} \vdash (\neg C > D)$$ Where > is 'implies' and ~ negation. I know how to use ...
1
vote
1answer
58 views

Induction with two variables in PA

This probably has been asked before, but apologies, I don't know how to locate it. I want to prove $\forall x,y: P(x, y)$. My premises are: $$P(0, 0) \wedge \\ [\forall x: P(x, 0)] \wedge \\ [\...
2
votes
2answers
80 views

Natural deduction: predicate logic proof (Prenex form)

I'm pretty familiar with proofs in propositional logic, but not so much with predicate logic. I'm trying to prove the following (which can be used during construction of prenex normal form). If $x$ ...
1
vote
1answer
98 views

show that for every consistent theory there is a complete consistent theory

Let $\mathcal{L}$ be any language of predicate logic, $\Sigma_0$ a consistent theory in $\mathcal{L}$. Let P be the set of all consistent theories $\Sigma \supseteq \Sigma_0$ in $\mathcal{L}$. With ...
-2
votes
2answers
46 views

Let f : R → R be a function, such that $|f(x)−f(y)|≥5|x−y| \:\forall \:x, y\in \mathbb{R}$. Show that $f$ is injective. [closed]

Intro to Math Proofs course Know basic concepts of Injection functions (one-to-one)
1
vote
0answers
70 views

Predicate Logic Hilbert Proof

In the Hilbert proof system for predicate logic, prove that the formula: $\exists x~\big(B(x)\to C(x)\big)\to\big(\forall x~B(x)\to\exists x~C(x)\big)$ I'm awful with Hilbert Proofs and have no idea ...
3
votes
0answers
100 views

Formal proof of $\exists x (\exists y P(y) \rightarrow P(x))$ and $(\forall x \exists y R(x,y))\rightarrow (\forall y \exists x R(y,x))$

within the following axiomatic system I've beeb trying to proof the formulas (1) $\forall x \exists y R(x,y) \rightarrow \forall y \exists x R(y,x) \\$ and (2) $\\ \exists x (\exists y P(y) \...
2
votes
2answers
82 views

How do we formally define “j-th smallest element”?

Let $A$ be a nonempty finite subset of $\mathbb{R}$. Firstly, let me write down how to define the term "the smallest element of $A$" formally. Suppose 'for every $x\in A$, there exists $y \in A$ ...
3
votes
2answers
97 views

Find a natural deduction proof to show ∃x∃y (S(x,y) ∨ S(y,x)) ⊢ ∃x∃y S(x,y) by predicate logic.

I'm trying to prove $\exists x \exists y (S(x,y) \lor S(y,x)) \vdash \exists x \exists y S(x,y)$ in natural deduction, and I have already applied existential elimination to get $S(x_0,y_0)$, with $x_0$...
1
vote
2answers
115 views

How is Post's tautology theorem used in this proof?

Could someone please explain to me how does the proof of I.4.3 reference I.4.1? In I.4.3, you are given hypotheses about A and B being theorems. However, I.4.1 talks about tautologies (as inputs) not ...
2
votes
2answers
64 views

Construct a deductive system where $1^n$ is provable iff n is not prime

I'd appreciate some help for the following exercise: Construct a (as simple as possible) deductive system where all sequences of the form 1n (which means 111... n-times) is provable if and only if n ...
1
vote
0answers
30 views

Definition of the spectrum in first order logic

I want to understand the definition of the spectrum and therefore I want to know, what it means that a model has n elements or that a model is of size n. What is said to be an element? Are these only ...
0
votes
2answers
38 views

Induction: Using P(n) vs P(n+1) is bad style?

I'm in a proofs class and we were discussing induction. One of the most common ways we (the students) had seen induction was to represent "Statement P hold for $n$" by $P(n)$. Thus, we take the ...
3
votes
1answer
83 views

Construct a deductive system where $1^n$ is provable iff $n$ is prime

I'd appreciate some help or at least a hint for the following exercise: Construct a (as simple as possible) deductive system where all sequences of the form $1^n$ (which means 111... $n$-times) is ...
0
votes
5answers
163 views

Starting with a false statement, how can one prove anything is true? [duplicate]

So I've been learning a bit of logic for class and heard that if you begin with a false statement, you can then prove anything to be true, however I don't entirely understand what this means or how to ...
0
votes
2answers
22 views

Is it possible to show that there is some multiple of 4 that when added to a multiple of 16, will give you perfect square?

Like given some multiple of 16, (in the integers), is it possible to show that there is some multiple of 4 that would make it a perfect square? For example, 32, you can add 4 to make it a perfect ...
0
votes
1answer
135 views

Prove by induction that the union of countable sets is countable

Say you have a set A_i for i in the natural numbers N, and that is a countable set. Then for all natural numbers n, the union of those sets is countable. I must prove this by induction, and I do ...