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
1
vote
4answers
54 views

Formal proof of implication

I am currently stuck on this particular task. I need to formally prove that (∃a ∀b (b<a)) → (∀a ∃b (a<b)) Now, what I have so far is that I need to prove ...
1
vote
1answer
46 views

$\Sigma ; \lnot \alpha \vdash k $. Prove that $\Sigma \vdash \alpha$

$k$ is a contradiction such that it belongs to a set of well-formed formulas. $\Sigma ; \lnot \alpha \vdash k $. Prove that $\Sigma \vdash \alpha$ where $\alpha$ is a well-formed formula. After ...
0
votes
1answer
96 views

Axiom Problems (Intro to Computer Logic)

"Show that—or prove that—$ \Gamma \vdash A $" means "write a $ \Gamma $-proof that establishes $ A $". The proof can be Equational or Hilbert-style. Show that $ A \equiv C \vdash A \rightarrow (B ...
0
votes
1answer
75 views

Need help for a proof ( sequent calculus )

I have to prove the following: $$\vdash((A \to B) \land (B \to A)) \to (A \leftrightarrow B)$$ But I'm totally stuck here after using introduction of implication and introduction of equivalence: \...
0
votes
1answer
45 views

Can a sequent be valid if the conclusion contains atoms that are not in the premise?

Is it possible to prove the validity of the following sequent: $p \vdash (p \to q) \to q$ Here, our premise is that $p$ is True. The conclusion references a new atom, $q$. I would argue that this ...
0
votes
1answer
63 views

Weakest theory equi-consistent to ZFC

I've recently read that ZF is equi-consistent to ZFC. From what I understand, to establish this we transform a formal proof of a contradiction in ZFC into a formal proof of a contradiction in ZF. We ...
1
vote
3answers
35 views

Prove that a sequence which converges at L, still converges at L when a fixed positive integer is added to the variable.

Here is the problem I am attempting to solve/prove: Let $(a_n)$ n∈N be a sequence that converges to L and let p be a fixed positive integer. Prove that the sequence $(a_{n+p})$ n∈N converges to L. I'...
-1
votes
3answers
35 views

How can I prove this in a systematic manner? [closed]

I have to prove the following claim. For all $n \in \mathbb{N}, 2$ divides $3n^{3} + 13n^{2} + 18n + 8.$ I want to have a systematic proof or even just a hint, to start.
0
votes
1answer
71 views

Prove $\forall n \in \mathbb N, \forall k\in \mathbb Z, \forall \ell \in \mathbb Z, \neg (n = 5k+3 \land n = 5\ell +1)$, Intended meaning?

I am understanding this question to prove $5k+3 \neq 5l+1$ for all values of l and k as long as the result is a natural number. Since it's for all, it can easily be disproved by finding any example ...
8
votes
1answer
156 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'...
0
votes
2answers
135 views

Let $a,b,c,d$ be real numbers such that $a<b < c<d$. Express the set $[a,b] \cup [c,d]$ as the difference of two sets [duplicate]

I am not sure how I would express these sets as a difference. My original attempt was to show that it is the set $[a,d]$ and take away the universal set. I would appreciate any help. Thank you in ...
1
vote
1answer
68 views

How to formalize my intution of this theorem on continuous functions?

Theorem : If a function $f$ is continuous on a closed and bounded interval $[a, b]$ then $f$ must be uniformly continuous in $[a, b]$ My Idea : I get the intuition that for a continuous function on a ...
1
vote
1answer
132 views

Book Recommendation

To start out with, I'm a junior in high school who is intrigued by the rigor of higher mathematics and is currently attempting to self study Volume 1 of Apostol's Calculus. I haven't had any previous ...
0
votes
0answers
29 views

Good list of theorems tobprove

HI I am a highschooler currently taking calc BC and I am looking for some fun theorems I could try to prove. I have proved a lot of trigonometric identities and the fundemental theorem of calculus and ...
1
vote
0answers
58 views

Prove $\Sigma \vdash \lnot(\phi \rightarrow \psi)$ iff $\Sigma \vdash \phi$ and $\Sigma \vdash \lnot \psi.$

$\Sigma$ is a set of sentences, the set $ L$ consists of all axioms of the forms: A1) $ \ \phi \rightarrow (\psi \rightarrow \phi)$ A2) $\ (\phi \rightarrow (\psi \rightarrow \theta)) \rightarrow (...
1
vote
2answers
133 views

(P → Q) v (Q → R), Fitch-style proof

I'm trying to construct a Fitch-style proof for $(P \to Q) \lor (Q \to R)$ using reductio ad absurdum and the introduction and elimination rules for conjunction, disjunction, and implication. I'm not ...
1
vote
2answers
77 views

Complement function: how to prove surjective?

Given some set A and a complement function C(K) = A - K from the power set of A onto the power set of A, how can I formally prove that it is surjective? I think I get it, but can't get it on paper. (...
-1
votes
1answer
76 views

Find a proof for the following tautology

I was introduced to Axiomatic Theory in last class and I need to know how to solve this kind of problem in the midterm next week. However, I have no idea how to solve these kind of problems. We had ...
0
votes
1answer
98 views

Formal Proof of WFF using Rules of Inference

I am currently hung up on a practice problem that requires a formal proof of a WFF using ONLY rules of inference. I've been attempting this for hours, but it seems like there is something i'm missing. ...
0
votes
2answers
87 views

Is the transitivity of subset proof incomplete everywere?

We are working in ZFC, so under first order logic we introduce the undefined predicate $\in$ and the ZFC axioms. (1) $\forall A,B,C ((\forall(x \in A \rightarrow x \in B) \land \forall(x \in B \...
4
votes
3answers
629 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 ...
2
votes
2answers
46 views

Need help with tautology proof without truth tables.

I am trying to prove $$[(p\to q)~\&~(q\to r)]\to (p\to r) $$ is a tautology using only logical laws. I have gotten part-way there but I got stuck and am not sure how to proceed. Please state ...
2
votes
1answer
815 views

Proving the distributive law with natural deduction

I have to prove the following logical equivalence, also known as one of the two distributive laws: $$ P \vee (Q \wedge R) \equiv (P \vee Q) \wedge (P \vee R) $$ I have solved the first part, $P \lor ...
1
vote
1answer
96 views

How to prove $\lnot (\alpha \rightarrow \lnot \beta) \vdash \lnot (\beta \rightarrow \lnot \alpha)$ in HPC

I have the three axioms $$\alpha \rightarrow (\beta \rightarrow \alpha)$$ $$\Big(\alpha \rightarrow (\beta \rightarrow\gamma)\Big)\rightarrow \Big((\alpha \rightarrow\beta)\rightarrow(\alpha\...
4
votes
1answer
88 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 ...
1
vote
1answer
250 views

Inductive proof using Fitch software

I am trying to prove the integer square root theorem $\forall x: \mathbb{N}, \exists y : \mathbb{N}((y^2 \leq x) \land (x < (y+1)^2))$ for $\lfloor \sqrt{x} \rfloor$. In words: for any natural ...
3
votes
1answer
70 views

Equivalence in Natural deduction in First-order logic 2

I would want to check with you guys if I've done the following natural deduction correct. The reason being that I haven't gotten any answer sheet for this task. Task Solve the following with natural ...
3
votes
3answers
90 views

Equivalence in natural deduction in First-order logic

Task $\vdash \exists x (P(x)\lor Q(x)) \iff \exists xP(x) \lor \exists xQ(x) $ My answer If we have $A \iff B$ then $A\vdash B$ and $B \vdash A$. So I started trying to see if I could prove $B$ ...
2
votes
1answer
86 views

Natural deduction in first-order logic

I've sat for more than an hour now and I don't understand how I'm supposed to solve the task below. $\{\forall x(P(x) \land Q(x)), \exists x\neg P(x)\} \vdash \exists x \neg Q(x) $ So I'm a bit ...
1
vote
1answer
76 views

Fitch Style Proof

¬(A↔B) conclusion ¬A↔B I'm having trouble with the second part of this proof. I think I managed the first part: 1 |¬(A↔B)$\,$ $\,$ A prem. 2 ||B $\,$ $\,$ A →intro 3 |||A $\,$ $\,$ ...
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 ...
2
votes
0answers
95 views

Reference request: the space of formalisms for proving function totality

I'd like to develop an intuition about the space of axiomatic systems (formalisms) that can be used to prove totality of Turing machines. To this end, I'm interested in the set of "totality proof ...
2
votes
2answers
125 views

Doubts about Goedel Completeness Theorem

My book (Mendelson) states this theorem the following way: (1) A logically valid formula of a first order theory is a theorem. On Wikipedia the statement is a little more general: (2) For any ...
-2
votes
4answers
87 views

How can you proof that $\lim_{n \to \infty} n!=\infty$?

When solving a limit of a succession last class involving $n!$, the professor said we could proof that $\lim_{n \to \infty} n!$ is $\infty$, but he left it as some sort of homework the actual process ...
0
votes
0answers
70 views

Prove by mathematical induction that $n^2 > n$ for all $n \geq 2$

Prove by mathematical induction that $n^2 > n$ for all $n \geq 2$. My attempt: When $n=2$ LHS , $2^2 =4$ RHS , $2$ When $n=2$, LHS $>$ RHS Assume true for $n=k$ $k^2>k$ RTP true for $...
0
votes
1answer
50 views

How to prove the following statement? [closed]

a=b ∨ a=c ∨ b=c = T I have expanded the LHS as follows. But have no clue how to continue from there (a=>b)∧(b=>a) ∨ (a=>c)∧(c=>a) ∨ (b=>c)∧(c=>b) Link for the question [Q (p)]. http://www.cs....
2
votes
2answers
23 views

What is the difference in meaning between these two antecedents …?

$$ (\forall x)(Mx \to Wx) \to \quad... \tag{1} $$ $$ (\forall x)(Mx \land Wx) \to \quad... \tag{2} $$ The consequent is clear: $\, (\exists y)(Fy \land Sy)$ The statement is: If every member of ...
2
votes
2answers
145 views

How to convert … to logical symbols?

If Bluenose is guilty then no witness is lying unless he is fearful. There is a witness who is fearful. Therefore, Bluenose is not guilty. $$B\to[(\forall x)(\,(Wx\land\lnot Fx)\to(\lnot Lx)\,)] \...
2
votes
1answer
171 views

Fitch-style Deductive Proof

I am having trouble with the following question: Give natural deduction proofs of the following formulas (from no assumptions): $p \to p$. Here is what I have so far: $$\begin{array}{|l}\hline~~\...
1
vote
0answers
32 views

How to make my analysis more rigorous?

I was dealing with 3-DOF attitude dynamics of rigid body in a geometrical framework and wanted to comment upon the following defined function $F$ at its maxima. Consider $F \in \mathbb{R} : F(e_{\...
3
votes
2answers
293 views

The intuitive meaning of “or” and “implies” in axiom schemes of a logical theory

In a Hilbert-style system, the axiom schemes can be written as (From Bourbaki, Book I): S1. If $A$ is a relation in $\mathscr C$, the relation $(A\text{ or }A) \Rightarrow A$ is an axiom of $\...
0
votes
2answers
394 views

Proving that d(n) is odd if and only if n is a perfect square

Here is the question (and answer) in its entirety. I have been tackling this for a little and I just can't seem to understand the solution whatsoever. I don't need to know how to prove it I need to ...
0
votes
2answers
138 views

Product of $(4k-1)$ primes can't be sum of 2 squares

I am trying to prove, Product of primes of the form $(4k-1)$ can't be sum of 2 squares. My approach is- Let the product is $M=m_1m_2...m_n$ where $ m_1, m_2, ...m_n$ are primes. Assume, $M$ can ...
1
vote
2answers
43 views

Prove By Induction $U_n=2^n+1.$

Given that $U_1=3,U_2=5,$ and $U_{n+2}-3U_{n+1}+2U_n=0.$ Show that $U_n=2^n+1.$ I'm stuck at showing that if $P(n+1)$ is true if $P(n)$ is true.
4
votes
2answers
102 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)...
3
votes
1answer
215 views

Conditional Statements/ Implication statements within a proof specifically linear algebra

I am sort of new to the mathstackexchange so excuse me for any mistakes that I make while writing this post. I've been working on proofs and ran into a conflicted view of how to prove conditional ...
2
votes
1answer
168 views

Natural deduction proof - problem with existential elimination

I have problems with the following proof: $$ \forall x \exists y (Rxy \land Py), \forall x \neg Rxx \vdash \neg \forall x \forall y (Px \implies (Py \implies x=y)) $$ The problem is with the ...
0
votes
2answers
306 views

How do I show that A iff B proves A implies B?

Prove that $ {A} \leftrightarrow B $ proves $ A \to B $ I have tried to use some logical axioms but can see no obvious one other than $$ (A \rightarrow B) \leftrightarrow ((A \lor B) \leftrightarrow ...
0
votes
1answer
50 views

Understanding the Arithmetic Rules in an Operational Semantics.

I am having difficulty understanding the meaning of these arithmetic rules in operational semantics. Hoping for a brief explanation of their meaning. The expressions are from here: Arithmetic ...
1
vote
0answers
31 views

Elementary proof for associativity of integers under addition [closed]

How to prove that integers obey associative law with respect to addition operation without using the concept of equivalence classes?