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
1answer
78 views

Prove a predicate formula in the constructive logic

Using the constructive logic (the axiom $A\lor\lnot A$ cannot be used), using quantifier axioms and Modus Ponens, and Generalization, prove the following: $\exists x(B(x) \to C(x)) \to (\forall xB(x) ...
1
vote
1answer
628 views

Proving that successor of a number is not zero

I am stuck proving the simple claim that $Sx \neq 0$ in say Peano Arithmetic (the first order theory of arithmetic) or Robinson Arithmetic or Presburger Arithmetic. I see that this is sometimes added ...
1
vote
1answer
236 views

Hilbert system (with inference rule of modus ponens), show $\vdash \exists x (Px \rightarrow \forall x Px)$

We're in first-order logic, using the Hilbert system (with inference rule of modus ponens), and the problem is to show $\vdash \exists x (Px \rightarrow \forall x Px)$. We just learned about this ...
1
vote
1answer
180 views

Suppose $A$ is an invertible matrix. Prove that $det(A^{-2}) = 1/(det(A))^2$

Suppose $A$ is an invertible matrix. Prove that $det(A^{-2}) = 1/(det(A))^2$ I want to just say $$det(A^{-2}) = 1/(det(A))^2$$ $$\Rightarrow (det(A^2))^{-1} = 1/(det(A))^2$$ $$ \Rightarrow 1/det(A^...
1
vote
2answers
4k views

prove that if a square matrix $A$ is invertible then $AA^T$ is invertible.

prove that if a square matrix $A$ is invertible then $AA^T$ is invertible. and also prove the opposite, that if $AA^T$ is invertible, then $A$ is invertible. i wrote that $det(A) = det(A^T)$ and ...
1
vote
3answers
1k views

Show that if $A$ is any square matrix such that $A^n = 0$ for some positive intiger $n$, then $A$ is not invertible. (answer check)

Show that if $A$ is any square matrix such that $A^n = 0$ for some positive integer $n$, then $A$ is not invertible. I'm not sure if my proof is good enough, or enough "work" as my teacher put it ...
1
vote
1answer
277 views

Can universal instantiation be used more than once?

I'm trying to follow a proof in a logic text and it seems like the author used universal instantiation twice to reach the needed result. I was under the impression that you could only use UI one time ...
1
vote
1answer
66 views

Is there a proof of this statement about deductions?

Is there a proof of the following statement: you cannot prove with natural deduction theorems that are unprovable in a Hilbert-style proof system? The logic in discussion is either propositional logic ...
1
vote
0answers
37 views

What is the proof for the factorization criterion?

** The Factorization Criterion ** Let $U$ be a statistic based on the random sample $Y_1, Y_2,...Y_n$. Then $U$ is a sufficient statistics for the estimation of a parameter $\theta$ if and only if ...
1
vote
1answer
73 views

Can axioms be premises in formal proofs?

If I use an axiom to prove a theorem, i.e. use the axioms of equality in FOL to prove the converse of the axiom of extensionality, do I list those axioms as premises in a formal proof? The answer ...
1
vote
1answer
58 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 = {∅,{∅}} ...
1
vote
1answer
57 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 \\ [\...
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 ...
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 ...
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
123 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 ...
1
vote
0answers
57 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
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_{\...
1
vote
0answers
28 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?
1
vote
0answers
59 views

Deduction of $\vdash \exists x (Px \rightarrow \forall y Py)$

I was reading this question and I was curious, since I haven't quite grasp this topic being fairly new and all, how much would it differ the "tree" or list of deductions if instead of $\vdash \exists ...
1
vote
2answers
47 views

What is a gross-looking formal axiomatic proof for a relatively simple proposition?

I'm looking for long and hard to follow derivations or symbolic proofs to motivate how tedious it is to actually reason within a formal system. I'm hoping there is an image of the proof, with few if ...
1
vote
1answer
249 views

Question on proving validity in predicate logic

Using the proof rules of predicate logic prove the validity of the following sequent: $$ \forall X \exists Y(P(X)\lor Q(Y))\vdash \exists Y \forall X(P(X)\lor Q(Y)) $$ I have been trying to prove ...
1
vote
0answers
61 views

Distinction between “implicit” and “explicit” formal proofs

Can anyone comment on the distinction between two different methods of formal proof? Since I'm pretty shaky on the methods and terminology of Proof Theory I a refer to them below as the "implicit" and ...
1
vote
0answers
71 views

Why, intuitively, are propositional resolution proofs so long?

I'm trying to gain an intuitive understanding of why propositional resolution proofs tend to be so long. As every essential prime implicant can be produced via resolution, intuitively I would have ...
1
vote
0answers
77 views

Formally proving that $a_i\delta_{ij} = a_j$

Using the summation convention and the Kronecker delta ($\delta$), one can show that $$a_i\delta_{ij} = a_j.$$ If one expands the expression, one is looking at $$ a_i\delta_{ij} = a_1\delta_{1j} + ...
1
vote
1answer
153 views

Propositional logical equivalence in Lemmon style proof

I am doing a bit of propositional logic and I was wondering does Lemmon style of proofing allows writing logical equivalence of some propositions. There is an example of biconditional that you can ...
1
vote
6answers
58 views

How do you prove questions of the form: Show that $A\to \text{ B or C or D}$?

How do you prove questions of the form: Show that $A\to \text{ B or C or D}$? For example, suppose the question was: $$\text{(x = 10) $\to$($x+1 = 11$) or ($x+2 = 4$) or ($x-1 = 8$)}$$ I don't know ...
1
vote
1answer
136 views

The existence of unprovably unprovable statements provable in ZFC [duplicate]

I am aware of Gödel's second incompleteness theorem, the proven existence of several unprovable statements (in ZFC), and the possibility that a formal system may include statements that are unprovably ...
1
vote
0answers
129 views

Stuck on proving ($p \Rightarrow q) \land (q \equiv r) \Rightarrow (p\Rightarrow r)$

I'm in a Foundations of Computer Science course and it's all about logic and proofs. Some proofs are harder than others, and I'm completely stuck on this proof. It comes out of the textbook Texts and ...
1
vote
1answer
71 views

Show that a given formula is not provable without the associative rule

This question is from Shoenfield's "Mathematical Logic", an exercise on page 25. Show that the formula $((x \neq x) \vee \neg(x \neq x \vee x \neq x)) \vee (x \neq x \vee x \neq x)$ is a theorem, ...
1
vote
2answers
41 views

Inequality with summations and roots

I'm trying to prove that $$\frac{1}{2}(2n + \sum_{i=1}^{n}2x_i^2-\sqrt{4(\sum_{i=1}^{n}2x_i)^2 + (-2n + \sum_{i=1}^{n}2x_i^2)^2}) > 0$$ For all $x_i \in {\rm I\!R}$ and $n>0$ I tried using the ...
1
vote
2answers
349 views

$(C + \bar{A})(AB + AB\bar{C})$ Simplifying Boolean

Basically I have this terrible teacher that only gave us a ton of different examples using DeMorgran's Law, and now that one of these can't be solved using DeMorgan's Law, I am pretty lost on what to ...
1
vote
0answers
38 views

How Does the Number of Lines of a Proof Change If Expanding a Condensed Detachment Proof into a Simultaneous Substitution and Detachment Proof?

For every condensed detachment proof, there exists a substitution and detachment proof. If both the antecedent of the major premise, e. g. one having form C$\alpha$$\beta$ or (p $\rightarrow$ q) ...
1
vote
0answers
147 views

Being a Mathematician [closed]

I love mathematics--the exploration of space and quantity and how areas of mathematics are interrelated. However, I think proofs of trivial theorems are boring and uninteresting. The more complex the ...
1
vote
1answer
63 views

Can we write formal (mechanical) proof of any theorem?

why formal proofs are not widely used? sometimes non formal proofs are cumbersome. are there any "important" theorems that have been proved formally
1
vote
0answers
267 views

If a set has an upper bound, it has infinitely many upper bounds.

Let $A$ be a subset of the real numbers, with $A \neq \emptyset$. Prove that if $x$ is an upper bound of $A$, then $A$ has infinitely many upper bounds. This seems like something that is pretty ...
1
vote
1answer
184 views

Spivak Calculus 3rd. Edition Chapter 1 Problem 12 (iii) and (iv) Proofs Critique

Here are my "proofs" for Spivak's Calculus Chapter 1 Problem 12. I am new to this level of rigour and I am attempting to intimate myself with more advanced topics of mathematics to prepare for next ...
1
vote
2answers
249 views

Formal deduction proof of predicates

I am trying to proof equality is transitive, that is, $\emptyset \vdash \forall x \forall y \forall z ((x=y) \land (y=z) \to(x=z))$ using formal deduction (17 rules) and also other rules (ex. To ...
1
vote
0answers
108 views

No Proof, Just Luck

I just read about the Goldbach Conjecture and it got me thinking about probabilities. Supposing that prime numbers are somewhat randomly distributed) then if we calculate the odds of a given even ...
1
vote
0answers
79 views

Isabelle and “Method of Coefficients”

I have been trying to use the Method of Coefficients in some combinatorial arguments. Since the result ended up being more complicated than I am comfortable with I would like to know if there is ...
1
vote
0answers
553 views

Existential and Universal Equivalence Proof

Taking ¬∀x:X.r≡∃x:X.¬r Is there a way of actually formally proving this? Not implementing it but proving how to go from a negated universal quantifier to a an existential with a negated element... ...
1
vote
0answers
149 views

(Another) Proof within Hilbert system

I know there are plenty of similar posts around, but I could not find an answer to this particular question (and I've been at it for two days now, getting nowhere). The proof I'm trying to construe in ...
1
vote
0answers
38 views

Logical systems and formal proof

Is there any good book dealing with various formal systems and a book for formal proofs. Or atleast some good notes. This page on wikipedia also says: 'This article needs attention from an expert in ...
1
vote
1answer
49 views

How to prove this inference in sequent calculus?

I'm using the event-B prover to proove some proof obligations. I have a relation representing a $table: table \in 1‥n \to \mathbb{N}$. I know that in a sorted table the following property is true: $\...
1
vote
1answer
719 views

Proof that minimum of sum of absolute differences is greater or equal of max value minus min value

Let's have an vector of natural numbers $[v_1, ..., v_N]$ my goal is to show that $$\sum_{i=1}^{N-1}|v_i - v_{i+1}| \ge v_{max} - v_{min}$$ where $v_{max} = \max_{i\in1...N}(v_i)$ and $v_{min} = \...
1
vote
1answer
87 views

Prove formally that $\frac {n^2 + 2}{3n^3 - 5n}\to 0$ as $n \to \infty$.

I'm reviewing some Sequences notes from a Mathematics Analysis course I'm taking. I'm finding the beginning of the formal proof below confusing. Some clarity on the following questions would be much ...
1
vote
2answers
628 views

How to prove this using natural deduction

$$⊢ P ∨ ¬P$$ I found this question on the net. I know the solution, but I find it complicated. How should I approach this sort of question? Or can you provide me with another solution?
1
vote
1answer
122 views

Easy question on Logic and Modes Ponens

I got confused with these: using ONLY this three axioms and Modus Ponens:$$1. \ F \implies (G\implies F) \\ 2. \ (F \implies (G\implies H))\implies ((F \implies G)\implies (F \implies H)) \\ 3. \ (\...
1
vote
2answers
146 views

What's the strength of logic without $\neg\neg\exists x P(x) \implies \exists x P(x)$?

As far as I understand, the main idea of constructive logic is that we only allow proof methods that let us show the statement $\exists x:P(x)$ only by constructing an explicit such object $x$, right? ...
1
vote
3answers
293 views

Giving a formal proof of p ⇒(q ⇒ r) $\vdash$ (p ⇒ r)∨(q ⇒ r) using the rules of inference.

I can prove this with semantic equivalences and truth tables but I'm struggling on the formal proof using rules of inference front. Given its format I would assume it must finish on V-introduction ...